MAYBE
Time: 0.001170
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))}
       Open
      
      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))}
       Open