MAYBE
ignored inputs:
(COMMENT rules to obtain PNF of first-order formulas with conjunctions and universal quantifiers )
(COMMENT Example 7 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>)) ]
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>)) > }
outBCP:  |- <  (forall [a](and <[]X1,(forall [a][]Y2_1)>)),   (forall [a](and <(forall [a][]X1),[]Y2_1>))  > is not closed
failed to show all BCPs are parallel closed
result: MAYBE
time: 5 msec.