MAYBE
ignored inputs:
(COMMENT Example 5.5 of [ Ayala-Lincon et al. , LSFA 2015 ] )

NRS:
   [ (0):  |- (not <(and <[]P,[]Q>)>) -> (or <(not []P),(not []Q)>),
     (1): b#Q |- (not <(forall [a][]Q)>) -> (exists [b](not [(a b)]Q)) ]
Check confluence by orthogonality
not abstract skeleton preserving
result: MAYBE
time: 0 msec.