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