(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),
     minus(s(?x),s(?y)) -> minus(?x,?y),
     minus(p(?x),p(?y)) -> minus(?x,?y),
     inv(?x) -> minus(0,?x),
     s(p(?x)) -> ?x,
     p(s(?x)) -> ?x ]
Apply Direct Methods...
Inner CPs:
   [ inv(?x_9) = p(inv(p(?x_9))),
     inv(?x_10) = s(inv(s(?x_10))),
     minus(?x_3,?x_10) = s(minus(?x_3,s(?x_10))),
     minus(?x_4,?x_9) = p(minus(?x_4,p(?x_9))),
     minus(?x_9,s(?y_6)) = minus(p(?x_9),?y_6),
     minus(s(?x_6),?x_9) = minus(?x_6,p(?x_9)),
     minus(?x_10,p(?y_7)) = minus(s(?x_10),?y_7),
     minus(p(?x_7),?x_10) = minus(?x_7,s(?x_10)),
     s(?x_10) = s(?x_10),
     p(?x_9) = p(?x_9) ]
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)),
     s(minus(p(?x_7),?y_3)) = minus(?x_7,?y_3),
     p(minus(0,?y_4)) = inv(s(?y_4)),
     p(minus(s(?x_6),?y_4)) = minus(?x_6,?y_4) ]
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_10) = p(inv(p(?x_10))),
     minus(0,s(?x)) = p(inv(?x)),
     inv(?x_10) = p(inv(p(?x_10))),
     minus(0,?x_11) = s(inv(s(?x_11))),
     minus(0,p(?x)) = s(inv(?x)),
     inv(?x_11) = s(inv(s(?x_11))),
     inv(0) = 0,
     inv(?x_11) = s(minus(0,s(?x_11))),
     inv(p(?y)) = s(minus(0,?y)),
     minus(?x_7,?y) = s(minus(p(?x_7),?y)),
     minus(?x,?x_11) = s(minus(?x,s(?x_11))),
     inv(?x_10) = p(minus(0,p(?x_10))),
     inv(s(?y)) = p(minus(0,?y)),
     minus(?x_6,?y) = p(minus(s(?x_6),?y)),
     minus(?x,?x_10) = p(minus(?x,p(?x_10))),
     0 = inv(0),
     s(minus(0,?y_4)) = inv(p(?y_4)),
     p(minus(0,?y_5)) = inv(s(?y_5)),
     p(minus(?x_10,?y)) = minus(p(?x_10),?y),
     minus(?x_10,?x_20) = minus(p(?x_10),p(?x_20)),
     p(minus(s(?x),?y)) = minus(?x,?y),
     minus(?x_10,s(?y)) = minus(p(?x_10),?y),
     minus(s(?x),?x_10) = minus(?x,p(?x_10)),
     s(minus(?x_11,?y)) = minus(s(?x_11),?y),
     minus(?x_11,?x_22) = minus(s(?x_11),s(?x_22)),
     s(minus(p(?x),?y)) = minus(?x,?y),
     minus(?x_11,p(?y)) = minus(s(?x_11),?y),
     minus(p(?x),?x_11) = minus(?x,s(?x_11)),
     0 = minus(0,0),
     p(inv(?x_1)) = minus(0,s(?x_1)),
     s(inv(?x_2)) = minus(0,p(?x_2)),
     s(?x_11) = s(?x_11),
     p(inv(?x_11)) = inv(s(?x_11)),
     p(minus(?x_6,?x_17)) = minus(?x_6,s(?x_17)),
     ?x_11 = p(s(?x_11)),
     p(inv(p(?x))) = inv(?x),
     p(minus(?x_6,p(?x))) = minus(?x_6,?x),
     p(?x) = p(?x),
     s(inv(?x_11)) = inv(p(?x_11)),
     s(minus(?x_5,?x_16)) = minus(?x_5,p(?x_16)),
     ?x_11 = s(p(?x_11)),
     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 <inv(?x_9), p(inv(p(?x_9)))> by Rules <10, 1> preceded by [(inv,1)]
 joinable by a reduction of rules <[], [([(p,1)],2),([],11)]>
Critical Pair <inv(?x_10), s(inv(s(?x_10)))> by Rules <11, 2> preceded by [(inv,1)]
 joinable by a reduction of rules <[], [([(s,1)],1),([],10)]>
Critical Pair <minus(?x_3,?x_10), s(minus(?x_3,s(?x_10)))> by Rules <11, 4> preceded by [(minus,2)]
 joinable by a reduction of rules <[], [([(s,1)],5),([],10)]>
Critical Pair <minus(?x_4,?x_9), p(minus(?x_4,p(?x_9)))> by Rules <10, 5> preceded by [(minus,2)]
 joinable by a reduction of rules <[], [([(p,1)],4),([],11)]>
Critical Pair <minus(?x_9,s(?y_6)), minus(p(?x_9),?y_6)> by Rules <10, 7> preceded by [(minus,1)]
unknown Diagram Decreasing
check Non-Confluence...
obtain 17 rules by 3 steps unfolding
obtain 55 candidates for checking non-joinability
check by TCAP-Approximation (success)
Witness for Non-Confluence: <p(minus(c_1,c_2)) <- minus(p(c_1),p(s(c_2))) -> minus(p(c_1),c_2)>
Direct Methods: not CR

Combined result: not CR
631.trs: Success(not CR)
NO
(43 msec.)