YES
Time: 0.057259
TRS:
 {          rev nil() -> nil(),
       rev cons(x, l) -> cons(rev1(x, l), rev2(x, l)),
  rev1(x, cons(y, l)) -> rev1(y, l),
     rev1(0(), nil()) -> 0(),
     rev1(s x, nil()) -> s x,
       rev2(x, nil()) -> nil(),
  rev2(x, cons(y, l)) -> rev cons(x, rev2(y, l))}
 DP:
  DP:
   {     rev# cons(x, l) -> rev1#(x, l),
         rev# cons(x, l) -> rev2#(x, l),
    rev1#(x, cons(y, l)) -> rev1#(y, l),
    rev2#(x, cons(y, l)) -> rev# cons(x, rev2(y, l)),
    rev2#(x, cons(y, l)) -> rev2#(y, l)}
  TRS:
  {          rev nil() -> nil(),
        rev cons(x, l) -> cons(rev1(x, l), rev2(x, l)),
   rev1(x, cons(y, l)) -> rev1(y, l),
      rev1(0(), nil()) -> 0(),
      rev1(s x, nil()) -> s x,
        rev2(x, nil()) -> nil(),
   rev2(x, cons(y, l)) -> rev cons(x, rev2(y, l))}
  UR:
   {     rev cons(x, l) -> cons(rev1(x, l), rev2(x, l)),
    rev1(x, cons(y, l)) -> rev1(y, l),
       rev1(0(), nil()) -> 0(),
       rev1(s x, nil()) -> s x,
         rev2(x, nil()) -> nil(),
    rev2(x, cons(y, l)) -> rev cons(x, rev2(y, l)),
                a(z, w) -> z,
                a(z, w) -> w}
   EDG:
    {(rev# cons(x, l) -> rev2#(x, l), rev2#(x, cons(y, l)) -> rev2#(y, l))
     (rev# cons(x, l) -> rev2#(x, 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)) -> rev2#(y, l), rev2#(x, cons(y, l)) -> rev# cons(x, 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))
     (rev1#(x, cons(y, l)) -> rev1#(y, l), rev1#(x, cons(y, l)) -> rev1#(y, l))
     (rev# cons(x, l) -> rev1#(x, l), rev1#(x, cons(y, l)) -> rev1#(y, l))}
    STATUS:
     arrows: 0.680000
     SCCS (2):
      Scc:
       {     rev# cons(x, l) -> rev2#(x, l),
        rev2#(x, cons(y, l)) -> rev# cons(x, rev2(y, l)),
        rev2#(x, cons(y, l)) -> rev2#(y, l)}
      Scc:
       {rev1#(x, cons(y, l)) -> rev1#(y, l)}
      
      SCC (3):
       Strict:
        {     rev# cons(x, l) -> rev2#(x, l),
         rev2#(x, cons(y, l)) -> rev# cons(x, rev2(y, l)),
         rev2#(x, cons(y, l)) -> rev2#(y, l)}
       Weak:
       {          rev nil() -> nil(),
             rev cons(x, l) -> cons(rev1(x, l), rev2(x, l)),
        rev1(x, cons(y, l)) -> rev1(y, l),
           rev1(0(), nil()) -> 0(),
           rev1(s x, nil()) -> s x,
             rev2(x, nil()) -> nil(),
        rev2(x, cons(y, l)) -> rev cons(x, rev2(y, l))}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [cons](x0, x1) = x0 + 1,
         
         [rev1](x0, x1) = x0 + 1,
         
         [rev2](x0, x1) = x0,
         
         [rev](x0) = x0,
         
         [s](x0) = 0,
         
         [nil] = 1,
         
         [0] = 0,
         
         [rev2#](x0, x1) = x0 + 1,
         
         [rev#](x0) = x0 + 1
        Strict:
         rev2#(x, cons(y, l)) -> rev2#(y, l)
         2 + 0x + 1l + 0y >= 1 + 1l + 0y
         rev2#(x, cons(y, l)) -> rev# cons(x, rev2(y, l))
         2 + 0x + 1l + 0y >= 2 + 0x + 1l + 0y
         rev# cons(x, l) -> rev2#(x, l)
         2 + 0x + 1l >= 1 + 0x + 1l
        Weak:
         rev2(x, cons(y, l)) -> rev cons(x, rev2(y, l))
         1 + 0x + 1l + 0y >= 1 + 0x + 1l + 0y
         rev2(x, nil()) -> nil()
         1 + 0x >= 1
         rev1(s x, nil()) -> s x
         2 + 0x >= 0 + 0x
         rev1(0(), nil()) -> 0()
         2 >= 0
         rev1(x, cons(y, l)) -> rev1(y, l)
         2 + 0x + 1l + 0y >= 1 + 1l + 0y
         rev cons(x, l) -> cons(rev1(x, l), rev2(x, l))
         1 + 0x + 1l >= 1 + 0x + 1l
         rev nil() -> nil()
         1 >= 1
       SCCS (0):
        
        
     
     SCC (1):
      Strict:
       {rev1#(x, cons(y, l)) -> rev1#(y, l)}
      Weak:
      {          rev nil() -> nil(),
            rev cons(x, l) -> cons(rev1(x, l), rev2(x, l)),
       rev1(x, cons(y, l)) -> rev1(y, l),
          rev1(0(), nil()) -> 0(),
          rev1(s x, nil()) -> s x,
            rev2(x, nil()) -> nil(),
       rev2(x, cons(y, l)) -> rev cons(x, rev2(y, l))}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [cons](x0, x1) = x0 + x1 + 1,
        
        [rev1](x0, x1) = x0 + x1,
        
        [rev2](x0, x1) = x0 + x1,
        
        [rev](x0) = x0 + 1,
        
        [s](x0) = 1,
        
        [nil] = 1,
        
        [0] = 1,
        
        [rev1#](x0, x1) = x0 + 1
       Strict:
        rev1#(x, cons(y, l)) -> rev1#(y, l)
        2 + 0x + 1l + 1y >= 1 + 1l + 0y
       Weak:
        rev2(x, cons(y, l)) -> rev cons(x, rev2(y, l))
        1 + 1x + 1l + 1y >= 2 + 1x + 1l + 1y
        rev2(x, nil()) -> nil()
        1 + 1x >= 1
        rev1(s x, nil()) -> s x
        2 + 0x >= 1 + 0x
        rev1(0(), nil()) -> 0()
        2 >= 1
        rev1(x, cons(y, l)) -> rev1(y, l)
        1 + 1x + 1l + 1y >= 0 + 1l + 1y
        rev cons(x, l) -> cons(rev1(x, l), rev2(x, l))
        2 + 1x + 1l >= 1 + 2x + 2l
        rev nil() -> nil()
        2 >= 1
      Qed