(ignored inputs)COMMENT experiments for [125] submitted by: Takahito Aoto Rewrite Rules: [ inv(0) -> 0, inv(s(?x)) -> p(inv(?x)), inv(p(?x)) -> s(inv(?x)), minus(?x,0) -> ?x, minus(?x,p(?y)) -> s(minus(?x,?y)), minus(?x,s(?y)) -> p(minus(?x,?y)), minus(0,?x) -> inv(?x), inv(?x) -> minus(0,?x), inv(minus(?x,?y)) -> minus(?y,?x), s(p(?x)) -> ?x, p(s(?x)) -> ?x ] Apply Direct Methods... Inner CPs: [ inv(?x_8) = p(inv(p(?x_8))), inv(?x_9) = s(inv(s(?x_9))), minus(?x_3,?x_9) = s(minus(?x_3,s(?x_9))), minus(?x_4,?x_8) = p(minus(?x_4,p(?x_8))), inv(?x_2) = minus(0,?x_2), inv(s(minus(?x_3,?y_3))) = minus(p(?y_3),?x_3), inv(p(minus(?x_4,?y_4))) = minus(s(?y_4),?x_4), inv(inv(?x_5)) = minus(?x_5,0), s(?x_9) = s(?x_9), p(?x_8) = p(?x_8) ] Outer CPs: [ 0 = minus(0,0), p(inv(?x)) = minus(0,s(?x)), s(inv(?x_1)) = minus(0,p(?x_1)), 0 = inv(0), s(minus(0,?y_3)) = inv(p(?y_3)), p(minus(0,?y_4)) = inv(s(?y_4)), minus(0,minus(?x_7,?y_7)) = minus(?y_7,?x_7) ] not Overlay, check Termination... unknown/not 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: [ minus(0,0) = 0, minus(0,?x_9) = p(inv(p(?x_9))), minus(0,s(?x)) = p(inv(?x)), inv(?x_9) = p(inv(p(?x_9))), minus(0,?x_10) = s(inv(s(?x_10))), minus(0,p(?x)) = s(inv(?x)), inv(?x_10) = s(inv(s(?x_10))), inv(0) = 0, minus(0,?x) = inv(?x), inv(?x_10) = s(minus(0,s(?x_10))), inv(p(?y)) = s(minus(0,?y)), minus(?x,?x_10) = s(minus(?x,s(?x_10))), minus(?x_10,?x) = inv(s(minus(?x,s(?x_10)))), minus(p(?y),?x) = inv(s(minus(?x,?y))), inv(?x_9) = p(minus(0,p(?x_9))), inv(s(?y)) = p(minus(0,?y)), minus(?x,?x_9) = p(minus(?x,p(?x_9))), minus(?x_9,?x) = inv(p(minus(?x,p(?x_9)))), minus(s(?y),?x) = inv(p(minus(?x,?y))), 0 = inv(0), s(minus(0,?y_4)) = inv(p(?y_4)), p(minus(0,?y_5)) = inv(s(?y_5)), minus(?x,0) = inv(inv(?x)), 0 = minus(0,0), p(inv(?x_1)) = minus(0,s(?x_1)), s(inv(?x_2)) = minus(0,p(?x_2)), minus(?y_7,?x_7) = minus(0,minus(?x_7,?y_7)), minus(0,?x) = minus(0,?x), minus(0,s(minus(?x,?y_5))) = minus(p(?y_5),?x), minus(0,p(minus(?x,?y_6))) = minus(s(?y_6),?x), minus(0,inv(?y)) = minus(?y,0), minus(0,minus(?x,?y)) = minus(?y,?x), inv(?x) = minus(0,?x), inv(s(minus(?x,?y_5))) = minus(p(?y_5),?x), inv(p(minus(?x,?y_6))) = minus(s(?y_6),?x), inv(inv(?y)) = minus(?y,0), s(?x_10) = s(?x_10), p(inv(?x_10)) = inv(s(?x_10)), p(minus(?x_6,?x_16)) = minus(?x_6,s(?x_16)), ?x_10 = p(s(?x_10)), p(inv(p(?x))) = inv(?x), p(minus(?x_6,p(?x))) = minus(?x_6,?x), p(?x) = p(?x), s(inv(?x_10)) = inv(p(?x_10)), s(minus(?x_5,?x_15)) = minus(?x_5,p(?x_15)), ?x_10 = s(p(?x_10)), s(inv(s(?x))) = inv(?x), s(minus(?x_5,s(?x))) = minus(?x_5,?x) ] 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 <9, 1> preceded by [(inv,1)] joinable by a reduction of rules <[], [([(p,1)],2),([],10)]> Critical Pair by Rules <10, 2> preceded by [(inv,1)] joinable by a reduction of rules <[], [([(s,1)],1),([],9)]> Critical Pair by Rules <10, 4> preceded by [(minus,2)] joinable by a reduction of rules <[], [([(s,1)],5),([],9)]> Critical Pair by Rules <9, 5> preceded by [(minus,2)] joinable by a reduction of rules <[], [([(p,1)],4),([],10)]> Critical Pair by Rules <3, 8> preceded by [(inv,1)] joinable by a reduction of rules <[([],7)], []> joinable by a reduction of rules <[], [([],6)]> Critical Pair by Rules <4, 8> preceded by [(inv,1)] unknown Diagram Decreasing check Non-Confluence... obtain 14 rules by 3 steps unfolding obtain 80 candidates for checking non-joinability check by TCAP-Approximation (success) Witness for Non-Confluence: minus(p(c_2),c_1)> Direct Methods: not CR Combined result: not CR 632.trs: Success(not CR) NO (45 msec.)