MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { and(tt(), T) -> T
  , isNatIList(IL) -> isNatList(activate(IL))
  , isNatIList(n__zeros()) -> tt()
  , isNatIList(n__cons(N, IL)) ->
    and(isNat(activate(N)), isNatIList(activate(IL)))
  , isNatList(n__cons(N, L)) ->
    and(isNat(activate(N)), isNatList(activate(L)))
  , isNatList(n__nil()) -> tt()
  , isNatList(n__take(N, IL)) ->
    and(isNat(activate(N)), isNatIList(activate(IL)))
  , activate(X) -> X
  , activate(n__0()) -> 0()
  , activate(n__s(X)) -> s(X)
  , activate(n__length(X)) -> length(X)
  , activate(n__zeros()) -> zeros()
  , activate(n__cons(X1, X2)) -> cons(X1, X2)
  , activate(n__nil()) -> nil()
  , activate(n__take(X1, X2)) -> take(X1, X2)
  , isNat(n__0()) -> tt()
  , isNat(n__s(N)) -> isNat(activate(N))
  , isNat(n__length(L)) -> isNatList(activate(L))
  , zeros() -> n__zeros()
  , zeros() -> cons(0(), n__zeros())
  , cons(X1, X2) -> n__cons(X1, X2)
  , 0() -> n__0()
  , take(X1, X2) -> n__take(X1, X2)
  , take(0(), IL) -> uTake1(isNatIList(IL))
  , take(s(M), cons(N, IL)) ->
    uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))),
           M,
           N,
           activate(IL))
  , uTake1(tt()) -> nil()
  , nil() -> n__nil()
  , s(X) -> n__s(X)
  , uTake2(tt(), M, N, IL) ->
    cons(activate(N), n__take(activate(M), activate(IL)))
  , length(X) -> n__length(X)
  , length(cons(N, L)) ->
    uLength(and(isNat(N), isNatList(activate(L))), activate(L))
  , uLength(tt(), L) -> s(length(activate(L))) }
Obligation:
  runtime complexity
Answer:
  MAYBE

None of the processors succeeded.

Details of failed attempt(s):
-----------------------------
1) 'WithProblem (timeout of 60 seconds)' failed due to the
   following reason:
   
   Computation stopped due to timeout after 60.0 seconds.

2) 'Best' failed due to the following reason:
   
   None of the processors succeeded.
   
   Details of failed attempt(s):
   -----------------------------
   1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)'
      failed due to the following reason:
      
      Computation stopped due to timeout after 30.0 seconds.
   
   2) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed
      due to the following reason:
      
      None of the processors succeeded.
      
      Details of failed attempt(s):
      -----------------------------
      1) 'Bounds with minimal-enrichment and initial automaton 'match''
         failed due to the following reason:
         
         match-boundness of the problem could not be verified.
      
      2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
         failed due to the following reason:
         
         match-boundness of the problem could not be verified.
      
   
   3) 'Best' failed due to the following reason:
      
      None of the processors succeeded.
      
      Details of failed attempt(s):
      -----------------------------
      1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the
         following reason:
         
         The processor is inapplicable, reason:
           Processor only applicable for innermost runtime complexity analysis
      
      2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due
         to the following reason:
         
         The processor is inapplicable, reason:
           Processor only applicable for innermost runtime complexity analysis
      
   

