NO
ignored inputs:
(COMMENT Example 1.2 of [ Suzuki et al. , PPL 2014 ] )

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

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

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

Proof:
 DP Processor:
  DPs:
   
  TRS:
   f(X) -> lambda(X)
  Qed
terminating
check each BCP has alpha-equivalent normal forms or not
BCPs:
(0 on 0): 
   {  |- < [a][]X_1 <= (f []X_1) => [a][]X_1 >,
      |- < [a][]X_1 <= (f []X_1) => [b][]X_1 > }
BCP:  |- <  [a][]X_1,   [b][]X_1  >
===> nf(lhs):[a][]X_1 and nf(rhs):[b][]X_1 are not aeq
some BCP is not joinable
result: NO
time: 4 msec.