YES
Time: 0.007811
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))}
  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))}
   SCCS (2):
    Scc:
     {rev1#(x, cons(y, l)) -> rev1#(y, l)}
    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 (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))}
     SPSC:
      Simple Projection:
       pi(rev1#) = 1
      Strict:
       {}
      Qed
    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:
       
     EDG:
      {}
      SCCS (0):
       
       Qed