MAYBE
ignored inputs:
(COMMENT rules to obtain PNF of first-order formulas with additional rules )
(COMMENT Example 44 [ FG07 , doi:10.1016/j.ic.2006.12.002 ] )

NRS:
   [ (0): a#P |- (and <[]P,(forall [a][]Q)>) -> (forall [a](and <[]P,[]Q>)),
     (1): a#P |- (and <(forall [a][]Q),[]P>) -> (forall [a](and <[]Q,[]P>)),
     (2): a#P |- (or <[]P,(forall [a][]Q)>) -> (forall [a](or <[]P,[]Q>)),
     (3): a#P |- (or <(forall [a][]Q),[]P>) -> (forall [a](or <[]Q,[]P>)),
     (4): a#P |- (and <[]P,(exists [a][]Q)>) -> (exists [a](and <[]P,[]Q>)),
     (5): a#P |- (and <(exists [a][]Q),[]P>) -> (exists [a](and <[]Q,[]P>)),
     (6): a#P |- (or <[]P,(exists [a][]Q)>) -> (exists [a](or <[]P,[]Q>)),
     (7): a#P |- (or <(exists [a][]Q),[]P>) -> (exists [a](or <[]Q,[]P>)),
     (8):  |- (not <(exists [a][]Q)>) -> (forall [a](not []Q)),
     (9):  |- (not <(forall [a][]Q)>) -> (exists [a](not []Q)),
     (10): a#X |- (forall [a][]X) -> []X,
     (11):  |- (and <(forall [a][]X),(forall [a][]Y)>) -> (forall [a](and <[]X,[]Y>)),
     (12): a#X |- (exists [a][]X) -> []X,
     (13):  |- (or <(exists [a][]X),(exists [a][]Y)>) -> (exists [a](or <[]X,[]Y>)) ]
