MAYBE
Trs:
 {                   reverse(xs) -> rev(xs, nil()),
      last(cons(x, cons(y, ys))) -> last(cons(y, ys)),
            last(cons(x, nil())) -> x,
         append(cons(x, xs), ys) -> cons(x, append(xs, ys)),
               append(nil(), ys) -> ys,
  dropLast(cons(x, cons(y, ys))) -> cons(x, dropLast(cons(y, ys))),
        dropLast(cons(x, nil())) -> nil(),
                 dropLast(nil()) -> nil(),
            isEmpty(cons(x, xs)) -> false(),
                  isEmpty(nil()) -> true(),
          if(true(), xs, ys, zs) -> zs,
         if(false(), xs, ys, zs) -> rev(xs, ys),
                     rev(xs, ys) -> if(isEmpty(xs), dropLast(xs), append(ys, last(xs)), ys)}
 Comment:
  We consider a duplicating trs.
  FAIL:
   Open