MAYBE MAYBE TRS: { minus(minus(x)) -> x, +(minus(x), +(x, y)) -> y, +(+(x, y), minus(y)) -> x, minux(+(x, y)) -> +(minus(y), minus(x)) } DUP: We consider a non-duplicating system. Trs: { minus(minus(x)) -> x, +(minus(x), +(x, y)) -> y, +(+(x, y), minus(y)) -> x, minux(+(x, y)) -> +(minus(y), minus(x)) } Fail