MAYBE
ignored inputs:
(COMMENT commutativity of universal quantification )
(COMMENT Example 5 of [ Suzuki et al. , SCSS 2016 ] )

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