NO
ignored inputs:
(COMMENT rules to obtain PNF of first-order formulas with conjunctions and universal quantifiers )
(COMMENT Example 7 of [ Suzuki et al. , SCSS 2016 ] )

NRS:
   [ (0): a#Y1 |- (and <(forall [a][]X1),[]Y1>) -> (forall [a](and <[]X1,[]Y1>)),
     (1): a#X2 |- (and <[]X2,(forall [a][]Y2)>) -> (forall [a](and <[]X2,[]Y2>)) ]
Check confluence by Knuth-Bendix criterion
uniform

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

Problem:
 and(pair_2(forall(lambda(X1)),Y1)) -> forall(lambda(and(pair_2(X1,Y1))))
 and(pair_2(X2,forall(lambda(Y2)))) -> forall(lambda(and(pair_2(X2,Y2))))

Proof:
 LPO Processor:
  precedence:
   pair_2 > and ~ forall ~ lambda
  problem:
   
  Qed
terminating
check each BCP has alpha-equivalent normal forms or not
BCPs:
(0 on 0): 
   { a#Y1_1 |- < (forall [a](and <[]X1_1,[]Y1_1>)) <= (and <(forall [a][]X1_1),[]Y1_1>) => (forall [a](and <[]X1_1,[]Y1_1>)) >,
     a#X1_1,a#Y1_1,b#Y1_1 |- < (forall [a](and <[(a b)]X1_1,[]Y1_1>)) <= (and <(forall [b][]X1_1),[]Y1_1>) => (forall [b](and <[]X1_1,[]Y1_1>)) > }
(0 on 1): 
   {  |- < (forall [a](and <[]X1,(forall [a][]Y2_1)>)) <= (and <(forall [a][]X1),(forall [a][]Y2_1)>) => (forall [a](and <(forall [a][]X1),[]Y2_1>)) >,
     a#Y2_1,b#X1 |- < (forall [a](and <[]X1,(forall [b][]Y2_1)>)) <= (and <(forall [a][]X1),(forall [b][]Y2_1)>) => (forall [b](and <(forall [a][]X1),[]Y2_1>)) > }
(1 on 0): 
   {  |- < (forall [a](and <(forall [a][]X1_1),[]Y2>)) <= (and <(forall [a][]X1_1),(forall [a][]Y2)>) => (forall [a](and <[]X1_1,(forall [a][]Y2)>)) >,
     a#X1_1,b#Y2 |- < (forall [a](and <(forall [b][]X1_1),[]Y2>)) <= (and <(forall [b][]X1_1),(forall [a][]Y2)>) => (forall [b](and <[]X1_1,(forall [a][]Y2)>)) > }
(1 on 1): 
   { a#X2_1 |- < (forall [a](and <[]X2_1,[]Y2_1>)) <= (and <[]X2_1,(forall [a][]Y2_1)>) => (forall [a](and <[]X2_1,[]Y2_1>)) >,
     a#Y2_1,a#X2_1,b#X2_1 |- < (forall [a](and <[]X2_1,[(a b)]Y2_1>)) <= (and <[]X2_1,(forall [b][]Y2_1)>) => (forall [b](and <[]X2_1,[]Y2_1>)) > }
BCP:  |- <  (forall [a](and <[]X1,(forall [a][]Y2_1)>)),   (forall [a](and <(forall [a][]X1),[]Y2_1>))  >
===> nf(lhs):(forall [a](and <[]X1,(forall [a][]Y2_1)>)) and nf(rhs):(forall [a](and <(forall [a][]X1),[]Y2_1>)) are not aeq
some BCP is not joinable
result: NO
time: 10 msec.