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