(ignored inputs)COMMENT Example 3 of \cite{GL06} Rewrite Rules: [ b -> a, b -> c, c -> h(b), c -> d, a -> h(a), d -> h(d) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ a = c, h(b) = d ] Overlay, check Innermost Termination... unknown Innermost Terminating unknown Knuth&Bendix Linear unknown Development Closed unknown Strongly Closed unknown Upside-Parallel-Closed/Outside-Closed (inner) Parallel CPs: (not computed) unknown Toyama (Parallel CPs) Simultaneous CPs: [ h(b) = d, d = h(b), a = c, c = a ] unknown Okui (Simultaneous CPs) unknown Strongly Depth-Preserving & Non-E-Overlapping check Locally Decreasing Diagrams by Rule Labelling... Critical Pair by Rules <1, 0> preceded by [] joinable by a reduction of rules <[([],2),([(h,1)],0)], [([],4)]> Critical Pair by Rules <3, 2> preceded by [] joinable by a reduction of rules <[([],5)], [([(h,1)],1),([(h,1)],3)]> unknown Diagram Decreasing check by Reduction-Preserving Completion... failure(empty P) unknown Reduction-Preserving Completion check Non-Confluence...Unknown Direct Methods: Can't judge Try Persistent Decomposition for... [ b -> a, b -> c, c -> h(b), c -> d, a -> h(a), d -> h(d) ] Sort Assignment: a : =>7 b : =>7 c : =>7 d : =>7 h : 7=>7 maximal types: {7} Persistent Decomposition failed: Can't judge Try Layer Preserving Decomposition for... [ b -> a, b -> c, c -> h(b), c -> d, a -> h(a), d -> h(d) ] Layer Preserving Decomposition failed: Can't judge Try Commutative Decomposition for... [ b -> a, b -> c, c -> h(b), c -> d, a -> h(a), d -> h(d) ] Outside Critical Pair: by Rules <1, 0> develop reducts from lhs term... <{3}, d> <{2}, h(b)> <{}, c> develop reducts from rhs term... <{4}, h(a)> <{}, a> Outside Critical Pair: by Rules <3, 2> develop reducts from lhs term... <{5}, h(d)> <{}, d> develop reducts from rhs term... <{1}, h(c)> <{0}, h(a)> <{}, h(b)> Try A Minimal Decomposition {0,1}{2,3}{4}{5} {0,1} (cm)Rewrite Rules: [ b -> a, b -> c ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ a = c ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), not WCR Knuth&Bendix Direct Methods: not CR {2,3} (cm)Rewrite Rules: [ c -> h(b), c -> d ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ h(b) = d ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), not WCR Knuth&Bendix Direct Methods: not CR {4} (cm)Rewrite Rules: [ a -> h(a) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... unknown Innermost Terminating unknown Knuth&Bendix Linear Development Closed Direct Methods: CR {5} (cm)Rewrite Rules: [ d -> h(d) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... unknown Innermost Terminating unknown Knuth&Bendix Linear Development Closed Direct Methods: CR Try to add other components to {0,1} Add {2,3} {0,1,2,3} (cm)Rewrite Rules: [ b -> a, b -> c, c -> h(b), c -> d ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ a = c, h(b) = d ] Overlay, check Innermost Termination... unknown Innermost Terminating unknown Knuth&Bendix Linear unknown Development Closed unknown Strongly Closed unknown Upside-Parallel-Closed/Outside-Closed (inner) Parallel CPs: (not computed) unknown Toyama (Parallel CPs) Simultaneous CPs: [ h(b) = d, d = h(b), a = c, c = a ] unknown Okui (Simultaneous CPs) unknown Strongly Depth-Preserving & Non-E-Overlapping check Locally Decreasing Diagrams by Rule Labelling... Critical Pair by Rules <1, 0> preceded by [] unknown Diagram Decreasing check by Reduction-Preserving Completion... failure(empty P) unknown Reduction-Preserving Completion check Non-Confluence...Find Non-Joinable CP reducts: from c Not Confluent Direct Methods: not CR Add {2,3}{4} {0,1,2,3,4} (cm)Rewrite Rules: [ b -> a, b -> c, c -> h(b), c -> d, a -> h(a) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ a = c, h(b) = d ] Overlay, check Innermost Termination... unknown Innermost Terminating unknown Knuth&Bendix Linear unknown Development Closed unknown Strongly Closed unknown Upside-Parallel-Closed/Outside-Closed (inner) Parallel CPs: (not computed) unknown Toyama (Parallel CPs) Simultaneous CPs: [ h(b) = d, d = h(b), a = c, c = a ] unknown Okui (Simultaneous CPs) unknown Strongly Depth-Preserving & Non-E-Overlapping check Locally Decreasing Diagrams by Rule Labelling... Critical Pair by Rules <1, 0> preceded by [] joinable by a reduction of rules <[([],2),([(h,1)],0)], [([],4)]> Critical Pair by Rules <3, 2> preceded by [] unknown Diagram Decreasing check by Reduction-Preserving Completion... failure(empty P) unknown Reduction-Preserving Completion check Non-Confluence...Find Non-Joinable CP reducts: from c Not Confluent Direct Methods: not CR Add {2,3}{5} {0,1,2,3,5} (cm)Rewrite Rules: [ b -> a, b -> c, c -> h(b), c -> d, d -> h(d) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ a = c, h(b) = d ] Overlay, check Innermost Termination... unknown Innermost Terminating unknown Knuth&Bendix Linear unknown Development Closed unknown Strongly Closed unknown Upside-Parallel-Closed/Outside-Closed (inner) Parallel CPs: (not computed) unknown Toyama (Parallel CPs) Simultaneous CPs: [ h(b) = d, d = h(b), a = c, c = a ] unknown Okui (Simultaneous CPs) unknown Strongly Depth-Preserving & Non-E-Overlapping check Locally Decreasing Diagrams by Rule Labelling... Critical Pair by Rules <1, 0> preceded by [] unknown Diagram Decreasing check by Reduction-Preserving Completion... failure(empty P) unknown Reduction-Preserving Completion check Non-Confluence...Find Non-Joinable CP reducts: from c Not Confluent Direct Methods: not CR Add {4} {0,1,4} (cm)Rewrite Rules: [ b -> a, b -> c, a -> h(a) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ a = c ] Overlay, check Innermost Termination... unknown Innermost Terminating unknown Knuth&Bendix Linear unknown Development Closed unknown Strongly Closed unknown Upside-Parallel-Closed/Outside-Closed (inner) Parallel CPs: (not computed) unknown Toyama (Parallel CPs) Simultaneous CPs: [ a = c, c = a ] unknown Okui (Simultaneous CPs) unknown Strongly Depth-Preserving & Non-E-Overlapping check Locally Decreasing Diagrams by Rule Labelling... Critical Pair by Rules <1, 0> preceded by [] unknown Diagram Decreasing check by Reduction-Preserving Completion... failure(empty P) unknown Reduction-Preserving Completion check Non-Confluence...Find Non-Joinable CP reducts: from b Not Confluent Direct Methods: not CR Add {5} {0,1,5} (cm)Rewrite Rules: [ b -> a, b -> c, d -> h(d) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ a = c ] Overlay, check Innermost Termination... unknown Innermost Terminating unknown Knuth&Bendix Linear unknown Development Closed unknown Strongly Closed unknown Upside-Parallel-Closed/Outside-Closed (inner) Parallel CPs: (not computed) unknown Toyama (Parallel CPs) Simultaneous CPs: [ a = c, c = a ] unknown Okui (Simultaneous CPs) unknown Strongly Depth-Preserving & Non-E-Overlapping check Locally Decreasing Diagrams by Rule Labelling... Critical Pair by Rules <1, 0> preceded by [] unknown Diagram Decreasing check by Reduction-Preserving Completion... failure(empty P) unknown Reduction-Preserving Completion check Non-Confluence...Find Non-Joinable CP reducts: from b Not Confluent Direct Methods: not CR Add {4}{5} {0,1,4,5} (cm)Rewrite Rules: [ b -> a, b -> c, a -> h(a), d -> h(d) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ a = c ] Overlay, check Innermost Termination... unknown Innermost Terminating unknown Knuth&Bendix Linear unknown Development Closed unknown Strongly Closed unknown Upside-Parallel-Closed/Outside-Closed (inner) Parallel CPs: (not computed) unknown Toyama (Parallel CPs) Simultaneous CPs: [ a = c, c = a ] unknown Okui (Simultaneous CPs) unknown Strongly Depth-Preserving & Non-E-Overlapping check Locally Decreasing Diagrams by Rule Labelling... Critical Pair by Rules <1, 0> preceded by [] unknown Diagram Decreasing check by Reduction-Preserving Completion... failure(empty P) unknown Reduction-Preserving Completion check Non-Confluence...Find Non-Joinable CP reducts: from b Not Confluent Direct Methods: not CR Commutative Decomposition failed: Can't judge No further decomposition possible Final result: Can't judge /local-scratch/hzankl/2012/cops2012/21.trs: Failure(unknown) (24 msec.)