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)))
  TDG 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)))
   graph:
    rev1#(x,cons(y,l)) -> rev1#(y,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)))
    rev2#(x,cons(y,l)) -> rev2#(y,l) ->
    rev2#(x,cons(y,l)) -> rev2#(y,l)
    rev2#(x,cons(y,l)) -> rev#(cons(x,rev2(y,l))) ->
    rev#(cons(x,l)) -> rev1#(x,l)
    rev2#(x,cons(y,l)) -> rev#(cons(x,rev2(y,l))) ->
    rev#(cons(x,l)) -> rev2#(x,l)
    rev#(cons(x,l)) -> rev1#(x,l) -> rev1#(x,cons(y,l)) -> rev1#(y,l)
    rev#(cons(x,l)) -> rev2#(x,l) ->
    rev2#(x,cons(y,l)) -> rev#(cons(x,rev2(y,l)))
    rev#(cons(x,l)) -> rev2#(x,l) -> rev2#(x,cons(y,l)) -> rev2#(y,l)
   SCC Processor:
    #sccs: 2
    #rules: 4
    #arcs: 8/25
    DPs:
     rev2#(x,cons(y,l)) -> rev2#(y,l)
     rev2#(x,cons(y,l)) -> rev#(cons(x,rev2(y,l)))
     rev#(cons(x,l)) -> rev2#(x,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:
      rev2#(x,cons(y,l)) -> rev2#(y,l)
      rev2#(x,cons(y,l)) -> rev#(cons(x,rev2(y,l)))
      rev#(cons(x,l)) -> rev2#(x,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)
     Arctic Interpretation Processor:
      dimension: 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:
       [rev2#](x0, x1) = x1,
       
       [rev#](x0) = x0 + 0,
       
       [s](x0) = 1x0 + 1,
       
       [0] = 6,
       
       [rev2](x0, x1) = x1,
       
       [rev1](x0, x1) = x0 + x1 + 0,
       
       [cons](x0, x1) = 4x1 + 0,
       
       [rev](x0) = x0 + 0,
       
       [nil] = 5
      orientation:
       rev2#(x,cons(y,l)) = 4l + 0 >= l = rev2#(y,l)
       
       rev2#(x,cons(y,l)) = 4l + 0 >= 4l + 0 = rev#(cons(x,rev2(y,l)))
       
       rev#(cons(x,l)) = 4l + 0 >= l = rev2#(x,l)
       
       rev2(x,nil()) = 5 >= 5 = nil()
       
       rev2(x,cons(y,l)) = 4l + 0 >= 4l + 0 = rev(cons(x,rev2(y,l)))
       
       rev(cons(x,l)) = 4l + 0 >= 4l + 0 = cons(rev1(x,l),rev2(x,l))
       
       rev1(0(),nil()) = 6 >= 6 = 0()
       
       rev1(s(x),nil()) = 1x + 5 >= 1x + 1 = s(x)
       
       rev1(x,cons(y,l)) = 4l + x + 0 >= l + y + 0 = rev1(y,l)
      problem:
       DPs:
        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)
      Restore Modifier:
       DPs:
        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)))
       SCC Processor:
        #sccs: 0
        #rules: 0
        #arcs: 5/1
        
    
    DPs:
     rev1#(x,cons(y,l)) -> rev1#(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)))
    Subterm Criterion Processor:
     simple projection:
      pi(rev1#) = 1
     problem:
      DPs:
       
      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)))
     Qed