MAYBE
ignored inputs:
(COMMENT rules to obtain PNF of first-order formulas with conjunctions and universal quantifiers + commutativity rule of universal quantifiers )
(COMMENT Example 12 of [ Suzuki et al. , SCSS 2016 ] )

NRS:
   [ (0): a#Y1 |- (and <(forall [a][]X1),[]Y1>) -> (forall [a](and <[]X1,[]Y1>)),
     (1): a#X2 |- (and <[]X2,(forall [a][]Y2)>) -> (forall [a](and <[]X2,[]Y2>)),
     (2):  |- (forall [a](forall [b][]X)) -> (forall [b](forall [a][]X)) ]
Check confluence by parallel closed criterion
left-linear
uniform
BCPs:
(0 on 0(out)): 
   { a#Y1_1 |- < (forall [a](and <[]X1_1,[]Y1_1>)) <= (and <(forall [a][]X1_1),[]Y1_1>) => (forall [a](and <[]X1_1,[]Y1_1>)) >,
     a#X1_1,a#Y1_1,b#Y1_1 |- < (forall [a](and <[(a b)]X1_1,[]Y1_1>)) <= (and <(forall [b][]X1_1),[]Y1_1>) => (forall [b](and <[]X1_1,[]Y1_1>)) > }
(0 on 1(out)): 
   {  |- < (forall [a](and <[]X1,(forall [a][]Y2_1)>)) <= (and <(forall [a][]X1),(forall [a][]Y2_1)>) => (forall [a](and <(forall [a][]X1),[]Y2_1>)) >,
     a#Y2_1,b#X1 |- < (forall [a](and <[]X1,(forall [b][]Y2_1)>)) <= (and <(forall [a][]X1),(forall [b][]Y2_1)>) => (forall [b](and <(forall [a][]X1),[]Y2_1>)) > }
(1 on 0(out)): 
   {  |- < (forall [a](and <(forall [a][]X1_1),[]Y2>)) <= (and <(forall [a][]X1_1),(forall [a][]Y2)>) => (forall [a](and <[]X1_1,(forall [a][]Y2)>)) >,
     a#X1_1,b#Y2 |- < (forall [a](and <(forall [b][]X1_1),[]Y2>)) <= (and <(forall [b][]X1_1),(forall [a][]Y2)>) => (forall [b](and <[]X1_1,(forall [a][]Y2)>)) > }
(1 on 1(out)): 
   { a#X2_1 |- < (forall [a](and <[]X2_1,[]Y2_1>)) <= (and <[]X2_1,(forall [a][]Y2_1)>) => (forall [a](and <[]X2_1,[]Y2_1>)) >,
     a#Y2_1,a#X2_1,b#X2_1 |- < (forall [a](and <[]X2_1,[(a b)]Y2_1>)) <= (and <[]X2_1,(forall [b][]Y2_1)>) => (forall [b](and <[]X2_1,[]Y2_1>)) > }
(2 on 0(in)): 
   { a#Y1_1 |- < (and <(forall [b](forall [a][]X)),[]Y1_1>) <= (and <(forall [a](forall [b][]X)),[]Y1_1>) => (forall [a](and <(forall [b][]X),[]Y1_1>)) >,
     b#Y1_1 |- < (and <(forall [b](forall [a][]X)),[]Y1_1>) <= (and <(forall [b](forall [a][(a b)]X)),[]Y1_1>) => (forall [b](and <(forall [a][(a b)]X),[]Y1_1>)) >,
     c#X,c#Y1_1 |- < (and <(forall [b](forall [a][]X)),[]Y1_1>) <= (and <(forall [c](forall [b][(a c)]X)),[]Y1_1>) => (forall [c](and <(forall [b][(a c)]X),[]Y1_1>)) > }
(2 on 1(in)): 
   { a#X2_1 |- < (and <[]X2_1,(forall [b](forall [a][]X))>) <= (and <[]X2_1,(forall [a](forall [b][]X))>) => (forall [a](and <[]X2_1,(forall [b][]X)>)) >,
     b#X2_1 |- < (and <[]X2_1,(forall [b](forall [a][]X))>) <= (and <[]X2_1,(forall [b](forall [a][(a b)]X))>) => (forall [b](and <[]X2_1,(forall [a][(a b)]X)>)) >,
     c#X,c#X2_1 |- < (and <[]X2_1,(forall [b](forall [a][]X))>) <= (and <[]X2_1,(forall [c](forall [b][(a c)]X))>) => (forall [c](and <[]X2_1,(forall [b][(a c)]X)>)) > }
(2 on 2(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)) > }
(2 on 2(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: a#Y1_1 |- <  (and <(forall [b](forall [a][]X)),[]Y1_1>),   (forall [a](and <(forall [b][]X),[]Y1_1>))  > is not closed
failed to show all BCPs are parallel closed
result: MAYBE
time: 14 msec.