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

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

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

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

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