YES (ignored inputs)COMMENT reduction failed Rewrite Rules: [ -(+(?x,?y)) -> +(-(?x),-(?y)), +(-(?x),-(?y)) -> -(+(?x,?y)) ] Apply Direct Methods... Inner CPs: [ -(-(+(?x_1,?y_1))) = +(-(-(?x_1)),-(-(?y_1))), +(+(-(?x),-(?y)),-(?y_1)) = -(+(+(?x,?y),?y_1)), +(-(?x_1),+(-(?x),-(?y))) = -(+(?x_1,+(?x,?y))) ] Outer CPs: [ ] not Overlay, check Termination... unknown/not Terminating unknown Knuth & Bendix Linear unknown Development Closed Strongly Closed Direct Methods: CR Combined result: CR /tmp/fileXGxPMf.trs: Success(CR) (22 msec.)