MAYBE
(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) ]
Linear
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Direct Methods: Can't judge

Combined result: Can't judge
631.trs: Failure(unknown CR)
(0 msec.)