MAYBE
(ignored inputs)COMMENT experiments for [125] submitted by: Takahito Aoto
input TRS:
   [ +(?x,?y) -> if(?y,?x,s(+(?x,-(?y,s(0))))),
     +(?x,?y) -> +(?y,?x),
     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))))),
     +(?x,?y) -> +(?y,?x),
     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:
   [ if(?y,?x,s(+(?x,-(?y,s(0))))) -> +(?x,?y),
     +(?x,?y) -> +(?y,?x),
     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) ]
Check distinct normal forms in critical pair closure...failed
problems/599.trs: Failure(unknown UNC)
(8 msec.)