MAYBE
Time: 0.007534
TRS:
 { cond(true(), n, l) -> l,
  cond(false(), n, l) -> tail nthtail(s n, l),
           ge(u, 0()) -> true(),
         ge(s u, s v) -> ge(u, v),
         ge(0(), s v) -> false(),
         length nil() -> 0(),
    length cons(x, l) -> s length l,
        nthtail(n, l) -> cond(ge(n, length l), n, l),
           tail nil() -> nil(),
      tail cons(x, l) -> l}
 DP:
  DP:
   {cond#(false(), n, l) -> nthtail#(s n, l),
    cond#(false(), n, l) -> tail# nthtail(s n, l),
           ge#(s u, s v) -> ge#(u, v),
      length# cons(x, l) -> length# l,
          nthtail#(n, l) -> cond#(ge(n, length l), n, l),
          nthtail#(n, l) -> ge#(n, length l),
          nthtail#(n, l) -> length# l}
  TRS:
  { cond(true(), n, l) -> l,
   cond(false(), n, l) -> tail nthtail(s n, l),
            ge(u, 0()) -> true(),
          ge(s u, s v) -> ge(u, v),
          ge(0(), s v) -> false(),
          length nil() -> 0(),
     length cons(x, l) -> s length l,
         nthtail(n, l) -> cond(ge(n, length l), n, l),
            tail nil() -> nil(),
       tail cons(x, l) -> l}
  EDG:
   {(nthtail#(n, l) -> ge#(n, length l), ge#(s u, s v) -> ge#(u, v))
    (nthtail#(n, l) -> cond#(ge(n, length l), n, l), cond#(false(), n, l) -> tail# nthtail(s n, l))
    (nthtail#(n, l) -> cond#(ge(n, length l), n, l), cond#(false(), n, l) -> nthtail#(s n, l))
    (nthtail#(n, l) -> length# l, length# cons(x, l) -> length# l)
    (length# cons(x, l) -> length# l, length# cons(x, l) -> length# l)
    (ge#(s u, s v) -> ge#(u, v), ge#(s u, s v) -> ge#(u, v))
    (cond#(false(), n, l) -> nthtail#(s n, l), nthtail#(n, l) -> cond#(ge(n, length l), n, l))
    (cond#(false(), n, l) -> nthtail#(s n, l), nthtail#(n, l) -> ge#(n, length l))
    (cond#(false(), n, l) -> nthtail#(s n, l), nthtail#(n, l) -> length# l)}
   STATUS:
    arrows: 0.816327
    SCCS (3):
     Scc:
      {cond#(false(), n, l) -> nthtail#(s n, l),
             nthtail#(n, l) -> cond#(ge(n, length l), n, l)}
     Scc:
      {length# cons(x, l) -> length# l}
     Scc:
      {ge#(s u, s v) -> ge#(u, v)}
     
     SCC (2):
      Strict:
       {cond#(false(), n, l) -> nthtail#(s n, l),
              nthtail#(n, l) -> cond#(ge(n, length l), n, l)}
      Weak:
      { cond(true(), n, l) -> l,
       cond(false(), n, l) -> tail nthtail(s n, l),
                ge(u, 0()) -> true(),
              ge(s u, s v) -> ge(u, v),
              ge(0(), s v) -> false(),
              length nil() -> 0(),
         length cons(x, l) -> s length l,
             nthtail(n, l) -> cond(ge(n, length l), n, l),
                tail nil() -> nil(),
           tail cons(x, l) -> l}
      Open
     
     SCC (1):
      Strict:
       {length# cons(x, l) -> length# l}
      Weak:
      { cond(true(), n, l) -> l,
       cond(false(), n, l) -> tail nthtail(s n, l),
                ge(u, 0()) -> true(),
              ge(s u, s v) -> ge(u, v),
              ge(0(), s v) -> false(),
              length nil() -> 0(),
         length cons(x, l) -> s length l,
             nthtail(n, l) -> cond(ge(n, length l), n, l),
                tail nil() -> nil(),
           tail cons(x, l) -> l}
      Open
     
     SCC (1):
      Strict:
       {ge#(s u, s v) -> ge#(u, v)}
      Weak:
      { cond(true(), n, l) -> l,
       cond(false(), n, l) -> tail nthtail(s n, l),
                ge(u, 0()) -> true(),
              ge(s u, s v) -> ge(u, v),
              ge(0(), s v) -> false(),
              length nil() -> 0(),
         length cons(x, l) -> s length l,
             nthtail(n, l) -> cond(ge(n, length l), n, l),
                tail nil() -> nil(),
           tail cons(x, l) -> l}
      Open