Check confluence by strongly closed criterion
linear
uniform
BCPs:
(0 on 0): 
   { a#P_1 |- < (forall [a](and <[]P_1,[]Q_1>)) <= (and <[]P_1,(forall [a][]Q_1)>) => (forall [a](and <[]P_1,[]Q_1>)) >,
     a#Q_1,a#P_1,b#P_1 |- < (forall [a](and <[]P_1,[(a b)]Q_1>)) <= (and <[]P_1,(forall [b][]Q_1)>) => (forall [b](and <[]P_1,[]Q_1>)) > }
(0 on 1): 
   {  |- < (forall [a](and <(forall [a][]Q_1),[]Q>)) <= (and <(forall [a][]Q_1),(forall [a][]Q)>) => (forall [a](and <[]Q_1,(forall [a][]Q)>)) >,
     a#Q_1,b#Q |- < (forall [a](and <(forall [b][]Q_1),[]Q>)) <= (and <(forall [b][]Q_1),(forall [a][]Q)>) => (forall [b](and <[]Q_1,(forall [a][]Q)>)) > }
(0 on 5): 
   {  |- < (forall [a](and <(exists [a][]Q_1),[]Q>)) <= (and <(exists [a][]Q_1),(forall [a][]Q)>) => (exists [a](and <[]Q_1,(forall [a][]Q)>)) >,
     a#Q_1,b#Q |- < (forall [a](and <(exists [b][]Q_1),[]Q>)) <= (and <(exists [b][]Q_1),(forall [a][]Q)>) => (exists [b](and <[]Q_1,(forall [a][]Q)>)) > }
(0 on 11): 
   {  |- < (forall [a](and <(forall [a][]X_1),[]Y_1>)) <= (and <(forall [a][]X_1),(forall [a][]Y_1)>) => (forall [a](and <[]X_1,[]Y_1>)) >,
     a#Y_1,a#X_1 |- < (forall [a](and <(forall [b][]X_1),[(a b)]Y_1>)) <= (and <(forall [b][]X_1),(forall [b][]Y_1)>) => (forall [b](and <[]X_1,[]Y_1>)) > }
(1 on 0): 
   {  |- < (forall [a](and <[]Q,(forall [a][]Q_1)>)) <= (and <(forall [a][]Q),(forall [a][]Q_1)>) => (forall [a](and <(forall [a][]Q),[]Q_1>)) >,
     a#Q_1,b#Q |- < (forall [a](and <[]Q,(forall [b][]Q_1)>)) <= (and <(forall [a][]Q),(forall [b][]Q_1)>) => (forall [b](and <(forall [a][]Q),[]Q_1>)) > }
(1 on 1): 
   { a#P_1 |- < (forall [a](and <[]Q_1,[]P_1>)) <= (and <(forall [a][]Q_1),[]P_1>) => (forall [a](and <[]Q_1,[]P_1>)) >,
     a#Q_1,a#P_1,b#P_1 |- < (forall [a](and <[(a b)]Q_1,[]P_1>)) <= (and <(forall [b][]Q_1),[]P_1>) => (forall [b](and <[]Q_1,[]P_1>)) > }
(1 on 4): 
   {  |- < (forall [a](and <[]Q,(exists [a][]Q_1)>)) <= (and <(forall [a][]Q),(exists [a][]Q_1)>) => (exists [a](and <(forall [a][]Q),[]Q_1>)) >,
     a#Q_1,b#Q |- < (forall [a](and <[]Q,(exists [b][]Q_1)>)) <= (and <(forall [a][]Q),(exists [b][]Q_1)>) => (exists [b](and <(forall [a][]Q),[]Q_1>)) > }
(1 on 11): 
   {  |- < (forall [a](and <[]X_1,(forall [a][]Y_1)>)) <= (and <(forall [a][]X_1),(forall [a][]Y_1)>) => (forall [a](and <[]X_1,[]Y_1>)) >,
     a#X_1,a#Y_1 |- < (forall [a](and <[(a b)]X_1,(forall [b][]Y_1)>)) <= (and <(forall [b][]X_1),(forall [b][]Y_1)>) => (forall [b](and <[]X_1,[]Y_1>)) > }
(2 on 2): 
   { a#P_1 |- < (forall [a](or <[]P_1,[]Q_1>)) <= (or <[]P_1,(forall [a][]Q_1)>) => (forall [a](or <[]P_1,[]Q_1>)) >,
     a#Q_1,a#P_1,b#P_1 |- < (forall [a](or <[]P_1,[(a b)]Q_1>)) <= (or <[]P_1,(forall [b][]Q_1)>) => (forall [b](or <[]P_1,[]Q_1>)) > }
(2 on 3): 
   {  |- < (forall [a](or <(forall [a][]Q_1),[]Q>)) <= (or <(forall [a][]Q_1),(forall [a][]Q)>) => (forall [a](or <[]Q_1,(forall [a][]Q)>)) >,
     a#Q_1,b#Q |- < (forall [a](or <(forall [b][]Q_1),[]Q>)) <= (or <(forall [b][]Q_1),(forall [a][]Q)>) => (forall [b](or <[]Q_1,(forall [a][]Q)>)) > }
(2 on 7): 
   {  |- < (forall [a](or <(exists [a][]Q_1),[]Q>)) <= (or <(exists [a][]Q_1),(forall [a][]Q)>) => (exists [a](or <[]Q_1,(forall [a][]Q)>)) >,
     a#Q_1,b#Q |- < (forall [a](or <(exists [b][]Q_1),[]Q>)) <= (or <(exists [b][]Q_1),(forall [a][]Q)>) => (exists [b](or <[]Q_1,(forall [a][]Q)>)) > }
(3 on 2): 
   {  |- < (forall [a](or <[]Q,(forall [a][]Q_1)>)) <= (or <(forall [a][]Q),(forall [a][]Q_1)>) => (forall [a](or <(forall [a][]Q),[]Q_1>)) >,
     a#Q_1,b#Q |- < (forall [a](or <[]Q,(forall [b][]Q_1)>)) <= (or <(forall [a][]Q),(forall [b][]Q_1)>) => (forall [b](or <(forall [a][]Q),[]Q_1>)) > }
(3 on 3): 
   { a#P_1 |- < (forall [a](or <[]Q_1,[]P_1>)) <= (or <(forall [a][]Q_1),[]P_1>) => (forall [a](or <[]Q_1,[]P_1>)) >,
     a#Q_1,a#P_1,b#P_1 |- < (forall [a](or <[(a b)]Q_1,[]P_1>)) <= (or <(forall [b][]Q_1),[]P_1>) => (forall [b](or <[]Q_1,[]P_1>)) > }
(3 on 6): 
   {  |- < (forall [a](or <[]Q,(exists [a][]Q_1)>)) <= (or <(forall [a][]Q),(exists [a][]Q_1)>) => (exists [a](or <(forall [a][]Q),[]Q_1>)) >,
     a#Q_1,b#Q |- < (forall [a](or <[]Q,(exists [b][]Q_1)>)) <= (or <(forall [a][]Q),(exists [b][]Q_1)>) => (exists [b](or <(forall [a][]Q),[]Q_1>)) > }
(4 on 1): 
   {  |- < (exists [a](and <(forall [a][]Q_1),[]Q>)) <= (and <(forall [a][]Q_1),(exists [a][]Q)>) => (forall [a](and <[]Q_1,(exists [a][]Q)>)) >,
     a#Q_1,b#Q |- < (exists [a](and <(forall [b][]Q_1),[]Q>)) <= (and <(forall [b][]Q_1),(exists [a][]Q)>) => (forall [b](and <[]Q_1,(exists [a][]Q)>)) > }
(4 on 4): 
   { a#P_1 |- < (exists [a](and <[]P_1,[]Q_1>)) <= (and <[]P_1,(exists [a][]Q_1)>) => (exists [a](and <[]P_1,[]Q_1>)) >,
     a#Q_1,a#P_1,b#P_1 |- < (exists [a](and <[]P_1,[(a b)]Q_1>)) <= (and <[]P_1,(exists [b][]Q_1)>) => (exists [b](and <[]P_1,[]Q_1>)) > }
(4 on 5): 
   {  |- < (exists [a](and <(exists [a][]Q_1),[]Q>)) <= (and <(exists [a][]Q_1),(exists [a][]Q)>) => (exists [a](and <[]Q_1,(exists [a][]Q)>)) >,
     a#Q_1,b#Q |- < (exists [a](and <(exists [b][]Q_1),[]Q>)) <= (and <(exists [b][]Q_1),(exists [a][]Q)>) => (exists [b](and <[]Q_1,(exists [a][]Q)>)) > }
(5 on 0): 
   {  |- < (exists [a](and <[]Q,(forall [a][]Q_1)>)) <= (and <(exists [a][]Q),(forall [a][]Q_1)>) => (forall [a](and <(exists [a][]Q),[]Q_1>)) >,
     a#Q_1,b#Q |- < (exists [a](and <[]Q,(forall [b][]Q_1)>)) <= (and <(exists [a][]Q),(forall [b][]Q_1)>) => (forall [b](and <(exists [a][]Q),[]Q_1>)) > }
(5 on 4): 
   {  |- < (exists [a](and <[]Q,(exists [a][]Q_1)>)) <= (and <(exists [a][]Q),(exists [a][]Q_1)>) => (exists [a](and <(exists [a][]Q),[]Q_1>)) >,
     a#Q_1,b#Q |- < (exists [a](and <[]Q,(exists [b][]Q_1)>)) <= (and <(exists [a][]Q),(exists [b][]Q_1)>) => (exists [b](and <(exists [a][]Q),[]Q_1>)) > }
(5 on 5): 
   { a#P_1 |- < (exists [a](and <[]Q_1,[]P_1>)) <= (and <(exists [a][]Q_1),[]P_1>) => (exists [a](and <[]Q_1,[]P_1>)) >,
     a#Q_1,a#P_1,b#P_1 |- < (exists [a](and <[(a b)]Q_1,[]P_1>)) <= (and <(exists [b][]Q_1),[]P_1>) => (exists [b](and <[]Q_1,[]P_1>)) > }
(6 on 3): 
   {  |- < (exists [a](or <(forall [a][]Q_1),[]Q>)) <= (or <(forall [a][]Q_1),(exists [a][]Q)>) => (forall [a](or <[]Q_1,(exists [a][]Q)>)) >,
     a#Q_1,b#Q |- < (exists [a](or <(forall [b][]Q_1),[]Q>)) <= (or <(forall [b][]Q_1),(exists [a][]Q)>) => (forall [b](or <[]Q_1,(exists [a][]Q)>)) > }
(6 on 6): 
   { a#P_1 |- < (exists [a](or <[]P_1,[]Q_1>)) <= (or <[]P_1,(exists [a][]Q_1)>) => (exists [a](or <[]P_1,[]Q_1>)) >,
     a#Q_1,a#P_1,b#P_1 |- < (exists [a](or <[]P_1,[(a b)]Q_1>)) <= (or <[]P_1,(exists [b][]Q_1)>) => (exists [b](or <[]P_1,[]Q_1>)) > }
(6 on 7): 
   {  |- < (exists [a](or <(exists [a][]Q_1),[]Q>)) <= (or <(exists [a][]Q_1),(exists [a][]Q)>) => (exists [a](or <[]Q_1,(exists [a][]Q)>)) >,
     a#Q_1,b#Q |- < (exists [a](or <(exists [b][]Q_1),[]Q>)) <= (or <(exists [b][]Q_1),(exists [a][]Q)>) => (exists [b](or <[]Q_1,(exists [a][]Q)>)) > }
(6 on 13): 
   {  |- < (exists [a](or <(exists [a][]X_1),[]Y_1>)) <= (or <(exists [a][]X_1),(exists [a][]Y_1)>) => (exists [a](or <[]X_1,[]Y_1>)) >,
     a#Y_1,a#X_1 |- < (exists [a](or <(exists [b][]X_1),[(a b)]Y_1>)) <= (or <(exists [b][]X_1),(exists [b][]Y_1)>) => (exists [b](or <[]X_1,[]Y_1>)) > }
(7 on 2): 
   {  |- < (exists [a](or <[]Q,(forall [a][]Q_1)>)) <= (or <(exists [a][]Q),(forall [a][]Q_1)>) => (forall [a](or <(exists [a][]Q),[]Q_1>)) >,
     a#Q_1,b#Q |- < (exists [a](or <[]Q,(forall [b][]Q_1)>)) <= (or <(exists [a][]Q),(forall [b][]Q_1)>) => (forall [b](or <(exists [a][]Q),[]Q_1>)) > }
(7 on 6): 
   {  |- < (exists [a](or <[]Q,(exists [a][]Q_1)>)) <= (or <(exists [a][]Q),(exists [a][]Q_1)>) => (exists [a](or <(exists [a][]Q),[]Q_1>)) >,
     a#Q_1,b#Q |- < (exists [a](or <[]Q,(exists [b][]Q_1)>)) <= (or <(exists [a][]Q),(exists [b][]Q_1)>) => (exists [b](or <(exists [a][]Q),[]Q_1>)) > }
(7 on 7): 
   { a#P_1 |- < (exists [a](or <[]Q_1,[]P_1>)) <= (or <(exists [a][]Q_1),[]P_1>) => (exists [a](or <[]Q_1,[]P_1>)) >,
     a#Q_1,a#P_1,b#P_1 |- < (exists [a](or <[(a b)]Q_1,[]P_1>)) <= (or <(exists [b][]Q_1),[]P_1>) => (exists [b](or <[]Q_1,[]P_1>)) > }
(7 on 13): 
   {  |- < (exists [a](or <[]X_1,(exists [a][]Y_1)>)) <= (or <(exists [a][]X_1),(exists [a][]Y_1)>) => (exists [a](or <[]X_1,[]Y_1>)) >,
     a#X_1,a#Y_1 |- < (exists [a](or <[(a b)]X_1,(exists [b][]Y_1)>)) <= (or <(exists [b][]X_1),(exists [b][]Y_1)>) => (exists [b](or <[]X_1,[]Y_1>)) > }
(8 on 8): 
   {  |- < (forall [a](not []Q_1)) <= (not <(exists [a][]Q_1)>) => (forall [a](not []Q_1)) >,
     a#Q_1 |- < (forall [a](not [(a b)]Q_1)) <= (not <(exists [b][]Q_1)>) => (forall [b](not []Q_1)) > }
(9 on 9): 
   {  |- < (exists [a](not []Q_1)) <= (not <(forall [a][]Q_1)>) => (exists [a](not []Q_1)) >,
     a#Q_1 |- < (exists [a](not [(a b)]Q_1)) <= (not <(forall [b][]Q_1)>) => (exists [b](not []Q_1)) > }
(10 on 0): 
   { a#P_1,a#Q_1 |- < (and <[]P_1,[]Q_1>) <= (and <[]P_1,(forall [a][]Q_1)>) => (forall [a](and <[]P_1,[]Q_1>)) >,
     b#P_1,a#Q_1,b#Q_1 |- < (and <[]P_1,[(a b)]Q_1>) <= (and <[]P_1,(forall [b][]Q_1)>) => (forall [b](and <[]P_1,[]Q_1>)) > }
(10 on 1): 
   { a#P_1,a#Q_1 |- < (and <[]Q_1,[]P_1>) <= (and <(forall [a][]Q_1),[]P_1>) => (forall [a](and <[]Q_1,[]P_1>)) >,
     b#P_1,a#Q_1,b#Q_1 |- < (and <[(a b)]Q_1,[]P_1>) <= (and <(forall [b][]Q_1),[]P_1>) => (forall [b](and <[]Q_1,[]P_1>)) > }
(10 on 2): 
   { a#P_1,a#Q_1 |- < (or <[]P_1,[]Q_1>) <= (or <[]P_1,(forall [a][]Q_1)>) => (forall [a](or <[]P_1,[]Q_1>)) >,
     b#P_1,a#Q_1,b#Q_1 |- < (or <[]P_1,[(a b)]Q_1>) <= (or <[]P_1,(forall [b][]Q_1)>) => (forall [b](or <[]P_1,[]Q_1>)) > }
(10 on 3): 
   { a#P_1,a#Q_1 |- < (or <[]Q_1,[]P_1>) <= (or <(forall [a][]Q_1),[]P_1>) => (forall [a](or <[]Q_1,[]P_1>)) >,
     b#P_1,a#Q_1,b#Q_1 |- < (or <[(a b)]Q_1,[]P_1>) <= (or <(forall [b][]Q_1),[]P_1>) => (forall [b](or <[]Q_1,[]P_1>)) > }
(10 on 9): 
   { a#Q_1 |- < (not <[]Q_1>) <= (not <(forall [a][]Q_1)>) => (exists [a](not []Q_1)) >,
     a#Q_1,b#Q_1 |- < (not <[(a b)]Q_1>) <= (not <(forall [b][]Q_1)>) => (exists [b](not []Q_1)) > }
(10 on 10): 
   { a#X_1 |- < []X_1 <= (forall [a][]X_1) => []X_1 >,
     b#X_1,a#X_1 |- < [(a b)]X_1 <= (forall [b][]X_1) => []X_1 > }
(10 on 11): 
   { a#X_1 |- < (and <[]X_1,(forall [a][]Y_1)>) <= (and <(forall [a][]X_1),(forall [a][]Y_1)>) => (forall [a](and <[]X_1,[]Y_1>)) >,
     a#X_1,b#X_1 |- < (and <[(a b)]X_1,(forall [b][]Y_1)>) <= (and <(forall [b][]X_1),(forall [b][]Y_1)>) => (forall [b](and <[]X_1,[]Y_1>)) >,
     a#Y_1 |- < (and <(forall [a][]X_1),[]Y_1>) <= (and <(forall [a][]X_1),(forall [a][]Y_1)>) => (forall [a](and <[]X_1,[]Y_1>)) >,
     a#Y_1,b#Y_1 |- < (and <(forall [b][]X_1),[(a b)]Y_1>) <= (and <(forall [b][]X_1),(forall [b][]Y_1)>) => (forall [b](and <[]X_1,[]Y_1>)) > }
(11 on 0): 
   {  |- < (forall [a](and <[]X,[]Q_1>)) <= (and <(forall [a][]X),(forall [a][]Q_1)>) => (forall [a](and <(forall [a][]X),[]Q_1>)) >,
     a#Q_1,b#X |- < (forall [a](and <[]X,[(a b)]Q_1>)) <= (and <(forall [a][]X),(forall [b][]Q_1)>) => (forall [b](and <(forall [a][]X),[]Q_1>)) > }
(11 on 1): 
   {  |- < (forall [a](and <[]Q_1,[]Y>)) <= (and <(forall [a][]Q_1),(forall [a][]Y)>) => (forall [a](and <[]Q_1,(forall [a][]Y)>)) >,
     a#Q_1,b#Y |- < (forall [a](and <[(a b)]Q_1,[]Y>)) <= (and <(forall [b][]Q_1),(forall [a][]Y)>) => (forall [b](and <[]Q_1,(forall [a][]Y)>)) > }
(11 on 11): 
   {  |- < (forall [a](and <[]X_1,[]Y_1>)) <= (and <(forall [a][]X_1),(forall [a][]Y_1)>) => (forall [a](and <[]X_1,[]Y_1>)) >,
     a#X_1,a#Y_1 |- < (forall [a](and <[(a b)]X_1,[(a b)]Y_1>)) <= (and <(forall [b][]X_1),(forall [b][]Y_1)>) => (forall [b](and <[]X_1,[]Y_1>)) > }
(12 on 4): 
   { a#P_1,a#Q_1 |- < (and <[]P_1,[]Q_1>) <= (and <[]P_1,(exists [a][]Q_1)>) => (exists [a](and <[]P_1,[]Q_1>)) >,
     b#P_1,a#Q_1,b#Q_1 |- < (and <[]P_1,[(a b)]Q_1>) <= (and <[]P_1,(exists [b][]Q_1)>) => (exists [b](and <[]P_1,[]Q_1>)) > }
(12 on 5): 
   { a#P_1,a#Q_1 |- < (and <[]Q_1,[]P_1>) <= (and <(exists [a][]Q_1),[]P_1>) => (exists [a](and <[]Q_1,[]P_1>)) >,
     b#P_1,a#Q_1,b#Q_1 |- < (and <[(a b)]Q_1,[]P_1>) <= (and <(exists [b][]Q_1),[]P_1>) => (exists [b](and <[]Q_1,[]P_1>)) > }
(12 on 6): 
   { a#P_1,a#Q_1 |- < (or <[]P_1,[]Q_1>) <= (or <[]P_1,(exists [a][]Q_1)>) => (exists [a](or <[]P_1,[]Q_1>)) >,
     b#P_1,a#Q_1,b#Q_1 |- < (or <[]P_1,[(a b)]Q_1>) <= (or <[]P_1,(exists [b][]Q_1)>) => (exists [b](or <[]P_1,[]Q_1>)) > }
(12 on 7): 
   { a#P_1,a#Q_1 |- < (or <[]Q_1,[]P_1>) <= (or <(exists [a][]Q_1),[]P_1>) => (exists [a](or <[]Q_1,[]P_1>)) >,
     b#P_1,a#Q_1,b#Q_1 |- < (or <[(a b)]Q_1,[]P_1>) <= (or <(exists [b][]Q_1),[]P_1>) => (exists [b](or <[]Q_1,[]P_1>)) > }
(12 on 8): 
   { a#Q_1 |- < (not <[]Q_1>) <= (not <(exists [a][]Q_1)>) => (forall [a](not []Q_1)) >,
     a#Q_1,b#Q_1 |- < (not <[(a b)]Q_1>) <= (not <(exists [b][]Q_1)>) => (forall [b](not []Q_1)) > }
(12 on 12): 
   { a#X_1 |- < []X_1 <= (exists [a][]X_1) => []X_1 >,
     b#X_1,a#X_1 |- < [(a b)]X_1 <= (exists [b][]X_1) => []X_1 > }
(12 on 13): 
   { a#X_1 |- < (or <[]X_1,(exists [a][]Y_1)>) <= (or <(exists [a][]X_1),(exists [a][]Y_1)>) => (exists [a](or <[]X_1,[]Y_1>)) >,
     a#X_1,b#X_1 |- < (or <[(a b)]X_1,(exists [b][]Y_1)>) <= (or <(exists [b][]X_1),(exists [b][]Y_1)>) => (exists [b](or <[]X_1,[]Y_1>)) >,
     a#Y_1 |- < (or <(exists [a][]X_1),[]Y_1>) <= (or <(exists [a][]X_1),(exists [a][]Y_1)>) => (exists [a](or <[]X_1,[]Y_1>)) >,
     a#Y_1,b#Y_1 |- < (or <(exists [b][]X_1),[(a b)]Y_1>) <= (or <(exists [b][]X_1),(exists [b][]Y_1)>) => (exists [b](or <[]X_1,[]Y_1>)) > }
(13 on 6): 
   {  |- < (exists [a](or <[]X,[]Q_1>)) <= (or <(exists [a][]X),(exists [a][]Q_1)>) => (exists [a](or <(exists [a][]X),[]Q_1>)) >,
     a#Q_1,b#X |- < (exists [a](or <[]X,[(a b)]Q_1>)) <= (or <(exists [a][]X),(exists [b][]Q_1)>) => (exists [b](or <(exists [a][]X),[]Q_1>)) > }
(13 on 7): 
   {  |- < (exists [a](or <[]Q_1,[]Y>)) <= (or <(exists [a][]Q_1),(exists [a][]Y)>) => (exists [a](or <[]Q_1,(exists [a][]Y)>)) >,
     a#Q_1,b#Y |- < (exists [a](or <[(a b)]Q_1,[]Y>)) <= (or <(exists [b][]Q_1),(exists [a][]Y)>) => (exists [b](or <[]Q_1,(exists [a][]Y)>)) > }
(13 on 13): 
   {  |- < (exists [a](or <[]X_1,[]Y_1>)) <= (or <(exists [a][]X_1),(exists [a][]Y_1)>) => (exists [a](or <[]X_1,[]Y_1>)) >,
     a#X_1,a#Y_1 |- < (exists [a](or <[(a b)]X_1,[(a b)]Y_1>)) <= (or <(exists [b][]X_1),(exists [b][]Y_1)>) => (exists [b](or <[]X_1,[]Y_1>)) > }
 |- <  (forall [a](and <(forall [a][]Q_1),[]Q>)),   (forall [a](and <[]Q_1,(forall [a][]Q)>))  > is not closed
failed to show all BCPs are strongly closed
result: MAYBE
time: 36 msec.