MAYBE
(ignored inputs)COMMENT TPDB SRS_Standard/Zantema_04/z067
Rewrite Rules:
   [ P(?x) -> Q(Q(p(?x))),
     p(p(?x)) -> q(q(?x)),
     p(Q(Q(?x))) -> Q(Q(p(?x))),
     Q(p(q(?x))) -> q(p(Q(?x))),
     q(q(p(?x))) -> p(q(q(?x))),
     q(Q(?x)) -> ?x,
     Q(q(?x)) -> ?x,
     p(P(?x)) -> ?x,
     P(p(?x)) -> ?x ]
Apply Direct Methods...
Inner CPs:
   [ p(Q(Q(p(?x_2)))) = q(q(Q(Q(?x_2)))),
     p(?x_7) = q(q(P(?x_7))),
     p(Q(q(p(Q(?x_3))))) = Q(Q(p(p(q(?x_3))))),
     p(Q(?x_6)) = Q(Q(p(q(?x_6)))),
     Q(p(p(q(q(?x_4))))) = q(p(Q(q(p(?x_4))))),
     Q(p(?x_5)) = q(p(Q(Q(?x_5)))),
     q(q(q(q(?x_1)))) = p(q(q(p(?x_1)))),
     q(q(Q(Q(p(?x_2))))) = p(q(q(Q(Q(?x_2))))),
     q(q(?x_7)) = p(q(q(P(?x_7)))),
     q(q(p(Q(?x_3)))) = p(q(?x_3)),
     q(?x_6) = q(?x_6),
     Q(p(q(q(?x_4)))) = q(p(?x_4)),
     Q(?x_5) = Q(?x_5),
     p(Q(Q(p(?x)))) = ?x,
     p(?x_8) = p(?x_8),
     P(q(q(?x_1))) = p(?x_1),
     P(Q(Q(p(?x_2)))) = Q(Q(?x_2)),
     P(?x_7) = P(?x_7),
     p(q(q(?x))) = q(q(p(?x))) ]
Outer CPs:
   [ Q(Q(p(p(?x_8)))) = ?x_8 ]
Linear
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Direct Methods: Can't judge

Combined result: Can't judge
942.trs: Failure(unknown CR)
(0 msec.)