YES
ignored inputs:
(COMMENT rules to obtain NNF of first-order formulas without DNE )

NRS:
   [ (0):  |- (not (exists [a][]Q)) -> (forall [a](not []Q)),
     (1):  |- (not (forall [a][]Q)) -> (exists [a](not []Q)),
     (2):  |- (not (and <[]P,[]Q>)) -> (or <(not []P),(not []Q)>),
     (3):  |- (not (or <[]P,[]Q>)) -> (and <(not []P),(not []Q)>) ]
Check confluence by parallel closed criterion
left-linear
uniform
BCPs:
(0 on 0(out)): 
   {  |- < (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)) > }
(1 on 1(out)): 
   {  |- < (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)) > }
(2 on 2(out)): 
   {  |- < (or <(not []P_1),(not []Q_1)>) <= (not (and <[]P_1,[]Q_1>)) => (or <(not []P_1),(not []Q_1)>) > }
(3 on 3(out)): 
   {  |- < (and <(not []P_1),(not []Q_1)>) <= (not (or <[]P_1,[]Q_1>)) => (and <(not []P_1),(not []Q_1)>) > }
all BCPs are parallel closed
result: YES
time: 4 msec.