TRS:
 {f(true(), x, y, z) -> f(gt(x, plus(y, z)), x, s(y), z),
  f(true(), x, y, z) -> f(gt(x, plus(y, z)), x, y, s(z)),
        plus(n, 0()) -> n,
       plus(n, s(m)) -> s(plus(n, m)),
          gt(0(), v) -> false(),
       gt(s(u), 0()) -> true(),
      gt(s(u), s(v)) -> gt(u, v)}
 Fail