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 orthogonality
abstract skeleton preserving
left-linear
check proper overlapping
a proper overlap exists
0-0
 |- < (forall [b](forall [b](forall [a][]X))) <= (forall [b](forall [a](forall [b][]X))) => (forall [a](forall [b](forall [b][]X))) >
found proper overlaps
result: MAYBE
time: 0 msec.