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

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