MAYBE
Trs:
 {                   rev(x) -> if(x, eq(0(), length(x)), nil(), 0(), length(x)),
  help(c, l, cons(x, y), z) -> if(append(y, cons(x, nil())), ge(c, l), cons(x, z), c, l),
              ge(0(), s(y)) -> false(),
             ge(s(x), s(y)) -> ge(x, y),
                 ge(x, 0()) -> true(),
     if(x, true(), z, c, l) -> z,
    if(x, false(), z, c, l) -> help(s(c), l, x, z),
           append(nil(), y) -> y,
      append(cons(x, y), z) -> cons(x, append(y, z)),
              length(nil()) -> 0(),
         length(cons(x, y)) -> s(length(y))}
 Comment:
  We consider a duplicating trs.
  FAIL:
   Open