YES (ignored inputs)COMMENT from the collection of \cite{AT2012} Rewrite Rules: [ +(?x,?y) -> +(?y,?x) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ ] Overlay, check Innermost Termination... unknown Innermost Terminating unknown Knuth & Bendix Linear Development Closed Direct Methods: CR Final result: CR 179.trs: Success(CR) (0 msec.)