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 orthogonality
abstract skeleton preserving
left-linear
check proper overlapping
no proper overlaps
result: YES
time: 1 msec.