MAYBE
ignored inputs:
(COMMENT rules to obtain PNF of first-order formulas with conjunctions and universal quantifiers + commutativity rule of universal quantifiers )
(COMMENT Example 12 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>)),
     (2):  |- (forall [a](forall [b][]X)) -> (forall [b](forall [a][]X)) ]
Check confluence by Knuth-Bendix criterion
uniform

writing to temporary file...
./run_snprover.sh ./SMLNJ-v053we.trs
NO

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))))
 forall(lambda(forall(lambda(X)))) -> forall(lambda(forall(lambda(X))))

Proof:
 Containment Processor:
  loop length: 1
  terms:
   forall(lambda(forall(lambda(X))))
  context: []
  substitution:
   X -> X
  Qed
termination proof failed
result: MAYBE
time: 0 msec.