MAYBE
Time: 0.007995
TRS:
 {        empty nil() -> true(),
     empty cons(x, l) -> false(),
      head cons(x, l) -> x,
           tail nil() -> nil(),
      tail cons(x, l) -> l,
            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, rev2(y, l)),
     if(true(), x, l) -> x,
    if(false(), x, l) -> last(head l, tail l),
           last(x, l) -> if(empty l, x, l)}
 DP:
  DP:
   {     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),
      if#(false(), x, l) -> head# l,
      if#(false(), x, l) -> tail# l,
      if#(false(), x, l) -> last#(head l, tail l),
             last#(x, l) -> empty# l,
             last#(x, l) -> if#(empty l, x, l)}
  TRS:
  {        empty nil() -> true(),
      empty cons(x, l) -> false(),
       head cons(x, l) -> x,
            tail nil() -> nil(),
       tail cons(x, l) -> l,
             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, rev2(y, l)),
      if(true(), x, l) -> x,
     if(false(), x, l) -> last(head l, tail l),
            last(x, l) -> if(empty l, x, 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)) -> rev# cons(x, rev2(y, l)), rev# cons(x, l) -> rev2#(x, l))
    (if#(false(), x, l) -> last#(head l, tail l), last#(x, l) -> empty# l)
    (if#(false(), x, l) -> last#(head l, tail l), last#(x, l) -> if#(empty l, x, 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))
    (last#(x, l) -> if#(empty l, x, l), if#(false(), x, l) -> head# l)
    (last#(x, l) -> if#(empty l, x, l), if#(false(), x, l) -> tail# l)
    (last#(x, l) -> if#(empty l, x, l), if#(false(), x, l) -> last#(head l, tail l))}
   STATUS:
    arrows: 0.843750
    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:
      {if#(false(), x, l) -> last#(head l, tail l),
              last#(x, l) -> if#(empty l, x, 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:
      {        empty nil() -> true(),
          empty cons(x, l) -> false(),
           head cons(x, l) -> x,
                tail nil() -> nil(),
           tail cons(x, l) -> l,
                 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, rev2(y, l)),
          if(true(), x, l) -> x,
         if(false(), x, l) -> last(head l, tail l),
                last(x, l) -> if(empty l, x, l)}
      Open
     SCC (2):
      Strict:
       {if#(false(), x, l) -> last#(head l, tail l),
               last#(x, l) -> if#(empty l, x, l)}
      Weak:
      {        empty nil() -> true(),
          empty cons(x, l) -> false(),
           head cons(x, l) -> x,
                tail nil() -> nil(),
           tail cons(x, l) -> l,
                 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, rev2(y, l)),
          if(true(), x, l) -> x,
         if(false(), x, l) -> last(head l, tail l),
                last(x, l) -> if(empty l, x, l)}
      Open