MAYBE
Trs:
 {       empty(nil()) -> true(),
    empty(cons(x, l)) -> false(),
     if(true(), x, l) -> x,
    if(false(), x, l) -> last(head(l), tail(l)),
          tail(nil()) -> nil(),
     tail(cons(x, l)) -> l,
     head(cons(x, l)) -> x,
           last(x, l) -> if(empty(l), x, l),
       rev2(x, nil()) -> nil(),
  rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l))),
           rev(nil()) -> nil(),
      rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l))}
 Comment:
  We consider a duplicating trs.
  FAIL:
   Open