MAYBE
Time: 0.067462
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}
  UR:
   { 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,
                a(y, z) -> y,
                a(y, z) -> z}
   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)}
    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)}
     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)}
      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}
          Fail
         
         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}
          POLY:
           Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
           Interpretation:
            [cond](x0, x1, x2) = 0,
            
            [ge](x0, x1) = x0 + 1,
            
            [nthtail](x0, x1) = x0 + 1,
            
            [cons](x0, x1) = x0 + 1,
            
            [length](x0) = x0 + 1,
            
            [tail](x0) = x0,
            
            [s](x0) = 1,
            
            [true] = 0,
            
            [false] = 0,
            
            [nil] = 1,
            
            [0] = 1,
            
            [length#](x0) = x0
           Strict:
            length# cons(x, l) -> length# l
            1 + 1l + 0x >= 0 + 1l
           Weak:
            tail cons(x, l) -> l
            1 + 1l + 0x >= 1l
            tail nil() -> nil()
            1 >= 1
            nthtail(n, l) -> cond(ge(n, length l), n, l)
            1 + 1n + 0l >= 0 + 0n + 0l
            length cons(x, l) -> s length l
            2 + 1l + 0x >= 1 + 0l
            length nil() -> 0()
            2 >= 1
            ge(0(), s v) -> false()
            2 + 0v >= 0
            ge(s u, s v) -> ge(u, v)
            2 + 0u + 0v >= 1 + 0u + 1v
            ge(u, 0()) -> true()
            2 + 0u >= 0
            cond(false(), n, l) -> tail nthtail(s n, l)
            0 + 0n + 0l >= 2 + 0n + 0l
            cond(true(), n, l) -> l
            0 + 0n + 0l >= 1l
          Qed
        
        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}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [cond](x0, x1, x2) = x0 + x1 + x2 + 1,
           
           [ge](x0, x1) = x0 + x1,
           
           [nthtail](x0, x1) = x0 + 1,
           
           [cons](x0, x1) = 0,
           
           [length](x0) = x0 + 1,
           
           [tail](x0) = x0,
           
           [s](x0) = x0 + 1,
           
           [true] = 1,
           
           [false] = 1,
           
           [nil] = 1,
           
           [0] = 0,
           
           [ge#](x0, x1) = x0
          Strict:
           ge#(s u, s v) -> ge#(u, v)
           1 + 0u + 1v >= 0 + 0u + 1v
          Weak:
           tail cons(x, l) -> l
           0 + 0l + 0x >= 1l
           tail nil() -> nil()
           1 >= 1
           nthtail(n, l) -> cond(ge(n, length l), n, l)
           1 + 1n + 0l >= 2 + 2n + 2l
           length cons(x, l) -> s length l
           1 + 0l + 0x >= 2 + 1l
           length nil() -> 0()
           2 >= 0
           ge(0(), s v) -> false()
           1 + 1v >= 1
           ge(s u, s v) -> ge(u, v)
           2 + 1u + 1v >= 0 + 1u + 1v
           ge(u, 0()) -> true()
           0 + 1u >= 1
           cond(false(), n, l) -> tail nthtail(s n, l)
           2 + 1n + 1l >= 2 + 1n + 0l
           cond(true(), n, l) -> l
           2 + 1n + 1l >= 1l
         Qed