YES (ignored inputs)COMMENT full experiments for [35] submitted by: Takahito Aoto and Yoshihito Toyama 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 149.trs: Success(CR) (0 msec.)