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 orthogonality
abstract skeleton preserving
left-linear
check proper overlapping
a proper overlap exists
0-2
 |- < (not (forall [a](not []Q))) <= (not (not (exists [a][]Q))) => (exists [a][]Q) >
found proper overlaps
result: MAYBE
time: 0 msec.