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