YES
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 strongly closed criterion
linear
uniform
BCPs:
(0 on 0): 
   {  |- < (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)) >,
      |- < (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))) > }
 |- <  (forall [b](forall [b](forall [a][]X))),   (forall [a](forall [b](forall [b][]X)))  > is closed at (forall [b](forall [b](forall [a][(a b)]X)))
 |- <  (forall [c](forall [b](forall [a][]X))),   (forall [a](forall [c](forall [b][]X)))  > is closed at (forall [c](forall [b](forall [a][(a b)]X)))
 |- <  (forall [a](forall [b](forall [a][]X))),   (forall [b](forall [a](forall [a][(a b)]X)))  > is closed at (forall [a](forall [b](forall [a][(a b)]X)))
 |- <  (forall [c](forall [b](forall [a][]X))),   (forall [b](forall [c](forall [a][(a b)]X)))  > is closed at (forall [c](forall [b](forall [a][(a b)]X)))
c#X |- <  (forall [b](forall [b](forall [a][]X))),   (forall [c](forall [b](forall [b][(a c)]X)))  > is closed at (forall [b](forall [b](forall [c][(c a)(a b)]X)))
c#X |- <  (forall [a](forall [b](forall [a][]X))),   (forall [c](forall [a](forall [b][(a c)]X)))  > is closed at (forall [a](forall [b](forall [c][(c a)(a b)]X)))
d#X |- <  (forall [c](forall [b](forall [a][]X))),   (forall [d](forall [c](forall [b][(a d)]X)))  > is closed at (forall [c](forall [b](forall [a][(a b)]X)))
all BCPs are strongly closed
result: YES
time: 676 msec.