YES

Problem:
 empty(nil()) -> true()
 empty(cons(x,l)) -> false()
 head(cons(x,l)) -> x
 tail(nil()) -> nil()
 tail(cons(x,l)) -> l
 rev(nil()) -> nil()
 rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
 last(x,l) -> if(empty(l),x,l)
 if(true(),x,l) -> x
 if(false(),x,l) -> last(head(l),tail(l))
 rev2(x,nil()) -> nil()
 rev2(x,cons(y,l)) -> rev(cons(x,rev2(y,l)))

Proof:
 DP Processor:
  DPs:
   rev#(cons(x,l)) -> rev2#(x,l)
   last#(x,l) -> empty#(l)
   last#(x,l) -> if#(empty(l),x,l)
   if#(false(),x,l) -> tail#(l)
   if#(false(),x,l) -> head#(l)
   if#(false(),x,l) -> last#(head(l),tail(l))
   rev2#(x,cons(y,l)) -> rev2#(y,l)
   rev2#(x,cons(y,l)) -> rev#(cons(x,rev2(y,l)))
  TRS:
   empty(nil()) -> true()
   empty(cons(x,l)) -> false()
   head(cons(x,l)) -> x
   tail(nil()) -> nil()
   tail(cons(x,l)) -> l
   rev(nil()) -> nil()
   rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
   last(x,l) -> if(empty(l),x,l)
   if(true(),x,l) -> x
   if(false(),x,l) -> last(head(l),tail(l))
   rev2(x,nil()) -> nil()
   rev2(x,cons(y,l)) -> rev(cons(x,rev2(y,l)))
  Usable Rule Processor:
   DPs:
    rev#(cons(x,l)) -> rev2#(x,l)
    last#(x,l) -> empty#(l)
    last#(x,l) -> if#(empty(l),x,l)
    if#(false(),x,l) -> tail#(l)
    if#(false(),x,l) -> head#(l)
    if#(false(),x,l) -> last#(head(l),tail(l))
    rev2#(x,cons(y,l)) -> rev2#(y,l)
    rev2#(x,cons(y,l)) -> rev#(cons(x,rev2(y,l)))
   TRS:
    empty(nil()) -> true()
    empty(cons(x,l)) -> false()
    tail(nil()) -> nil()
    tail(cons(x,l)) -> l
    head(cons(x,l)) -> x
    rev2(x,nil()) -> nil()
    rev2(x,cons(y,l)) -> rev(cons(x,rev2(y,l)))
    rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
   Matrix Interpretation Processor: dim=1
    
    usable rules:
     empty(nil()) -> true()
     empty(cons(x,l)) -> false()
     tail(nil()) -> nil()
     tail(cons(x,l)) -> l
     rev2(x,nil()) -> nil()
     rev2(x,cons(y,l)) -> rev(cons(x,rev2(y,l)))
     rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
    interpretation:
     [if#](x0, x1, x2) = x0 + 3/2x2 + 3,
     
     [last#](x0, x1) = 3x1 + 7/2,
     
     [rev2#](x0, x1) = 3x1,
     
     [rev#](x0) = x0,
     
     [tail#](x0) = 3/2x0,
     
     [head#](x0) = 0,
     
     [empty#](x0) = 0,
     
     [rev2](x0, x1) = x1,
     
     [rev1](x0, x1) = 0,
     
     [rev](x0) = x0,
     
     [tail](x0) = 1/2x0,
     
     [head](x0) = 5/2x0 + 2,
     
     [false] = 1,
     
     [cons](x0, x1) = 3x1 + 3,
     
     [true] = 0,
     
     [empty](x0) = 3/2x0,
     
     [nil] = 0
    orientation:
     rev#(cons(x,l)) = 3l + 3 >= 3l = rev2#(x,l)
     
     last#(x,l) = 3l + 7/2 >= 0 = empty#(l)
     
     last#(x,l) = 3l + 7/2 >= 3l + 3 = if#(empty(l),x,l)
     
     if#(false(),x,l) = 3/2l + 4 >= 3/2l = tail#(l)
     
     if#(false(),x,l) = 3/2l + 4 >= 0 = head#(l)
     
     if#(false(),x,l) = 3/2l + 4 >= 3/2l + 7/2 = last#(head(l),tail(l))
     
     rev2#(x,cons(y,l)) = 9l + 9 >= 3l = rev2#(y,l)
     
     rev2#(x,cons(y,l)) = 9l + 9 >= 3l + 3 = rev#(cons(x,rev2(y,l)))
     
     empty(nil()) = 0 >= 0 = true()
     
     empty(cons(x,l)) = 9/2l + 9/2 >= 1 = false()
     
     tail(nil()) = 0 >= 0 = nil()
     
     tail(cons(x,l)) = 3/2l + 3/2 >= l = l
     
     head(cons(x,l)) = 15/2l + 19/2 >= x = x
     
     rev2(x,nil()) = 0 >= 0 = nil()
     
     rev2(x,cons(y,l)) = 3l + 3 >= 3l + 3 = rev(cons(x,rev2(y,l)))
     
     rev(cons(x,l)) = 3l + 3 >= 3l + 3 = cons(rev1(x,l),rev2(x,l))
    problem:
     DPs:
      
     TRS:
      empty(nil()) -> true()
      empty(cons(x,l)) -> false()
      tail(nil()) -> nil()
      tail(cons(x,l)) -> l
      head(cons(x,l)) -> x
      rev2(x,nil()) -> nil()
      rev2(x,cons(y,l)) -> rev(cons(x,rev2(y,l)))
      rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
    Qed