TRS:
 { +(0(), y) -> y,
  +(s(x), y) -> s(+(x, y)),
  +(s(x), y) -> +(x, s(y))}
 Fail