MAYBE
Trs:
 {       g(0()) -> s(0()),
        g(s(x)) -> -(s(x), f(g(x))),
         f(0()) -> 0(),
        f(s(x)) -> -(s(x), g(f(x))),
   -(0(), s(y)) -> 0(),
  -(s(x), s(y)) -> -(x, y),
      -(x, 0()) -> x}
 Comment:
  We consider a duplicating trs.
  FAIL:
   Open