MAYBE
ignored inputs:
(COMMENT commutativity of universal quantification )
(COMMENT Example 5 of [ Suzuki et al. , SCSS 2016 ] )

NRS:
   [ (0):  |- (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-5baOwQ.trs
NO

Problem:
 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.