YES
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 strongly closed criterion
linear
uniform
BCPs:
(0 on 0): 
   {  |- < (or <(not []P_1),(not []Q_1)>) <= (not <(and <[]P_1,[]Q_1>)>) => (or <(not []P_1),(not []Q_1)>) > }
(1 on 1): 
   { b#Q_1 |- < (exists [b](not [(a b)]Q_1)) <= (not <(forall [a][]Q_1)>) => (exists [b](not [(a b)]Q_1)) >,
     b#Q_1,c#Q_1 |- < (exists [b](not [(a b)]Q_1)) <= (not <(forall [a][]Q_1)>) => (exists [c](not [(a c)]Q_1)) >,
     a#Q_1 |- < (exists [b](not []Q_1)) <= (not <(forall [b][]Q_1)>) => (exists [a](not [(a b)]Q_1)) >,
     c#Q_1,a#Q_1 |- < (exists [b](not []Q_1)) <= (not <(forall [b][]Q_1)>) => (exists [c](not [(b c)]Q_1)) >,
     b#Q_1,a#Q_1 |- < (exists [b](not [(b a)(a c)]Q_1)) <= (not <(forall [c][]Q_1)>) => (exists [a](not [(a c)]Q_1)) >,
     b#Q_1,a#Q_1 |- < (exists [b](not [(b a)(a c)]Q_1)) <= (not <(forall [c][]Q_1)>) => (exists [b](not [(b c)]Q_1)) >,
     b#Q_1,a#Q_1,c#Q_1 |- < (exists [b](not [(b a)(a d)]Q_1)) <= (not <(forall [d][]Q_1)>) => (exists [c](not [(c d)]Q_1)) > }
all BCPs are strongly closed
result: YES
time: 0 msec.