TIMEOUT
MAYBE
Trs:
 {      minux(+(x, y)) -> +(minus(y), minus(x)),
       minus(minus(x)) -> x,
  +(minus(x), +(x, y)) -> y,
  +(+(x, y), minus(y)) -> x}
 Open