YES
ignored inputs:
(COMMENT Example 5.5 of [ Ayala-Lincon et al. , LSFA 2015 ] )

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

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

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

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