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

NRS:
   [ (0):  |- (lam [a](app <[]X,a>)) -> []X ]
Check confluence by parallel closed criterion
left-linear
not uniform
result: MAYBE
time: 0 msec.