YES
ignored inputs:
(COMMENT rules to obtain NNF of first-order formulas )

NRS:
   [ (0):  |- (not (exists [a][]Q)) -> (forall [a](not []Q)),
     (1):  |- (not (forall [a][]Q)) -> (exists [a](not []Q)),
     (2):  |- (not (and <[]P,[]Q>)) -> (or <(not []P),(not []Q)>),
     (3):  |- (not (or <[]P,[]Q>)) -> (and <(not []P),(not []Q)>),
     (4):  |- (not (not []P)) -> []P ]
Check confluence by Knuth-Bendix criterion
uniform

writing to temporary file...
./run_snprover.sh ./SMLNJ-Dgf0Ty.trs
YES

Problem:
 not(exists(lambda(Q))) -> forall(lambda(not(Q)))
 not(forall(lambda(Q))) -> exists(lambda(not(Q)))
 not(and(pair_2(P,Q))) -> or(pair_2(not(P),not(Q)))
 not(or(pair_2(P,Q))) -> and(pair_2(not(P),not(Q)))
 not(not(P)) -> P

Proof:
 DP Processor:
  DPs:
   not#(exists(lambda(Q))) -> not#(Q)
   not#(forall(lambda(Q))) -> not#(Q)
   not#(and(pair_2(P,Q))) -> not#(Q)
   not#(and(pair_2(P,Q))) -> not#(P)
   not#(or(pair_2(P,Q))) -> not#(Q)
   not#(or(pair_2(P,Q))) -> not#(P)
  TRS:
   not(exists(lambda(Q))) -> forall(lambda(not(Q)))
   not(forall(lambda(Q))) -> exists(lambda(not(Q)))
   not(and(pair_2(P,Q))) -> or(pair_2(not(P),not(Q)))
   not(or(pair_2(P,Q))) -> and(pair_2(not(P),not(Q)))
   not(not(P)) -> P
  Subterm Criterion Processor:
   simple projection:
    pi(not#) = 0
   problem:
    DPs:
     
    TRS:
     not(exists(lambda(Q))) -> forall(lambda(not(Q)))
     not(forall(lambda(Q))) -> exists(lambda(not(Q)))
     not(and(pair_2(P,Q))) -> or(pair_2(not(P),not(Q)))
     not(or(pair_2(P,Q))) -> and(pair_2(not(P),not(Q)))
     not(not(P)) -> P
   Qed
terminating
check each BCP has alpha-equivalent normal forms or not
BCPs:
(0 on 0): 
   {  |- < (forall [a](not []Q_1)) <= (not (exists [a][]Q_1)) => (forall [a](not []Q_1)) >,
     a#Q_1 |- < (forall [a](not [(a b)]Q_1)) <= (not (exists [b][]Q_1)) => (forall [b](not []Q_1)) > }
(0 on 4): 
   {  |- < (not (forall [a](not []Q))) <= (not (not (exists [a][]Q))) => (exists [a][]Q) > }
(1 on 1): 
   {  |- < (exists [a](not []Q_1)) <= (not (forall [a][]Q_1)) => (exists [a](not []Q_1)) >,
     a#Q_1 |- < (exists [a](not [(a b)]Q_1)) <= (not (forall [b][]Q_1)) => (exists [b](not []Q_1)) > }
(1 on 4): 
   {  |- < (not (exists [a](not []Q))) <= (not (not (forall [a][]Q))) => (forall [a][]Q) > }
(2 on 2): 
   {  |- < (or <(not []P_1),(not []Q_1)>) <= (not (and <[]P_1,[]Q_1>)) => (or <(not []P_1),(not []Q_1)>) > }
(2 on 4): 
   {  |- < (not (or <(not []P),(not []Q)>)) <= (not (not (and <[]P,[]Q>))) => (and <[]P,[]Q>) > }
(3 on 3): 
   {  |- < (and <(not []P_1),(not []Q_1)>) <= (not (or <[]P_1,[]Q_1>)) => (and <(not []P_1),(not []Q_1)>) > }
(3 on 4): 
   {  |- < (not (and <(not []P),(not []Q)>)) <= (not (not (or <[]P,[]Q>))) => (or <[]P,[]Q>) > }
(4 on 4): 
   {  |- < []P_1 <= (not (not []P_1)) => []P_1 >,
      |- < (not []P) <= (not (not (not []P))) => (not []P) > }
BCP:  |- <  (not (forall [a](not []Q))),   (exists [a][]Q)  >
===> nf(lhs):(exists [a][]Q) and nf(rhs):(exists [a][]Q) are aeq
BCP:  |- <  (not (exists [a](not []Q))),   (forall [a][]Q)  >
===> nf(lhs):(forall [a][]Q) and nf(rhs):(forall [a][]Q) are aeq
BCP:  |- <  (not (or <(not []P),(not []Q)>)),   (and <[]P,[]Q>)  >
===> nf(lhs):(and <[]P,[]Q>) and nf(rhs):(and <[]P,[]Q>) are aeq
BCP:  |- <  (not (and <(not []P),(not []Q)>)),   (or <[]P,[]Q>)  >
===> nf(lhs):(or <[]P,[]Q>) and nf(rhs):(or <[]P,[]Q>) are aeq
all BCPs are joinable
result: YES
time: 13 msec.