MAYBE

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

Strict Trs:
  { zeros() -> cons(0(), n__zeros())
  , zeros() -> n__zeros()
  , cons(X1, X2) -> n__cons(X1, X2)
  , 0() -> n__0()
  , U11(tt(), V1) -> U12(isNatList(activate(V1)))
  , U12(tt()) -> tt()
  , isNatList(n__take(V1, V2)) ->
    U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
        activate(V1),
        activate(V2))
  , isNatList(n__cons(V1, V2)) ->
    U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
        activate(V1),
        activate(V2))
  , isNatList(n__nil()) -> tt()
  , activate(X) -> X
  , activate(n__zeros()) -> zeros()
  , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2))
  , activate(n__0()) -> 0()
  , activate(n__length(X)) -> length(activate(X))
  , activate(n__s(X)) -> s(activate(X))
  , activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
  , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
  , activate(n__nil()) -> nil()
  , activate(n__and(X1, X2)) -> and(activate(X1), X2)
  , activate(n__isNat(X)) -> isNat(X)
  , activate(n__isNatKind(X)) -> isNatKind(X)
  , U21(tt(), V1) -> U22(isNat(activate(V1)))
  , U22(tt()) -> tt()
  , isNat(X) -> n__isNat(X)
  , isNat(n__0()) -> tt()
  , isNat(n__length(V1)) ->
    U11(isNatIListKind(activate(V1)), activate(V1))
  , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
  , U31(tt(), V) -> U32(isNatList(activate(V)))
  , U32(tt()) -> tt()
  , U41(tt(), V1, V2) -> U42(isNat(activate(V1)), activate(V2))
  , U42(tt(), V2) -> U43(isNatIList(activate(V2)))
  , U43(tt()) -> tt()
  , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V))
  , isNatIList(n__zeros()) -> tt()
  , isNatIList(n__cons(V1, V2)) ->
    U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
        activate(V1),
        activate(V2))
  , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
  , U52(tt(), V2) -> U53(isNatList(activate(V2)))
  , U53(tt()) -> tt()
  , U61(tt(), V1, V2) -> U62(isNat(activate(V1)), activate(V2))
  , U62(tt(), V2) -> U63(isNatIList(activate(V2)))
  , U63(tt()) -> tt()
  , U71(tt(), L) -> s(length(activate(L)))
  , s(X) -> n__s(X)
  , length(X) -> n__length(X)
  , length(cons(N, L)) ->
    U71(and(and(isNatList(activate(L)),
                n__isNatIListKind(activate(L))),
            n__and(n__isNat(N), n__isNatKind(N))),
        activate(L))
  , length(nil()) -> 0()
  , U81(tt()) -> nil()
  , nil() -> n__nil()
  , U91(tt(), IL, M, N) ->
    cons(activate(N), n__take(activate(M), activate(IL)))
  , and(X1, X2) -> n__and(X1, X2)
  , and(tt(), X) -> activate(X)
  , isNatIListKind(X) -> n__isNatIListKind(X)
  , isNatIListKind(n__zeros()) -> tt()
  , isNatIListKind(n__take(V1, V2)) ->
    and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
  , isNatIListKind(n__cons(V1, V2)) ->
    and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
  , isNatIListKind(n__nil()) -> tt()
  , isNatKind(X) -> n__isNatKind(X)
  , isNatKind(n__0()) -> tt()
  , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
  , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
  , take(X1, X2) -> n__take(X1, X2)
  , take(0(), IL) -> U81(and(isNatIList(IL), n__isNatIListKind(IL)))
  , take(s(M), cons(N, IL)) ->
    U91(and(and(isNatIList(activate(IL)),
                n__isNatIListKind(activate(IL))),
            n__and(n__and(n__isNat(M), n__isNatKind(M)),
                   n__and(n__isNat(N), n__isNatKind(N)))),
        activate(IL),
        M,
        N) }
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 perSymbol-enrichment and initial automaton 'match''
         failed due to the following reason:
         
         match-boundness of the problem could not be verified.
      
      2) 'Bounds with minimal-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) '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
      
      2) '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
      
   

