MAYBE (ignored inputs)COMMENT handcrafted "UNC & ~NFP" submitted by: Franziska Rapp Rewrite Rules: [ if(true,a,?x) -> a, if(true,b,?x) -> b, if(true,g(a),?x) -> g(a), if(true,g(b),?x) -> g(b), if(false,?x,a) -> a, if(false,?x,b) -> b, if(false,?x,g(a)) -> g(a), if(false,?x,g(b)) -> g(b), g(a) -> g(g(a)), g(b) -> a, f(a,b) -> b, f(g(g(a)),?x) -> b ] Apply Direct Methods... Inner CPs: [ if(true,g(g(a)),?x_2) = g(a), if(true,a,?x_3) = g(b), if(false,?x_6,g(g(a))) = g(a), if(false,?x_7,a) = g(b), f(g(g(g(a))),?x_8) = b ] 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: [ if(true,g(g(a)),?x) = g(a), if(true,a,?x) = g(b), if(false,?x,g(g(a))) = g(a), if(false,?x,a) = g(b), g(a) = if(true,g(g(a)),?x_2), g(a) = if(false,?x_6,g(g(a))), b = f(g(g(g(a))),?x_8), g(b) = if(true,a,?x_3), g(b) = if(false,?x_7,a), f(g(g(g(a))),?x) = b ] 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 <8, 2> preceded by [(if,2)] unknown Diagram Decreasing check Non-Confluence... obtain 15 rules by 3 steps unfolding obtain 43 candidates for checking non-joinability check by TCAP-Approximation (failure) check by Ordering(rpo), check by Tree-Automata Approximation (success) where F = {(a,0),(b,0),(f,2),(g,1),(if,3),(c_1,0),(true,0),(false,0)} Q = {q_0,q_1,q_{c_1},q_{g(g(a))},q_{a},q_{g(a)},q_{g(g(g(a)))}} Qf = {q_0,q_1} Delta = [ a -> q_{a}, b -> q_1, f(q_{g(g(g(a)))},q_{c_1}) -> q_0, g(q_{g(g(a))}) -> q_{g(g(g(a)))}, g(q_{a}) -> q_{g(a)}, g(q_{g(a)}) -> q_{g(g(a))}, g(q_{g(a)}) -> q_{g(a)}, c_1 -> q_{c_1} ] (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... STEP: 1 (parallel) S: [ if(true,a,?x) -> a, if(true,b,?x) -> b, if(true,g(a),?x) -> g(a), if(true,g(b),?x) -> g(b), if(false,?x,a) -> a, if(false,?x,b) -> b, if(false,?x,g(a)) -> g(a), if(false,?x,g(b)) -> g(b), g(b) -> a, f(a,b) -> b, f(g(g(a)),?x) -> b ] P: [ g(a) -> g(g(a)) ] P: not reversible failure(Step 1) STEP: 2 (linear) S: [ if(true,a,?x) -> a, if(true,b,?x) -> b, if(true,g(a),?x) -> g(a), if(true,g(b),?x) -> g(b), if(false,?x,a) -> a, if(false,?x,b) -> b, if(false,?x,g(a)) -> g(a), if(false,?x,g(b)) -> g(b), g(b) -> a, f(a,b) -> b, f(g(g(a)),?x) -> b ] P: [ g(a) -> g(g(a)) ] P: not reversible failure(Step 2) STEP: 3 (relative) S: [ if(true,a,?x) -> a, if(true,b,?x) -> b, if(true,g(a),?x) -> g(a), if(true,g(b),?x) -> g(b), if(false,?x,a) -> a, if(false,?x,b) -> b, if(false,?x,g(a)) -> g(a), if(false,?x,g(b)) -> g(b), g(b) -> a, f(a,b) -> b, f(g(g(a)),?x) -> b ] P: [ g(a) -> g(g(a)) ] P: not reversible failure(Step 3) failure(no possibility remains) unknown Reduction-Preserving Completion check by Ordered Rewriting... remove redundants rules and split R-part: [ if(true,a,?x) -> a, if(true,b,?x) -> b, if(true,g(a),?x) -> g(a), if(true,g(b),?x) -> g(b), if(false,?x,a) -> a, if(false,?x,b) -> b, if(false,?x,g(a)) -> g(a), if(false,?x,g(b)) -> g(b), g(a) -> g(g(a)), g(b) -> a, f(a,b) -> b, f(g(g(a)),?x) -> b ] E-part: [ ] ...failed to find a suitable LPO. unknown Confluence by Ordered Rewriting Direct Methods: Can't judge Try Persistent Decomposition for... [ if(true,a,?x) -> a, if(true,b,?x) -> b, if(true,g(a),?x) -> g(a), if(true,g(b),?x) -> g(b), if(false,?x,a) -> a, if(false,?x,b) -> b, if(false,?x,g(a)) -> g(a), if(false,?x,g(b)) -> g(b), g(a) -> g(g(a)), g(b) -> a, f(a,b) -> b, f(g(g(a)),?x) -> b ] Sort Assignment: a : =>23 b : =>23 f : 23*23=>23 g : 23=>23 if : 17*23*23=>23 true : =>17 false : =>17 maximal types: {17,23} Persistent Decomposition failed: Can't judge Try Layer Preserving Decomposition for... [ if(true,a,?x) -> a, if(true,b,?x) -> b, if(true,g(a),?x) -> g(a), if(true,g(b),?x) -> g(b), if(false,?x,a) -> a, if(false,?x,b) -> b, if(false,?x,g(a)) -> g(a), if(false,?x,g(b)) -> g(b), g(a) -> g(g(a)), g(b) -> a, f(a,b) -> b, f(g(g(a)),?x) -> b ] Layer Preserving Decomposition failed: Can't judge Try Commutative Decomposition for... [ if(true,a,?x) -> a, if(true,b,?x) -> b, if(true,g(a),?x) -> g(a), if(true,g(b),?x) -> g(b), if(false,?x,a) -> a, if(false,?x,b) -> b, if(false,?x,g(a)) -> g(a), if(false,?x,g(b)) -> g(b), g(a) -> g(g(a)), g(b) -> a, f(a,b) -> b, f(g(g(a)),?x) -> b ] Inside Critical Pair: by Rules <8, 2> develop reducts from lhs term... <{8}, if(true,g(g(g(a))),?x_2)> <{}, if(true,g(g(a)),?x_2)> develop reducts from rhs term... <{8}, g(g(a))> <{}, g(a)> Inside Critical Pair: by Rules <9, 3> develop reducts from lhs term... <{0}, a> <{}, if(true,a,?x_3)> develop reducts from rhs term... <{9}, a> <{}, g(b)> Inside Critical Pair: by Rules <8, 6> develop reducts from lhs term... <{8}, if(false,?x_6,g(g(g(a))))> <{}, if(false,?x_6,g(g(a)))> develop reducts from rhs term... <{8}, g(g(a))> <{}, g(a)> Inside Critical Pair: by Rules <9, 7> develop reducts from lhs term... <{4}, a> <{}, if(false,?x_7,a)> develop reducts from rhs term... <{9}, a> <{}, g(b)> Inside Critical Pair: by Rules <8, 11> develop reducts from lhs term... <{8}, f(g(g(g(g(a)))),?x_8)> <{}, f(g(g(g(a))),?x_8)> develop reducts from rhs term... <{}, b> Try A Minimal Decomposition {0,3}{4,7}{11,6,2,8}{1}{5}{9}{10} {0,3} (cm)Rewrite Rules: [ if(true,a,?x) -> a, if(true,g(b),?x) -> g(b) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {4,7} (cm)Rewrite Rules: [ if(false,?x,a) -> a, if(false,?x,g(b)) -> g(b) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {11,6,2,8} (cm)Rewrite Rules: [ f(g(g(a)),?x) -> b, if(false,?x,g(a)) -> g(a), if(true,g(a),?x) -> g(a), g(a) -> g(g(a)) ] Apply Direct Methods... Inner CPs: [ f(g(g(g(a))),?x) = b, if(false,?x_1,g(g(a))) = g(a), if(true,g(g(a)),?x_2) = g(a) ] 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: [ f(g(g(g(a))),?x) = b, if(false,?x,g(g(a))) = g(a), if(true,g(g(a)),?x) = g(a), b = f(g(g(g(a))),?x), g(a) = if(false,?x_1,g(g(a))), g(a) = if(true,g(g(a)),?x_2) ] 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 [(f,1),(g,1)] unknown Diagram Decreasing check Non-Confluence... obtain 8 rules by 3 steps unfolding obtain 96 candidates for checking non-joinability check by TCAP-Approximation (failure) check by Ordering(rpo), check by Tree-Automata Approximation (success) where F = {(a,0),(b,0),(f,2),(g,1),(if,3),(c_1,0),(true,0),(false,0)} Q = {q_0,q_1,q_{c_1},q_{g(g(a))},q_{a},q_{g(a)},q_{g(g(g(a)))}} Qf = {q_0,q_1} Delta = [ a -> q_{a}, b -> q_1, f(q_{g(g(g(a)))},q_{c_1}) -> q_0, g(q_{g(g(a))}) -> q_{g(g(g(a)))}, g(q_{a}) -> q_{g(a)}, g(q_{g(a)}) -> q_{g(g(a))}, g(q_{g(a)}) -> q_{g(a)}, c_1 -> q_{c_1} ] (failure) check by Interpretation(mod2) (failure) check by Descendants-Approximation, check by Ordering(poly) (success) Polynomial Interpretation: a:= (1) b:= (8) f:= (1)*x1 g:= (1)+(2)*x1 c_1:= (9) [g(g(a))]-[g(a)] = (4) >= 0 [b]-[f(g(g(a)),?x)] = (1) >= 0 [f(g(g(g(a))),c_1)]-[b] = (7) > 0 (success) Witness for Non-Confluence: b> Direct Methods: not CR {1} (cm)Rewrite Rules: [ if(true,b,?x) -> b ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {5} (cm)Rewrite Rules: [ if(false,?x,b) -> b ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {9} (cm)Rewrite Rules: [ g(b) -> a ] 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: [ f(a,b) -> b ] 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 {3,9}{4,7}{11,6,2,8}{0}{1}{5}{10} {3,9} (cm)Rewrite Rules: [ if(true,g(b),?x) -> g(b), g(b) -> a ] Apply Direct Methods... Inner CPs: [ if(true,a,?x) = g(b) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {4,7} (cm)Rewrite Rules: [ if(false,?x,a) -> a, if(false,?x,g(b)) -> g(b) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {11,6,2,8} (cm)Rewrite Rules: [ f(g(g(a)),?x) -> b, if(false,?x,g(a)) -> g(a), if(true,g(a),?x) -> g(a), g(a) -> g(g(a)) ] Apply Direct Methods... Inner CPs: [ f(g(g(g(a))),?x) = b, if(false,?x_1,g(g(a))) = g(a), if(true,g(g(a)),?x_2) = g(a) ] 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: [ f(g(g(g(a))),?x) = b, if(false,?x,g(g(a))) = g(a), if(true,g(g(a)),?x) = g(a), b = f(g(g(g(a))),?x), g(a) = if(false,?x_1,g(g(a))), g(a) = if(true,g(g(a)),?x_2) ] 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 [(f,1),(g,1)] unknown Diagram Decreasing check Non-Confluence... obtain 8 rules by 3 steps unfolding obtain 96 candidates for checking non-joinability check by TCAP-Approximation (failure) check by Ordering(rpo), check by Tree-Automata Approximation (success) where F = {(a,0),(b,0),(f,2),(g,1),(if,3),(c_1,0),(true,0),(false,0)} Q = {q_0,q_1,q_{c_1},q_{g(g(a))},q_{a},q_{g(a)},q_{g(g(g(a)))}} Qf = {q_0,q_1} Delta = [ a -> q_{a}, b -> q_1, f(q_{g(g(g(a)))},q_{c_1}) -> q_0, g(q_{g(g(a))}) -> q_{g(g(g(a)))}, g(q_{a}) -> q_{g(a)}, g(q_{g(a)}) -> q_{g(g(a))}, g(q_{g(a)}) -> q_{g(a)}, c_1 -> q_{c_1} ] (failure) check by Interpretation(mod2) (failure) check by Descendants-Approximation, check by Ordering(poly) (success) Polynomial Interpretation: a:= (1) b:= (8) f:= (1)*x1 g:= (1)+(2)*x1 c_1:= (9) [g(g(a))]-[g(a)] = (4) >= 0 [b]-[f(g(g(a)),?x)] = (1) >= 0 [f(g(g(g(a))),c_1)]-[b] = (7) > 0 (success) Witness for Non-Confluence: b> Direct Methods: not CR {0} (cm)Rewrite Rules: [ if(true,a,?x) -> a ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {1} (cm)Rewrite Rules: [ if(true,b,?x) -> b ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {5} (cm)Rewrite Rules: [ if(false,?x,b) -> b ] 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: [ f(a,b) -> b ] 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,3}{7,9}{11,6,2,8}{1}{4}{5}{10} {0,3} (cm)Rewrite Rules: [ if(true,a,?x) -> a, if(true,g(b),?x) -> g(b) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {7,9} (cm)Rewrite Rules: [ if(false,?x,g(b)) -> g(b), g(b) -> a ] Apply Direct Methods... Inner CPs: [ if(false,?x,a) = g(b) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {11,6,2,8} (cm)Rewrite Rules: [ f(g(g(a)),?x) -> b, if(false,?x,g(a)) -> g(a), if(true,g(a),?x) -> g(a), g(a) -> g(g(a)) ] Apply Direct Methods... Inner CPs: [ f(g(g(g(a))),?x) = b, if(false,?x_1,g(g(a))) = g(a), if(true,g(g(a)),?x_2) = g(a) ] 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: [ f(g(g(g(a))),?x) = b, if(false,?x,g(g(a))) = g(a), if(true,g(g(a)),?x) = g(a), b = f(g(g(g(a))),?x), g(a) = if(false,?x_1,g(g(a))), g(a) = if(true,g(g(a)),?x_2) ] 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 [(f,1),(g,1)] unknown Diagram Decreasing check Non-Confluence... obtain 8 rules by 3 steps unfolding obtain 96 candidates for checking non-joinability check by TCAP-Approximation (failure) check by Ordering(rpo), check by Tree-Automata Approximation (success) where F = {(a,0),(b,0),(f,2),(g,1),(if,3),(c_1,0),(true,0),(false,0)} Q = {q_0,q_1,q_{c_1},q_{g(g(a))},q_{a},q_{g(a)},q_{g(g(g(a)))}} Qf = {q_0,q_1} Delta = [ a -> q_{a}, b -> q_1, f(q_{g(g(g(a)))},q_{c_1}) -> q_0, g(q_{g(g(a))}) -> q_{g(g(g(a)))}, g(q_{a}) -> q_{g(a)}, g(q_{g(a)}) -> q_{g(g(a))}, g(q_{g(a)}) -> q_{g(a)}, c_1 -> q_{c_1} ] (failure) check by Interpretation(mod2) (failure) check by Descendants-Approximation, check by Ordering(poly) (success) Polynomial Interpretation: a:= (1) b:= (8) f:= (1)*x1 g:= (1)+(2)*x1 c_1:= (9) [g(g(a))]-[g(a)] = (4) >= 0 [b]-[f(g(g(a)),?x)] = (1) >= 0 [f(g(g(g(a))),c_1)]-[b] = (7) > 0 (success) Witness for Non-Confluence: b> Direct Methods: not CR {1} (cm)Rewrite Rules: [ if(true,b,?x) -> b ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {4} (cm)Rewrite Rules: [ if(false,?x,a) -> a ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {5} (cm)Rewrite Rules: [ if(false,?x,b) -> b ] 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: [ f(a,b) -> b ] 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 {7,3,9}{11,6,2,8}{0}{1}{4}{5}{10} {7,3,9} (cm)Rewrite Rules: [ if(false,?x,g(b)) -> g(b), if(true,g(b),?x) -> g(b), g(b) -> a ] Apply Direct Methods... Inner CPs: [ if(false,?x,a) = g(b), if(true,a,?x_1) = g(b) ] Outer CPs: [ ] not Overlay, check Termination... Terminating, not WCR Knuth & Bendix Direct Methods: not CR {11,6,2,8} (cm)Rewrite Rules: [ f(g(g(a)),?x) -> b, if(false,?x,g(a)) -> g(a), if(true,g(a),?x) -> g(a), g(a) -> g(g(a)) ] Apply Direct Methods... Inner CPs: [ f(g(g(g(a))),?x) = b, if(false,?x_1,g(g(a))) = g(a), if(true,g(g(a)),?x_2) = g(a) ] 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: [ f(g(g(g(a))),?x) = b, if(false,?x,g(g(a))) = g(a), if(true,g(g(a)),?x) = g(a), b = f(g(g(g(a))),?x), g(a) = if(false,?x_1,g(g(a))), g(a) = if(true,g(g(a)),?x_2) ] 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 [(f,1),(g,1)] unknown Diagram Decreasing check Non-Confluence... obtain 8 rules by 3 steps unfolding obtain 96 candidates for checking non-joinability check by TCAP-Approximation (failure) check by Ordering(rpo), check by Tree-Automata Approximation (success) where F = {(a,0),(b,0),(f,2),(g,1),(if,3),(c_1,0),(true,0),(false,0)} Q = {q_0,q_1,q_{c_1},q_{g(g(a))},q_{a},q_{g(a)},q_{g(g(g(a)))}} Qf = {q_0,q_1} Delta = [ a -> q_{a}, b -> q_1, f(q_{g(g(g(a)))},q_{c_1}) -> q_0, g(q_{g(g(a))}) -> q_{g(g(g(a)))}, g(q_{a}) -> q_{g(a)}, g(q_{g(a)}) -> q_{g(g(a))}, g(q_{g(a)}) -> q_{g(a)}, c_1 -> q_{c_1} ] (failure) check by Interpretation(mod2) (failure) check by Descendants-Approximation, check by Ordering(poly) (success) Polynomial Interpretation: a:= (1) b:= (8) f:= (1)*x1 g:= (1)+(2)*x1 c_1:= (9) [g(g(a))]-[g(a)] = (4) >= 0 [b]-[f(g(g(a)),?x)] = (1) >= 0 [f(g(g(g(a))),c_1)]-[b] = (7) > 0 (success) Witness for Non-Confluence: b> Direct Methods: not CR {0} (cm)Rewrite Rules: [ if(true,a,?x) -> a ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {1} (cm)Rewrite Rules: [ if(true,b,?x) -> b ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {4} (cm)Rewrite Rules: [ if(false,?x,a) -> a ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... Innermost Terminating (hence Terminating), WCR Knuth & Bendix Direct Methods: CR {5} (cm)Rewrite Rules: [ if(false,?x,b) -> b ] 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: [ f(a,b) -> b ] 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 741.trs: Failure(unknown CR) (1301 msec.)