NO (ignored inputs)COMMENT reduction failed Rewrite Rules: [ +(0,?y) -> ?y, +(s(?x),?y) -> s(+(?x,?y)), +(?x,0) -> +(0,?x), +(?x,s(?y)) -> +(s(?y),?x) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ 0 = +(0,0), s(?y_3) = +(s(?y_3),0), s(+(?x_1,0)) = +(0,s(?x_1)), s(+(?x_1,s(?y_3))) = +(s(?y_3),s(?x_1)) ] 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: [ +(0,0) = 0, +(s(?y_3),0) = s(?y_3), +(0,s(?x)) = s(+(?x,0)), +(s(?y_3),s(?x)) = s(+(?x,s(?y_3))), 0 = +(0,0), s(+(?x_2,0)) = +(0,s(?x_2)), s(?y) = +(s(?y),0), s(+(?x_2,s(?y))) = +(s(?y),s(?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 <+(0,0), 0> by Rules <2, 0> preceded by [] joinable by a reduction of rules <[([],0)], []> Critical Pair <+(s(?y_3),0), s(?y_3)> by Rules <3, 0> preceded by [] joinable by a reduction of rules <[([],2),([],0)], []> Critical Pair <+(0,s(?x_1)), s(+(?x_1,0))> by Rules <2, 1> preceded by [] joinable by a reduction of rules <[([],3),([],1)], []> joinable by a reduction of rules <[([],0)], [([(s,1)],2),([(s,1)],0)]> Critical Pair <+(s(?y_3),s(?x_1)), s(+(?x_1,s(?y_3)))> by Rules <3, 1> preceded by [] joinable by a reduction of rules <[([],3),([],1)], []> unknown Diagram Decreasing check Non-Confluence... obtain 9 rules by 3 steps unfolding obtain 35 candidates for checking non-joinability check by TCAP-Approximation (success) (failure) check by Ordering(rpo), check by Tree-Automata Approximation (success) Witness for Non-Confluence: s(s(+(c_2,c_1)))> Direct Methods: not CR Combined result: not CR /tmp/fileWFmWdu.trs: Success(not CR) (189 msec.)