MAYBE
ignored inputs:
(COMMENT alpha reduction rule of the lambda calculus )

NRS:
   [ (0): b#X |- (lam [a][]X) -> (lam [b][(a b)]X) ]
Check confluence by Knuth-Bendix criterion
uniform

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

Problem:
 lam(lambda(X)) -> lam(lambda(X))

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