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

NRS:
   [ (0):  |- (f []X) -> (f [a][]X) ]
Check confluence by strongly closed criterion
linear
uniform
BCPs:
(0 on 0): 
   {  |- < (f [a][]X_1) <= (f []X_1) => (f [a][]X_1) >,
      |- < (f [a][]X_1) <= (f []X_1) => (f [b][]X_1) > }
 |- <  (f [a][]X_1),   (f [b][]X_1)  > is not closed
failed to show all BCPs are strongly closed
result: MAYBE
time: 0 msec.