3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed
   due to the following reason:
   
   We add the following weak dependency pairs:
   
   Strict DPs:
     { and^#(tt(), T) -> c_1(T)
     , isNatIList^#(IL) -> c_2(isNatList^#(activate(IL)))
     , isNatIList^#(n__zeros()) -> c_3()
     , isNatIList^#(n__cons(N, IL)) ->
       c_4(and^#(isNat(activate(N)), isNatIList(activate(IL))))
     , isNatList^#(n__cons(N, L)) ->
       c_5(and^#(isNat(activate(N)), isNatList(activate(L))))
     , isNatList^#(n__nil()) -> c_6()
     , isNatList^#(n__take(N, IL)) ->
       c_7(and^#(isNat(activate(N)), isNatIList(activate(IL))))
     , activate^#(X) -> c_8(X)
     , activate^#(n__0()) -> c_9(0^#())
     , activate^#(n__s(X)) -> c_10(s^#(X))
     , activate^#(n__length(X)) -> c_11(length^#(X))
     , activate^#(n__zeros()) -> c_12(zeros^#())
     , activate^#(n__cons(X1, X2)) -> c_13(cons^#(X1, X2))
     , activate^#(n__nil()) -> c_14(nil^#())
     , activate^#(n__take(X1, X2)) -> c_15(take^#(X1, X2))
     , 0^#() -> c_22()
     , s^#(X) -> c_28(X)
     , length^#(X) -> c_30(X)
     , length^#(cons(N, L)) ->
       c_31(uLength^#(and(isNat(N), isNatList(activate(L))), activate(L)))
     , zeros^#() -> c_19()
     , zeros^#() -> c_20(cons^#(0(), n__zeros()))
     , cons^#(X1, X2) -> c_21(X1, X2)
     , nil^#() -> c_27()
     , take^#(X1, X2) -> c_23(X1, X2)
     , take^#(0(), IL) -> c_24(uTake1^#(isNatIList(IL)))
     , take^#(s(M), cons(N, IL)) ->
       c_25(uTake2^#(and(isNat(M),
                         and(isNat(N), isNatIList(activate(IL)))),
                     M,
                     N,
                     activate(IL)))
     , isNat^#(n__0()) -> c_16()
     , isNat^#(n__s(N)) -> c_17(isNat^#(activate(N)))
     , isNat^#(n__length(L)) -> c_18(isNatList^#(activate(L)))
     , uTake1^#(tt()) -> c_26(nil^#())
     , uTake2^#(tt(), M, N, IL) ->
       c_29(cons^#(activate(N), n__take(activate(M), activate(IL))))
     , uLength^#(tt(), L) -> c_32(s^#(length(activate(L)))) }
   
   and mark the set of starting terms.
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { and^#(tt(), T) -> c_1(T)
     , isNatIList^#(IL) -> c_2(isNatList^#(activate(IL)))
     , isNatIList^#(n__zeros()) -> c_3()
     , isNatIList^#(n__cons(N, IL)) ->
       c_4(and^#(isNat(activate(N)), isNatIList(activate(IL))))
     , isNatList^#(n__cons(N, L)) ->
       c_5(and^#(isNat(activate(N)), isNatList(activate(L))))
     , isNatList^#(n__nil()) -> c_6()
     , isNatList^#(n__take(N, IL)) ->
       c_7(and^#(isNat(activate(N)), isNatIList(activate(IL))))
     , activate^#(X) -> c_8(X)
     , activate^#(n__0()) -> c_9(0^#())
     , activate^#(n__s(X)) -> c_10(s^#(X))
     , activate^#(n__length(X)) -> c_11(length^#(X))
     , activate^#(n__zeros()) -> c_12(zeros^#())
     , activate^#(n__cons(X1, X2)) -> c_13(cons^#(X1, X2))
     , activate^#(n__nil()) -> c_14(nil^#())
     , activate^#(n__take(X1, X2)) -> c_15(take^#(X1, X2))
     , 0^#() -> c_22()
     , s^#(X) -> c_28(X)
     , length^#(X) -> c_30(X)
     , length^#(cons(N, L)) ->
       c_31(uLength^#(and(isNat(N), isNatList(activate(L))), activate(L)))
     , zeros^#() -> c_19()
     , zeros^#() -> c_20(cons^#(0(), n__zeros()))
     , cons^#(X1, X2) -> c_21(X1, X2)
     , nil^#() -> c_27()
     , take^#(X1, X2) -> c_23(X1, X2)
     , take^#(0(), IL) -> c_24(uTake1^#(isNatIList(IL)))
     , take^#(s(M), cons(N, IL)) ->
       c_25(uTake2^#(and(isNat(M),
                         and(isNat(N), isNatIList(activate(IL)))),
                     M,
                     N,
                     activate(IL)))
     , isNat^#(n__0()) -> c_16()
     , isNat^#(n__s(N)) -> c_17(isNat^#(activate(N)))
     , isNat^#(n__length(L)) -> c_18(isNatList^#(activate(L)))
     , uTake1^#(tt()) -> c_26(nil^#())
     , uTake2^#(tt(), M, N, IL) ->
       c_29(cons^#(activate(N), n__take(activate(M), activate(IL))))
     , uLength^#(tt(), L) -> c_32(s^#(length(activate(L)))) }
   Strict Trs:
     { and(tt(), T) -> T
     , isNatIList(IL) -> isNatList(activate(IL))
     , isNatIList(n__zeros()) -> tt()
     , isNatIList(n__cons(N, IL)) ->
       and(isNat(activate(N)), isNatIList(activate(IL)))
     , isNatList(n__cons(N, L)) ->
       and(isNat(activate(N)), isNatList(activate(L)))
     , isNatList(n__nil()) -> tt()
     , isNatList(n__take(N, IL)) ->
       and(isNat(activate(N)), isNatIList(activate(IL)))
     , activate(X) -> X
     , activate(n__0()) -> 0()
     , activate(n__s(X)) -> s(X)
     , activate(n__length(X)) -> length(X)
     , activate(n__zeros()) -> zeros()
     , activate(n__cons(X1, X2)) -> cons(X1, X2)
     , activate(n__nil()) -> nil()
     , activate(n__take(X1, X2)) -> take(X1, X2)
     , isNat(n__0()) -> tt()
     , isNat(n__s(N)) -> isNat(activate(N))
     , isNat(n__length(L)) -> isNatList(activate(L))
     , zeros() -> n__zeros()
     , zeros() -> cons(0(), n__zeros())
     , cons(X1, X2) -> n__cons(X1, X2)
     , 0() -> n__0()
     , take(X1, X2) -> n__take(X1, X2)
     , take(0(), IL) -> uTake1(isNatIList(IL))
     , take(s(M), cons(N, IL)) ->
       uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))),
              M,
              N,
              activate(IL))
     , uTake1(tt()) -> nil()
     , nil() -> n__nil()
     , s(X) -> n__s(X)
     , uTake2(tt(), M, N, IL) ->
       cons(activate(N), n__take(activate(M), activate(IL)))
     , length(X) -> n__length(X)
     , length(cons(N, L)) ->
       uLength(and(isNat(N), isNatList(activate(L))), activate(L))
     , uLength(tt(), L) -> s(length(activate(L))) }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of {3,6,16,20,23,27} by
   applications of Pre({3,6,16,20,23,27}) =
   {1,2,8,9,12,14,17,18,22,24,28,29,30}. Here rules are labeled as
   follows:
   
     DPs:
       { 1: and^#(tt(), T) -> c_1(T)
       , 2: isNatIList^#(IL) -> c_2(isNatList^#(activate(IL)))
       , 3: isNatIList^#(n__zeros()) -> c_3()
       , 4: isNatIList^#(n__cons(N, IL)) ->
            c_4(and^#(isNat(activate(N)), isNatIList(activate(IL))))
       , 5: isNatList^#(n__cons(N, L)) ->
            c_5(and^#(isNat(activate(N)), isNatList(activate(L))))
       , 6: isNatList^#(n__nil()) -> c_6()
       , 7: isNatList^#(n__take(N, IL)) ->
            c_7(and^#(isNat(activate(N)), isNatIList(activate(IL))))
       , 8: activate^#(X) -> c_8(X)
       , 9: activate^#(n__0()) -> c_9(0^#())
       , 10: activate^#(n__s(X)) -> c_10(s^#(X))
       , 11: activate^#(n__length(X)) -> c_11(length^#(X))
       , 12: activate^#(n__zeros()) -> c_12(zeros^#())
       , 13: activate^#(n__cons(X1, X2)) -> c_13(cons^#(X1, X2))
       , 14: activate^#(n__nil()) -> c_14(nil^#())
       , 15: activate^#(n__take(X1, X2)) -> c_15(take^#(X1, X2))
       , 16: 0^#() -> c_22()
       , 17: s^#(X) -> c_28(X)
       , 18: length^#(X) -> c_30(X)
       , 19: length^#(cons(N, L)) ->
             c_31(uLength^#(and(isNat(N), isNatList(activate(L))), activate(L)))
       , 20: zeros^#() -> c_19()
       , 21: zeros^#() -> c_20(cons^#(0(), n__zeros()))
       , 22: cons^#(X1, X2) -> c_21(X1, X2)
       , 23: nil^#() -> c_27()
       , 24: take^#(X1, X2) -> c_23(X1, X2)
       , 25: take^#(0(), IL) -> c_24(uTake1^#(isNatIList(IL)))
       , 26: take^#(s(M), cons(N, IL)) ->
             c_25(uTake2^#(and(isNat(M),
                               and(isNat(N), isNatIList(activate(IL)))),
                           M,
                           N,
                           activate(IL)))
       , 27: isNat^#(n__0()) -> c_16()
       , 28: isNat^#(n__s(N)) -> c_17(isNat^#(activate(N)))
       , 29: isNat^#(n__length(L)) -> c_18(isNatList^#(activate(L)))
       , 30: uTake1^#(tt()) -> c_26(nil^#())
       , 31: uTake2^#(tt(), M, N, IL) ->
             c_29(cons^#(activate(N), n__take(activate(M), activate(IL))))
       , 32: uLength^#(tt(), L) -> c_32(s^#(length(activate(L)))) }
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { and^#(tt(), T) -> c_1(T)
     , isNatIList^#(IL) -> c_2(isNatList^#(activate(IL)))
     , isNatIList^#(n__cons(N, IL)) ->
       c_4(and^#(isNat(activate(N)), isNatIList(activate(IL))))
     , isNatList^#(n__cons(N, L)) ->
       c_5(and^#(isNat(activate(N)), isNatList(activate(L))))
     , isNatList^#(n__take(N, IL)) ->
       c_7(and^#(isNat(activate(N)), isNatIList(activate(IL))))
     , activate^#(X) -> c_8(X)
     , activate^#(n__0()) -> c_9(0^#())
     , activate^#(n__s(X)) -> c_10(s^#(X))
     , activate^#(n__length(X)) -> c_11(length^#(X))
     , activate^#(n__zeros()) -> c_12(zeros^#())
     , activate^#(n__cons(X1, X2)) -> c_13(cons^#(X1, X2))
     , activate^#(n__nil()) -> c_14(nil^#())
     , activate^#(n__take(X1, X2)) -> c_15(take^#(X1, X2))
     , s^#(X) -> c_28(X)
     , length^#(X) -> c_30(X)
     , length^#(cons(N, L)) ->
       c_31(uLength^#(and(isNat(N), isNatList(activate(L))), activate(L)))
     , zeros^#() -> c_20(cons^#(0(), n__zeros()))
     , cons^#(X1, X2) -> c_21(X1, X2)
     , take^#(X1, X2) -> c_23(X1, X2)
     , take^#(0(), IL) -> c_24(uTake1^#(isNatIList(IL)))
     , take^#(s(M), cons(N, IL)) ->
       c_25(uTake2^#(and(isNat(M),
                         and(isNat(N), isNatIList(activate(IL)))),
                     M,
                     N,
                     activate(IL)))
     , isNat^#(n__s(N)) -> c_17(isNat^#(activate(N)))
     , isNat^#(n__length(L)) -> c_18(isNatList^#(activate(L)))
     , uTake1^#(tt()) -> c_26(nil^#())
     , uTake2^#(tt(), M, N, IL) ->
       c_29(cons^#(activate(N), n__take(activate(M), activate(IL))))
     , uLength^#(tt(), L) -> c_32(s^#(length(activate(L)))) }
   Strict Trs:
     { and(tt(), T) -> T
     , isNatIList(IL) -> isNatList(activate(IL))
     , isNatIList(n__zeros()) -> tt()
     , isNatIList(n__cons(N, IL)) ->
       and(isNat(activate(N)), isNatIList(activate(IL)))
     , isNatList(n__cons(N, L)) ->
       and(isNat(activate(N)), isNatList(activate(L)))
     , isNatList(n__nil()) -> tt()
     , isNatList(n__take(N, IL)) ->
       and(isNat(activate(N)), isNatIList(activate(IL)))
     , activate(X) -> X
     , activate(n__0()) -> 0()
     , activate(n__s(X)) -> s(X)
     , activate(n__length(X)) -> length(X)
     , activate(n__zeros()) -> zeros()
     , activate(n__cons(X1, X2)) -> cons(X1, X2)
     , activate(n__nil()) -> nil()
     , activate(n__take(X1, X2)) -> take(X1, X2)
     , isNat(n__0()) -> tt()
     , isNat(n__s(N)) -> isNat(activate(N))
     , isNat(n__length(L)) -> isNatList(activate(L))
     , zeros() -> n__zeros()
     , zeros() -> cons(0(), n__zeros())
     , cons(X1, X2) -> n__cons(X1, X2)
     , 0() -> n__0()
     , take(X1, X2) -> n__take(X1, X2)
     , take(0(), IL) -> uTake1(isNatIList(IL))
     , take(s(M), cons(N, IL)) ->
       uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))),
              M,
              N,
              activate(IL))
     , uTake1(tt()) -> nil()
     , nil() -> n__nil()
     , s(X) -> n__s(X)
     , uTake2(tt(), M, N, IL) ->
       cons(activate(N), n__take(activate(M), activate(IL)))
     , length(X) -> n__length(X)
     , length(cons(N, L)) ->
       uLength(and(isNat(N), isNatList(activate(L))), activate(L))
     , uLength(tt(), L) -> s(length(activate(L))) }
   Weak DPs:
     { isNatIList^#(n__zeros()) -> c_3()
     , isNatList^#(n__nil()) -> c_6()
     , 0^#() -> c_22()
     , zeros^#() -> c_19()
     , nil^#() -> c_27()
     , isNat^#(n__0()) -> c_16() }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of {7,12,24} by applications
   of Pre({7,12,24}) = {1,6,14,15,18,19,20}. Here rules are labeled as
   follows:
   
     DPs:
       { 1: and^#(tt(), T) -> c_1(T)
       , 2: isNatIList^#(IL) -> c_2(isNatList^#(activate(IL)))
       , 3: isNatIList^#(n__cons(N, IL)) ->
            c_4(and^#(isNat(activate(N)), isNatIList(activate(IL))))
       , 4: isNatList^#(n__cons(N, L)) ->
            c_5(and^#(isNat(activate(N)), isNatList(activate(L))))
       , 5: isNatList^#(n__take(N, IL)) ->
            c_7(and^#(isNat(activate(N)), isNatIList(activate(IL))))
       , 6: activate^#(X) -> c_8(X)
       , 7: activate^#(n__0()) -> c_9(0^#())
       , 8: activate^#(n__s(X)) -> c_10(s^#(X))
       , 9: activate^#(n__length(X)) -> c_11(length^#(X))
       , 10: activate^#(n__zeros()) -> c_12(zeros^#())
       , 11: activate^#(n__cons(X1, X2)) -> c_13(cons^#(X1, X2))
       , 12: activate^#(n__nil()) -> c_14(nil^#())
       , 13: activate^#(n__take(X1, X2)) -> c_15(take^#(X1, X2))
       , 14: s^#(X) -> c_28(X)
       , 15: length^#(X) -> c_30(X)
       , 16: length^#(cons(N, L)) ->
             c_31(uLength^#(and(isNat(N), isNatList(activate(L))), activate(L)))
       , 17: zeros^#() -> c_20(cons^#(0(), n__zeros()))
       , 18: cons^#(X1, X2) -> c_21(X1, X2)
       , 19: take^#(X1, X2) -> c_23(X1, X2)
       , 20: take^#(0(), IL) -> c_24(uTake1^#(isNatIList(IL)))
       , 21: take^#(s(M), cons(N, IL)) ->
             c_25(uTake2^#(and(isNat(M),
                               and(isNat(N), isNatIList(activate(IL)))),
                           M,
                           N,
                           activate(IL)))
       , 22: isNat^#(n__s(N)) -> c_17(isNat^#(activate(N)))
       , 23: isNat^#(n__length(L)) -> c_18(isNatList^#(activate(L)))
       , 24: uTake1^#(tt()) -> c_26(nil^#())
       , 25: uTake2^#(tt(), M, N, IL) ->
             c_29(cons^#(activate(N), n__take(activate(M), activate(IL))))
       , 26: uLength^#(tt(), L) -> c_32(s^#(length(activate(L))))
       , 27: isNatIList^#(n__zeros()) -> c_3()
       , 28: isNatList^#(n__nil()) -> c_6()
       , 29: 0^#() -> c_22()
       , 30: zeros^#() -> c_19()
       , 31: nil^#() -> c_27()
       , 32: isNat^#(n__0()) -> c_16() }
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { and^#(tt(), T) -> c_1(T)
     , isNatIList^#(IL) -> c_2(isNatList^#(activate(IL)))
     , isNatIList^#(n__cons(N, IL)) ->
       c_4(and^#(isNat(activate(N)), isNatIList(activate(IL))))
     , isNatList^#(n__cons(N, L)) ->
       c_5(and^#(isNat(activate(N)), isNatList(activate(L))))
     , isNatList^#(n__take(N, IL)) ->
       c_7(and^#(isNat(activate(N)), isNatIList(activate(IL))))
     , activate^#(X) -> c_8(X)
     , activate^#(n__s(X)) -> c_10(s^#(X))
     , activate^#(n__length(X)) -> c_11(length^#(X))
     , activate^#(n__zeros()) -> c_12(zeros^#())
     , activate^#(n__cons(X1, X2)) -> c_13(cons^#(X1, X2))
     , activate^#(n__take(X1, X2)) -> c_15(take^#(X1, X2))
     , s^#(X) -> c_28(X)
     , length^#(X) -> c_30(X)
     , length^#(cons(N, L)) ->
       c_31(uLength^#(and(isNat(N), isNatList(activate(L))), activate(L)))
     , zeros^#() -> c_20(cons^#(0(), n__zeros()))
     , cons^#(X1, X2) -> c_21(X1, X2)
     , take^#(X1, X2) -> c_23(X1, X2)
     , take^#(0(), IL) -> c_24(uTake1^#(isNatIList(IL)))
     , take^#(s(M), cons(N, IL)) ->
       c_25(uTake2^#(and(isNat(M),
                         and(isNat(N), isNatIList(activate(IL)))),
                     M,
                     N,
                     activate(IL)))
     , isNat^#(n__s(N)) -> c_17(isNat^#(activate(N)))
     , isNat^#(n__length(L)) -> c_18(isNatList^#(activate(L)))
     , uTake2^#(tt(), M, N, IL) ->
       c_29(cons^#(activate(N), n__take(activate(M), activate(IL))))
     , uLength^#(tt(), L) -> c_32(s^#(length(activate(L)))) }
   Strict Trs:
     { and(tt(), T) -> T
     , isNatIList(IL) -> isNatList(activate(IL))
     , isNatIList(n__zeros()) -> tt()
     , isNatIList(n__cons(N, IL)) ->
       and(isNat(activate(N)), isNatIList(activate(IL)))
     , isNatList(n__cons(N, L)) ->
       and(isNat(activate(N)), isNatList(activate(L)))
     , isNatList(n__nil()) -> tt()
     , isNatList(n__take(N, IL)) ->
       and(isNat(activate(N)), isNatIList(activate(IL)))
     , activate(X) -> X
     , activate(n__0()) -> 0()
     , activate(n__s(X)) -> s(X)
     , activate(n__length(X)) -> length(X)
     , activate(n__zeros()) -> zeros()
     , activate(n__cons(X1, X2)) -> cons(X1, X2)
     , activate(n__nil()) -> nil()
     , activate(n__take(X1, X2)) -> take(X1, X2)
     , isNat(n__0()) -> tt()
     , isNat(n__s(N)) -> isNat(activate(N))
     , isNat(n__length(L)) -> isNatList(activate(L))
     , zeros() -> n__zeros()
     , zeros() -> cons(0(), n__zeros())
     , cons(X1, X2) -> n__cons(X1, X2)
     , 0() -> n__0()
     , take(X1, X2) -> n__take(X1, X2)
     , take(0(), IL) -> uTake1(isNatIList(IL))
     , take(s(M), cons(N, IL)) ->
       uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))),
              M,
              N,
              activate(IL))
     , uTake1(tt()) -> nil()
     , nil() -> n__nil()
     , s(X) -> n__s(X)
     , uTake2(tt(), M, N, IL) ->
       cons(activate(N), n__take(activate(M), activate(IL)))
     , length(X) -> n__length(X)
     , length(cons(N, L)) ->
       uLength(and(isNat(N), isNatList(activate(L))), activate(L))
     , uLength(tt(), L) -> s(length(activate(L))) }
   Weak DPs:
     { isNatIList^#(n__zeros()) -> c_3()
     , isNatList^#(n__nil()) -> c_6()
     , activate^#(n__0()) -> c_9(0^#())
     , activate^#(n__nil()) -> c_14(nil^#())
     , 0^#() -> c_22()
     , zeros^#() -> c_19()
     , nil^#() -> c_27()
     , isNat^#(n__0()) -> c_16()
     , uTake1^#(tt()) -> c_26(nil^#()) }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of {18} by applications of
   Pre({18}) = {1,6,11,12,13,16,17}. Here rules are labeled as
   follows:
   
     DPs:
       { 1: and^#(tt(), T) -> c_1(T)
       , 2: isNatIList^#(IL) -> c_2(isNatList^#(activate(IL)))
       , 3: isNatIList^#(n__cons(N, IL)) ->
            c_4(and^#(isNat(activate(N)), isNatIList(activate(IL))))
       , 4: isNatList^#(n__cons(N, L)) ->
            c_5(and^#(isNat(activate(N)), isNatList(activate(L))))
       , 5: isNatList^#(n__take(N, IL)) ->
            c_7(and^#(isNat(activate(N)), isNatIList(activate(IL))))
       , 6: activate^#(X) -> c_8(X)
       , 7: activate^#(n__s(X)) -> c_10(s^#(X))
       , 8: activate^#(n__length(X)) -> c_11(length^#(X))
       , 9: activate^#(n__zeros()) -> c_12(zeros^#())
       , 10: activate^#(n__cons(X1, X2)) -> c_13(cons^#(X1, X2))
       , 11: activate^#(n__take(X1, X2)) -> c_15(take^#(X1, X2))
       , 12: s^#(X) -> c_28(X)
       , 13: length^#(X) -> c_30(X)
       , 14: length^#(cons(N, L)) ->
             c_31(uLength^#(and(isNat(N), isNatList(activate(L))), activate(L)))
       , 15: zeros^#() -> c_20(cons^#(0(), n__zeros()))
       , 16: cons^#(X1, X2) -> c_21(X1, X2)
       , 17: take^#(X1, X2) -> c_23(X1, X2)
       , 18: take^#(0(), IL) -> c_24(uTake1^#(isNatIList(IL)))
       , 19: take^#(s(M), cons(N, IL)) ->
             c_25(uTake2^#(and(isNat(M),
                               and(isNat(N), isNatIList(activate(IL)))),
                           M,
                           N,
                           activate(IL)))
       , 20: isNat^#(n__s(N)) -> c_17(isNat^#(activate(N)))
       , 21: isNat^#(n__length(L)) -> c_18(isNatList^#(activate(L)))
       , 22: uTake2^#(tt(), M, N, IL) ->
             c_29(cons^#(activate(N), n__take(activate(M), activate(IL))))
       , 23: uLength^#(tt(), L) -> c_32(s^#(length(activate(L))))
       , 24: isNatIList^#(n__zeros()) -> c_3()
       , 25: isNatList^#(n__nil()) -> c_6()
       , 26: activate^#(n__0()) -> c_9(0^#())
       , 27: activate^#(n__nil()) -> c_14(nil^#())
       , 28: 0^#() -> c_22()
       , 29: zeros^#() -> c_19()
       , 30: nil^#() -> c_27()
       , 31: isNat^#(n__0()) -> c_16()
       , 32: uTake1^#(tt()) -> c_26(nil^#()) }
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { and^#(tt(), T) -> c_1(T)
     , isNatIList^#(IL) -> c_2(isNatList^#(activate(IL)))
     , isNatIList^#(n__cons(N, IL)) ->
       c_4(and^#(isNat(activate(N)), isNatIList(activate(IL))))
     , isNatList^#(n__cons(N, L)) ->
       c_5(and^#(isNat(activate(N)), isNatList(activate(L))))
     , isNatList^#(n__take(N, IL)) ->
       c_7(and^#(isNat(activate(N)), isNatIList(activate(IL))))
     , activate^#(X) -> c_8(X)
     , activate^#(n__s(X)) -> c_10(s^#(X))
     , activate^#(n__length(X)) -> c_11(length^#(X))
     , activate^#(n__zeros()) -> c_12(zeros^#())
     , activate^#(n__cons(X1, X2)) -> c_13(cons^#(X1, X2))
     , activate^#(n__take(X1, X2)) -> c_15(take^#(X1, X2))
     , s^#(X) -> c_28(X)
     , length^#(X) -> c_30(X)
     , length^#(cons(N, L)) ->
       c_31(uLength^#(and(isNat(N), isNatList(activate(L))), activate(L)))
     , zeros^#() -> c_20(cons^#(0(), n__zeros()))
     , cons^#(X1, X2) -> c_21(X1, X2)
     , take^#(X1, X2) -> c_23(X1, X2)
     , take^#(s(M), cons(N, IL)) ->
       c_25(uTake2^#(and(isNat(M),
                         and(isNat(N), isNatIList(activate(IL)))),
                     M,
                     N,
                     activate(IL)))
     , isNat^#(n__s(N)) -> c_17(isNat^#(activate(N)))
     , isNat^#(n__length(L)) -> c_18(isNatList^#(activate(L)))
     , uTake2^#(tt(), M, N, IL) ->
       c_29(cons^#(activate(N), n__take(activate(M), activate(IL))))
     , uLength^#(tt(), L) -> c_32(s^#(length(activate(L)))) }
   Strict Trs:
     { and(tt(), T) -> T
     , isNatIList(IL) -> isNatList(activate(IL))
     , isNatIList(n__zeros()) -> tt()
     , isNatIList(n__cons(N, IL)) ->
       and(isNat(activate(N)), isNatIList(activate(IL)))
     , isNatList(n__cons(N, L)) ->
       and(isNat(activate(N)), isNatList(activate(L)))
     , isNatList(n__nil()) -> tt()
     , isNatList(n__take(N, IL)) ->
       and(isNat(activate(N)), isNatIList(activate(IL)))
     , activate(X) -> X
     , activate(n__0()) -> 0()
     , activate(n__s(X)) -> s(X)
     , activate(n__length(X)) -> length(X)
     , activate(n__zeros()) -> zeros()
     , activate(n__cons(X1, X2)) -> cons(X1, X2)
     , activate(n__nil()) -> nil()
     , activate(n__take(X1, X2)) -> take(X1, X2)
     , isNat(n__0()) -> tt()
     , isNat(n__s(N)) -> isNat(activate(N))
     , isNat(n__length(L)) -> isNatList(activate(L))
     , zeros() -> n__zeros()
     , zeros() -> cons(0(), n__zeros())
     , cons(X1, X2) -> n__cons(X1, X2)
     , 0() -> n__0()
     , take(X1, X2) -> n__take(X1, X2)
     , take(0(), IL) -> uTake1(isNatIList(IL))
     , take(s(M), cons(N, IL)) ->
       uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))),
              M,
              N,
              activate(IL))
     , uTake1(tt()) -> nil()
     , nil() -> n__nil()
     , s(X) -> n__s(X)
     , uTake2(tt(), M, N, IL) ->
       cons(activate(N), n__take(activate(M), activate(IL)))
     , length(X) -> n__length(X)
     , length(cons(N, L)) ->
       uLength(and(isNat(N), isNatList(activate(L))), activate(L))
     , uLength(tt(), L) -> s(length(activate(L))) }
   Weak DPs:
     { isNatIList^#(n__zeros()) -> c_3()
     , isNatList^#(n__nil()) -> c_6()
     , activate^#(n__0()) -> c_9(0^#())
     , activate^#(n__nil()) -> c_14(nil^#())
     , 0^#() -> c_22()
     , zeros^#() -> c_19()
     , nil^#() -> c_27()
     , take^#(0(), IL) -> c_24(uTake1^#(isNatIList(IL)))
     , isNat^#(n__0()) -> c_16()
     , uTake1^#(tt()) -> c_26(nil^#()) }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   Empty strict component of the problem is NOT empty.


Arrrr..