MAYBE
Trs:
 { ifPlus(true(), x, y, z) -> y,
  ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z)),
         plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z),
            le(s(x), s(y)) -> le(x, y),
             le(s(x), 0()) -> false(),
                le(0(), y) -> true(),
                   sum(xs) -> sumIter(xs, 0()),
                plus(x, y) -> plusIter(x, y, 0()),
   ifSum(true(), xs, x, y) -> x,
  ifSum(false(), xs, x, y) -> sumIter(tail(xs), y),
            sumIter(xs, x) -> ifSum(isempty(xs), xs, x, plus(x, head(xs))),
            isempty(nil()) -> true(),
      isempty(cons(x, xs)) -> false(),
               head(nil()) -> error(),
         head(cons(x, xs)) -> x,
               tail(nil()) -> nil(),
         tail(cons(x, xs)) -> xs,
                       a() -> b(),
                       a() -> c()}
 Comment:
  We consider a duplicating trs.
  FAIL:
   Open