(ignored inputs)COMMENT doi:10.1007/s10817-011-9238-x [33] p. 499 with small correction: b1/c1 instead of b0/c0 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 31 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... [ 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 Combined result: Can't judge 116.trs: Failure(unknown CR) MAYBE (2275 msec.)