NO
ignored inputs:
(COMMENT Example 19 of [ SKAT15 , doi:10.4230/LIPIcs.RTA.2015.301 ] )

NRS:
   [ (0):  |- (ucetaexp []X) -> (lam [a](app <[]X,a>)) ]
Check confluence by Knuth-Bendix criterion
uniform

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

Problem:
 ucetaexp(X) -> lam(lambda(app(pair_2(X,diamond()))))

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