(ignored inputs)COMMENT TPDB SRS_Standard/Zantema_04/z068 Rewrite Rules: [ C(?x) -> c(?x), c(c(?x)) -> ?x, b(b(?x)) -> B(?x), B(B(?x)) -> b(?x), c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))), b(B(?x)) -> ?x, B(b(?x)) -> ?x, c(C(?x)) -> ?x, C(c(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ c(B(c(b(c(B(c(b(?x_4)))))))) = B(c(b(c(?x_4)))), c(?x_7) = C(?x_7), b(?x_5) = B(B(?x_5)), B(?x_6) = b(b(?x_6)), c(B(c(b(?x_1)))) = B(c(b(c(B(c(b(c(?x_1)))))))), c(B(c(b(?x_7)))) = B(c(b(c(B(c(b(C(?x_7)))))))), b(b(?x_3)) = B(?x_3), b(?x_6) = b(?x_6), B(B(?x_2)) = b(?x_2), B(?x_5) = B(?x_5), c(c(?x)) = ?x, c(?x_8) = c(?x_8), C(?x_1) = c(?x_1), C(B(c(b(c(B(c(b(?x_4)))))))) = B(c(b(c(?x_4)))), C(?x_7) = C(?x_7), c(?x) = c(?x), b(B(?x)) = B(b(?x)), B(b(?x)) = b(B(?x)), c(B(c(b(B(c(b(c(B(c(b(?x))))))))))) = B(c(b(c(B(c(b(B(c(b(c(?x))))))))))) ] Outer CPs: [ c(c(?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 inner CP cond (upside-parallel) innter CP Cond (outside) unknown Upside-Parallel-Closed/Outside-Closed (inner) Parallel CPs: (not computed) unknown Toyama (Parallel CPs) Simultaneous CPs: [ ?x_8 = c(c(?x_8)), c(?x_1) = c(?x_1), c(B(c(b(c(B(c(b(?x_5)))))))) = B(c(b(c(?x_5)))), c(?x_8) = C(?x_8), B(c(b(c(B(c(b(?x_5))))))) = c(B(c(b(c(?x_5))))), ?x_8 = c(C(?x_8)), B(c(b(c(B(c(b(B(c(b(c(B(c(b(?x_5)))))))))))))) = c(B(c(b(B(c(b(c(?x_5)))))))), B(c(b(c(B(c(b(?x_8))))))) = c(B(c(b(C(?x_8))))), ?x_1 = C(c(?x_1)), B(c(b(c(B(c(b(?x_5))))))) = C(B(c(b(c(?x_5))))), ?x_8 = C(C(?x_8)), B(c(b(c(B(c(b(c(?x)))))))) = c(B(c(b(?x)))), b(B(?x_1)) = B(b(?x_1)), b(?x_6) = B(B(?x_6)), B(B(?x_1)) = b(B(b(?x_1))), B(?x_6) = b(B(B(?x_6))), B(?x_1) = B(B(b(?x_1))), ?x_6 = B(B(B(?x_6))), B(b(?x)) = b(B(?x)), B(?x_7) = b(b(?x_7)), b(b(?x_1)) = B(b(B(?x_1))), b(?x_7) = B(b(b(?x_7))), b(?x_1) = b(b(B(?x_1))), ?x_7 = b(b(b(?x_7))), c(B(c(b(B(c(b(c(B(c(b(?x_1))))))))))) = B(c(b(c(B(c(b(B(c(b(c(?x_1))))))))))), c(B(c(b(?x_3)))) = B(c(b(c(B(c(b(c(?x_3)))))))), c(B(c(b(?x_8)))) = B(c(b(c(B(c(b(C(?x_8)))))))), B(c(b(c(B(c(b(B(c(b(B(c(b(c(B(c(b(?x_1))))))))))))))))) = c(B(c(b(B(c(b(c(B(c(b(B(c(b(c(?x_1))))))))))))))), B(c(b(c(B(c(b(B(c(b(?x_3)))))))))) = c(B(c(b(B(c(b(c(B(c(b(c(?x_3)))))))))))), B(c(b(c(B(c(b(B(c(b(?x_8)))))))))) = c(B(c(b(B(c(b(c(B(c(b(C(?x_8)))))))))))), B(c(b(B(c(b(c(B(c(b(?x_1)))))))))) = c(B(c(b(c(B(c(b(B(c(b(c(?x_1)))))))))))), B(c(b(?x_3))) = c(B(c(b(c(B(c(b(c(?x_3))))))))), B(c(b(?x_8))) = c(B(c(b(c(B(c(b(C(?x_8))))))))), B(c(b(B(c(b(c(B(c(b(?x_1)))))))))) = C(B(c(b(c(B(c(b(B(c(b(c(?x_1)))))))))))), B(c(b(?x_3))) = C(B(c(b(c(B(c(b(c(?x_3))))))))), B(c(b(?x_8))) = C(B(c(b(c(B(c(b(C(?x_8))))))))), B(c(b(c(B(c(b(B(c(b(c(?x))))))))))) = c(B(c(b(B(c(b(c(B(c(b(?x))))))))))), B(c(b(c(?x)))) = c(B(c(b(c(B(c(b(?x)))))))), B(c(b(c(?x)))) = C(B(c(b(c(B(c(b(?x)))))))), b(b(?x_5)) = B(?x_5), b(?x_7) = b(?x_7), ?x_7 = B(b(?x_7)), B(B(?x)) = b(?x), B(?x) = B(?x), ?x_7 = b(B(?x_7)), c(c(?x)) = ?x, C(?x) = c(?x), B(c(b(c(B(c(b(C(?x)))))))) = c(B(c(b(?x)))), C(?x) = C(?x), C(B(c(b(c(B(c(b(?x_6)))))))) = B(c(b(c(?x_6)))) ] 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 <4, 1> preceded by [(c,1)] joinable by a reduction of rules <[([],4),([(B,1),(c,1),(b,1),(c,1),(B,1),(c,1)],5),([(B,1),(c,1),(b,1),(c,1),(B,1)],1),([(B,1),(c,1),(b,1),(c,1)],6)], []> Critical Pair by Rules <7, 1> preceded by [(c,1)] joinable by a reduction of rules <[], [([],0)]> Critical Pair by Rules <5, 2> preceded by [(b,1)] joinable by a reduction of rules <[], [([],3)]> Critical Pair by Rules <6, 3> preceded by [(B,1)] joinable by a reduction of rules <[], [([],2)]> Critical Pair by Rules <1, 4> preceded by [(c,1),(B,1),(c,1),(b,1)] joinable by a reduction of rules <[], [([(B,1),(c,1),(b,1)],4),([(B,1),(c,1)],5),([(B,1)],1),([],6)]> Critical Pair by Rules <7, 4> preceded by [(c,1),(B,1),(c,1),(b,1)] joinable by a reduction of rules <[], [([(B,1),(c,1),(b,1),(c,1),(B,1),(c,1),(b,1)],0),([(B,1),(c,1),(b,1)],4),([(B,1),(c,1)],5),([(B,1)],1),([],6)]> Critical Pair by Rules <3, 5> preceded by [(b,1)] joinable by a reduction of rules <[([],2)], []> Critical Pair by Rules <6, 5> preceded by [(b,1)] joinable by a reduction of rules <[], []> Critical Pair by Rules <2, 6> preceded by [(B,1)] joinable by a reduction of rules <[([],3)], []> Critical Pair by Rules <5, 6> preceded by [(B,1)] joinable by a reduction of rules <[], []> Critical Pair by Rules <0, 7> preceded by [(c,1)] joinable by a reduction of rules <[([],1)], []> Critical Pair by Rules <8, 7> preceded by [(c,1)] joinable by a reduction of rules <[], []> Critical Pair by Rules <1, 8> preceded by [(C,1)] joinable by a reduction of rules <[([],0)], []> Critical Pair by Rules <4, 8> preceded by [(C,1)] joinable by a reduction of rules <[([],0),([],4),([(B,1),(c,1),(b,1),(c,1),(B,1),(c,1)],5),([(B,1),(c,1),(b,1),(c,1),(B,1)],1),([(B,1),(c,1),(b,1),(c,1)],6)], []> Critical Pair by Rules <7, 8> preceded by [(C,1)] joinable by a reduction of rules <[], []> Critical Pair by Rules <1, 1> preceded by [(c,1)] joinable by a reduction of rules <[], []> Critical Pair by Rules <2, 2> preceded by [(b,1)] joinable by a reduction of rules <[([],5)], [([],6)]> Critical Pair by Rules <3, 3> preceded by [(B,1)] joinable by a reduction of rules <[([],6)], [([],5)]> Critical Pair by Rules <4, 4> preceded by [(c,1),(B,1),(c,1),(b,1)] joinable by a reduction of rules <[([(c,1),(B,1),(c,1)],5),([(c,1),(B,1)],1),([(c,1)],6),([],1)], [([(B,1),(c,1),(b,1),(c,1),(B,1),(c,1)],5),([(B,1),(c,1),(b,1),(c,1),(B,1)],1),([(B,1),(c,1),(b,1),(c,1)],6),([(B,1),(c,1),(b,1)],1)]> Critical Pair by Rules <8, 0> preceded by [] joinable by a reduction of rules <[], [([],1)]> unknown Diagram Decreasing check Non-Confluence... obtain 10 rules by 3 steps unfolding obtain 35 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... [ C(?x) -> c(?x), c(c(?x)) -> ?x, b(b(?x)) -> B(?x), B(B(?x)) -> b(?x), c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))), b(B(?x)) -> ?x, B(b(?x)) -> ?x, c(C(?x)) -> ?x, C(c(?x)) -> ?x ] Sort Assignment: B : 18=>18 C : 18=>18 b : 18=>18 c : 18=>18 maximal types: {18} Persistent Decomposition failed: Can't judge Try Layer Preserving Decomposition for... [ C(?x) -> c(?x), c(c(?x)) -> ?x, b(b(?x)) -> B(?x), B(B(?x)) -> b(?x), c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))), b(B(?x)) -> ?x, B(b(?x)) -> ?x, c(C(?x)) -> ?x, C(c(?x)) -> ?x ] Layer Preserving Decomposition failed: Can't judge Try Commutative Decomposition for... [ C(?x) -> c(?x), c(c(?x)) -> ?x, b(b(?x)) -> B(?x), B(B(?x)) -> b(?x), c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))), b(B(?x)) -> ?x, B(b(?x)) -> ?x, c(C(?x)) -> ?x, C(c(?x)) -> ?x ] Outside Critical Pair: by Rules <8, 0> develop reducts from lhs term... <{}, ?x_8> develop reducts from rhs term... <{1}, ?x_8> <{}, c(c(?x_8))> Inside Critical Pair: by Rules <4, 1> develop reducts from lhs term... <{4}, B(c(b(c(B(c(b(B(c(b(?x_4))))))))))> <{}, c(B(c(b(c(B(c(b(?x_4))))))))> develop reducts from rhs term... <{}, B(c(b(c(?x_4))))> Inside Critical Pair: by Rules <7, 1> develop reducts from lhs term... <{}, c(?x_7)> develop reducts from rhs term... <{0}, c(?x_7)> <{}, C(?x_7)> Inside Critical Pair: by Rules <5, 2> develop reducts from lhs term... <{}, b(?x_5)> develop reducts from rhs term... <{3}, b(?x_5)> <{}, B(B(?x_5))> Inside Critical Pair: by Rules <6, 3> develop reducts from lhs term... <{}, B(?x_6)> develop reducts from rhs term... <{2}, B(?x_6)> <{}, b(b(?x_6))> Inside Critical Pair: by Rules <1, 4> develop reducts from lhs term... <{}, c(B(c(b(?x_1))))> develop reducts from rhs term... <{4}, B(c(b(B(c(b(c(B(c(b(?x_1))))))))))> <{}, B(c(b(c(B(c(b(c(?x_1))))))))> Inside Critical Pair: by Rules <7, 4> develop reducts from lhs term... <{}, c(B(c(b(?x_7))))> develop reducts from rhs term... <{0}, B(c(b(c(B(c(b(c(?x_7))))))))> <{}, B(c(b(c(B(c(b(C(?x_7))))))))> Inside Critical Pair: by Rules <3, 5> develop reducts from lhs term... <{2}, B(?x_3)> <{}, b(b(?x_3))> develop reducts from rhs term... <{}, B(?x_3)> Inside Critical Pair: by Rules <6, 5> develop reducts from lhs term... <{}, b(?x_6)> develop reducts from rhs term... <{}, b(?x_6)> Inside Critical Pair: by Rules <2, 6> develop reducts from lhs term... <{3}, b(?x_2)> <{}, B(B(?x_2))> develop reducts from rhs term... <{}, b(?x_2)> Inside Critical Pair: by Rules <5, 6> develop reducts from lhs term... <{}, B(?x_5)> develop reducts from rhs term... <{}, B(?x_5)> Inside Critical Pair: by Rules <0, 7> develop reducts from lhs term... <{1}, ?x> <{}, c(c(?x))> develop reducts from rhs term... <{}, ?x> Inside Critical Pair: by Rules <8, 7> develop reducts from lhs term... <{}, c(?x_8)> develop reducts from rhs term... <{}, c(?x_8)> Inside Critical Pair: by Rules <1, 8> develop reducts from lhs term... <{0}, c(?x_1)> <{}, C(?x_1)> develop reducts from rhs term... <{}, c(?x_1)> Inside Critical Pair: by Rules <4, 8> develop reducts from lhs term... <{0}, c(B(c(b(c(B(c(b(?x_4))))))))> <{}, C(B(c(b(c(B(c(b(?x_4))))))))> develop reducts from rhs term... <{}, B(c(b(c(?x_4))))> Inside Critical Pair: by Rules <7, 8> develop reducts from lhs term... <{0}, c(?x_7)> <{}, C(?x_7)> develop reducts from rhs term... <{0}, c(?x_7)> <{}, C(?x_7)> Try A Minimal Decomposition {2,5}{3,6}{8,7,1,4}{0} {2,5} (cm)Rewrite Rules: [ b(b(?x)) -> B(?x), b(B(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ b(?x_1) = B(B(?x_1)), b(B(?x)) = B(b(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {3,6} (cm)Rewrite Rules: [ B(B(?x)) -> b(?x), B(b(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ B(?x_1) = b(b(?x_1)), B(b(?x)) = b(B(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {8,7,1,4} (cm)Rewrite Rules: [ C(c(?x)) -> ?x, c(C(?x)) -> ?x, c(c(?x)) -> ?x, c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))) ] Apply Direct Methods... Inner CPs: [ C(?x_1) = C(?x_1), C(?x_2) = c(?x_2), C(B(c(b(c(B(c(b(?x_3)))))))) = B(c(b(c(?x_3)))), c(?x) = c(?x), c(?x_1) = C(?x_1), c(B(c(b(c(B(c(b(?x_3)))))))) = B(c(b(c(?x_3)))), c(B(c(b(?x_1)))) = B(c(b(c(B(c(b(C(?x_1)))))))), c(B(c(b(?x_2)))) = B(c(b(c(B(c(b(c(?x_2)))))))), c(?x) = c(?x), c(B(c(b(B(c(b(c(B(c(b(?x))))))))))) = B(c(b(c(B(c(b(B(c(b(c(?x))))))))))) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {0} (cm)Rewrite Rules: [ C(?x) -> c(?x) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR Try A Minimal Decomposition {0,8,7,1,4}{2,5}{3,6} {0,8,7,1,4} (cm)Rewrite Rules: [ C(?x) -> c(?x), C(c(?x)) -> ?x, c(C(?x)) -> ?x, c(c(?x)) -> ?x, c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))) ] Apply Direct Methods... Inner CPs: [ C(?x_2) = C(?x_2), C(?x_3) = c(?x_3), C(B(c(b(c(B(c(b(?x_4)))))))) = B(c(b(c(?x_4)))), c(c(?x)) = ?x, c(?x_1) = c(?x_1), c(?x_2) = C(?x_2), c(B(c(b(c(B(c(b(?x_4)))))))) = B(c(b(c(?x_4)))), c(B(c(b(?x_2)))) = B(c(b(c(B(c(b(C(?x_2)))))))), c(B(c(b(?x_3)))) = B(c(b(c(B(c(b(c(?x_3)))))))), c(?x) = c(?x), c(B(c(b(B(c(b(c(B(c(b(?x))))))))))) = B(c(b(c(B(c(b(B(c(b(c(?x))))))))))) ] Outer CPs: [ c(c(?x_1)) = ?x_1 ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {2,5} (cm)Rewrite Rules: [ b(b(?x)) -> B(?x), b(B(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ b(?x_1) = B(B(?x_1)), b(B(?x)) = B(b(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {3,6} (cm)Rewrite Rules: [ B(B(?x)) -> b(?x), B(b(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ B(?x_1) = b(b(?x_1)), B(b(?x)) = b(B(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR Try A Minimal Decomposition {6,3,5}{8,7,1,4}{0}{2} {6,3,5} (cm)Rewrite Rules: [ B(b(?x)) -> ?x, B(B(?x)) -> b(?x), b(B(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ B(?x_2) = B(?x_2), B(?x) = b(b(?x)), b(?x) = b(?x), b(b(?x_1)) = B(?x_1), B(b(?x)) = b(B(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {8,7,1,4} (cm)Rewrite Rules: [ C(c(?x)) -> ?x, c(C(?x)) -> ?x, c(c(?x)) -> ?x, c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))) ] Apply Direct Methods... Inner CPs: [ C(?x_1) = C(?x_1), C(?x_2) = c(?x_2), C(B(c(b(c(B(c(b(?x_3)))))))) = B(c(b(c(?x_3)))), c(?x) = c(?x), c(?x_1) = C(?x_1), c(B(c(b(c(B(c(b(?x_3)))))))) = B(c(b(c(?x_3)))), c(B(c(b(?x_1)))) = B(c(b(c(B(c(b(C(?x_1)))))))), c(B(c(b(?x_2)))) = B(c(b(c(B(c(b(c(?x_2)))))))), c(?x) = c(?x), c(B(c(b(B(c(b(c(B(c(b(?x))))))))))) = B(c(b(c(B(c(b(B(c(b(c(?x))))))))))) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {0} (cm)Rewrite Rules: [ C(?x) -> c(?x) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {2} (cm)Rewrite Rules: [ b(b(?x)) -> B(?x) ] Apply Direct Methods... Inner CPs: [ b(B(?x)) = B(b(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR Try A Minimal Decomposition {0,8,7,1,4}{6,3,5}{2} {0,8,7,1,4} (cm)Rewrite Rules: [ C(?x) -> c(?x), C(c(?x)) -> ?x, c(C(?x)) -> ?x, c(c(?x)) -> ?x, c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))) ] Apply Direct Methods... Inner CPs: [ C(?x_2) = C(?x_2), C(?x_3) = c(?x_3), C(B(c(b(c(B(c(b(?x_4)))))))) = B(c(b(c(?x_4)))), c(c(?x)) = ?x, c(?x_1) = c(?x_1), c(?x_2) = C(?x_2), c(B(c(b(c(B(c(b(?x_4)))))))) = B(c(b(c(?x_4)))), c(B(c(b(?x_2)))) = B(c(b(c(B(c(b(C(?x_2)))))))), c(B(c(b(?x_3)))) = B(c(b(c(B(c(b(c(?x_3)))))))), c(?x) = c(?x), c(B(c(b(B(c(b(c(B(c(b(?x))))))))))) = B(c(b(c(B(c(b(B(c(b(c(?x))))))))))) ] Outer CPs: [ c(c(?x_1)) = ?x_1 ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {6,3,5} (cm)Rewrite Rules: [ B(b(?x)) -> ?x, B(B(?x)) -> b(?x), b(B(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ B(?x_2) = B(?x_2), B(?x) = b(b(?x)), b(?x) = b(?x), b(b(?x_1)) = B(?x_1), B(b(?x)) = b(B(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {2} (cm)Rewrite Rules: [ b(b(?x)) -> B(?x) ] Apply Direct Methods... Inner CPs: [ b(B(?x)) = B(b(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR Try A Minimal Decomposition {6,3,2,5}{8,7,1,4}{0} {6,3,2,5} (cm)Rewrite Rules: [ B(b(?x)) -> ?x, B(B(?x)) -> b(?x), b(b(?x)) -> B(?x), b(B(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ B(B(?x_2)) = b(?x_2), B(?x_3) = B(?x_3), B(?x) = b(b(?x)), b(?x_3) = B(B(?x_3)), b(?x) = b(?x), b(b(?x_1)) = B(?x_1), B(b(?x)) = b(B(?x)), b(B(?x)) = B(b(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, WCR Knuth & Bendix Direct Methods: CR {8,7,1,4} (cm)Rewrite Rules: [ C(c(?x)) -> ?x, c(C(?x)) -> ?x, c(c(?x)) -> ?x, c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))) ] Apply Direct Methods... Inner CPs: [ C(?x_1) = C(?x_1), C(?x_2) = c(?x_2), C(B(c(b(c(B(c(b(?x_3)))))))) = B(c(b(c(?x_3)))), c(?x) = c(?x), c(?x_1) = C(?x_1), c(B(c(b(c(B(c(b(?x_3)))))))) = B(c(b(c(?x_3)))), c(B(c(b(?x_1)))) = B(c(b(c(B(c(b(C(?x_1)))))))), c(B(c(b(?x_2)))) = B(c(b(c(B(c(b(c(?x_2)))))))), c(?x) = c(?x), c(B(c(b(B(c(b(c(B(c(b(?x))))))))))) = B(c(b(c(B(c(b(B(c(b(c(?x))))))))))) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {0} (cm)Rewrite Rules: [ C(?x) -> c(?x) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR Try A Minimal Decomposition {0,8,7,1,4}{6,3,2,5} {0,8,7,1,4} (cm)Rewrite Rules: [ C(?x) -> c(?x), C(c(?x)) -> ?x, c(C(?x)) -> ?x, c(c(?x)) -> ?x, c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))) ] Apply Direct Methods... Inner CPs: [ C(?x_2) = C(?x_2), C(?x_3) = c(?x_3), C(B(c(b(c(B(c(b(?x_4)))))))) = B(c(b(c(?x_4)))), c(c(?x)) = ?x, c(?x_1) = c(?x_1), c(?x_2) = C(?x_2), c(B(c(b(c(B(c(b(?x_4)))))))) = B(c(b(c(?x_4)))), c(B(c(b(?x_2)))) = B(c(b(c(B(c(b(C(?x_2)))))))), c(B(c(b(?x_3)))) = B(c(b(c(B(c(b(c(?x_3)))))))), c(?x) = c(?x), c(B(c(b(B(c(b(c(B(c(b(?x))))))))))) = B(c(b(c(B(c(b(B(c(b(c(?x))))))))))) ] Outer CPs: [ c(c(?x_1)) = ?x_1 ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {6,3,2,5} (cm)Rewrite Rules: [ B(b(?x)) -> ?x, B(B(?x)) -> b(?x), b(b(?x)) -> B(?x), b(B(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ B(B(?x_2)) = b(?x_2), B(?x_3) = B(?x_3), B(?x) = b(b(?x)), b(?x_3) = B(B(?x_3)), b(?x) = b(?x), b(b(?x_1)) = B(?x_1), B(b(?x)) = b(B(?x)), b(B(?x)) = B(b(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, WCR Knuth & Bendix Direct Methods: CR Try A Minimal Decomposition {6,2,5}{8,7,1,4}{0}{3} {6,2,5} (cm)Rewrite Rules: [ B(b(?x)) -> ?x, b(b(?x)) -> B(?x), b(B(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ B(B(?x_1)) = b(?x_1), B(?x_2) = B(?x_2), b(?x_2) = B(B(?x_2)), b(?x) = b(?x), b(B(?x)) = B(b(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {8,7,1,4} (cm)Rewrite Rules: [ C(c(?x)) -> ?x, c(C(?x)) -> ?x, c(c(?x)) -> ?x, c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))) ] Apply Direct Methods... Inner CPs: [ C(?x_1) = C(?x_1), C(?x_2) = c(?x_2), C(B(c(b(c(B(c(b(?x_3)))))))) = B(c(b(c(?x_3)))), c(?x) = c(?x), c(?x_1) = C(?x_1), c(B(c(b(c(B(c(b(?x_3)))))))) = B(c(b(c(?x_3)))), c(B(c(b(?x_1)))) = B(c(b(c(B(c(b(C(?x_1)))))))), c(B(c(b(?x_2)))) = B(c(b(c(B(c(b(c(?x_2)))))))), c(?x) = c(?x), c(B(c(b(B(c(b(c(B(c(b(?x))))))))))) = B(c(b(c(B(c(b(B(c(b(c(?x))))))))))) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {0} (cm)Rewrite Rules: [ C(?x) -> c(?x) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {3} (cm)Rewrite Rules: [ B(B(?x)) -> b(?x) ] Apply Direct Methods... Inner CPs: [ B(b(?x)) = b(B(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR Try A Minimal Decomposition {0,8,7,1,4}{6,2,5}{3} {0,8,7,1,4} (cm)Rewrite Rules: [ C(?x) -> c(?x), C(c(?x)) -> ?x, c(C(?x)) -> ?x, c(c(?x)) -> ?x, c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))) ] Apply Direct Methods... Inner CPs: [ C(?x_2) = C(?x_2), C(?x_3) = c(?x_3), C(B(c(b(c(B(c(b(?x_4)))))))) = B(c(b(c(?x_4)))), c(c(?x)) = ?x, c(?x_1) = c(?x_1), c(?x_2) = C(?x_2), c(B(c(b(c(B(c(b(?x_4)))))))) = B(c(b(c(?x_4)))), c(B(c(b(?x_2)))) = B(c(b(c(B(c(b(C(?x_2)))))))), c(B(c(b(?x_3)))) = B(c(b(c(B(c(b(c(?x_3)))))))), c(?x) = c(?x), c(B(c(b(B(c(b(c(B(c(b(?x))))))))))) = B(c(b(c(B(c(b(B(c(b(c(?x))))))))))) ] Outer CPs: [ c(c(?x_1)) = ?x_1 ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {6,2,5} (cm)Rewrite Rules: [ B(b(?x)) -> ?x, b(b(?x)) -> B(?x), b(B(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ B(B(?x_1)) = b(?x_1), B(?x_2) = B(?x_2), b(?x_2) = B(B(?x_2)), b(?x) = b(?x), b(B(?x)) = B(b(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {3} (cm)Rewrite Rules: [ B(B(?x)) -> b(?x) ] Apply Direct Methods... Inner CPs: [ B(b(?x)) = b(B(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR Try A Minimal Decomposition {3,6,2,5}{8,7,1,4}{0} {3,6,2,5} (cm)Rewrite Rules: [ B(B(?x)) -> b(?x), B(b(?x)) -> ?x, b(b(?x)) -> B(?x), b(B(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ B(?x_1) = b(b(?x_1)), B(B(?x_2)) = b(?x_2), B(?x_3) = B(?x_3), b(?x_3) = B(B(?x_3)), b(b(?x)) = B(?x), b(?x_1) = b(?x_1), B(b(?x)) = b(B(?x)), b(B(?x)) = B(b(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, WCR Knuth & Bendix Direct Methods: CR {8,7,1,4} (cm)Rewrite Rules: [ C(c(?x)) -> ?x, c(C(?x)) -> ?x, c(c(?x)) -> ?x, c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))) ] Apply Direct Methods... Inner CPs: [ C(?x_1) = C(?x_1), C(?x_2) = c(?x_2), C(B(c(b(c(B(c(b(?x_3)))))))) = B(c(b(c(?x_3)))), c(?x) = c(?x), c(?x_1) = C(?x_1), c(B(c(b(c(B(c(b(?x_3)))))))) = B(c(b(c(?x_3)))), c(B(c(b(?x_1)))) = B(c(b(c(B(c(b(C(?x_1)))))))), c(B(c(b(?x_2)))) = B(c(b(c(B(c(b(c(?x_2)))))))), c(?x) = c(?x), c(B(c(b(B(c(b(c(B(c(b(?x))))))))))) = B(c(b(c(B(c(b(B(c(b(c(?x))))))))))) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {0} (cm)Rewrite Rules: [ C(?x) -> c(?x) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR Try A Minimal Decomposition {0,8,7,1,4}{3,6,2,5} {0,8,7,1,4} (cm)Rewrite Rules: [ C(?x) -> c(?x), C(c(?x)) -> ?x, c(C(?x)) -> ?x, c(c(?x)) -> ?x, c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))) ] Apply Direct Methods... Inner CPs: [ C(?x_2) = C(?x_2), C(?x_3) = c(?x_3), C(B(c(b(c(B(c(b(?x_4)))))))) = B(c(b(c(?x_4)))), c(c(?x)) = ?x, c(?x_1) = c(?x_1), c(?x_2) = C(?x_2), c(B(c(b(c(B(c(b(?x_4)))))))) = B(c(b(c(?x_4)))), c(B(c(b(?x_2)))) = B(c(b(c(B(c(b(C(?x_2)))))))), c(B(c(b(?x_3)))) = B(c(b(c(B(c(b(c(?x_3)))))))), c(?x) = c(?x), c(B(c(b(B(c(b(c(B(c(b(?x))))))))))) = B(c(b(c(B(c(b(B(c(b(c(?x))))))))))) ] Outer CPs: [ c(c(?x_1)) = ?x_1 ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {3,6,2,5} (cm)Rewrite Rules: [ B(B(?x)) -> b(?x), B(b(?x)) -> ?x, b(b(?x)) -> B(?x), b(B(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ B(?x_1) = b(b(?x_1)), B(B(?x_2)) = b(?x_2), B(?x_3) = B(?x_3), b(?x_3) = B(B(?x_3)), b(b(?x)) = B(?x), b(?x_1) = b(?x_1), B(b(?x)) = b(B(?x)), b(B(?x)) = B(b(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, WCR Knuth & Bendix Direct Methods: CR Try A Minimal Decomposition {6,3,2,5}{8,7,1,4}{0} {6,3,2,5} (cm)Rewrite Rules: [ B(b(?x)) -> ?x, B(B(?x)) -> b(?x), b(b(?x)) -> B(?x), b(B(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ B(B(?x_2)) = b(?x_2), B(?x_3) = B(?x_3), B(?x) = b(b(?x)), b(?x_3) = B(B(?x_3)), b(?x) = b(?x), b(b(?x_1)) = B(?x_1), B(b(?x)) = b(B(?x)), b(B(?x)) = B(b(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, WCR Knuth & Bendix Direct Methods: CR {8,7,1,4} (cm)Rewrite Rules: [ C(c(?x)) -> ?x, c(C(?x)) -> ?x, c(c(?x)) -> ?x, c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))) ] Apply Direct Methods... Inner CPs: [ C(?x_1) = C(?x_1), C(?x_2) = c(?x_2), C(B(c(b(c(B(c(b(?x_3)))))))) = B(c(b(c(?x_3)))), c(?x) = c(?x), c(?x_1) = C(?x_1), c(B(c(b(c(B(c(b(?x_3)))))))) = B(c(b(c(?x_3)))), c(B(c(b(?x_1)))) = B(c(b(c(B(c(b(C(?x_1)))))))), c(B(c(b(?x_2)))) = B(c(b(c(B(c(b(c(?x_2)))))))), c(?x) = c(?x), c(B(c(b(B(c(b(c(B(c(b(?x))))))))))) = B(c(b(c(B(c(b(B(c(b(c(?x))))))))))) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {0} (cm)Rewrite Rules: [ C(?x) -> c(?x) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR Try A Minimal Decomposition {0,8,7,1,4}{6,3,2,5} {0,8,7,1,4} (cm)Rewrite Rules: [ C(?x) -> c(?x), C(c(?x)) -> ?x, c(C(?x)) -> ?x, c(c(?x)) -> ?x, c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))) ] Apply Direct Methods... Inner CPs: [ C(?x_2) = C(?x_2), C(?x_3) = c(?x_3), C(B(c(b(c(B(c(b(?x_4)))))))) = B(c(b(c(?x_4)))), c(c(?x)) = ?x, c(?x_1) = c(?x_1), c(?x_2) = C(?x_2), c(B(c(b(c(B(c(b(?x_4)))))))) = B(c(b(c(?x_4)))), c(B(c(b(?x_2)))) = B(c(b(c(B(c(b(C(?x_2)))))))), c(B(c(b(?x_3)))) = B(c(b(c(B(c(b(c(?x_3)))))))), c(?x) = c(?x), c(B(c(b(B(c(b(c(B(c(b(?x))))))))))) = B(c(b(c(B(c(b(B(c(b(c(?x))))))))))) ] Outer CPs: [ c(c(?x_1)) = ?x_1 ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {6,3,2,5} (cm)Rewrite Rules: [ B(b(?x)) -> ?x, B(B(?x)) -> b(?x), b(b(?x)) -> B(?x), b(B(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ B(B(?x_2)) = b(?x_2), B(?x_3) = B(?x_3), B(?x) = b(b(?x)), b(?x_3) = B(B(?x_3)), b(?x) = b(?x), b(b(?x_1)) = B(?x_1), B(b(?x)) = b(B(?x)), b(B(?x)) = B(b(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, WCR Knuth & Bendix Direct Methods: CR Try A Minimal Decomposition {2,5,3,6}{8,7,1,4}{0} {2,5,3,6} (cm)Rewrite Rules: [ b(b(?x)) -> B(?x), b(B(?x)) -> ?x, B(B(?x)) -> b(?x), B(b(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ b(?x_1) = B(B(?x_1)), b(b(?x_2)) = B(?x_2), b(?x_3) = b(?x_3), B(?x_3) = b(b(?x_3)), B(B(?x)) = b(?x), B(?x_1) = B(?x_1), b(B(?x)) = B(b(?x)), B(b(?x)) = b(B(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, WCR Knuth & Bendix Direct Methods: CR {8,7,1,4} (cm)Rewrite Rules: [ C(c(?x)) -> ?x, c(C(?x)) -> ?x, c(c(?x)) -> ?x, c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))) ] Apply Direct Methods... Inner CPs: [ C(?x_1) = C(?x_1), C(?x_2) = c(?x_2), C(B(c(b(c(B(c(b(?x_3)))))))) = B(c(b(c(?x_3)))), c(?x) = c(?x), c(?x_1) = C(?x_1), c(B(c(b(c(B(c(b(?x_3)))))))) = B(c(b(c(?x_3)))), c(B(c(b(?x_1)))) = B(c(b(c(B(c(b(C(?x_1)))))))), c(B(c(b(?x_2)))) = B(c(b(c(B(c(b(c(?x_2)))))))), c(?x) = c(?x), c(B(c(b(B(c(b(c(B(c(b(?x))))))))))) = B(c(b(c(B(c(b(B(c(b(c(?x))))))))))) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {0} (cm)Rewrite Rules: [ C(?x) -> c(?x) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR Try A Minimal Decomposition {0,8,7,1,4}{2,5,3,6} {0,8,7,1,4} (cm)Rewrite Rules: [ C(?x) -> c(?x), C(c(?x)) -> ?x, c(C(?x)) -> ?x, c(c(?x)) -> ?x, c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))) ] Apply Direct Methods... Inner CPs: [ C(?x_2) = C(?x_2), C(?x_3) = c(?x_3), C(B(c(b(c(B(c(b(?x_4)))))))) = B(c(b(c(?x_4)))), c(c(?x)) = ?x, c(?x_1) = c(?x_1), c(?x_2) = C(?x_2), c(B(c(b(c(B(c(b(?x_4)))))))) = B(c(b(c(?x_4)))), c(B(c(b(?x_2)))) = B(c(b(c(B(c(b(C(?x_2)))))))), c(B(c(b(?x_3)))) = B(c(b(c(B(c(b(c(?x_3)))))))), c(?x) = c(?x), c(B(c(b(B(c(b(c(B(c(b(?x))))))))))) = B(c(b(c(B(c(b(B(c(b(c(?x))))))))))) ] Outer CPs: [ c(c(?x_1)) = ?x_1 ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {2,5,3,6} (cm)Rewrite Rules: [ b(b(?x)) -> B(?x), b(B(?x)) -> ?x, B(B(?x)) -> b(?x), B(b(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ b(?x_1) = B(B(?x_1)), b(b(?x_2)) = B(?x_2), b(?x_3) = b(?x_3), B(?x_3) = b(b(?x_3)), B(B(?x)) = b(?x), B(?x_1) = B(?x_1), b(B(?x)) = B(b(?x)), B(b(?x)) = b(B(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, WCR Knuth & Bendix Direct Methods: CR Try A Minimal Decomposition {2,5,3,6}{8,7,1,4}{0} {2,5,3,6} (cm)Rewrite Rules: [ b(b(?x)) -> B(?x), b(B(?x)) -> ?x, B(B(?x)) -> b(?x), B(b(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ b(?x_1) = B(B(?x_1)), b(b(?x_2)) = B(?x_2), b(?x_3) = b(?x_3), B(?x_3) = b(b(?x_3)), B(B(?x)) = b(?x), B(?x_1) = B(?x_1), b(B(?x)) = B(b(?x)), B(b(?x)) = b(B(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, WCR Knuth & Bendix Direct Methods: CR {8,7,1,4} (cm)Rewrite Rules: [ C(c(?x)) -> ?x, c(C(?x)) -> ?x, c(c(?x)) -> ?x, c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))) ] Apply Direct Methods... Inner CPs: [ C(?x_1) = C(?x_1), C(?x_2) = c(?x_2), C(B(c(b(c(B(c(b(?x_3)))))))) = B(c(b(c(?x_3)))), c(?x) = c(?x), c(?x_1) = C(?x_1), c(B(c(b(c(B(c(b(?x_3)))))))) = B(c(b(c(?x_3)))), c(B(c(b(?x_1)))) = B(c(b(c(B(c(b(C(?x_1)))))))), c(B(c(b(?x_2)))) = B(c(b(c(B(c(b(c(?x_2)))))))), c(?x) = c(?x), c(B(c(b(B(c(b(c(B(c(b(?x))))))))))) = B(c(b(c(B(c(b(B(c(b(c(?x))))))))))) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {0} (cm)Rewrite Rules: [ C(?x) -> c(?x) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR Try A Minimal Decomposition {2,5,3,6}{0,8,7,1,4} {2,5,3,6} (cm)Rewrite Rules: [ b(b(?x)) -> B(?x), b(B(?x)) -> ?x, B(B(?x)) -> b(?x), B(b(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ b(?x_1) = B(B(?x_1)), b(b(?x_2)) = B(?x_2), b(?x_3) = b(?x_3), B(?x_3) = b(b(?x_3)), B(B(?x)) = b(?x), B(?x_1) = B(?x_1), b(B(?x)) = B(b(?x)), B(b(?x)) = b(B(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, WCR Knuth & Bendix Direct Methods: CR {0,8,7,1,4} (cm)Rewrite Rules: [ C(?x) -> c(?x), C(c(?x)) -> ?x, c(C(?x)) -> ?x, c(c(?x)) -> ?x, c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))) ] Apply Direct Methods... Inner CPs: [ C(?x_2) = C(?x_2), C(?x_3) = c(?x_3), C(B(c(b(c(B(c(b(?x_4)))))))) = B(c(b(c(?x_4)))), c(c(?x)) = ?x, c(?x_1) = c(?x_1), c(?x_2) = C(?x_2), c(B(c(b(c(B(c(b(?x_4)))))))) = B(c(b(c(?x_4)))), c(B(c(b(?x_2)))) = B(c(b(c(B(c(b(C(?x_2)))))))), c(B(c(b(?x_3)))) = B(c(b(c(B(c(b(c(?x_3)))))))), c(?x) = c(?x), c(B(c(b(B(c(b(c(B(c(b(?x))))))))))) = B(c(b(c(B(c(b(B(c(b(c(?x))))))))))) ] Outer CPs: [ c(c(?x_1)) = ?x_1 ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR Try A Minimal Decomposition {2,5}{3,6}{8,0,4,1,7} {2,5} (cm)Rewrite Rules: [ b(b(?x)) -> B(?x), b(B(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ b(?x_1) = B(B(?x_1)), b(B(?x)) = B(b(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {3,6} (cm)Rewrite Rules: [ B(B(?x)) -> b(?x), B(b(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ B(?x_1) = b(b(?x_1)), B(b(?x)) = b(B(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {8,0,4,1,7} (cm)Rewrite Rules: [ C(c(?x)) -> ?x, C(?x) -> c(?x), c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))), c(c(?x)) -> ?x, c(C(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ C(B(c(b(c(B(c(b(?x_2)))))))) = B(c(b(c(?x_2)))), C(?x_3) = c(?x_3), C(?x_4) = C(?x_4), c(B(c(b(?x_3)))) = B(c(b(c(B(c(b(c(?x_3)))))))), c(B(c(b(?x_4)))) = B(c(b(c(B(c(b(C(?x_4)))))))), c(B(c(b(c(B(c(b(?x_2)))))))) = B(c(b(c(?x_2)))), c(?x_4) = C(?x_4), c(?x) = c(?x), c(c(?x_1)) = ?x_1, c(B(c(b(B(c(b(c(B(c(b(?x))))))))))) = B(c(b(c(B(c(b(B(c(b(c(?x))))))))))), c(?x) = c(?x) ] Outer CPs: [ ?x = c(c(?x)) ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR Try A Minimal Decomposition {0,8,4,1,7}{2,5}{3,6} {0,8,4,1,7} (cm)Rewrite Rules: [ C(?x) -> c(?x), C(c(?x)) -> ?x, c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))), c(c(?x)) -> ?x, c(C(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ C(B(c(b(c(B(c(b(?x_2)))))))) = B(c(b(c(?x_2)))), C(?x_3) = c(?x_3), C(?x_4) = C(?x_4), c(B(c(b(?x_3)))) = B(c(b(c(B(c(b(c(?x_3)))))))), c(B(c(b(?x_4)))) = B(c(b(c(B(c(b(C(?x_4)))))))), c(B(c(b(c(B(c(b(?x_2)))))))) = B(c(b(c(?x_2)))), c(?x_4) = C(?x_4), c(c(?x)) = ?x, c(?x_1) = c(?x_1), c(B(c(b(B(c(b(c(B(c(b(?x))))))))))) = B(c(b(c(B(c(b(B(c(b(c(?x))))))))))), c(?x) = c(?x) ] Outer CPs: [ c(c(?x_1)) = ?x_1 ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {2,5} (cm)Rewrite Rules: [ b(b(?x)) -> B(?x), b(B(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ b(?x_1) = B(B(?x_1)), b(B(?x)) = B(b(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {3,6} (cm)Rewrite Rules: [ B(B(?x)) -> b(?x), B(b(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ B(?x_1) = b(b(?x_1)), B(b(?x)) = b(B(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR Try A Minimal Decomposition {6,3,5}{8,0,4,1,7}{2} {6,3,5} (cm)Rewrite Rules: [ B(b(?x)) -> ?x, B(B(?x)) -> b(?x), b(B(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ B(?x_2) = B(?x_2), B(?x) = b(b(?x)), b(?x) = b(?x), b(b(?x_1)) = B(?x_1), B(b(?x)) = b(B(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {8,0,4,1,7} (cm)Rewrite Rules: [ C(c(?x)) -> ?x, C(?x) -> c(?x), c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))), c(c(?x)) -> ?x, c(C(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ C(B(c(b(c(B(c(b(?x_2)))))))) = B(c(b(c(?x_2)))), C(?x_3) = c(?x_3), C(?x_4) = C(?x_4), c(B(c(b(?x_3)))) = B(c(b(c(B(c(b(c(?x_3)))))))), c(B(c(b(?x_4)))) = B(c(b(c(B(c(b(C(?x_4)))))))), c(B(c(b(c(B(c(b(?x_2)))))))) = B(c(b(c(?x_2)))), c(?x_4) = C(?x_4), c(?x) = c(?x), c(c(?x_1)) = ?x_1, c(B(c(b(B(c(b(c(B(c(b(?x))))))))))) = B(c(b(c(B(c(b(B(c(b(c(?x))))))))))), c(?x) = c(?x) ] Outer CPs: [ ?x = c(c(?x)) ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {2} (cm)Rewrite Rules: [ b(b(?x)) -> B(?x) ] Apply Direct Methods... Inner CPs: [ b(B(?x)) = B(b(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR Try A Minimal Decomposition {0,8,4,1,7}{6,3,5}{2} {0,8,4,1,7} (cm)Rewrite Rules: [ C(?x) -> c(?x), C(c(?x)) -> ?x, c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))), c(c(?x)) -> ?x, c(C(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ C(B(c(b(c(B(c(b(?x_2)))))))) = B(c(b(c(?x_2)))), C(?x_3) = c(?x_3), C(?x_4) = C(?x_4), c(B(c(b(?x_3)))) = B(c(b(c(B(c(b(c(?x_3)))))))), c(B(c(b(?x_4)))) = B(c(b(c(B(c(b(C(?x_4)))))))), c(B(c(b(c(B(c(b(?x_2)))))))) = B(c(b(c(?x_2)))), c(?x_4) = C(?x_4), c(c(?x)) = ?x, c(?x_1) = c(?x_1), c(B(c(b(B(c(b(c(B(c(b(?x))))))))))) = B(c(b(c(B(c(b(B(c(b(c(?x))))))))))), c(?x) = c(?x) ] Outer CPs: [ c(c(?x_1)) = ?x_1 ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {6,3,5} (cm)Rewrite Rules: [ B(b(?x)) -> ?x, B(B(?x)) -> b(?x), b(B(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ B(?x_2) = B(?x_2), B(?x) = b(b(?x)), b(?x) = b(?x), b(b(?x_1)) = B(?x_1), B(b(?x)) = b(B(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {2} (cm)Rewrite Rules: [ b(b(?x)) -> B(?x) ] Apply Direct Methods... Inner CPs: [ b(B(?x)) = B(b(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR Try A Minimal Decomposition {6,2,5}{8,0,4,1,7}{3} {6,2,5} (cm)Rewrite Rules: [ B(b(?x)) -> ?x, b(b(?x)) -> B(?x), b(B(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ B(B(?x_1)) = b(?x_1), B(?x_2) = B(?x_2), b(?x_2) = B(B(?x_2)), b(?x) = b(?x), b(B(?x)) = B(b(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {8,0,4,1,7} (cm)Rewrite Rules: [ C(c(?x)) -> ?x, C(?x) -> c(?x), c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))), c(c(?x)) -> ?x, c(C(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ C(B(c(b(c(B(c(b(?x_2)))))))) = B(c(b(c(?x_2)))), C(?x_3) = c(?x_3), C(?x_4) = C(?x_4), c(B(c(b(?x_3)))) = B(c(b(c(B(c(b(c(?x_3)))))))), c(B(c(b(?x_4)))) = B(c(b(c(B(c(b(C(?x_4)))))))), c(B(c(b(c(B(c(b(?x_2)))))))) = B(c(b(c(?x_2)))), c(?x_4) = C(?x_4), c(?x) = c(?x), c(c(?x_1)) = ?x_1, c(B(c(b(B(c(b(c(B(c(b(?x))))))))))) = B(c(b(c(B(c(b(B(c(b(c(?x))))))))))), c(?x) = c(?x) ] Outer CPs: [ ?x = c(c(?x)) ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {3} (cm)Rewrite Rules: [ B(B(?x)) -> b(?x) ] Apply Direct Methods... Inner CPs: [ B(b(?x)) = b(B(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR Try A Minimal Decomposition {0,8,4,1,7}{6,2,5}{3} {0,8,4,1,7} (cm)Rewrite Rules: [ C(?x) -> c(?x), C(c(?x)) -> ?x, c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))), c(c(?x)) -> ?x, c(C(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ C(B(c(b(c(B(c(b(?x_2)))))))) = B(c(b(c(?x_2)))), C(?x_3) = c(?x_3), C(?x_4) = C(?x_4), c(B(c(b(?x_3)))) = B(c(b(c(B(c(b(c(?x_3)))))))), c(B(c(b(?x_4)))) = B(c(b(c(B(c(b(C(?x_4)))))))), c(B(c(b(c(B(c(b(?x_2)))))))) = B(c(b(c(?x_2)))), c(?x_4) = C(?x_4), c(c(?x)) = ?x, c(?x_1) = c(?x_1), c(B(c(b(B(c(b(c(B(c(b(?x))))))))))) = B(c(b(c(B(c(b(B(c(b(c(?x))))))))))), c(?x) = c(?x) ] Outer CPs: [ c(c(?x_1)) = ?x_1 ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {6,2,5} (cm)Rewrite Rules: [ B(b(?x)) -> ?x, b(b(?x)) -> B(?x), b(B(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ B(B(?x_1)) = b(?x_1), B(?x_2) = B(?x_2), b(?x_2) = B(B(?x_2)), b(?x) = b(?x), b(B(?x)) = B(b(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {3} (cm)Rewrite Rules: [ B(B(?x)) -> b(?x) ] Apply Direct Methods... Inner CPs: [ B(b(?x)) = b(B(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR Try A Minimal Decomposition {2,5,3,6}{8,0,7,1,4} {2,5,3,6} (cm)Rewrite Rules: [ b(b(?x)) -> B(?x), b(B(?x)) -> ?x, B(B(?x)) -> b(?x), B(b(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ b(?x_1) = B(B(?x_1)), b(b(?x_2)) = B(?x_2), b(?x_3) = b(?x_3), B(?x_3) = b(b(?x_3)), B(B(?x)) = b(?x), B(?x_1) = B(?x_1), b(B(?x)) = B(b(?x)), B(b(?x)) = b(B(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, WCR Knuth & Bendix Direct Methods: CR {8,0,7,1,4} (cm)Rewrite Rules: [ C(c(?x)) -> ?x, C(?x) -> c(?x), c(C(?x)) -> ?x, c(c(?x)) -> ?x, c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))) ] Apply Direct Methods... Inner CPs: [ C(?x_2) = C(?x_2), C(?x_3) = c(?x_3), C(B(c(b(c(B(c(b(?x_4)))))))) = B(c(b(c(?x_4)))), c(?x) = c(?x), c(c(?x_1)) = ?x_1, c(?x_2) = C(?x_2), c(B(c(b(c(B(c(b(?x_4)))))))) = B(c(b(c(?x_4)))), c(B(c(b(?x_2)))) = B(c(b(c(B(c(b(C(?x_2)))))))), c(B(c(b(?x_3)))) = B(c(b(c(B(c(b(c(?x_3)))))))), c(?x) = c(?x), c(B(c(b(B(c(b(c(B(c(b(?x))))))))))) = B(c(b(c(B(c(b(B(c(b(c(?x))))))))))) ] Outer CPs: [ ?x = c(c(?x)) ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR Try A Minimal Decomposition {2,5,3,6}{0,8,7,1,4} {2,5,3,6} (cm)Rewrite Rules: [ b(b(?x)) -> B(?x), b(B(?x)) -> ?x, B(B(?x)) -> b(?x), B(b(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ b(?x_1) = B(B(?x_1)), b(b(?x_2)) = B(?x_2), b(?x_3) = b(?x_3), B(?x_3) = b(b(?x_3)), B(B(?x)) = b(?x), B(?x_1) = B(?x_1), b(B(?x)) = B(b(?x)), B(b(?x)) = b(B(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, WCR Knuth & Bendix Direct Methods: CR {0,8,7,1,4} (cm)Rewrite Rules: [ C(?x) -> c(?x), C(c(?x)) -> ?x, c(C(?x)) -> ?x, c(c(?x)) -> ?x, c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))) ] Apply Direct Methods... Inner CPs: [ C(?x_2) = C(?x_2), C(?x_3) = c(?x_3), C(B(c(b(c(B(c(b(?x_4)))))))) = B(c(b(c(?x_4)))), c(c(?x)) = ?x, c(?x_1) = c(?x_1), c(?x_2) = C(?x_2), c(B(c(b(c(B(c(b(?x_4)))))))) = B(c(b(c(?x_4)))), c(B(c(b(?x_2)))) = B(c(b(c(B(c(b(C(?x_2)))))))), c(B(c(b(?x_3)))) = B(c(b(c(B(c(b(c(?x_3)))))))), c(?x) = c(?x), c(B(c(b(B(c(b(c(B(c(b(?x))))))))))) = B(c(b(c(B(c(b(B(c(b(c(?x))))))))))) ] Outer CPs: [ c(c(?x_1)) = ?x_1 ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR Try A Minimal Decomposition {2,5,3,6}{8,0,4,1,7} {2,5,3,6} (cm)Rewrite Rules: [ b(b(?x)) -> B(?x), b(B(?x)) -> ?x, B(B(?x)) -> b(?x), B(b(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ b(?x_1) = B(B(?x_1)), b(b(?x_2)) = B(?x_2), b(?x_3) = b(?x_3), B(?x_3) = b(b(?x_3)), B(B(?x)) = b(?x), B(?x_1) = B(?x_1), b(B(?x)) = B(b(?x)), B(b(?x)) = b(B(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, WCR Knuth & Bendix Direct Methods: CR {8,0,4,1,7} (cm)Rewrite Rules: [ C(c(?x)) -> ?x, C(?x) -> c(?x), c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))), c(c(?x)) -> ?x, c(C(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ C(B(c(b(c(B(c(b(?x_2)))))))) = B(c(b(c(?x_2)))), C(?x_3) = c(?x_3), C(?x_4) = C(?x_4), c(B(c(b(?x_3)))) = B(c(b(c(B(c(b(c(?x_3)))))))), c(B(c(b(?x_4)))) = B(c(b(c(B(c(b(C(?x_4)))))))), c(B(c(b(c(B(c(b(?x_2)))))))) = B(c(b(c(?x_2)))), c(?x_4) = C(?x_4), c(?x) = c(?x), c(c(?x_1)) = ?x_1, c(B(c(b(B(c(b(c(B(c(b(?x))))))))))) = B(c(b(c(B(c(b(B(c(b(c(?x))))))))))), c(?x) = c(?x) ] Outer CPs: [ ?x = c(c(?x)) ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR Try A Minimal Decomposition {2,5,3,6}{0,8,4,1,7} {2,5,3,6} (cm)Rewrite Rules: [ b(b(?x)) -> B(?x), b(B(?x)) -> ?x, B(B(?x)) -> b(?x), B(b(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ b(?x_1) = B(B(?x_1)), b(b(?x_2)) = B(?x_2), b(?x_3) = b(?x_3), B(?x_3) = b(b(?x_3)), B(B(?x)) = b(?x), B(?x_1) = B(?x_1), b(B(?x)) = B(b(?x)), B(b(?x)) = b(B(?x)) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, WCR Knuth & Bendix Direct Methods: CR {0,8,4,1,7} (cm)Rewrite Rules: [ C(?x) -> c(?x), C(c(?x)) -> ?x, c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))), c(c(?x)) -> ?x, c(C(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ C(B(c(b(c(B(c(b(?x_2)))))))) = B(c(b(c(?x_2)))), C(?x_3) = c(?x_3), C(?x_4) = C(?x_4), c(B(c(b(?x_3)))) = B(c(b(c(B(c(b(c(?x_3)))))))), c(B(c(b(?x_4)))) = B(c(b(c(B(c(b(C(?x_4)))))))), c(B(c(b(c(B(c(b(?x_2)))))))) = B(c(b(c(?x_2)))), c(?x_4) = C(?x_4), c(c(?x)) = ?x, c(?x_1) = c(?x_1), c(B(c(b(B(c(b(c(B(c(b(?x))))))))))) = B(c(b(c(B(c(b(B(c(b(c(?x))))))))))), c(?x) = c(?x) ] Outer CPs: [ c(c(?x_1)) = ?x_1 ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR Commutative Decomposition failed: Can't judge No further decomposition possible Combined result: Can't judge 944.trs: Failure(unknown CR) MAYBE (13261 msec.)