(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 ] not Overlay, check Termination... unknown/not Terminating unknown Knuth & Bendix Linear unknown Development Closed unknown Strongly Closed unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow unknown Upside-Parallel-Closed/Outside-Closed (inner) Parallel CPs: (not computed) unknown Toyama (Parallel CPs) Simultaneous CPs: [ ?x_8 = Q(Q(p(p(?x_8)))), ?x = p(Q(Q(p(?x)))), p(q(q(?x_1))) = q(q(p(?x_1))), p(Q(Q(p(?x_3)))) = q(q(Q(Q(?x_3)))), p(?x_8) = q(q(P(?x_8))), q(q(q(q(?x_1)))) = p(q(q(p(?x_1)))), q(q(Q(Q(p(?x_3))))) = p(q(q(Q(Q(?x_3))))), q(q(?x_8)) = p(q(q(P(?x_8)))), p(q(q(q(q(?x_1))))) = q(q(q(q(p(?x_1))))), p(q(q(Q(Q(p(?x_3)))))) = q(q(q(q(Q(Q(?x_3)))))), p(q(q(?x_8))) = q(q(q(q(P(?x_8))))), q(q(?x_1)) = P(q(q(p(?x_1)))), Q(Q(p(?x_3))) = P(q(q(Q(Q(?x_3))))), ?x_8 = P(q(q(P(?x_8)))), q(q(p(?x))) = p(q(q(?x))), p(q(q(p(?x)))) = q(q(q(q(?x)))), p(?x) = P(q(q(?x))), p(Q(q(p(Q(?x_4))))) = Q(Q(p(p(q(?x_4))))), p(Q(?x_7)) = Q(Q(p(q(?x_7)))), q(q(Q(q(p(Q(?x_4)))))) = p(Q(Q(p(p(q(?x_4)))))), q(q(Q(?x_7))) = p(Q(Q(p(q(?x_7))))), p(q(q(Q(q(p(Q(?x_4))))))) = q(q(Q(Q(p(p(q(?x_4))))))), p(q(q(Q(?x_7)))) = q(q(Q(Q(p(q(?x_7)))))), Q(q(p(Q(?x_4)))) = P(Q(Q(p(p(q(?x_4)))))), Q(?x_7) = P(Q(Q(p(q(?x_7))))), q(q(Q(Q(?x)))) = p(Q(Q(p(?x)))), p(q(q(Q(Q(?x))))) = q(q(Q(Q(p(?x))))), Q(Q(?x)) = P(Q(Q(p(?x)))), Q(p(p(q(q(?x_5))))) = q(p(Q(q(p(?x_5))))), Q(p(?x_6)) = q(p(Q(Q(?x_6)))), Q(Q(p(p(p(q(q(?x_5))))))) = p(Q(q(p(Q(q(p(?x_5))))))), Q(Q(p(p(?x_6)))) = p(Q(q(p(Q(Q(?x_6)))))), p(p(q(q(?x_5)))) = q(q(p(Q(q(p(?x_5)))))), p(?x_6) = q(q(p(Q(Q(?x_6))))), Q(Q(p(p(q(?x))))) = p(Q(q(p(Q(?x))))), p(q(?x)) = q(q(p(Q(?x)))), q(p(Q(q(q(q(?x_3)))))) = Q(p(p(q(q(p(?x_3)))))), q(p(Q(q(Q(Q(p(?x_4))))))) = Q(p(p(q(q(Q(Q(?x_4))))))), q(p(Q(q(?x_8)))) = Q(p(p(q(q(P(?x_8)))))), q(q(q(?x_3))) = Q(p(q(q(p(?x_3))))), q(Q(Q(p(?x_4)))) = Q(p(q(q(Q(Q(?x_4)))))), q(?x_8) = Q(p(q(q(P(?x_8))))), q(p(Q(q(p(?x))))) = Q(p(p(q(q(?x))))), q(p(?x)) = Q(p(q(q(?x)))), q(q(p(Q(?x_5)))) = p(q(?x_5)), q(?x_7) = q(?x_7), q(p(Q(q(p(Q(?x_5)))))) = Q(p(p(q(?x_5)))), q(p(Q(?x_7))) = Q(p(q(?x_7))), ?x_7 = Q(q(?x_7)), q(p(Q(Q(?x)))) = Q(p(?x)), Q(?x) = Q(?x), Q(p(q(q(?x_6)))) = q(p(?x_6)), Q(Q(p(p(q(q(?x_6)))))) = p(Q(q(p(?x_6)))), Q(Q(p(?x_7))) = p(Q(Q(?x_7))), ?x_7 = q(Q(?x_7)), Q(Q(p(q(?x)))) = p(Q(?x)), p(Q(Q(p(?x)))) = ?x, p(?x_9) = p(?x_9), q(q(Q(Q(p(?x))))) = p(?x), q(q(?x_9)) = p(p(?x_9)), p(q(q(Q(Q(p(?x)))))) = q(q(?x)), Q(Q(p(?x))) = P(?x), ?x_9 = P(p(?x_9)), q(q(P(?x))) = p(?x), p(q(q(P(?x)))) = q(q(?x)), P(?x) = P(?x), Q(Q(p(q(q(?x_3))))) = p(?x_3), Q(Q(p(Q(Q(p(?x_4)))))) = Q(Q(?x_4)), Q(Q(p(p(?x)))) = ?x, P(q(q(?x_3))) = p(?x_3), P(Q(Q(p(?x_4)))) = Q(Q(?x_4)), ?x_9 = p(P(?x_9)) ] unknown Okui (Simultaneous CPs) unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping check Locally Decreasing Diagrams by Rule Labelling... Critical Pair by Rules <2, 1> preceded by [(p,1)] joinable by a reduction of rules <[([],2),([(Q,1),(Q,1)],1),([(Q,1)],6),([],6)], [([(q,1)],5),([],5)]> Critical Pair by Rules <7, 1> preceded by [(p,1)] joinable by a reduction of rules <[], [([(q,1),(q,1)],0),([(q,1)],5),([],5)]> Critical Pair by Rules <3, 2> preceded by [(p,1),(Q,1)] joinable by a reduction of rules <[([(p,1)],6),([],1),([(q,1)],5)], [([(Q,1),(Q,1)],1),([(Q,1)],6),([],6)]> Critical Pair by Rules <6, 2> preceded by [(p,1),(Q,1)] joinable by a reduction of rules <[], [([(Q,1)],3),([],6)]> Critical Pair by Rules <4, 3> preceded by [(Q,1),(p,1)] joinable by a reduction of rules <[([(Q,1)],1),([],6)], [([(q,1),(p,1)],6),([(q,1)],1)]> Critical Pair by Rules <5, 3> preceded by [(Q,1),(p,1)] joinable by a reduction of rules <[], [([(q,1)],2),([],5)]> Critical Pair by Rules <1, 4> preceded by [(q,1),(q,1)] joinable by a reduction of rules <[], [([(p,1)],4),([],1)]> Critical Pair by Rules <2, 4> preceded by [(q,1),(q,1)] joinable by a reduction of rules <[([(q,1)],5),([],5)], [([(p,1),(q,1)],5),([(p,1)],5)]> Critical Pair by Rules <7, 4> preceded by [(q,1),(q,1)] joinable by a reduction of rules <[], [([(p,1),(q,1),(q,1)],0),([(p,1),(q,1)],5),([(p,1)],5),([],1)]> Critical Pair by Rules <3, 5> preceded by [(q,1)] joinable by a reduction of rules <[([],4),([(p,1),(q,1)],5)], []> Critical Pair by Rules <6, 5> preceded by [(q,1)] joinable by a reduction of rules <[], []> Critical Pair by Rules <4, 6> preceded by [(Q,1)] joinable by a reduction of rules <[([],3),([(q,1),(p,1)],6)], []> Critical Pair by Rules <5, 6> preceded by [(Q,1)] joinable by a reduction of rules <[], []> Critical Pair by Rules <0, 7> preceded by [(p,1)] joinable by a reduction of rules <[([],2),([(Q,1),(Q,1)],1),([(Q,1)],6),([],6)], []> Critical Pair by Rules <8, 7> preceded by [(p,1)] joinable by a reduction of rules <[], []> Critical Pair by Rules <1, 8> preceded by [(P,1)] joinable by a reduction of rules <[([],0),([(Q,1)],3),([(Q,1),(q,1),(p,1)],6),([],6)], []> joinable by a reduction of rules <[([],0),([(Q,1)],3),([],6),([(p,1)],6)], []> Critical Pair by Rules <2, 8> preceded by [(P,1)] joinable by a reduction of rules <[([],0),([(Q,1),(Q,1)],2),([(Q,1),(Q,1),(Q,1),(Q,1)],1),([(Q,1),(Q,1),(Q,1)],6),([(Q,1),(Q,1)],6)], []> Critical Pair by Rules <7, 8> preceded by [(P,1)] joinable by a reduction of rules <[], []> Critical Pair by Rules <1, 1> preceded by [(p,1)] joinable by a reduction of rules <[], [([],4)]> Critical Pair by Rules <8, 0> preceded by [] joinable by a reduction of rules <[], [([(Q,1),(Q,1)],1),([(Q,1)],6),([],6)]> unknown Diagram Decreasing check Non-Confluence... obtain 13 rules by 3 steps unfolding obtain 100 candidates for checking non-joinability check by TCAP-Approximation (failure) check by Ordering(rpo), check by Tree-Automata Approximation (failure) check by Interpretation(mod2) (failure) check by Descendants-Approximation, check by Ordering(poly) (failure) unknown Non-Confluence unknown Huet (modulo AC) check by Reduction-Preserving Completion... failure(empty P) unknown Reduction-Preserving Completion Direct Methods: Can't judge Try Persistent Decomposition for... [ 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 ] Sort Assignment: P : 18=>18 Q : 18=>18 p : 18=>18 q : 18=>18 maximal types: {18} Persistent Decomposition failed: Can't judge Try Layer Preserving Decomposition for... [ 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 ] Layer Preserving Decomposition failed: Can't judge Try Commutative Decomposition for... [ 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 ] Outside Critical Pair: by Rules <8, 0> develop reducts from lhs term... <{}, ?x_8> develop reducts from rhs term... <{1}, Q(Q(q(q(?x_8))))> <{}, Q(Q(p(p(?x_8))))> Inside Critical Pair: by Rules <2, 1> develop reducts from lhs term... <{2}, Q(Q(p(p(?x_2))))> <{}, p(Q(Q(p(?x_2))))> develop reducts from rhs term... <{5}, q(Q(?x_2))> <{}, q(q(Q(Q(?x_2))))> Inside Critical Pair: by Rules <7, 1> develop reducts from lhs term... <{}, p(?x_7)> develop reducts from rhs term... <{0}, q(q(Q(Q(p(?x_7)))))> <{}, q(q(P(?x_7)))> Inside Critical Pair: by Rules <3, 2> develop reducts from lhs term... <{6}, p(p(Q(?x_3)))> <{}, p(Q(q(p(Q(?x_3)))))> develop reducts from rhs term... <{1}, Q(Q(q(q(q(?x_3)))))> <{}, Q(Q(p(p(q(?x_3)))))> Inside Critical Pair: by Rules <6, 2> develop reducts from lhs term... <{}, p(Q(?x_6))> develop reducts from rhs term... <{3}, Q(q(p(Q(?x_6))))> <{}, Q(Q(p(q(?x_6))))> Inside Critical Pair: by Rules <4, 3> develop reducts from lhs term... <{1}, Q(q(q(q(q(?x_4)))))> <{}, Q(p(p(q(q(?x_4)))))> develop reducts from rhs term... <{6}, q(p(p(?x_4)))> <{}, q(p(Q(q(p(?x_4)))))> Inside Critical Pair: by Rules <5, 3> develop reducts from lhs term... <{}, Q(p(?x_5))> develop reducts from rhs term... <{2}, q(Q(Q(p(?x_5))))> <{}, q(p(Q(Q(?x_5))))> Inside Critical Pair: by Rules <1, 4> develop reducts from lhs term... <{}, q(q(q(q(?x_1))))> develop reducts from rhs term... <{4}, p(p(q(q(?x_1))))> <{}, p(q(q(p(?x_1))))> Inside Critical Pair: by Rules <2, 4> develop reducts from lhs term... <{5}, q(Q(p(?x_2)))> <{}, q(q(Q(Q(p(?x_2)))))> develop reducts from rhs term... <{5}, p(q(Q(?x_2)))> <{}, p(q(q(Q(Q(?x_2)))))> Inside Critical Pair: by Rules <7, 4> develop reducts from lhs term... <{}, q(q(?x_7))> develop reducts from rhs term... <{0}, p(q(q(Q(Q(p(?x_7))))))> <{}, p(q(q(P(?x_7))))> Inside Critical Pair: by Rules <3, 5> develop reducts from lhs term... <{4}, p(q(q(Q(?x_3))))> <{}, q(q(p(Q(?x_3))))> develop reducts from rhs term... <{}, p(q(?x_3))> Inside Critical Pair: by Rules <6, 5> develop reducts from lhs term... <{}, q(?x_6)> develop reducts from rhs term... <{}, q(?x_6)> Inside Critical Pair: by Rules <4, 6> develop reducts from lhs term... <{3}, q(p(Q(q(?x_4))))> <{}, Q(p(q(q(?x_4))))> develop reducts from rhs term... <{}, q(p(?x_4))> Inside Critical Pair: by Rules <5, 6> develop reducts from lhs term... <{}, Q(?x_5)> develop reducts from rhs term... <{}, Q(?x_5)> Inside Critical Pair: by Rules <0, 7> develop reducts from lhs term... <{2}, Q(Q(p(p(?x))))> <{}, p(Q(Q(p(?x))))> develop reducts from rhs term... <{}, ?x> Inside Critical Pair: by Rules <8, 7> develop reducts from lhs term... <{}, p(?x_8)> develop reducts from rhs term... <{}, p(?x_8)> Inside Critical Pair: by Rules <1, 8> develop reducts from lhs term... <{0}, Q(Q(p(q(q(?x_1)))))> <{}, P(q(q(?x_1)))> develop reducts from rhs term... <{}, p(?x_1)> Inside Critical Pair: by Rules <2, 8> develop reducts from lhs term... <{0}, Q(Q(p(Q(Q(p(?x_2))))))> <{}, P(Q(Q(p(?x_2))))> develop reducts from rhs term... <{}, Q(Q(?x_2))> Inside Critical Pair: by Rules <7, 8> develop reducts from lhs term... <{0}, Q(Q(p(?x_7)))> <{}, P(?x_7)> develop reducts from rhs term... <{0}, Q(Q(p(?x_7)))> <{}, P(?x_7)> Commutative Decomposition failed: Can't judge No further decomposition possible Combined result: Can't judge 942.trs: Failure(unknown CR) MAYBE (1996 msec.)