MAYBE
(ignored inputs)COMMENT experiments for [125] submitted by: Takahito Aoto
input TRS:
   [ +(?x,?y) -> if(?y,?x,s(+(?x,-(?y,s(0))))),
     if(0,?y,?z) -> ?y,
     if(s(?x),?y,?z) -> ?z,
     if(?x,?y,?y) -> ?y,
     -(?x,0) -> ?x,
     -(0,s(?y)) -> 0,
     -(s(?x),s(?y)) -> -(?x,?y) ]
TRS:
   [ +(?x,?y) -> if(?y,?x,s(+(?x,-(?y,s(0))))),
     if(0,?y,?z) -> ?y,
     if(s(?x),?y,?z) -> ?z,
     if(?x,?y,?y) -> ?y,
     -(?x,0) -> ?x,
     -(0,s(?y)) -> 0,
     -(s(?x),s(?y)) -> -(?x,?y) ]
New rules by rule reversing:
   [ +(?x,?y) -> +(?x,?y),
     if(?y,?x,s(+(?x,-(?y,s(0))))) -> +(?x,?y),
     if(0,?y,?z) -> ?y,
     if(s(?x),?y,?z) -> ?z,
     if(?x,?y,?y) -> ?y,
     -(?x,0) -> ?x,
     -(0,s(?y)) -> 0,
     -(s(?x),s(?y)) -> -(?x,?y) ]
unknown UNC Completion (Strongly Closed)
problems/598.trs: Failure(unknown UNC)
(0 msec.)