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),
     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 ]
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),
     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 ]
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),
     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 ]
convertible distinct normal forms: p(minus(s(?x_6),?y_4)) = minus(?x_6,?y_4)
UNC Completion (Development Closed)
problems/631.trs: Success(not UNC)
(0 msec.)