YES (ignored inputs)COMMENT from the collection of \cite{AT2012} 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 Final result: CR 149.trs: Success(CR) (0 msec.)