MAYBE
ignored inputs:
(COMMENT rules to obtain NNF of first-order formulas with negations and quantifers )
(COMMENT Example 29 of [ Suzuki et al. , SCSS 2016 ] )

NRS:
   [ (0):  |- (not (exists [a][]Q)) -> (forall [a](not []Q)),
     (1):  |- (not (forall [a][]Q)) -> (exists [a](not []Q)),
     (2):  |- (not (not []P)) -> []P ]
Check confluence by strongly closed criterion
linear
uniform
BCPs:
(0 on 0): 
   {  |- < (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)) > }
(0 on 2): 
   {  |- < (not (forall [a](not []Q))) <= (not (not (exists [a][]Q))) => (exists [a][]Q) > }
(1 on 1): 
   {  |- < (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)) > }
(1 on 2): 
   {  |- < (not (exists [a](not []Q))) <= (not (not (forall [a][]Q))) => (forall [a][]Q) > }
(2 on 2): 
   {  |- < []P_1 <= (not (not []P_1)) => []P_1 >,
      |- < (not []P) <= (not (not (not []P))) => (not []P) > }
 |- <  (not (forall [a](not []Q))),   (exists [a][]Q)  > is not closed
failed to show all BCPs are strongly closed
result: MAYBE
time: 0 msec.