YES (ignored inputs)COMMENT reduction failed Rewrite Rules: [ -(+(?x,?y)) -> +(-(?x),-(?y)), +(?x,?y) -> +(?y,?x) ] Apply Direct Methods... Inner CPs: [ -(+(?y_1,?x_1)) = +(-(?x_1),-(?y_1)) ] 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/fileWK5D2n.trs: Success(CR) (0 msec.)