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