MAYBE (ignored inputs)COMMENT Example from [HM11] , p. 499 {with small correction: b1/c1 instead of b0/c0}: doi: http://dx.doi.org/10.1007/s10817-011-9238-x Rewrite Rules: [ a1 -> b1, a1 -> c1, b1 -> b2, c1 -> c2, a2 -> b2, a2 -> c2, b2 -> b3, c2 -> c3, a3 -> b3, a3 -> c3, b3 -> b4, c3 -> c4, a4 -> b4, a4 -> c4, b4 -> b5, c4 -> c5, a5 -> b5, a5 -> c5, b5 -> b6, c5 -> c6, a6 -> b6, a6 -> c6, b6 -> b7, c6 -> b7, b7 -> b1, b7 -> c1 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ b1 = c1, b2 = c2, b3 = c3, b4 = c4, b5 = c5, b6 = c6, b1 = c1 ] Overlay, check Innermost Termination... unknown Innermost 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: [ c1 = b1, b1 = c1, c2 = b2, b2 = c2, c3 = b3, b3 = c3, c4 = b4, b4 = c4, c5 = b5, b5 = c5, c6 = b6, b6 = c6 ] 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 <1, 0> preceded by [] unknown Diagram Decreasing check Non-Confluence... obtain 36 rules by 3 steps unfolding strenghten b1 and b2 strenghten b1 and c1 strenghten b1 and c2 strenghten b2 and b3 strenghten b2 and c1 strenghten b2 and c2 strenghten b2 and c3 strenghten b3 and b4 strenghten b3 and c2 strenghten b3 and c3 strenghten b4 and c4 strenghten b5 and c5 strenghten b6 and c6 strenghten c1 and b1 strenghten c1 and b2 strenghten c1 and c2 strenghten c2 and b2 strenghten c2 and b3 strenghten c2 and c3 strenghten c3 and b3 strenghten c3 and b4 obtain 100 candidates for checking non-joinability check by TCAP-Approximation (failure) check by Root-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... [ a1 -> b1, a1 -> c1, b1 -> b2, c1 -> c2, a2 -> b2, a2 -> c2, b2 -> b3, c2 -> c3, a3 -> b3, a3 -> c3, b3 -> b4, c3 -> c4, a4 -> b4, a4 -> c4, b4 -> b5, c4 -> c5, a5 -> b5, a5 -> c5, b5 -> b6, c5 -> c6, a6 -> b6, a6 -> c6, b6 -> b7, c6 -> b7, b7 -> b1, b7 -> c1 ] Sort Assignment: a1 : =>20 a2 : =>20 a3 : =>20 a4 : =>20 a5 : =>20 a6 : =>20 b1 : =>20 b2 : =>20 b3 : =>20 b4 : =>20 b5 : =>20 b6 : =>20 b7 : =>20 c1 : =>20 c2 : =>20 c3 : =>20 c4 : =>20 c5 : =>20 c6 : =>20 maximal types: {20} Persistent Decomposition failed: Can't judge Try Layer Preserving Decomposition for... [ a1 -> b1, a1 -> c1, b1 -> b2, c1 -> c2, a2 -> b2, a2 -> c2, b2 -> b3, c2 -> c3, a3 -> b3, a3 -> c3, b3 -> b4, c3 -> c4, a4 -> b4, a4 -> c4, b4 -> b5, c4 -> c5, a5 -> b5, a5 -> c5, b5 -> b6, c5 -> c6, a6 -> b6, a6 -> c6, b6 -> b7, c6 -> b7, b7 -> b1, b7 -> c1 ] Layer Preserving Decomposition failed: Can't judge Try Commutative Decomposition for... [ a1 -> b1, a1 -> c1, b1 -> b2, c1 -> c2, a2 -> b2, a2 -> c2, b2 -> b3, c2 -> c3, a3 -> b3, a3 -> c3, b3 -> b4, c3 -> c4, a4 -> b4, a4 -> c4, b4 -> b5, c4 -> c5, a5 -> b5, a5 -> c5, b5 -> b6, c5 -> c6, a6 -> b6, a6 -> c6, b6 -> b7, c6 -> b7, b7 -> b1, b7 -> c1 ] Outside Critical Pair: by Rules <1, 0> develop reducts from lhs term... <{3}, c2> <{}, c1> develop reducts from rhs term... <{2}, b2> <{}, b1> Outside Critical Pair: by Rules <5, 4> develop reducts from lhs term... <{7}, c3> <{}, c2> develop reducts from rhs term... <{6}, b3> <{}, b2> Outside Critical Pair: by Rules <9, 8> develop reducts from lhs term... <{11}, c4> <{}, c3> develop reducts from rhs term... <{10}, b4> <{}, b3> Outside Critical Pair: by Rules <13, 12> develop reducts from lhs term... <{15}, c5> <{}, c4> develop reducts from rhs term... <{14}, b5> <{}, b4> Outside Critical Pair: by Rules <17, 16> develop reducts from lhs term... <{19}, c6> <{}, c5> develop reducts from rhs term... <{18}, b6> <{}, b5> Outside Critical Pair: by Rules <21, 20> develop reducts from lhs term... <{23}, b7> <{}, c6> develop reducts from rhs term... <{22}, b7> <{}, b6> Outside Critical Pair: by Rules <25, 24> develop reducts from lhs term... <{3}, c2> <{}, c1> develop reducts from rhs term... <{2}, b2> <{}, b1> Try A Minimal Decomposition {0,1}{4,5}{8,9}{12,13}{16,17}{21,22}{20,23}{24,25}{2}{3}{6}{7}{10}{11}{14}{15}{18}{19} {0,1} (cm)Rewrite Rules: [ a1 -> b1, a1 -> c1 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ b1 = c1 ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), not WCR Knuth & Bendix Direct Methods: not CR {4,5} (cm)Rewrite Rules: [ a2 -> b2, a2 -> c2 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ b2 = c2 ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), not WCR Knuth & Bendix Direct Methods: not CR {8,9} (cm)Rewrite Rules: [ a3 -> b3, a3 -> c3 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ b3 = c3 ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), not WCR Knuth & Bendix Direct Methods: not CR {12,13} (cm)Rewrite Rules: [ a4 -> b4, a4 -> c4 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ b4 = c4 ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), not WCR Knuth & Bendix Direct Methods: not CR {16,17} (cm)Rewrite Rules: [ a5 -> b5, a5 -> c5 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ b5 = c5 ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), not WCR Knuth & Bendix Direct Methods: not CR {21,22} (cm)Rewrite Rules: [ a6 -> c6, b6 -> b7 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {20,23} (cm)Rewrite Rules: [ a6 -> b6, c6 -> b7 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {24,25} (cm)Rewrite Rules: [ b7 -> b1, b7 -> c1 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ b1 = c1 ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), not WCR Knuth & Bendix Direct Methods: not CR {2} (cm)Rewrite Rules: [ b1 -> b2 ] 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: [ c1 -> c2 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {6} (cm)Rewrite Rules: [ b2 -> b3 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {7} (cm)Rewrite Rules: [ c2 -> c3 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {10} (cm)Rewrite Rules: [ b3 -> b4 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {11} (cm)Rewrite Rules: [ c3 -> c4 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {14} (cm)Rewrite Rules: [ b4 -> b5 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {15} (cm)Rewrite Rules: [ c4 -> c5 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {18} (cm)Rewrite Rules: [ b5 -> b6 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {19} (cm)Rewrite Rules: [ c5 -> c6 ] 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,1}{4,5}{8,9}{12,13}{16,17}{20,21}{24,25}{2}{3}{6}{7}{10}{11}{14}{15}{18}{19}{22}{23} {0,1} (cm)Rewrite Rules: [ a1 -> b1, a1 -> c1 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ b1 = c1 ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), not WCR Knuth & Bendix Direct Methods: not CR {4,5} (cm)Rewrite Rules: [ a2 -> b2, a2 -> c2 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ b2 = c2 ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), not WCR Knuth & Bendix Direct Methods: not CR {8,9} (cm)Rewrite Rules: [ a3 -> b3, a3 -> c3 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ b3 = c3 ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), not WCR Knuth & Bendix Direct Methods: not CR {12,13} (cm)Rewrite Rules: [ a4 -> b4, a4 -> c4 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ b4 = c4 ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), not WCR Knuth & Bendix Direct Methods: not CR {16,17} (cm)Rewrite Rules: [ a5 -> b5, a5 -> c5 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ b5 = c5 ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), not WCR Knuth & Bendix Direct Methods: not CR {20,21} (cm)Rewrite Rules: [ a6 -> b6, a6 -> c6 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ b6 = c6 ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), not WCR Knuth & Bendix Direct Methods: not CR {24,25} (cm)Rewrite Rules: [ b7 -> b1, b7 -> c1 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ b1 = c1 ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), not WCR Knuth & Bendix Direct Methods: not CR {2} (cm)Rewrite Rules: [ b1 -> b2 ] 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: [ c1 -> c2 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {6} (cm)Rewrite Rules: [ b2 -> b3 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {7} (cm)Rewrite Rules: [ c2 -> c3 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {10} (cm)Rewrite Rules: [ b3 -> b4 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {11} (cm)Rewrite Rules: [ c3 -> c4 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {14} (cm)Rewrite Rules: [ b4 -> b5 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {15} (cm)Rewrite Rules: [ c4 -> c5 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {18} (cm)Rewrite Rules: [ b5 -> b6 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {19} (cm)Rewrite Rules: [ c5 -> c6 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {22} (cm)Rewrite Rules: [ b6 -> b7 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {23} (cm)Rewrite Rules: [ c6 -> b7 ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR Commutative Decomposition failed: Can't judge No further decomposition possible Final result: Can't judge 116.trs: Failure(unknown) (2640 msec.)