YES

Problem:
 rev(nil()) -> nil()
 rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
 rev1(0(),nil()) -> 0()
 rev1(s(x),nil()) -> s(x)
 rev1(x,cons(y,l)) -> rev1(y,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)
   rev#(cons(x,l)) -> rev1#(x,l)
   rev1#(x,cons(y,l)) -> rev1#(y,l)
   rev2#(x,cons(y,l)) -> rev2#(y,l)
   rev2#(x,cons(y,l)) -> rev#(cons(x,rev2(y,l)))
  TRS:
   rev(nil()) -> nil()
   rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
   rev1(0(),nil()) -> 0()
   rev1(s(x),nil()) -> s(x)
   rev1(x,cons(y,l)) -> rev1(y,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)
    rev#(cons(x,l)) -> rev1#(x,l)
    rev1#(x,cons(y,l)) -> rev1#(y,l)
    rev2#(x,cons(y,l)) -> rev2#(y,l)
    rev2#(x,cons(y,l)) -> rev#(cons(x,rev2(y,l)))
   TRS:
    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))
    rev1(0(),nil()) -> 0()
    rev1(s(x),nil()) -> s(x)
    rev1(x,cons(y,l)) -> rev1(y,l)
   Matrix Interpretation Processor: dim=1
    
    usable rules:
     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:
     [rev1#](x0, x1) = x1,
     
     [rev2#](x0, x1) = 2x1,
     
     [rev#](x0) = x0,
     
     [s](x0) = 2x0 + 3,
     
     [0] = 1,
     
     [rev2](x0, x1) = x1,
     
     [rev1](x0, x1) = 5x0 + 1,
     
     [cons](x0, x1) = 2x1 + 1,
     
     [rev](x0) = x0,
     
     [nil] = 3
    orientation:
     rev#(cons(x,l)) = 2l + 1 >= 2l = rev2#(x,l)
     
     rev#(cons(x,l)) = 2l + 1 >= l = rev1#(x,l)
     
     rev1#(x,cons(y,l)) = 2l + 1 >= l = rev1#(y,l)
     
     rev2#(x,cons(y,l)) = 4l + 2 >= 2l = rev2#(y,l)
     
     rev2#(x,cons(y,l)) = 4l + 2 >= 2l + 1 = rev#(cons(x,rev2(y,l)))
     
     rev2(x,nil()) = 3 >= 3 = nil()
     
     rev2(x,cons(y,l)) = 2l + 1 >= 2l + 1 = rev(cons(x,rev2(y,l)))
     
     rev(cons(x,l)) = 2l + 1 >= 2l + 1 = cons(rev1(x,l),rev2(x,l))
     
     rev1(0(),nil()) = 6 >= 1 = 0()
     
     rev1(s(x),nil()) = 10x + 16 >= 2x + 3 = s(x)
     
     rev1(x,cons(y,l)) = 5x + 1 >= 5y + 1 = rev1(y,l)
    problem:
     DPs:
      
     TRS:
      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))
      rev1(0(),nil()) -> 0()
      rev1(s(x),nil()) -> s(x)
      rev1(x,cons(y,l)) -> rev1(y,l)
    Qed