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