MAYBE (ignored inputs)COMMENT the following rules are removed from the original TRS C ( x ) -> c ( x ) c ( C ( x ) ) -> x C ( c ( x ) ) -> x Rewrite Rules: [ 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 ] Apply Direct Methods... Inner CPs: [ c(B(c(b(c(B(c(b(?x_3)))))))) = B(c(b(c(?x_3)))), b(?x_4) = B(B(?x_4)), B(?x_5) = b(b(?x_5)), c(B(c(b(?x)))) = B(c(b(c(B(c(b(c(?x)))))))), b(b(?x_2)) = B(?x_2), b(?x_5) = b(?x_5), B(B(?x_1)) = b(?x_1), B(?x_4) = B(?x_4), 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: [ ] 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: [ c(?x_1) = c(?x_1), c(B(c(b(c(B(c(b(?x_4)))))))) = B(c(b(c(?x_4)))), ?x_1 = c(c(?x_1)), B(c(b(c(B(c(b(?x_4))))))) = c(B(c(b(c(?x_4))))), B(c(b(c(B(c(b(B(c(b(c(B(c(b(?x_4)))))))))))))) = c(B(c(b(B(c(b(c(?x_4)))))))), B(c(b(c(B(c(b(c(?x)))))))) = c(B(c(b(?x)))), b(B(?x_1)) = B(b(?x_1)), b(?x_5) = B(B(?x_5)), B(B(?x_1)) = b(B(b(?x_1))), B(?x_5) = b(B(B(?x_5))), B(?x_1) = B(B(b(?x_1))), ?x_5 = B(B(B(?x_5))), B(b(?x)) = b(B(?x)), 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))), 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_2)))) = B(c(b(c(B(c(b(c(?x_2)))))))), 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_2)))))))))) = c(B(c(b(B(c(b(c(B(c(b(c(?x_2)))))))))))), 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_2))) = c(B(c(b(c(B(c(b(c(?x_2))))))))), 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(b(?x_4)) = B(?x_4), b(?x_6) = b(?x_6), ?x_6 = B(b(?x_6)), B(B(?x)) = b(?x), B(?x) = B(?x), ?x_6 = b(B(?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 <3, 0> preceded by [(c,1)] joinable by a reduction of rules <[([],3),([(B,1),(c,1),(b,1),(c,1),(B,1),(c,1)],4),([(B,1),(c,1),(b,1),(c,1),(B,1)],0),([(B,1),(c,1),(b,1),(c,1)],5)], []> Critical Pair by Rules <4, 1> preceded by [(b,1)] joinable by a reduction of rules <[], [([],2)]> Critical Pair by Rules <5, 2> preceded by [(B,1)] joinable by a reduction of rules <[], [([],1)]> Critical Pair by Rules <0, 3> preceded by [(c,1),(B,1),(c,1),(b,1)] joinable by a reduction of rules <[], [([(B,1),(c,1),(b,1)],3),([(B,1),(c,1)],4),([(B,1)],0),([],5)]> Critical Pair by Rules <2, 4> preceded by [(b,1)] joinable by a reduction of rules <[([],1)], []> Critical Pair by Rules <5, 4> preceded by [(b,1)] joinable by a reduction of rules <[], []> Critical Pair by Rules <1, 5> preceded by [(B,1)] joinable by a reduction of rules <[([],2)], []> Critical Pair by Rules <4, 5> preceded by [(B,1)] joinable by a reduction of rules <[], []> Critical Pair by Rules <0, 0> preceded by [(c,1)] joinable by a reduction of rules <[], []> Critical Pair by Rules <1, 1> preceded by [(b,1)] joinable by a reduction of rules <[([],4)], [([],5)]> Critical Pair by Rules <2, 2> preceded by [(B,1)] joinable by a reduction of rules <[([],5)], [([],4)]> Critical Pair by Rules <3, 3> preceded by [(c,1),(B,1),(c,1),(b,1)] joinable by a reduction of rules <[([(c,1),(B,1),(c,1)],4),([(c,1),(B,1)],0),([(c,1)],5),([],0)], [([(B,1),(c,1),(b,1),(c,1),(B,1),(c,1)],4),([(B,1),(c,1),(b,1),(c,1),(B,1)],0),([(B,1),(c,1),(b,1),(c,1)],5),([(B,1),(c,1),(b,1)],0)]> unknown Diagram Decreasing check Non-Confluence... obtain 7 rules by 3 steps unfolding obtain 31 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 check by Ordered Rewriting... remove redundants rules and split R-part: [ 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 ] E-part: [ ] ...failed to find a suitable LPO. unknown Confluence by Ordered Rewriting Direct Methods: Can't judge Try Persistent Decomposition for... [ 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 ] Sort Assignment: B : 13=>13 b : 13=>13 c : 13=>13 maximal types: {13} Persistent Decomposition failed: Can't judge Try Layer Preserving Decomposition for... [ 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 ] Layer Preserving Decomposition failed: Can't judge Try Commutative Decomposition for... [ 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 ] Inside Critical Pair: by Rules <3, 0> develop reducts from lhs term... <{3}, B(c(b(c(B(c(b(B(c(b(?x_3))))))))))> <{}, c(B(c(b(c(B(c(b(?x_3))))))))> develop reducts from rhs term... <{}, B(c(b(c(?x_3))))> Inside Critical Pair: by Rules <4, 1> develop reducts from lhs term... <{}, b(?x_4)> develop reducts from rhs term... <{2}, b(?x_4)> <{}, B(B(?x_4))> Inside Critical Pair: by Rules <5, 2> develop reducts from lhs term... <{}, B(?x_5)> develop reducts from rhs term... <{1}, B(?x_5)> <{}, b(b(?x_5))> Inside Critical Pair: by Rules <0, 3> develop reducts from lhs term... <{}, c(B(c(b(?x))))> develop reducts from rhs term... <{3}, B(c(b(B(c(b(c(B(c(b(?x))))))))))> <{}, B(c(b(c(B(c(b(c(?x))))))))> Inside Critical Pair: by Rules <2, 4> develop reducts from lhs term... <{1}, B(?x_2)> <{}, b(b(?x_2))> develop reducts from rhs term... <{}, B(?x_2)> Inside Critical Pair: by Rules <5, 4> develop reducts from lhs term... <{}, b(?x_5)> develop reducts from rhs term... <{}, b(?x_5)> Inside Critical Pair: by Rules <1, 5> develop reducts from lhs term... <{2}, b(?x_1)> <{}, B(B(?x_1))> develop reducts from rhs term... <{}, b(?x_1)> Inside Critical Pair: by Rules <4, 5> develop reducts from lhs term... <{}, B(?x_4)> develop reducts from rhs term... <{}, B(?x_4)> Try A Minimal Decomposition {0,3}{1,4}{2,5} {0,3} (cm)Rewrite Rules: [ c(c(?x)) -> ?x, c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))) ] Apply Direct Methods... Inner CPs: [ c(B(c(b(c(B(c(b(?x_1)))))))) = B(c(b(c(?x_1)))), c(B(c(b(?x)))) = B(c(b(c(B(c(b(c(?x)))))))), 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 {1,4} (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 {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 Try A Minimal Decomposition {0,3}{5,2,4}{1} {0,3} (cm)Rewrite Rules: [ c(c(?x)) -> ?x, c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))) ] Apply Direct Methods... Inner CPs: [ c(B(c(b(c(B(c(b(?x_1)))))))) = B(c(b(c(?x_1)))), c(B(c(b(?x)))) = B(c(b(c(B(c(b(c(?x)))))))), 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 {5,2,4} (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 {1} (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,3}{5,2,1,4} {0,3} (cm)Rewrite Rules: [ c(c(?x)) -> ?x, c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))) ] Apply Direct Methods... Inner CPs: [ c(B(c(b(c(B(c(b(?x_1)))))))) = B(c(b(c(?x_1)))), c(B(c(b(?x)))) = B(c(b(c(B(c(b(c(?x)))))))), 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 {5,2,1,4} (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 {0,3}{5,1,4}{2} {0,3} (cm)Rewrite Rules: [ c(c(?x)) -> ?x, c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))) ] Apply Direct Methods... Inner CPs: [ c(B(c(b(c(B(c(b(?x_1)))))))) = B(c(b(c(?x_1)))), c(B(c(b(?x)))) = B(c(b(c(B(c(b(c(?x)))))))), 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 {5,1,4} (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 {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,3}{2,5,1,4} {0,3} (cm)Rewrite Rules: [ c(c(?x)) -> ?x, c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))) ] Apply Direct Methods... Inner CPs: [ c(B(c(b(c(B(c(b(?x_1)))))))) = B(c(b(c(?x_1)))), c(B(c(b(?x)))) = B(c(b(c(B(c(b(c(?x)))))))), 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 {2,5,1,4} (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 {0,3}{5,2,1,4} {0,3} (cm)Rewrite Rules: [ c(c(?x)) -> ?x, c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))) ] Apply Direct Methods... Inner CPs: [ c(B(c(b(c(B(c(b(?x_1)))))))) = B(c(b(c(?x_1)))), c(B(c(b(?x)))) = B(c(b(c(B(c(b(c(?x)))))))), 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 {5,2,1,4} (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 {1,4,2,5}{0,3} {1,4,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 {0,3} (cm)Rewrite Rules: [ c(c(?x)) -> ?x, c(B(c(b(c(?x))))) -> B(c(b(c(B(c(b(?x))))))) ] Apply Direct Methods... Inner CPs: [ c(B(c(b(c(B(c(b(?x_1)))))))) = B(c(b(c(?x_1)))), c(B(c(b(?x)))) = B(c(b(c(B(c(b(c(?x)))))))), 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 Commutative Decomposition failed: Can't judge No further decomposition possible Combined result: Can't judge /tmp/fileomQx8a.trs: Failure(unknown CR) (10018 msec.)