YES (ignored inputs)COMMENT submitted by: Yusuke Oi used by secret problem 2019 COPS #1128 Rewrite Rules: [ -(0,?x) -> 0, -(?x,0) -> ?x, -(s(?x),s(?y)) -> -(?x,?y) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ 0 = 0 ] Linear (inner) Parallel CPs: [ ] Toyama (Parallel CPs) Direct Methods: CR Combined result: CR 1127.trs: Success(CR) (0 msec.)