NO
(ignored inputs)COMMENT experiments for [125] submitted by: Takahito Aoto
input TRS:
   [ 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 ]
TRS:
   [ 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 ]
New rules by rule reversing:
   [ 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) -> inv(?x),
     minus(0,?x) -> inv(?x),
     inv(minus(?x,?y)) -> minus(?y,?x),
     s(p(?x)) -> ?x,
     p(s(?x)) -> ?x ]
constructed TRS:
   [ 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) -> inv(?x),
     minus(0,?x) -> inv(?x),
     inv(minus(?x,?y)) -> minus(?y,?x),
     s(p(?x)) -> ?x,
     p(s(?x)) -> ?x,
     p(inv(p(?x_9))) -> inv(?x_9),
     s(inv(s(?x_10))) -> inv(?x_10),
     s(minus(?x_3,s(?x_10))) -> minus(?x_3,?x_10),
     p(minus(?x_4,p(?x_9))) -> minus(?x_4,?x_9),
     inv(?x_2) -> inv(?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)) -> ?x_5 ]
convertible distinct normal forms: s(minus(?x_20,?x_13)) = minus(s(?x_20),?x_13)
UNC Completion (Development Closed)
problems/632.trs: Success(not UNC)
(8 msec.)