MAYBE
Time: 0.093531
TRS:
 {rev1(X, cons(Y, L)) -> rev1(Y, L),
     rev1(0(), nil()) -> 0(),
     rev1(s X, nil()) -> s X,
            rev nil() -> nil(),
       rev cons(X, L) -> cons(rev1(X, L), rev2(X, L)),
       rev2(X, nil()) -> nil(),
  rev2(X, cons(Y, L)) -> rev cons(X, rev rev2(Y, L))}
 DP:
  DP:
   {rev1#(X, cons(Y, L)) -> rev1#(Y, L),
         rev# cons(X, L) -> rev1#(X, L),
         rev# cons(X, L) -> rev2#(X, L),
    rev2#(X, cons(Y, L)) -> rev# cons(X, rev rev2(Y, L)),
    rev2#(X, cons(Y, L)) -> rev# rev2(Y, L),
    rev2#(X, cons(Y, L)) -> rev2#(Y, L)}
  TRS:
  {rev1(X, cons(Y, L)) -> rev1(Y, L),
      rev1(0(), nil()) -> 0(),
      rev1(s X, nil()) -> s X,
             rev nil() -> nil(),
        rev cons(X, L) -> cons(rev1(X, L), rev2(X, L)),
        rev2(X, nil()) -> nil(),
   rev2(X, cons(Y, L)) -> rev cons(X, rev rev2(Y, L))}
  UR:
   {rev1(X, cons(Y, L)) -> rev1(Y, L),
       rev1(0(), nil()) -> 0(),
       rev1(s X, nil()) -> s X,
              rev nil() -> nil(),
         rev cons(X, L) -> cons(rev1(X, L), rev2(X, L)),
         rev2(X, nil()) -> nil(),
    rev2(X, cons(Y, L)) -> rev cons(X, rev rev2(Y, L)),
                a(x, y) -> x,
                a(x, y) -> y}
   EDG:
    {(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)) -> rev2#(Y, L))
     (rev2#(X, cons(Y, L)) -> rev2#(Y, L), rev2#(X, cons(Y, L)) -> rev# rev2(Y, L))
     (rev2#(X, cons(Y, L)) -> rev2#(Y, L), rev2#(X, cons(Y, L)) -> rev# cons(X, rev rev2(Y, L)))
     (rev2#(X, cons(Y, L)) -> rev# rev2(Y, L), rev# cons(X, L) -> rev2#(X, L))
     (rev2#(X, cons(Y, L)) -> rev# rev2(Y, L), rev# cons(X, L) -> rev1#(X, L))
     (rev2#(X, cons(Y, L)) -> rev# cons(X, rev rev2(Y, L)), rev# cons(X, L) -> rev1#(X, L))
     (rev2#(X, cons(Y, L)) -> rev# cons(X, rev rev2(Y, L)), rev# cons(X, L) -> rev2#(X, L))
     (rev# cons(X, L) -> rev2#(X, L), rev2#(X, cons(Y, L)) -> rev# cons(X, rev rev2(Y, L)))
     (rev# cons(X, L) -> rev2#(X, L), rev2#(X, cons(Y, L)) -> rev# rev2(Y, L))
     (rev# cons(X, L) -> rev2#(X, L), rev2#(X, cons(Y, L)) -> rev2#(Y, L))
     (rev1#(X, cons(Y, L)) -> rev1#(Y, L), rev1#(X, cons(Y, L)) -> rev1#(Y, L))}
    STATUS:
     arrows: 0.666667
     SCCS (2):
      Scc:
       {     rev# cons(X, L) -> rev2#(X, L),
        rev2#(X, cons(Y, L)) -> rev# cons(X, rev rev2(Y, L)),
        rev2#(X, cons(Y, L)) -> rev# rev2(Y, L),
        rev2#(X, cons(Y, L)) -> rev2#(Y, L)}
      Scc:
       {rev1#(X, cons(Y, L)) -> rev1#(Y, L)}
      
      SCC (4):
       Strict:
        {     rev# cons(X, L) -> rev2#(X, L),
         rev2#(X, cons(Y, L)) -> rev# cons(X, rev rev2(Y, L)),
         rev2#(X, cons(Y, L)) -> rev# rev2(Y, L),
         rev2#(X, cons(Y, L)) -> rev2#(Y, L)}
       Weak:
       {rev1(X, cons(Y, L)) -> rev1(Y, L),
           rev1(0(), nil()) -> 0(),
           rev1(s X, nil()) -> s X,
                  rev nil() -> nil(),
             rev cons(X, L) -> cons(rev1(X, L), rev2(X, L)),
             rev2(X, nil()) -> nil(),
        rev2(X, cons(Y, L)) -> rev cons(X, rev rev2(Y, L))}
       Open
      
      SCC (1):
       Strict:
        {rev1#(X, cons(Y, L)) -> rev1#(Y, L)}
       Weak:
       {rev1(X, cons(Y, L)) -> rev1(Y, L),
           rev1(0(), nil()) -> 0(),
           rev1(s X, nil()) -> s X,
                  rev nil() -> nil(),
             rev cons(X, L) -> cons(rev1(X, L), rev2(X, L)),
             rev2(X, nil()) -> nil(),
        rev2(X, cons(Y, L)) -> rev cons(X, rev rev2(Y, L))}
       Open