MAYBE
Time: 0.003187
TRS:
 {                isEmpty nil() -> true(),
            isEmpty cons(x, xs) -> false(),
            last cons(x, nil()) -> x,
      last cons(x, cons(y, ys)) -> last cons(y, ys),
                 dropLast nil() -> nil(),
        dropLast cons(x, nil()) -> nil(),
  dropLast cons(x, cons(y, ys)) -> cons(x, dropLast cons(y, ys)),
              append(nil(), ys) -> ys,
        append(cons(x, xs), ys) -> cons(x, append(xs, ys)),
                    rev(xs, ys) -> if(isEmpty xs, dropLast xs, append(ys, last xs), ys),
                     reverse xs -> rev(xs, nil()),
         if(true(), xs, ys, zs) -> zs,
        if(false(), xs, ys, zs) -> rev(xs, ys)}
 DP:
  DP:
   {    last# cons(x, cons(y, ys)) -> last# cons(y, ys),
    dropLast# cons(x, cons(y, ys)) -> dropLast# cons(y, ys),
          append#(cons(x, xs), ys) -> append#(xs, ys),
                      rev#(xs, ys) -> isEmpty# xs,
                      rev#(xs, ys) -> last# xs,
                      rev#(xs, ys) -> dropLast# xs,
                      rev#(xs, ys) -> append#(ys, last xs),
                      rev#(xs, ys) -> if#(isEmpty xs, dropLast xs, append(ys, last xs), ys),
                       reverse# xs -> rev#(xs, nil()),
          if#(false(), xs, ys, zs) -> rev#(xs, ys)}
  TRS:
  {                isEmpty nil() -> true(),
             isEmpty cons(x, xs) -> false(),
             last cons(x, nil()) -> x,
       last cons(x, cons(y, ys)) -> last cons(y, ys),
                  dropLast nil() -> nil(),
         dropLast cons(x, nil()) -> nil(),
   dropLast cons(x, cons(y, ys)) -> cons(x, dropLast cons(y, ys)),
               append(nil(), ys) -> ys,
         append(cons(x, xs), ys) -> cons(x, append(xs, ys)),
                     rev(xs, ys) -> if(isEmpty xs, dropLast xs, append(ys, last xs), ys),
                      reverse xs -> rev(xs, nil()),
          if(true(), xs, ys, zs) -> zs,
         if(false(), xs, ys, zs) -> rev(xs, ys)}
  EDG:
   {(rev#(xs, ys) -> last# xs, last# cons(x, cons(y, ys)) -> last# cons(y, ys))
    (rev#(xs, ys) -> append#(ys, last xs), append#(cons(x, xs), ys) -> append#(xs, ys))
    (rev#(xs, ys) -> if#(isEmpty xs, dropLast xs, append(ys, last xs), ys), if#(false(), xs, ys, zs) -> rev#(xs, ys))
    (last# cons(x, cons(y, ys)) -> last# cons(y, ys), last# cons(x, cons(y, ys)) -> last# cons(y, ys))
    (reverse# xs -> rev#(xs, nil()), rev#(xs, ys) -> if#(isEmpty xs, dropLast xs, append(ys, last xs), ys))
    (reverse# xs -> rev#(xs, nil()), rev#(xs, ys) -> append#(ys, last xs))
    (reverse# xs -> rev#(xs, nil()), rev#(xs, ys) -> dropLast# xs)
    (reverse# xs -> rev#(xs, nil()), rev#(xs, ys) -> last# xs)
    (reverse# xs -> rev#(xs, nil()), rev#(xs, ys) -> isEmpty# xs)
    (dropLast# cons(x, cons(y, ys)) -> dropLast# cons(y, ys), dropLast# cons(x, cons(y, ys)) -> dropLast# cons(y, ys))
    (if#(false(), xs, ys, zs) -> rev#(xs, ys), rev#(xs, ys) -> isEmpty# xs)
    (if#(false(), xs, ys, zs) -> rev#(xs, ys), rev#(xs, ys) -> last# xs)
    (if#(false(), xs, ys, zs) -> rev#(xs, ys), rev#(xs, ys) -> dropLast# xs)
    (if#(false(), xs, ys, zs) -> rev#(xs, ys), rev#(xs, ys) -> append#(ys, last xs))
    (if#(false(), xs, ys, zs) -> rev#(xs, ys), rev#(xs, ys) -> if#(isEmpty xs, dropLast xs, append(ys, last xs), ys))
    (append#(cons(x, xs), ys) -> append#(xs, ys), append#(cons(x, xs), ys) -> append#(xs, ys))
    (rev#(xs, ys) -> dropLast# xs, dropLast# cons(x, cons(y, ys)) -> dropLast# cons(y, ys))}
   STATUS:
    arrows: 0.830000
    SCCS (4):
     Scc:
      {            rev#(xs, ys) -> if#(isEmpty xs, dropLast xs, append(ys, last xs), ys),
       if#(false(), xs, ys, zs) -> rev#(xs, ys)}
     Scc:
      {append#(cons(x, xs), ys) -> append#(xs, ys)}
     Scc:
      {dropLast# cons(x, cons(y, ys)) -> dropLast# cons(y, ys)}
     Scc:
      {last# cons(x, cons(y, ys)) -> last# cons(y, ys)}
     
     
     SCC (2):
      Strict:
       {            rev#(xs, ys) -> if#(isEmpty xs, dropLast xs, append(ys, last xs), ys),
        if#(false(), xs, ys, zs) -> rev#(xs, ys)}
      Weak:
      {                isEmpty nil() -> true(),
                 isEmpty cons(x, xs) -> false(),
                 last cons(x, nil()) -> x,
           last cons(x, cons(y, ys)) -> last cons(y, ys),
                      dropLast nil() -> nil(),
             dropLast cons(x, nil()) -> nil(),
       dropLast cons(x, cons(y, ys)) -> cons(x, dropLast cons(y, ys)),
                   append(nil(), ys) -> ys,
             append(cons(x, xs), ys) -> cons(x, append(xs, ys)),
                         rev(xs, ys) -> if(isEmpty xs, dropLast xs, append(ys, last xs), ys),
                          reverse xs -> rev(xs, nil()),
              if(true(), xs, ys, zs) -> zs,
             if(false(), xs, ys, zs) -> rev(xs, ys)}
      Open
     
     SCC (1):
      Strict:
       {append#(cons(x, xs), ys) -> append#(xs, ys)}
      Weak:
      {                isEmpty nil() -> true(),
                 isEmpty cons(x, xs) -> false(),
                 last cons(x, nil()) -> x,
           last cons(x, cons(y, ys)) -> last cons(y, ys),
                      dropLast nil() -> nil(),
             dropLast cons(x, nil()) -> nil(),
       dropLast cons(x, cons(y, ys)) -> cons(x, dropLast cons(y, ys)),
                   append(nil(), ys) -> ys,
             append(cons(x, xs), ys) -> cons(x, append(xs, ys)),
                         rev(xs, ys) -> if(isEmpty xs, dropLast xs, append(ys, last xs), ys),
                          reverse xs -> rev(xs, nil()),
              if(true(), xs, ys, zs) -> zs,
             if(false(), xs, ys, zs) -> rev(xs, ys)}
      Open
     
     SCC (1):
      Strict:
       {dropLast# cons(x, cons(y, ys)) -> dropLast# cons(y, ys)}
      Weak:
      {                isEmpty nil() -> true(),
                 isEmpty cons(x, xs) -> false(),
                 last cons(x, nil()) -> x,
           last cons(x, cons(y, ys)) -> last cons(y, ys),
                      dropLast nil() -> nil(),
             dropLast cons(x, nil()) -> nil(),
       dropLast cons(x, cons(y, ys)) -> cons(x, dropLast cons(y, ys)),
                   append(nil(), ys) -> ys,
             append(cons(x, xs), ys) -> cons(x, append(xs, ys)),
                         rev(xs, ys) -> if(isEmpty xs, dropLast xs, append(ys, last xs), ys),
                          reverse xs -> rev(xs, nil()),
              if(true(), xs, ys, zs) -> zs,
             if(false(), xs, ys, zs) -> rev(xs, ys)}
      Open
     
     SCC (1):
      Strict:
       {last# cons(x, cons(y, ys)) -> last# cons(y, ys)}
      Weak:
      {                isEmpty nil() -> true(),
                 isEmpty cons(x, xs) -> false(),
                 last cons(x, nil()) -> x,
           last cons(x, cons(y, ys)) -> last cons(y, ys),
                      dropLast nil() -> nil(),
             dropLast cons(x, nil()) -> nil(),
       dropLast cons(x, cons(y, ys)) -> cons(x, dropLast cons(y, ys)),
                   append(nil(), ys) -> ys,
             append(cons(x, xs), ys) -> cons(x, append(xs, ys)),
                         rev(xs, ys) -> if(isEmpty xs, dropLast xs, append(ys, last xs), ys),
                          reverse xs -> rev(xs, nil()),
              if(true(), xs, ys, zs) -> zs,
             if(false(), xs, ys, zs) -> rev(xs, ys)}
      Open