3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed
   due to the following reason:
   
   We add the following weak dependency pairs:
   
   Strict DPs:
     { zeros^#() -> c_1(cons^#(0(), n__zeros()))
     , zeros^#() -> c_2()
     , cons^#(X1, X2) -> c_3(X1, X2)
     , 0^#() -> c_4()
     , U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1))))
     , U12^#(tt()) -> c_6()
     , isNatList^#(n__take(V1, V2)) ->
       c_7(U61^#(and(isNatKind(activate(V1)),
                     n__isNatIListKind(activate(V2))),
                 activate(V1),
                 activate(V2)))
     , isNatList^#(n__cons(V1, V2)) ->
       c_8(U51^#(and(isNatKind(activate(V1)),
                     n__isNatIListKind(activate(V2))),
                 activate(V1),
                 activate(V2)))
     , isNatList^#(n__nil()) -> c_9()
     , U61^#(tt(), V1, V2) ->
       c_39(U62^#(isNat(activate(V1)), activate(V2)))
     , U51^#(tt(), V1, V2) ->
       c_36(U52^#(isNat(activate(V1)), activate(V2)))
     , activate^#(X) -> c_10(X)
     , activate^#(n__zeros()) -> c_11(zeros^#())
     , activate^#(n__take(X1, X2)) ->
       c_12(take^#(activate(X1), activate(X2)))
     , activate^#(n__0()) -> c_13(0^#())
     , activate^#(n__length(X)) -> c_14(length^#(activate(X)))
     , activate^#(n__s(X)) -> c_15(s^#(activate(X)))
     , activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2))
     , activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X))
     , activate^#(n__nil()) -> c_18(nil^#())
     , activate^#(n__and(X1, X2)) -> c_19(and^#(activate(X1), X2))
     , activate^#(n__isNat(X)) -> c_20(isNat^#(X))
     , activate^#(n__isNatKind(X)) -> c_21(isNatKind^#(X))
     , take^#(X1, X2) -> c_61(X1, X2)
     , take^#(0(), IL) ->
       c_62(U81^#(and(isNatIList(IL), n__isNatIListKind(IL))))
     , take^#(s(M), cons(N, IL)) ->
       c_63(U91^#(and(and(isNatIList(activate(IL)),
                          n__isNatIListKind(activate(IL))),
                      n__and(n__and(n__isNat(M), n__isNatKind(M)),
                             n__and(n__isNat(N), n__isNatKind(N)))),
                  activate(IL),
                  M,
                  N))
     , length^#(X) -> c_44(X)
     , length^#(cons(N, L)) ->
       c_45(U71^#(and(and(isNatList(activate(L)),
                          n__isNatIListKind(activate(L))),
                      n__and(n__isNat(N), n__isNatKind(N))),
                  activate(L)))
     , length^#(nil()) -> c_46(0^#())
     , s^#(X) -> c_43(X)
     , isNatIListKind^#(X) -> c_52(X)
     , isNatIListKind^#(n__zeros()) -> c_53()
     , isNatIListKind^#(n__take(V1, V2)) ->
       c_54(and^#(isNatKind(activate(V1)),
                  n__isNatIListKind(activate(V2))))
     , isNatIListKind^#(n__cons(V1, V2)) ->
       c_55(and^#(isNatKind(activate(V1)),
                  n__isNatIListKind(activate(V2))))
     , isNatIListKind^#(n__nil()) -> c_56()
     , nil^#() -> c_48()
     , and^#(X1, X2) -> c_50(X1, X2)
     , and^#(tt(), X) -> c_51(activate^#(X))
     , isNat^#(X) -> c_24(X)
     , isNat^#(n__0()) -> c_25()
     , isNat^#(n__length(V1)) ->
       c_26(U11^#(isNatIListKind(activate(V1)), activate(V1)))
     , isNat^#(n__s(V1)) ->
       c_27(U21^#(isNatKind(activate(V1)), activate(V1)))
     , isNatKind^#(X) -> c_57(X)
     , isNatKind^#(n__0()) -> c_58()
     , isNatKind^#(n__length(V1)) ->
       c_59(isNatIListKind^#(activate(V1)))
     , isNatKind^#(n__s(V1)) -> c_60(isNatKind^#(activate(V1)))
     , U21^#(tt(), V1) -> c_22(U22^#(isNat(activate(V1))))
     , U22^#(tt()) -> c_23()
     , U31^#(tt(), V) -> c_28(U32^#(isNatList(activate(V))))
     , U32^#(tt()) -> c_29()
     , U41^#(tt(), V1, V2) ->
       c_30(U42^#(isNat(activate(V1)), activate(V2)))
     , U42^#(tt(), V2) -> c_31(U43^#(isNatIList(activate(V2))))
     , U43^#(tt()) -> c_32()
     , isNatIList^#(V) ->
       c_33(U31^#(isNatIListKind(activate(V)), activate(V)))
     , isNatIList^#(n__zeros()) -> c_34()
     , isNatIList^#(n__cons(V1, V2)) ->
       c_35(U41^#(and(isNatKind(activate(V1)),
                      n__isNatIListKind(activate(V2))),
                  activate(V1),
                  activate(V2)))
     , U52^#(tt(), V2) -> c_37(U53^#(isNatList(activate(V2))))
     , U53^#(tt()) -> c_38()
     , U62^#(tt(), V2) -> c_40(U63^#(isNatIList(activate(V2))))
     , U63^#(tt()) -> c_41()
     , U71^#(tt(), L) -> c_42(s^#(length(activate(L))))
     , U81^#(tt()) -> c_47(nil^#())
     , U91^#(tt(), IL, M, N) ->
       c_49(cons^#(activate(N), n__take(activate(M), activate(IL)))) }
   
   and mark the set of starting terms.
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { zeros^#() -> c_1(cons^#(0(), n__zeros()))
     , zeros^#() -> c_2()
     , cons^#(X1, X2) -> c_3(X1, X2)
     , 0^#() -> c_4()
     , U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1))))
     , U12^#(tt()) -> c_6()
     , isNatList^#(n__take(V1, V2)) ->
       c_7(U61^#(and(isNatKind(activate(V1)),
                     n__isNatIListKind(activate(V2))),
                 activate(V1),
                 activate(V2)))
     , isNatList^#(n__cons(V1, V2)) ->
       c_8(U51^#(and(isNatKind(activate(V1)),
                     n__isNatIListKind(activate(V2))),
                 activate(V1),
                 activate(V2)))
     , isNatList^#(n__nil()) -> c_9()
     , U61^#(tt(), V1, V2) ->
       c_39(U62^#(isNat(activate(V1)), activate(V2)))
     , U51^#(tt(), V1, V2) ->
       c_36(U52^#(isNat(activate(V1)), activate(V2)))
     , activate^#(X) -> c_10(X)
     , activate^#(n__zeros()) -> c_11(zeros^#())
     , activate^#(n__take(X1, X2)) ->
       c_12(take^#(activate(X1), activate(X2)))
     , activate^#(n__0()) -> c_13(0^#())
     , activate^#(n__length(X)) -> c_14(length^#(activate(X)))
     , activate^#(n__s(X)) -> c_15(s^#(activate(X)))
     , activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2))
     , activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X))
     , activate^#(n__nil()) -> c_18(nil^#())
     , activate^#(n__and(X1, X2)) -> c_19(and^#(activate(X1), X2))
     , activate^#(n__isNat(X)) -> c_20(isNat^#(X))
     , activate^#(n__isNatKind(X)) -> c_21(isNatKind^#(X))
     , take^#(X1, X2) -> c_61(X1, X2)
     , take^#(0(), IL) ->
       c_62(U81^#(and(isNatIList(IL), n__isNatIListKind(IL))))
     , take^#(s(M), cons(N, IL)) ->
       c_63(U91^#(and(and(isNatIList(activate(IL)),
                          n__isNatIListKind(activate(IL))),
                      n__and(n__and(n__isNat(M), n__isNatKind(M)),
                             n__and(n__isNat(N), n__isNatKind(N)))),
                  activate(IL),
                  M,
                  N))
     , length^#(X) -> c_44(X)
     , length^#(cons(N, L)) ->
       c_45(U71^#(and(and(isNatList(activate(L)),
                          n__isNatIListKind(activate(L))),
                      n__and(n__isNat(N), n__isNatKind(N))),
                  activate(L)))
     , length^#(nil()) -> c_46(0^#())
     , s^#(X) -> c_43(X)
     , isNatIListKind^#(X) -> c_52(X)
     , isNatIListKind^#(n__zeros()) -> c_53()
     , isNatIListKind^#(n__take(V1, V2)) ->
       c_54(and^#(isNatKind(activate(V1)),
                  n__isNatIListKind(activate(V2))))
     , isNatIListKind^#(n__cons(V1, V2)) ->
       c_55(and^#(isNatKind(activate(V1)),
                  n__isNatIListKind(activate(V2))))
     , isNatIListKind^#(n__nil()) -> c_56()
     , nil^#() -> c_48()
     , and^#(X1, X2) -> c_50(X1, X2)
     , and^#(tt(), X) -> c_51(activate^#(X))
     , isNat^#(X) -> c_24(X)
     , isNat^#(n__0()) -> c_25()
     , isNat^#(n__length(V1)) ->
       c_26(U11^#(isNatIListKind(activate(V1)), activate(V1)))
     , isNat^#(n__s(V1)) ->
       c_27(U21^#(isNatKind(activate(V1)), activate(V1)))
     , isNatKind^#(X) -> c_57(X)
     , isNatKind^#(n__0()) -> c_58()
     , isNatKind^#(n__length(V1)) ->
       c_59(isNatIListKind^#(activate(V1)))
     , isNatKind^#(n__s(V1)) -> c_60(isNatKind^#(activate(V1)))
     , U21^#(tt(), V1) -> c_22(U22^#(isNat(activate(V1))))
     , U22^#(tt()) -> c_23()
     , U31^#(tt(), V) -> c_28(U32^#(isNatList(activate(V))))
     , U32^#(tt()) -> c_29()
     , U41^#(tt(), V1, V2) ->
       c_30(U42^#(isNat(activate(V1)), activate(V2)))
     , U42^#(tt(), V2) -> c_31(U43^#(isNatIList(activate(V2))))
     , U43^#(tt()) -> c_32()
     , isNatIList^#(V) ->
       c_33(U31^#(isNatIListKind(activate(V)), activate(V)))
     , isNatIList^#(n__zeros()) -> c_34()
     , isNatIList^#(n__cons(V1, V2)) ->
       c_35(U41^#(and(isNatKind(activate(V1)),
                      n__isNatIListKind(activate(V2))),
                  activate(V1),
                  activate(V2)))
     , U52^#(tt(), V2) -> c_37(U53^#(isNatList(activate(V2))))
     , U53^#(tt()) -> c_38()
     , U62^#(tt(), V2) -> c_40(U63^#(isNatIList(activate(V2))))
     , U63^#(tt()) -> c_41()
     , U71^#(tt(), L) -> c_42(s^#(length(activate(L))))
     , U81^#(tt()) -> c_47(nil^#())
     , U91^#(tt(), IL, M, N) ->
       c_49(cons^#(activate(N), n__take(activate(M), activate(IL)))) }
   Strict Trs:
     { zeros() -> cons(0(), n__zeros())
     , zeros() -> n__zeros()
     , cons(X1, X2) -> n__cons(X1, X2)
     , 0() -> n__0()
     , U11(tt(), V1) -> U12(isNatList(activate(V1)))
     , U12(tt()) -> tt()
     , isNatList(n__take(V1, V2)) ->
       U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
           activate(V1),
           activate(V2))
     , isNatList(n__cons(V1, V2)) ->
       U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
           activate(V1),
           activate(V2))
     , isNatList(n__nil()) -> tt()
     , activate(X) -> X
     , activate(n__zeros()) -> zeros()
     , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2))
     , activate(n__0()) -> 0()
     , activate(n__length(X)) -> length(activate(X))
     , activate(n__s(X)) -> s(activate(X))
     , activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
     , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
     , activate(n__nil()) -> nil()
     , activate(n__and(X1, X2)) -> and(activate(X1), X2)
     , activate(n__isNat(X)) -> isNat(X)
     , activate(n__isNatKind(X)) -> isNatKind(X)
     , U21(tt(), V1) -> U22(isNat(activate(V1)))
     , U22(tt()) -> tt()
     , isNat(X) -> n__isNat(X)
     , isNat(n__0()) -> tt()
     , isNat(n__length(V1)) ->
       U11(isNatIListKind(activate(V1)), activate(V1))
     , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
     , U31(tt(), V) -> U32(isNatList(activate(V)))
     , U32(tt()) -> tt()
     , U41(tt(), V1, V2) -> U42(isNat(activate(V1)), activate(V2))
     , U42(tt(), V2) -> U43(isNatIList(activate(V2)))
     , U43(tt()) -> tt()
     , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V))
     , isNatIList(n__zeros()) -> tt()
     , isNatIList(n__cons(V1, V2)) ->
       U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
           activate(V1),
           activate(V2))
     , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
     , U52(tt(), V2) -> U53(isNatList(activate(V2)))
     , U53(tt()) -> tt()
     , U61(tt(), V1, V2) -> U62(isNat(activate(V1)), activate(V2))
     , U62(tt(), V2) -> U63(isNatIList(activate(V2)))
     , U63(tt()) -> tt()
     , U71(tt(), L) -> s(length(activate(L)))
     , s(X) -> n__s(X)
     , length(X) -> n__length(X)
     , length(cons(N, L)) ->
       U71(and(and(isNatList(activate(L)),
                   n__isNatIListKind(activate(L))),
               n__and(n__isNat(N), n__isNatKind(N))),
           activate(L))
     , length(nil()) -> 0()
     , U81(tt()) -> nil()
     , nil() -> n__nil()
     , U91(tt(), IL, M, N) ->
       cons(activate(N), n__take(activate(M), activate(IL)))
     , and(X1, X2) -> n__and(X1, X2)
     , and(tt(), X) -> activate(X)
     , isNatIListKind(X) -> n__isNatIListKind(X)
     , isNatIListKind(n__zeros()) -> tt()
     , isNatIListKind(n__take(V1, V2)) ->
       and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
     , isNatIListKind(n__cons(V1, V2)) ->
       and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
     , isNatIListKind(n__nil()) -> tt()
     , isNatKind(X) -> n__isNatKind(X)
     , isNatKind(n__0()) -> tt()
     , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
     , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
     , take(X1, X2) -> n__take(X1, X2)
     , take(0(), IL) -> U81(and(isNatIList(IL), n__isNatIListKind(IL)))
     , take(s(M), cons(N, IL)) ->
       U91(and(and(isNatIList(activate(IL)),
                   n__isNatIListKind(activate(IL))),
               n__and(n__and(n__isNat(M), n__isNatKind(M)),
                      n__and(n__isNat(N), n__isNatKind(N)))),
           activate(IL),
           M,
           N) }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of
   {2,4,6,9,32,35,36,40,44,48,50,53,55,58,60} by applications of
   Pre({2,4,6,9,32,35,36,40,44,48,50,53,55,58,60}) =
   {3,5,12,13,15,19,20,22,23,24,27,29,30,31,37,39,43,45,46,47,49,52,57,59,62}.
   Here rules are labeled as follows:
   
     DPs:
       { 1: zeros^#() -> c_1(cons^#(0(), n__zeros()))
       , 2: zeros^#() -> c_2()
       , 3: cons^#(X1, X2) -> c_3(X1, X2)
       , 4: 0^#() -> c_4()
       , 5: U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1))))
       , 6: U12^#(tt()) -> c_6()
       , 7: isNatList^#(n__take(V1, V2)) ->
            c_7(U61^#(and(isNatKind(activate(V1)),
                          n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2)))
       , 8: isNatList^#(n__cons(V1, V2)) ->
            c_8(U51^#(and(isNatKind(activate(V1)),
                          n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2)))
       , 9: isNatList^#(n__nil()) -> c_9()
       , 10: U61^#(tt(), V1, V2) ->
             c_39(U62^#(isNat(activate(V1)), activate(V2)))
       , 11: U51^#(tt(), V1, V2) ->
             c_36(U52^#(isNat(activate(V1)), activate(V2)))
       , 12: activate^#(X) -> c_10(X)
       , 13: activate^#(n__zeros()) -> c_11(zeros^#())
       , 14: activate^#(n__take(X1, X2)) ->
             c_12(take^#(activate(X1), activate(X2)))
       , 15: activate^#(n__0()) -> c_13(0^#())
       , 16: activate^#(n__length(X)) -> c_14(length^#(activate(X)))
       , 17: activate^#(n__s(X)) -> c_15(s^#(activate(X)))
       , 18: activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2))
       , 19: activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X))
       , 20: activate^#(n__nil()) -> c_18(nil^#())
       , 21: activate^#(n__and(X1, X2)) -> c_19(and^#(activate(X1), X2))
       , 22: activate^#(n__isNat(X)) -> c_20(isNat^#(X))
       , 23: activate^#(n__isNatKind(X)) -> c_21(isNatKind^#(X))
       , 24: take^#(X1, X2) -> c_61(X1, X2)
       , 25: take^#(0(), IL) ->
             c_62(U81^#(and(isNatIList(IL), n__isNatIListKind(IL))))
       , 26: take^#(s(M), cons(N, IL)) ->
             c_63(U91^#(and(and(isNatIList(activate(IL)),
                                n__isNatIListKind(activate(IL))),
                            n__and(n__and(n__isNat(M), n__isNatKind(M)),
                                   n__and(n__isNat(N), n__isNatKind(N)))),
                        activate(IL),
                        M,
                        N))
       , 27: length^#(X) -> c_44(X)
       , 28: length^#(cons(N, L)) ->
             c_45(U71^#(and(and(isNatList(activate(L)),
                                n__isNatIListKind(activate(L))),
                            n__and(n__isNat(N), n__isNatKind(N))),
                        activate(L)))
       , 29: length^#(nil()) -> c_46(0^#())
       , 30: s^#(X) -> c_43(X)
       , 31: isNatIListKind^#(X) -> c_52(X)
       , 32: isNatIListKind^#(n__zeros()) -> c_53()
       , 33: isNatIListKind^#(n__take(V1, V2)) ->
             c_54(and^#(isNatKind(activate(V1)),
                        n__isNatIListKind(activate(V2))))
       , 34: isNatIListKind^#(n__cons(V1, V2)) ->
             c_55(and^#(isNatKind(activate(V1)),
                        n__isNatIListKind(activate(V2))))
       , 35: isNatIListKind^#(n__nil()) -> c_56()
       , 36: nil^#() -> c_48()
       , 37: and^#(X1, X2) -> c_50(X1, X2)
       , 38: and^#(tt(), X) -> c_51(activate^#(X))
       , 39: isNat^#(X) -> c_24(X)
       , 40: isNat^#(n__0()) -> c_25()
       , 41: isNat^#(n__length(V1)) ->
             c_26(U11^#(isNatIListKind(activate(V1)), activate(V1)))
       , 42: isNat^#(n__s(V1)) ->
             c_27(U21^#(isNatKind(activate(V1)), activate(V1)))
       , 43: isNatKind^#(X) -> c_57(X)
       , 44: isNatKind^#(n__0()) -> c_58()
       , 45: isNatKind^#(n__length(V1)) ->
             c_59(isNatIListKind^#(activate(V1)))
       , 46: isNatKind^#(n__s(V1)) -> c_60(isNatKind^#(activate(V1)))
       , 47: U21^#(tt(), V1) -> c_22(U22^#(isNat(activate(V1))))
       , 48: U22^#(tt()) -> c_23()
       , 49: U31^#(tt(), V) -> c_28(U32^#(isNatList(activate(V))))
       , 50: U32^#(tt()) -> c_29()
       , 51: U41^#(tt(), V1, V2) ->
             c_30(U42^#(isNat(activate(V1)), activate(V2)))
       , 52: U42^#(tt(), V2) -> c_31(U43^#(isNatIList(activate(V2))))
       , 53: U43^#(tt()) -> c_32()
       , 54: isNatIList^#(V) ->
             c_33(U31^#(isNatIListKind(activate(V)), activate(V)))
       , 55: isNatIList^#(n__zeros()) -> c_34()
       , 56: isNatIList^#(n__cons(V1, V2)) ->
             c_35(U41^#(and(isNatKind(activate(V1)),
                            n__isNatIListKind(activate(V2))),
                        activate(V1),
                        activate(V2)))
       , 57: U52^#(tt(), V2) -> c_37(U53^#(isNatList(activate(V2))))
       , 58: U53^#(tt()) -> c_38()
       , 59: U62^#(tt(), V2) -> c_40(U63^#(isNatIList(activate(V2))))
       , 60: U63^#(tt()) -> c_41()
       , 61: U71^#(tt(), L) -> c_42(s^#(length(activate(L))))
       , 62: U81^#(tt()) -> c_47(nil^#())
       , 63: U91^#(tt(), IL, M, N) ->
             c_49(cons^#(activate(N), n__take(activate(M), activate(IL)))) }
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { zeros^#() -> c_1(cons^#(0(), n__zeros()))
     , cons^#(X1, X2) -> c_3(X1, X2)
     , U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1))))
     , isNatList^#(n__take(V1, V2)) ->
       c_7(U61^#(and(isNatKind(activate(V1)),
                     n__isNatIListKind(activate(V2))),
                 activate(V1),
                 activate(V2)))
     , isNatList^#(n__cons(V1, V2)) ->
       c_8(U51^#(and(isNatKind(activate(V1)),
                     n__isNatIListKind(activate(V2))),
                 activate(V1),
                 activate(V2)))
     , U61^#(tt(), V1, V2) ->
       c_39(U62^#(isNat(activate(V1)), activate(V2)))
     , U51^#(tt(), V1, V2) ->
       c_36(U52^#(isNat(activate(V1)), activate(V2)))
     , activate^#(X) -> c_10(X)
     , activate^#(n__zeros()) -> c_11(zeros^#())
     , activate^#(n__take(X1, X2)) ->
       c_12(take^#(activate(X1), activate(X2)))
     , activate^#(n__0()) -> c_13(0^#())
     , activate^#(n__length(X)) -> c_14(length^#(activate(X)))
     , activate^#(n__s(X)) -> c_15(s^#(activate(X)))
     , activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2))
     , activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X))
     , activate^#(n__nil()) -> c_18(nil^#())
     , activate^#(n__and(X1, X2)) -> c_19(and^#(activate(X1), X2))
     , activate^#(n__isNat(X)) -> c_20(isNat^#(X))
     , activate^#(n__isNatKind(X)) -> c_21(isNatKind^#(X))
     , take^#(X1, X2) -> c_61(X1, X2)
     , take^#(0(), IL) ->
       c_62(U81^#(and(isNatIList(IL), n__isNatIListKind(IL))))
     , take^#(s(M), cons(N, IL)) ->
       c_63(U91^#(and(and(isNatIList(activate(IL)),
                          n__isNatIListKind(activate(IL))),
                      n__and(n__and(n__isNat(M), n__isNatKind(M)),
                             n__and(n__isNat(N), n__isNatKind(N)))),
                  activate(IL),
                  M,
                  N))
     , length^#(X) -> c_44(X)
     , length^#(cons(N, L)) ->
       c_45(U71^#(and(and(isNatList(activate(L)),
                          n__isNatIListKind(activate(L))),
                      n__and(n__isNat(N), n__isNatKind(N))),
                  activate(L)))
     , length^#(nil()) -> c_46(0^#())
     , s^#(X) -> c_43(X)
     , isNatIListKind^#(X) -> c_52(X)
     , isNatIListKind^#(n__take(V1, V2)) ->
       c_54(and^#(isNatKind(activate(V1)),
                  n__isNatIListKind(activate(V2))))
     , isNatIListKind^#(n__cons(V1, V2)) ->
       c_55(and^#(isNatKind(activate(V1)),
                  n__isNatIListKind(activate(V2))))
     , and^#(X1, X2) -> c_50(X1, X2)
     , and^#(tt(), X) -> c_51(activate^#(X))
     , isNat^#(X) -> c_24(X)
     , isNat^#(n__length(V1)) ->
       c_26(U11^#(isNatIListKind(activate(V1)), activate(V1)))
     , isNat^#(n__s(V1)) ->
       c_27(U21^#(isNatKind(activate(V1)), activate(V1)))
     , isNatKind^#(X) -> c_57(X)
     , isNatKind^#(n__length(V1)) ->
       c_59(isNatIListKind^#(activate(V1)))
     , isNatKind^#(n__s(V1)) -> c_60(isNatKind^#(activate(V1)))
     , U21^#(tt(), V1) -> c_22(U22^#(isNat(activate(V1))))
     , U31^#(tt(), V) -> c_28(U32^#(isNatList(activate(V))))
     , U41^#(tt(), V1, V2) ->
       c_30(U42^#(isNat(activate(V1)), activate(V2)))
     , U42^#(tt(), V2) -> c_31(U43^#(isNatIList(activate(V2))))
     , isNatIList^#(V) ->
       c_33(U31^#(isNatIListKind(activate(V)), activate(V)))
     , isNatIList^#(n__cons(V1, V2)) ->
       c_35(U41^#(and(isNatKind(activate(V1)),
                      n__isNatIListKind(activate(V2))),
                  activate(V1),
                  activate(V2)))
     , U52^#(tt(), V2) -> c_37(U53^#(isNatList(activate(V2))))
     , U62^#(tt(), V2) -> c_40(U63^#(isNatIList(activate(V2))))
     , U71^#(tt(), L) -> c_42(s^#(length(activate(L))))
     , U81^#(tt()) -> c_47(nil^#())
     , U91^#(tt(), IL, M, N) ->
       c_49(cons^#(activate(N), n__take(activate(M), activate(IL)))) }
   Strict Trs:
     { zeros() -> cons(0(), n__zeros())
     , zeros() -> n__zeros()
     , cons(X1, X2) -> n__cons(X1, X2)
     , 0() -> n__0()
     , U11(tt(), V1) -> U12(isNatList(activate(V1)))
     , U12(tt()) -> tt()
     , isNatList(n__take(V1, V2)) ->
       U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
           activate(V1),
           activate(V2))
     , isNatList(n__cons(V1, V2)) ->
       U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
           activate(V1),
           activate(V2))
     , isNatList(n__nil()) -> tt()
     , activate(X) -> X
     , activate(n__zeros()) -> zeros()
     , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2))
     , activate(n__0()) -> 0()
     , activate(n__length(X)) -> length(activate(X))
     , activate(n__s(X)) -> s(activate(X))
     , activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
     , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
     , activate(n__nil()) -> nil()
     , activate(n__and(X1, X2)) -> and(activate(X1), X2)
     , activate(n__isNat(X)) -> isNat(X)
     , activate(n__isNatKind(X)) -> isNatKind(X)
     , U21(tt(), V1) -> U22(isNat(activate(V1)))
     , U22(tt()) -> tt()
     , isNat(X) -> n__isNat(X)
     , isNat(n__0()) -> tt()
     , isNat(n__length(V1)) ->
       U11(isNatIListKind(activate(V1)), activate(V1))
     , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
     , U31(tt(), V) -> U32(isNatList(activate(V)))
     , U32(tt()) -> tt()
     , U41(tt(), V1, V2) -> U42(isNat(activate(V1)), activate(V2))
     , U42(tt(), V2) -> U43(isNatIList(activate(V2)))
     , U43(tt()) -> tt()
     , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V))
     , isNatIList(n__zeros()) -> tt()
     , isNatIList(n__cons(V1, V2)) ->
       U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
           activate(V1),
           activate(V2))
     , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
     , U52(tt(), V2) -> U53(isNatList(activate(V2)))
     , U53(tt()) -> tt()
     , U61(tt(), V1, V2) -> U62(isNat(activate(V1)), activate(V2))
     , U62(tt(), V2) -> U63(isNatIList(activate(V2)))
     , U63(tt()) -> tt()
     , U71(tt(), L) -> s(length(activate(L)))
     , s(X) -> n__s(X)
     , length(X) -> n__length(X)
     , length(cons(N, L)) ->
       U71(and(and(isNatList(activate(L)),
                   n__isNatIListKind(activate(L))),
               n__and(n__isNat(N), n__isNatKind(N))),
           activate(L))
     , length(nil()) -> 0()
     , U81(tt()) -> nil()
     , nil() -> n__nil()
     , U91(tt(), IL, M, N) ->
       cons(activate(N), n__take(activate(M), activate(IL)))
     , and(X1, X2) -> n__and(X1, X2)
     , and(tt(), X) -> activate(X)
     , isNatIListKind(X) -> n__isNatIListKind(X)
     , isNatIListKind(n__zeros()) -> tt()
     , isNatIListKind(n__take(V1, V2)) ->
       and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
     , isNatIListKind(n__cons(V1, V2)) ->
       and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
     , isNatIListKind(n__nil()) -> tt()
     , isNatKind(X) -> n__isNatKind(X)
     , isNatKind(n__0()) -> tt()
     , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
     , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
     , take(X1, X2) -> n__take(X1, X2)
     , take(0(), IL) -> U81(and(isNatIList(IL), n__isNatIListKind(IL)))
     , take(s(M), cons(N, IL)) ->
       U91(and(and(isNatIList(activate(IL)),
                   n__isNatIListKind(activate(IL))),
               n__and(n__and(n__isNat(M), n__isNatKind(M)),
                      n__and(n__isNat(N), n__isNatKind(N)))),
           activate(IL),
           M,
           N) }
   Weak DPs:
     { zeros^#() -> c_2()
     , 0^#() -> c_4()
     , U12^#(tt()) -> c_6()
     , isNatList^#(n__nil()) -> c_9()
     , isNatIListKind^#(n__zeros()) -> c_53()
     , isNatIListKind^#(n__nil()) -> c_56()
     , nil^#() -> c_48()
     , isNat^#(n__0()) -> c_25()
     , isNatKind^#(n__0()) -> c_58()
     , U22^#(tt()) -> c_23()
     , U32^#(tt()) -> c_29()
     , U43^#(tt()) -> c_32()
     , isNatIList^#(n__zeros()) -> c_34()
     , U53^#(tt()) -> c_38()
     , U63^#(tt()) -> c_41() }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of
   {3,11,16,25,38,39,41,44,45,47} by applications of
   Pre({3,11,16,25,38,39,41,44,45,47}) =
   {2,6,7,8,12,20,21,23,26,27,30,31,32,33,34,35,40,42}. Here rules are
   labeled as follows:
   
     DPs:
       { 1: zeros^#() -> c_1(cons^#(0(), n__zeros()))
       , 2: cons^#(X1, X2) -> c_3(X1, X2)
       , 3: U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1))))
       , 4: isNatList^#(n__take(V1, V2)) ->
            c_7(U61^#(and(isNatKind(activate(V1)),
                          n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2)))
       , 5: isNatList^#(n__cons(V1, V2)) ->
            c_8(U51^#(and(isNatKind(activate(V1)),
                          n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2)))
       , 6: U61^#(tt(), V1, V2) ->
            c_39(U62^#(isNat(activate(V1)), activate(V2)))
       , 7: U51^#(tt(), V1, V2) ->
            c_36(U52^#(isNat(activate(V1)), activate(V2)))
       , 8: activate^#(X) -> c_10(X)
       , 9: activate^#(n__zeros()) -> c_11(zeros^#())
       , 10: activate^#(n__take(X1, X2)) ->
             c_12(take^#(activate(X1), activate(X2)))
       , 11: activate^#(n__0()) -> c_13(0^#())
       , 12: activate^#(n__length(X)) -> c_14(length^#(activate(X)))
       , 13: activate^#(n__s(X)) -> c_15(s^#(activate(X)))
       , 14: activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2))
       , 15: activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X))
       , 16: activate^#(n__nil()) -> c_18(nil^#())
       , 17: activate^#(n__and(X1, X2)) -> c_19(and^#(activate(X1), X2))
       , 18: activate^#(n__isNat(X)) -> c_20(isNat^#(X))
       , 19: activate^#(n__isNatKind(X)) -> c_21(isNatKind^#(X))
       , 20: take^#(X1, X2) -> c_61(X1, X2)
       , 21: take^#(0(), IL) ->
             c_62(U81^#(and(isNatIList(IL), n__isNatIListKind(IL))))
       , 22: take^#(s(M), cons(N, IL)) ->
             c_63(U91^#(and(and(isNatIList(activate(IL)),
                                n__isNatIListKind(activate(IL))),
                            n__and(n__and(n__isNat(M), n__isNatKind(M)),
                                   n__and(n__isNat(N), n__isNatKind(N)))),
                        activate(IL),
                        M,
                        N))
       , 23: length^#(X) -> c_44(X)
       , 24: length^#(cons(N, L)) ->
             c_45(U71^#(and(and(isNatList(activate(L)),
                                n__isNatIListKind(activate(L))),
                            n__and(n__isNat(N), n__isNatKind(N))),
                        activate(L)))
       , 25: length^#(nil()) -> c_46(0^#())
       , 26: s^#(X) -> c_43(X)
       , 27: isNatIListKind^#(X) -> c_52(X)
       , 28: isNatIListKind^#(n__take(V1, V2)) ->
             c_54(and^#(isNatKind(activate(V1)),
                        n__isNatIListKind(activate(V2))))
       , 29: isNatIListKind^#(n__cons(V1, V2)) ->
             c_55(and^#(isNatKind(activate(V1)),
                        n__isNatIListKind(activate(V2))))
       , 30: and^#(X1, X2) -> c_50(X1, X2)
       , 31: and^#(tt(), X) -> c_51(activate^#(X))
       , 32: isNat^#(X) -> c_24(X)
       , 33: isNat^#(n__length(V1)) ->
             c_26(U11^#(isNatIListKind(activate(V1)), activate(V1)))
       , 34: isNat^#(n__s(V1)) ->
             c_27(U21^#(isNatKind(activate(V1)), activate(V1)))
       , 35: isNatKind^#(X) -> c_57(X)
       , 36: isNatKind^#(n__length(V1)) ->
             c_59(isNatIListKind^#(activate(V1)))
       , 37: isNatKind^#(n__s(V1)) -> c_60(isNatKind^#(activate(V1)))
       , 38: U21^#(tt(), V1) -> c_22(U22^#(isNat(activate(V1))))
       , 39: U31^#(tt(), V) -> c_28(U32^#(isNatList(activate(V))))
       , 40: U41^#(tt(), V1, V2) ->
             c_30(U42^#(isNat(activate(V1)), activate(V2)))
       , 41: U42^#(tt(), V2) -> c_31(U43^#(isNatIList(activate(V2))))
       , 42: isNatIList^#(V) ->
             c_33(U31^#(isNatIListKind(activate(V)), activate(V)))
       , 43: isNatIList^#(n__cons(V1, V2)) ->
             c_35(U41^#(and(isNatKind(activate(V1)),
                            n__isNatIListKind(activate(V2))),
                        activate(V1),
                        activate(V2)))
       , 44: U52^#(tt(), V2) -> c_37(U53^#(isNatList(activate(V2))))
       , 45: U62^#(tt(), V2) -> c_40(U63^#(isNatIList(activate(V2))))
       , 46: U71^#(tt(), L) -> c_42(s^#(length(activate(L))))
       , 47: U81^#(tt()) -> c_47(nil^#())
       , 48: U91^#(tt(), IL, M, N) ->
             c_49(cons^#(activate(N), n__take(activate(M), activate(IL))))
       , 49: zeros^#() -> c_2()
       , 50: 0^#() -> c_4()
       , 51: U12^#(tt()) -> c_6()
       , 52: isNatList^#(n__nil()) -> c_9()
       , 53: isNatIListKind^#(n__zeros()) -> c_53()
       , 54: isNatIListKind^#(n__nil()) -> c_56()
       , 55: nil^#() -> c_48()
       , 56: isNat^#(n__0()) -> c_25()
       , 57: isNatKind^#(n__0()) -> c_58()
       , 58: U22^#(tt()) -> c_23()
       , 59: U32^#(tt()) -> c_29()
       , 60: U43^#(tt()) -> c_32()
       , 61: isNatIList^#(n__zeros()) -> c_34()
       , 62: U53^#(tt()) -> c_38()
       , 63: U63^#(tt()) -> c_41() }
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { zeros^#() -> c_1(cons^#(0(), n__zeros()))
     , cons^#(X1, X2) -> c_3(X1, X2)
     , isNatList^#(n__take(V1, V2)) ->
       c_7(U61^#(and(isNatKind(activate(V1)),
                     n__isNatIListKind(activate(V2))),
                 activate(V1),
                 activate(V2)))
     , isNatList^#(n__cons(V1, V2)) ->
       c_8(U51^#(and(isNatKind(activate(V1)),
                     n__isNatIListKind(activate(V2))),
                 activate(V1),
                 activate(V2)))
     , U61^#(tt(), V1, V2) ->
       c_39(U62^#(isNat(activate(V1)), activate(V2)))
     , U51^#(tt(), V1, V2) ->
       c_36(U52^#(isNat(activate(V1)), activate(V2)))
     , activate^#(X) -> c_10(X)
     , activate^#(n__zeros()) -> c_11(zeros^#())
     , activate^#(n__take(X1, X2)) ->
       c_12(take^#(activate(X1), activate(X2)))
     , activate^#(n__length(X)) -> c_14(length^#(activate(X)))
     , activate^#(n__s(X)) -> c_15(s^#(activate(X)))
     , activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2))
     , activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X))
     , activate^#(n__and(X1, X2)) -> c_19(and^#(activate(X1), X2))
     , activate^#(n__isNat(X)) -> c_20(isNat^#(X))
     , activate^#(n__isNatKind(X)) -> c_21(isNatKind^#(X))
     , take^#(X1, X2) -> c_61(X1, X2)
     , take^#(0(), IL) ->
       c_62(U81^#(and(isNatIList(IL), n__isNatIListKind(IL))))
     , take^#(s(M), cons(N, IL)) ->
       c_63(U91^#(and(and(isNatIList(activate(IL)),
                          n__isNatIListKind(activate(IL))),
                      n__and(n__and(n__isNat(M), n__isNatKind(M)),
                             n__and(n__isNat(N), n__isNatKind(N)))),
                  activate(IL),
                  M,
                  N))
     , length^#(X) -> c_44(X)
     , length^#(cons(N, L)) ->
       c_45(U71^#(and(and(isNatList(activate(L)),
                          n__isNatIListKind(activate(L))),
                      n__and(n__isNat(N), n__isNatKind(N))),
                  activate(L)))
     , s^#(X) -> c_43(X)
     , isNatIListKind^#(X) -> c_52(X)
     , isNatIListKind^#(n__take(V1, V2)) ->
       c_54(and^#(isNatKind(activate(V1)),
                  n__isNatIListKind(activate(V2))))
     , isNatIListKind^#(n__cons(V1, V2)) ->
       c_55(and^#(isNatKind(activate(V1)),
                  n__isNatIListKind(activate(V2))))
     , and^#(X1, X2) -> c_50(X1, X2)
     , and^#(tt(), X) -> c_51(activate^#(X))
     , isNat^#(X) -> c_24(X)
     , isNat^#(n__length(V1)) ->
       c_26(U11^#(isNatIListKind(activate(V1)), activate(V1)))
     , isNat^#(n__s(V1)) ->
       c_27(U21^#(isNatKind(activate(V1)), activate(V1)))
     , isNatKind^#(X) -> c_57(X)
     , isNatKind^#(n__length(V1)) ->
       c_59(isNatIListKind^#(activate(V1)))
     , isNatKind^#(n__s(V1)) -> c_60(isNatKind^#(activate(V1)))
     , U41^#(tt(), V1, V2) ->
       c_30(U42^#(isNat(activate(V1)), activate(V2)))
     , isNatIList^#(V) ->
       c_33(U31^#(isNatIListKind(activate(V)), activate(V)))
     , isNatIList^#(n__cons(V1, V2)) ->
       c_35(U41^#(and(isNatKind(activate(V1)),
                      n__isNatIListKind(activate(V2))),
                  activate(V1),
                  activate(V2)))
     , U71^#(tt(), L) -> c_42(s^#(length(activate(L))))
     , U91^#(tt(), IL, M, N) ->
       c_49(cons^#(activate(N), n__take(activate(M), activate(IL)))) }
   Strict Trs:
     { zeros() -> cons(0(), n__zeros())
     , zeros() -> n__zeros()
     , cons(X1, X2) -> n__cons(X1, X2)
     , 0() -> n__0()
     , U11(tt(), V1) -> U12(isNatList(activate(V1)))
     , U12(tt()) -> tt()
     , isNatList(n__take(V1, V2)) ->
       U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
           activate(V1),
           activate(V2))
     , isNatList(n__cons(V1, V2)) ->
       U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
           activate(V1),
           activate(V2))
     , isNatList(n__nil()) -> tt()
     , activate(X) -> X
     , activate(n__zeros()) -> zeros()
     , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2))
     , activate(n__0()) -> 0()
     , activate(n__length(X)) -> length(activate(X))
     , activate(n__s(X)) -> s(activate(X))
     , activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
     , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
     , activate(n__nil()) -> nil()
     , activate(n__and(X1, X2)) -> and(activate(X1), X2)
     , activate(n__isNat(X)) -> isNat(X)
     , activate(n__isNatKind(X)) -> isNatKind(X)
     , U21(tt(), V1) -> U22(isNat(activate(V1)))
     , U22(tt()) -> tt()
     , isNat(X) -> n__isNat(X)
     , isNat(n__0()) -> tt()
     , isNat(n__length(V1)) ->
       U11(isNatIListKind(activate(V1)), activate(V1))
     , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
     , U31(tt(), V) -> U32(isNatList(activate(V)))
     , U32(tt()) -> tt()
     , U41(tt(), V1, V2) -> U42(isNat(activate(V1)), activate(V2))
     , U42(tt(), V2) -> U43(isNatIList(activate(V2)))
     , U43(tt()) -> tt()
     , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V))
     , isNatIList(n__zeros()) -> tt()
     , isNatIList(n__cons(V1, V2)) ->
       U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
           activate(V1),
           activate(V2))
     , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
     , U52(tt(), V2) -> U53(isNatList(activate(V2)))
     , U53(tt()) -> tt()
     , U61(tt(), V1, V2) -> U62(isNat(activate(V1)), activate(V2))
     , U62(tt(), V2) -> U63(isNatIList(activate(V2)))
     , U63(tt()) -> tt()
     , U71(tt(), L) -> s(length(activate(L)))
     , s(X) -> n__s(X)
     , length(X) -> n__length(X)
     , length(cons(N, L)) ->
       U71(and(and(isNatList(activate(L)),
                   n__isNatIListKind(activate(L))),
               n__and(n__isNat(N), n__isNatKind(N))),
           activate(L))
     , length(nil()) -> 0()
     , U81(tt()) -> nil()
     , nil() -> n__nil()
     , U91(tt(), IL, M, N) ->
       cons(activate(N), n__take(activate(M), activate(IL)))
     , and(X1, X2) -> n__and(X1, X2)
     , and(tt(), X) -> activate(X)
     , isNatIListKind(X) -> n__isNatIListKind(X)
     , isNatIListKind(n__zeros()) -> tt()
     , isNatIListKind(n__take(V1, V2)) ->
       and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
     , isNatIListKind(n__cons(V1, V2)) ->
       and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
     , isNatIListKind(n__nil()) -> tt()
     , isNatKind(X) -> n__isNatKind(X)
     , isNatKind(n__0()) -> tt()
     , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
     , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
     , take(X1, X2) -> n__take(X1, X2)
     , take(0(), IL) -> U81(and(isNatIList(IL), n__isNatIListKind(IL)))
     , take(s(M), cons(N, IL)) ->
       U91(and(and(isNatIList(activate(IL)),
                   n__isNatIListKind(activate(IL))),
               n__and(n__and(n__isNat(M), n__isNatKind(M)),
                      n__and(n__isNat(N), n__isNatKind(N)))),
           activate(IL),
           M,
           N) }
   Weak DPs:
     { zeros^#() -> c_2()
     , 0^#() -> c_4()
     , U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1))))
     , U12^#(tt()) -> c_6()
     , isNatList^#(n__nil()) -> c_9()
     , activate^#(n__0()) -> c_13(0^#())
     , activate^#(n__nil()) -> c_18(nil^#())
     , length^#(nil()) -> c_46(0^#())
     , isNatIListKind^#(n__zeros()) -> c_53()
     , isNatIListKind^#(n__nil()) -> c_56()
     , nil^#() -> c_48()
     , isNat^#(n__0()) -> c_25()
     , isNatKind^#(n__0()) -> c_58()
     , U21^#(tt(), V1) -> c_22(U22^#(isNat(activate(V1))))
     , U22^#(tt()) -> c_23()
     , U31^#(tt(), V) -> c_28(U32^#(isNatList(activate(V))))
     , U32^#(tt()) -> c_29()
     , U42^#(tt(), V2) -> c_31(U43^#(isNatIList(activate(V2))))
     , U43^#(tt()) -> c_32()
     , isNatIList^#(n__zeros()) -> c_34()
     , U52^#(tt(), V2) -> c_37(U53^#(isNatList(activate(V2))))
     , U53^#(tt()) -> c_38()
     , U62^#(tt(), V2) -> c_40(U63^#(isNatIList(activate(V2))))
     , U63^#(tt()) -> c_41()
     , U81^#(tt()) -> c_47(nil^#()) }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of {5,6,18,29,30,34,35} by
   applications of Pre({5,6,18,29,30,34,35}) =
   {2,3,4,7,9,15,17,20,22,23,26,28,31,36}. Here rules are labeled as
   follows:
   
     DPs:
       { 1: zeros^#() -> c_1(cons^#(0(), n__zeros()))
       , 2: cons^#(X1, X2) -> c_3(X1, X2)
       , 3: isNatList^#(n__take(V1, V2)) ->
            c_7(U61^#(and(isNatKind(activate(V1)),
                          n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2)))
       , 4: isNatList^#(n__cons(V1, V2)) ->
            c_8(U51^#(and(isNatKind(activate(V1)),
                          n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2)))
       , 5: U61^#(tt(), V1, V2) ->
            c_39(U62^#(isNat(activate(V1)), activate(V2)))
       , 6: U51^#(tt(), V1, V2) ->
            c_36(U52^#(isNat(activate(V1)), activate(V2)))
       , 7: activate^#(X) -> c_10(X)
       , 8: activate^#(n__zeros()) -> c_11(zeros^#())
       , 9: activate^#(n__take(X1, X2)) ->
            c_12(take^#(activate(X1), activate(X2)))
       , 10: activate^#(n__length(X)) -> c_14(length^#(activate(X)))
       , 11: activate^#(n__s(X)) -> c_15(s^#(activate(X)))
       , 12: activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2))
       , 13: activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X))
       , 14: activate^#(n__and(X1, X2)) -> c_19(and^#(activate(X1), X2))
       , 15: activate^#(n__isNat(X)) -> c_20(isNat^#(X))
       , 16: activate^#(n__isNatKind(X)) -> c_21(isNatKind^#(X))
       , 17: take^#(X1, X2) -> c_61(X1, X2)
       , 18: take^#(0(), IL) ->
             c_62(U81^#(and(isNatIList(IL), n__isNatIListKind(IL))))
       , 19: take^#(s(M), cons(N, IL)) ->
             c_63(U91^#(and(and(isNatIList(activate(IL)),
                                n__isNatIListKind(activate(IL))),
                            n__and(n__and(n__isNat(M), n__isNatKind(M)),
                                   n__and(n__isNat(N), n__isNatKind(N)))),
                        activate(IL),
                        M,
                        N))
       , 20: length^#(X) -> c_44(X)
       , 21: length^#(cons(N, L)) ->
             c_45(U71^#(and(and(isNatList(activate(L)),
                                n__isNatIListKind(activate(L))),
                            n__and(n__isNat(N), n__isNatKind(N))),
                        activate(L)))
       , 22: s^#(X) -> c_43(X)
       , 23: isNatIListKind^#(X) -> c_52(X)
       , 24: isNatIListKind^#(n__take(V1, V2)) ->
             c_54(and^#(isNatKind(activate(V1)),
                        n__isNatIListKind(activate(V2))))
       , 25: isNatIListKind^#(n__cons(V1, V2)) ->
             c_55(and^#(isNatKind(activate(V1)),
                        n__isNatIListKind(activate(V2))))
       , 26: and^#(X1, X2) -> c_50(X1, X2)
       , 27: and^#(tt(), X) -> c_51(activate^#(X))
       , 28: isNat^#(X) -> c_24(X)
       , 29: isNat^#(n__length(V1)) ->
             c_26(U11^#(isNatIListKind(activate(V1)), activate(V1)))
       , 30: isNat^#(n__s(V1)) ->
             c_27(U21^#(isNatKind(activate(V1)), activate(V1)))
       , 31: isNatKind^#(X) -> c_57(X)
       , 32: isNatKind^#(n__length(V1)) ->
             c_59(isNatIListKind^#(activate(V1)))
       , 33: isNatKind^#(n__s(V1)) -> c_60(isNatKind^#(activate(V1)))
       , 34: U41^#(tt(), V1, V2) ->
             c_30(U42^#(isNat(activate(V1)), activate(V2)))
       , 35: isNatIList^#(V) ->
             c_33(U31^#(isNatIListKind(activate(V)), activate(V)))
       , 36: isNatIList^#(n__cons(V1, V2)) ->
             c_35(U41^#(and(isNatKind(activate(V1)),
                            n__isNatIListKind(activate(V2))),
                        activate(V1),
                        activate(V2)))
       , 37: U71^#(tt(), L) -> c_42(s^#(length(activate(L))))
       , 38: U91^#(tt(), IL, M, N) ->
             c_49(cons^#(activate(N), n__take(activate(M), activate(IL))))
       , 39: zeros^#() -> c_2()
       , 40: 0^#() -> c_4()
       , 41: U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1))))
       , 42: U12^#(tt()) -> c_6()
       , 43: isNatList^#(n__nil()) -> c_9()
       , 44: activate^#(n__0()) -> c_13(0^#())
       , 45: activate^#(n__nil()) -> c_18(nil^#())
       , 46: length^#(nil()) -> c_46(0^#())
       , 47: isNatIListKind^#(n__zeros()) -> c_53()
       , 48: isNatIListKind^#(n__nil()) -> c_56()
       , 49: nil^#() -> c_48()
       , 50: isNat^#(n__0()) -> c_25()
       , 51: isNatKind^#(n__0()) -> c_58()
       , 52: U21^#(tt(), V1) -> c_22(U22^#(isNat(activate(V1))))
       , 53: U22^#(tt()) -> c_23()
       , 54: U31^#(tt(), V) -> c_28(U32^#(isNatList(activate(V))))
       , 55: U32^#(tt()) -> c_29()
       , 56: U42^#(tt(), V2) -> c_31(U43^#(isNatIList(activate(V2))))
       , 57: U43^#(tt()) -> c_32()
       , 58: isNatIList^#(n__zeros()) -> c_34()
       , 59: U52^#(tt(), V2) -> c_37(U53^#(isNatList(activate(V2))))
       , 60: U53^#(tt()) -> c_38()
       , 61: U62^#(tt(), V2) -> c_40(U63^#(isNatIList(activate(V2))))
       , 62: U63^#(tt()) -> c_41()
       , 63: U81^#(tt()) -> c_47(nil^#()) }
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { zeros^#() -> c_1(cons^#(0(), n__zeros()))
     , cons^#(X1, X2) -> c_3(X1, X2)
     , isNatList^#(n__take(V1, V2)) ->
       c_7(U61^#(and(isNatKind(activate(V1)),
                     n__isNatIListKind(activate(V2))),
                 activate(V1),
                 activate(V2)))
     , isNatList^#(n__cons(V1, V2)) ->
       c_8(U51^#(and(isNatKind(activate(V1)),
                     n__isNatIListKind(activate(V2))),
                 activate(V1),
                 activate(V2)))
     , activate^#(X) -> c_10(X)
     , activate^#(n__zeros()) -> c_11(zeros^#())
     , activate^#(n__take(X1, X2)) ->
       c_12(take^#(activate(X1), activate(X2)))
     , activate^#(n__length(X)) -> c_14(length^#(activate(X)))
     , activate^#(n__s(X)) -> c_15(s^#(activate(X)))
     , activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2))
     , activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X))
     , activate^#(n__and(X1, X2)) -> c_19(and^#(activate(X1), X2))
     , activate^#(n__isNat(X)) -> c_20(isNat^#(X))
     , activate^#(n__isNatKind(X)) -> c_21(isNatKind^#(X))
     , take^#(X1, X2) -> c_61(X1, X2)
     , take^#(s(M), cons(N, IL)) ->
       c_63(U91^#(and(and(isNatIList(activate(IL)),
                          n__isNatIListKind(activate(IL))),
                      n__and(n__and(n__isNat(M), n__isNatKind(M)),
                             n__and(n__isNat(N), n__isNatKind(N)))),
                  activate(IL),
                  M,
                  N))
     , length^#(X) -> c_44(X)
     , length^#(cons(N, L)) ->
       c_45(U71^#(and(and(isNatList(activate(L)),
                          n__isNatIListKind(activate(L))),
                      n__and(n__isNat(N), n__isNatKind(N))),
                  activate(L)))
     , s^#(X) -> c_43(X)
     , isNatIListKind^#(X) -> c_52(X)
     , isNatIListKind^#(n__take(V1, V2)) ->
       c_54(and^#(isNatKind(activate(V1)),
                  n__isNatIListKind(activate(V2))))
     , isNatIListKind^#(n__cons(V1, V2)) ->
       c_55(and^#(isNatKind(activate(V1)),
                  n__isNatIListKind(activate(V2))))
     , and^#(X1, X2) -> c_50(X1, X2)
     , and^#(tt(), X) -> c_51(activate^#(X))
     , isNat^#(X) -> c_24(X)
     , isNatKind^#(X) -> c_57(X)
     , isNatKind^#(n__length(V1)) ->
       c_59(isNatIListKind^#(activate(V1)))
     , isNatKind^#(n__s(V1)) -> c_60(isNatKind^#(activate(V1)))
     , isNatIList^#(n__cons(V1, V2)) ->
       c_35(U41^#(and(isNatKind(activate(V1)),
                      n__isNatIListKind(activate(V2))),
                  activate(V1),
                  activate(V2)))
     , U71^#(tt(), L) -> c_42(s^#(length(activate(L))))
     , U91^#(tt(), IL, M, N) ->
       c_49(cons^#(activate(N), n__take(activate(M), activate(IL)))) }
   Strict Trs:
     { zeros() -> cons(0(), n__zeros())
     , zeros() -> n__zeros()
     , cons(X1, X2) -> n__cons(X1, X2)
     , 0() -> n__0()
     , U11(tt(), V1) -> U12(isNatList(activate(V1)))
     , U12(tt()) -> tt()
     , isNatList(n__take(V1, V2)) ->
       U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
           activate(V1),
           activate(V2))
     , isNatList(n__cons(V1, V2)) ->
       U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
           activate(V1),
           activate(V2))
     , isNatList(n__nil()) -> tt()
     , activate(X) -> X
     , activate(n__zeros()) -> zeros()
     , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2))
     , activate(n__0()) -> 0()
     , activate(n__length(X)) -> length(activate(X))
     , activate(n__s(X)) -> s(activate(X))
     , activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
     , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
     , activate(n__nil()) -> nil()
     , activate(n__and(X1, X2)) -> and(activate(X1), X2)
     , activate(n__isNat(X)) -> isNat(X)
     , activate(n__isNatKind(X)) -> isNatKind(X)
     , U21(tt(), V1) -> U22(isNat(activate(V1)))
     , U22(tt()) -> tt()
     , isNat(X) -> n__isNat(X)
     , isNat(n__0()) -> tt()
     , isNat(n__length(V1)) ->
       U11(isNatIListKind(activate(V1)), activate(V1))
     , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
     , U31(tt(), V) -> U32(isNatList(activate(V)))
     , U32(tt()) -> tt()
     , U41(tt(), V1, V2) -> U42(isNat(activate(V1)), activate(V2))
     , U42(tt(), V2) -> U43(isNatIList(activate(V2)))
     , U43(tt()) -> tt()
     , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V))
     , isNatIList(n__zeros()) -> tt()
     , isNatIList(n__cons(V1, V2)) ->
       U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
           activate(V1),
           activate(V2))
     , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
     , U52(tt(), V2) -> U53(isNatList(activate(V2)))
     , U53(tt()) -> tt()
     , U61(tt(), V1, V2) -> U62(isNat(activate(V1)), activate(V2))
     , U62(tt(), V2) -> U63(isNatIList(activate(V2)))
     , U63(tt()) -> tt()
     , U71(tt(), L) -> s(length(activate(L)))
     , s(X) -> n__s(X)
     , length(X) -> n__length(X)
     , length(cons(N, L)) ->
       U71(and(and(isNatList(activate(L)),
                   n__isNatIListKind(activate(L))),
               n__and(n__isNat(N), n__isNatKind(N))),
           activate(L))
     , length(nil()) -> 0()
     , U81(tt()) -> nil()
     , nil() -> n__nil()
     , U91(tt(), IL, M, N) ->
       cons(activate(N), n__take(activate(M), activate(IL)))
     , and(X1, X2) -> n__and(X1, X2)
     , and(tt(), X) -> activate(X)
     , isNatIListKind(X) -> n__isNatIListKind(X)
     , isNatIListKind(n__zeros()) -> tt()
     , isNatIListKind(n__take(V1, V2)) ->
       and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
     , isNatIListKind(n__cons(V1, V2)) ->
       and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
     , isNatIListKind(n__nil()) -> tt()
     , isNatKind(X) -> n__isNatKind(X)
     , isNatKind(n__0()) -> tt()
     , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
     , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
     , take(X1, X2) -> n__take(X1, X2)
     , take(0(), IL) -> U81(and(isNatIList(IL), n__isNatIListKind(IL)))
     , take(s(M), cons(N, IL)) ->
       U91(and(and(isNatIList(activate(IL)),
                   n__isNatIListKind(activate(IL))),
               n__and(n__and(n__isNat(M), n__isNatKind(M)),
                      n__and(n__isNat(N), n__isNatKind(N)))),
           activate(IL),
           M,
           N) }
   Weak DPs:
     { zeros^#() -> c_2()
     , 0^#() -> c_4()
     , U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1))))
     , U12^#(tt()) -> c_6()
     , isNatList^#(n__nil()) -> c_9()
     , U61^#(tt(), V1, V2) ->
       c_39(U62^#(isNat(activate(V1)), activate(V2)))
     , U51^#(tt(), V1, V2) ->
       c_36(U52^#(isNat(activate(V1)), activate(V2)))
     , activate^#(n__0()) -> c_13(0^#())
     , activate^#(n__nil()) -> c_18(nil^#())
     , take^#(0(), IL) ->
       c_62(U81^#(and(isNatIList(IL), n__isNatIListKind(IL))))
     , length^#(nil()) -> c_46(0^#())
     , isNatIListKind^#(n__zeros()) -> c_53()
     , isNatIListKind^#(n__nil()) -> c_56()
     , nil^#() -> c_48()
     , isNat^#(n__0()) -> c_25()
     , isNat^#(n__length(V1)) ->
       c_26(U11^#(isNatIListKind(activate(V1)), activate(V1)))
     , isNat^#(n__s(V1)) ->
       c_27(U21^#(isNatKind(activate(V1)), activate(V1)))
     , isNatKind^#(n__0()) -> c_58()
     , U21^#(tt(), V1) -> c_22(U22^#(isNat(activate(V1))))
     , U22^#(tt()) -> c_23()
     , U31^#(tt(), V) -> c_28(U32^#(isNatList(activate(V))))
     , U32^#(tt()) -> c_29()
     , U41^#(tt(), V1, V2) ->
       c_30(U42^#(isNat(activate(V1)), activate(V2)))
     , U42^#(tt(), V2) -> c_31(U43^#(isNatIList(activate(V2))))
     , U43^#(tt()) -> c_32()
     , isNatIList^#(V) ->
       c_33(U31^#(isNatIListKind(activate(V)), activate(V)))
     , isNatIList^#(n__zeros()) -> c_34()
     , U52^#(tt(), V2) -> c_37(U53^#(isNatList(activate(V2))))
     , U53^#(tt()) -> c_38()
     , U62^#(tt(), V2) -> c_40(U63^#(isNatIList(activate(V2))))
     , U63^#(tt()) -> c_41()
     , U81^#(tt()) -> c_47(nil^#()) }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of {3,4,29} by applications
   of Pre({3,4,29}) = {2,5,15,17,19,20,23,25,26}. Here rules are
   labeled as follows:
   
     DPs:
       { 1: zeros^#() -> c_1(cons^#(0(), n__zeros()))
       , 2: cons^#(X1, X2) -> c_3(X1, X2)
       , 3: isNatList^#(n__take(V1, V2)) ->
            c_7(U61^#(and(isNatKind(activate(V1)),
                          n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2)))
       , 4: isNatList^#(n__cons(V1, V2)) ->
            c_8(U51^#(and(isNatKind(activate(V1)),
                          n__isNatIListKind(activate(V2))),
                      activate(V1),
                      activate(V2)))
       , 5: activate^#(X) -> c_10(X)
       , 6: activate^#(n__zeros()) -> c_11(zeros^#())
       , 7: activate^#(n__take(X1, X2)) ->
            c_12(take^#(activate(X1), activate(X2)))
       , 8: activate^#(n__length(X)) -> c_14(length^#(activate(X)))
       , 9: activate^#(n__s(X)) -> c_15(s^#(activate(X)))
       , 10: activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2))
       , 11: activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X))
       , 12: activate^#(n__and(X1, X2)) -> c_19(and^#(activate(X1), X2))
       , 13: activate^#(n__isNat(X)) -> c_20(isNat^#(X))
       , 14: activate^#(n__isNatKind(X)) -> c_21(isNatKind^#(X))
       , 15: take^#(X1, X2) -> c_61(X1, X2)
       , 16: take^#(s(M), cons(N, IL)) ->
             c_63(U91^#(and(and(isNatIList(activate(IL)),
                                n__isNatIListKind(activate(IL))),
                            n__and(n__and(n__isNat(M), n__isNatKind(M)),
                                   n__and(n__isNat(N), n__isNatKind(N)))),
                        activate(IL),
                        M,
                        N))
       , 17: length^#(X) -> c_44(X)
       , 18: length^#(cons(N, L)) ->
             c_45(U71^#(and(and(isNatList(activate(L)),
                                n__isNatIListKind(activate(L))),
                            n__and(n__isNat(N), n__isNatKind(N))),
                        activate(L)))
       , 19: s^#(X) -> c_43(X)
       , 20: isNatIListKind^#(X) -> c_52(X)
       , 21: isNatIListKind^#(n__take(V1, V2)) ->
             c_54(and^#(isNatKind(activate(V1)),
                        n__isNatIListKind(activate(V2))))
       , 22: isNatIListKind^#(n__cons(V1, V2)) ->
             c_55(and^#(isNatKind(activate(V1)),
                        n__isNatIListKind(activate(V2))))
       , 23: and^#(X1, X2) -> c_50(X1, X2)
       , 24: and^#(tt(), X) -> c_51(activate^#(X))
       , 25: isNat^#(X) -> c_24(X)
       , 26: isNatKind^#(X) -> c_57(X)
       , 27: isNatKind^#(n__length(V1)) ->
             c_59(isNatIListKind^#(activate(V1)))
       , 28: isNatKind^#(n__s(V1)) -> c_60(isNatKind^#(activate(V1)))
       , 29: isNatIList^#(n__cons(V1, V2)) ->
             c_35(U41^#(and(isNatKind(activate(V1)),
                            n__isNatIListKind(activate(V2))),
                        activate(V1),
                        activate(V2)))
       , 30: U71^#(tt(), L) -> c_42(s^#(length(activate(L))))
       , 31: U91^#(tt(), IL, M, N) ->
             c_49(cons^#(activate(N), n__take(activate(M), activate(IL))))
       , 32: zeros^#() -> c_2()
       , 33: 0^#() -> c_4()
       , 34: U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1))))
       , 35: U12^#(tt()) -> c_6()
       , 36: isNatList^#(n__nil()) -> c_9()
       , 37: U61^#(tt(), V1, V2) ->
             c_39(U62^#(isNat(activate(V1)), activate(V2)))
       , 38: U51^#(tt(), V1, V2) ->
             c_36(U52^#(isNat(activate(V1)), activate(V2)))
       , 39: activate^#(n__0()) -> c_13(0^#())
       , 40: activate^#(n__nil()) -> c_18(nil^#())
       , 41: take^#(0(), IL) ->
             c_62(U81^#(and(isNatIList(IL), n__isNatIListKind(IL))))
       , 42: length^#(nil()) -> c_46(0^#())
       , 43: isNatIListKind^#(n__zeros()) -> c_53()
       , 44: isNatIListKind^#(n__nil()) -> c_56()
       , 45: nil^#() -> c_48()
       , 46: isNat^#(n__0()) -> c_25()
       , 47: isNat^#(n__length(V1)) ->
             c_26(U11^#(isNatIListKind(activate(V1)), activate(V1)))
       , 48: isNat^#(n__s(V1)) ->
             c_27(U21^#(isNatKind(activate(V1)), activate(V1)))
       , 49: isNatKind^#(n__0()) -> c_58()
       , 50: U21^#(tt(), V1) -> c_22(U22^#(isNat(activate(V1))))
       , 51: U22^#(tt()) -> c_23()
       , 52: U31^#(tt(), V) -> c_28(U32^#(isNatList(activate(V))))
       , 53: U32^#(tt()) -> c_29()
       , 54: U41^#(tt(), V1, V2) ->
             c_30(U42^#(isNat(activate(V1)), activate(V2)))
       , 55: U42^#(tt(), V2) -> c_31(U43^#(isNatIList(activate(V2))))
       , 56: U43^#(tt()) -> c_32()
       , 57: isNatIList^#(V) ->
             c_33(U31^#(isNatIListKind(activate(V)), activate(V)))
       , 58: isNatIList^#(n__zeros()) -> c_34()
       , 59: U52^#(tt(), V2) -> c_37(U53^#(isNatList(activate(V2))))
       , 60: U53^#(tt()) -> c_38()
       , 61: U62^#(tt(), V2) -> c_40(U63^#(isNatIList(activate(V2))))
       , 62: U63^#(tt()) -> c_41()
       , 63: U81^#(tt()) -> c_47(nil^#()) }
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { zeros^#() -> c_1(cons^#(0(), n__zeros()))
     , cons^#(X1, X2) -> c_3(X1, X2)
     , activate^#(X) -> c_10(X)
     , activate^#(n__zeros()) -> c_11(zeros^#())
     , activate^#(n__take(X1, X2)) ->
       c_12(take^#(activate(X1), activate(X2)))
     , activate^#(n__length(X)) -> c_14(length^#(activate(X)))
     , activate^#(n__s(X)) -> c_15(s^#(activate(X)))
     , activate^#(n__cons(X1, X2)) -> c_16(cons^#(activate(X1), X2))
     , activate^#(n__isNatIListKind(X)) -> c_17(isNatIListKind^#(X))
     , activate^#(n__and(X1, X2)) -> c_19(and^#(activate(X1), X2))
     , activate^#(n__isNat(X)) -> c_20(isNat^#(X))
     , activate^#(n__isNatKind(X)) -> c_21(isNatKind^#(X))
     , take^#(X1, X2) -> c_61(X1, X2)
     , take^#(s(M), cons(N, IL)) ->
       c_63(U91^#(and(and(isNatIList(activate(IL)),
                          n__isNatIListKind(activate(IL))),
                      n__and(n__and(n__isNat(M), n__isNatKind(M)),
                             n__and(n__isNat(N), n__isNatKind(N)))),
                  activate(IL),
                  M,
                  N))
     , length^#(X) -> c_44(X)
     , length^#(cons(N, L)) ->
       c_45(U71^#(and(and(isNatList(activate(L)),
                          n__isNatIListKind(activate(L))),
                      n__and(n__isNat(N), n__isNatKind(N))),
                  activate(L)))
     , s^#(X) -> c_43(X)
     , isNatIListKind^#(X) -> c_52(X)
     , isNatIListKind^#(n__take(V1, V2)) ->
       c_54(and^#(isNatKind(activate(V1)),
                  n__isNatIListKind(activate(V2))))
     , isNatIListKind^#(n__cons(V1, V2)) ->
       c_55(and^#(isNatKind(activate(V1)),
                  n__isNatIListKind(activate(V2))))
     , and^#(X1, X2) -> c_50(X1, X2)
     , and^#(tt(), X) -> c_51(activate^#(X))
     , isNat^#(X) -> c_24(X)
     , isNatKind^#(X) -> c_57(X)
     , isNatKind^#(n__length(V1)) ->
       c_59(isNatIListKind^#(activate(V1)))
     , isNatKind^#(n__s(V1)) -> c_60(isNatKind^#(activate(V1)))
     , U71^#(tt(), L) -> c_42(s^#(length(activate(L))))
     , U91^#(tt(), IL, M, N) ->
       c_49(cons^#(activate(N), n__take(activate(M), activate(IL)))) }
   Strict Trs:
     { zeros() -> cons(0(), n__zeros())
     , zeros() -> n__zeros()
     , cons(X1, X2) -> n__cons(X1, X2)
     , 0() -> n__0()
     , U11(tt(), V1) -> U12(isNatList(activate(V1)))
     , U12(tt()) -> tt()
     , isNatList(n__take(V1, V2)) ->
       U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
           activate(V1),
           activate(V2))
     , isNatList(n__cons(V1, V2)) ->
       U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
           activate(V1),
           activate(V2))
     , isNatList(n__nil()) -> tt()
     , activate(X) -> X
     , activate(n__zeros()) -> zeros()
     , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2))
     , activate(n__0()) -> 0()
     , activate(n__length(X)) -> length(activate(X))
     , activate(n__s(X)) -> s(activate(X))
     , activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
     , activate(n__isNatIListKind(X)) -> isNatIListKind(X)
     , activate(n__nil()) -> nil()
     , activate(n__and(X1, X2)) -> and(activate(X1), X2)
     , activate(n__isNat(X)) -> isNat(X)
     , activate(n__isNatKind(X)) -> isNatKind(X)
     , U21(tt(), V1) -> U22(isNat(activate(V1)))
     , U22(tt()) -> tt()
     , isNat(X) -> n__isNat(X)
     , isNat(n__0()) -> tt()
     , isNat(n__length(V1)) ->
       U11(isNatIListKind(activate(V1)), activate(V1))
     , isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1))
     , U31(tt(), V) -> U32(isNatList(activate(V)))
     , U32(tt()) -> tt()
     , U41(tt(), V1, V2) -> U42(isNat(activate(V1)), activate(V2))
     , U42(tt(), V2) -> U43(isNatIList(activate(V2)))
     , U43(tt()) -> tt()
     , isNatIList(V) -> U31(isNatIListKind(activate(V)), activate(V))
     , isNatIList(n__zeros()) -> tt()
     , isNatIList(n__cons(V1, V2)) ->
       U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))),
           activate(V1),
           activate(V2))
     , U51(tt(), V1, V2) -> U52(isNat(activate(V1)), activate(V2))
     , U52(tt(), V2) -> U53(isNatList(activate(V2)))
     , U53(tt()) -> tt()
     , U61(tt(), V1, V2) -> U62(isNat(activate(V1)), activate(V2))
     , U62(tt(), V2) -> U63(isNatIList(activate(V2)))
     , U63(tt()) -> tt()
     , U71(tt(), L) -> s(length(activate(L)))
     , s(X) -> n__s(X)
     , length(X) -> n__length(X)
     , length(cons(N, L)) ->
       U71(and(and(isNatList(activate(L)),
                   n__isNatIListKind(activate(L))),
               n__and(n__isNat(N), n__isNatKind(N))),
           activate(L))
     , length(nil()) -> 0()
     , U81(tt()) -> nil()
     , nil() -> n__nil()
     , U91(tt(), IL, M, N) ->
       cons(activate(N), n__take(activate(M), activate(IL)))
     , and(X1, X2) -> n__and(X1, X2)
     , and(tt(), X) -> activate(X)
     , isNatIListKind(X) -> n__isNatIListKind(X)
     , isNatIListKind(n__zeros()) -> tt()
     , isNatIListKind(n__take(V1, V2)) ->
       and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
     , isNatIListKind(n__cons(V1, V2)) ->
       and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2)))
     , isNatIListKind(n__nil()) -> tt()
     , isNatKind(X) -> n__isNatKind(X)
     , isNatKind(n__0()) -> tt()
     , isNatKind(n__length(V1)) -> isNatIListKind(activate(V1))
     , isNatKind(n__s(V1)) -> isNatKind(activate(V1))
     , take(X1, X2) -> n__take(X1, X2)
     , take(0(), IL) -> U81(and(isNatIList(IL), n__isNatIListKind(IL)))
     , take(s(M), cons(N, IL)) ->
       U91(and(and(isNatIList(activate(IL)),
                   n__isNatIListKind(activate(IL))),
               n__and(n__and(n__isNat(M), n__isNatKind(M)),
                      n__and(n__isNat(N), n__isNatKind(N)))),
           activate(IL),
           M,
           N) }
   Weak DPs:
     { zeros^#() -> c_2()
     , 0^#() -> c_4()
     , U11^#(tt(), V1) -> c_5(U12^#(isNatList(activate(V1))))
     , U12^#(tt()) -> c_6()
     , isNatList^#(n__take(V1, V2)) ->
       c_7(U61^#(and(isNatKind(activate(V1)),
                     n__isNatIListKind(activate(V2))),
                 activate(V1),
                 activate(V2)))
     , isNatList^#(n__cons(V1, V2)) ->
       c_8(U51^#(and(isNatKind(activate(V1)),
                     n__isNatIListKind(activate(V2))),
                 activate(V1),
                 activate(V2)))
     , isNatList^#(n__nil()) -> c_9()
     , U61^#(tt(), V1, V2) ->
       c_39(U62^#(isNat(activate(V1)), activate(V2)))
     , U51^#(tt(), V1, V2) ->
       c_36(U52^#(isNat(activate(V1)), activate(V2)))
     , activate^#(n__0()) -> c_13(0^#())
     , activate^#(n__nil()) -> c_18(nil^#())
     , take^#(0(), IL) ->
       c_62(U81^#(and(isNatIList(IL), n__isNatIListKind(IL))))
     , length^#(nil()) -> c_46(0^#())
     , isNatIListKind^#(n__zeros()) -> c_53()
     , isNatIListKind^#(n__nil()) -> c_56()
     , nil^#() -> c_48()
     , isNat^#(n__0()) -> c_25()
     , isNat^#(n__length(V1)) ->
       c_26(U11^#(isNatIListKind(activate(V1)), activate(V1)))
     , isNat^#(n__s(V1)) ->
       c_27(U21^#(isNatKind(activate(V1)), activate(V1)))
     , isNatKind^#(n__0()) -> c_58()
     , U21^#(tt(), V1) -> c_22(U22^#(isNat(activate(V1))))
     , U22^#(tt()) -> c_23()
     , U31^#(tt(), V) -> c_28(U32^#(isNatList(activate(V))))
     , U32^#(tt()) -> c_29()
     , U41^#(tt(), V1, V2) ->
       c_30(U42^#(isNat(activate(V1)), activate(V2)))
     , U42^#(tt(), V2) -> c_31(U43^#(isNatIList(activate(V2))))
     , U43^#(tt()) -> c_32()
     , isNatIList^#(V) ->
       c_33(U31^#(isNatIListKind(activate(V)), activate(V)))
     , isNatIList^#(n__zeros()) -> c_34()
     , isNatIList^#(n__cons(V1, V2)) ->
       c_35(U41^#(and(isNatKind(activate(V1)),
                      n__isNatIListKind(activate(V2))),
                  activate(V1),
                  activate(V2)))
     , U52^#(tt(), V2) -> c_37(U53^#(isNatList(activate(V2))))
     , U53^#(tt()) -> c_38()
     , U62^#(tt(), V2) -> c_40(U63^#(isNatIList(activate(V2))))
     , U63^#(tt()) -> c_41()
     , U81^#(tt()) -> c_47(nil^#()) }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   Empty strict component of the problem is NOT empty.


Arrrr..