MAYBE
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 strongly closed criterion
linear
uniform
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>)) > }
 |- <  (lam [a](app <[]X_1,a>)),   (lam [b](app <[]X_1,b>))  > is not closed
failed to show all BCPs are strongly closed
result: MAYBE
time: 0 msec.