MAYBE

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

Strict Trs:
  { a__zeros() -> cons(0(), zeros())
  , a__zeros() -> zeros()
  , a__U11(X1, X2) -> U11(X1, X2)
  , a__U11(tt(), L) -> s(a__length(mark(L)))
  , a__length(X) -> length(X)
  , a__length(cons(N, L)) ->
    a__U11(a__and(a__isNatList(L), isNat(N)), L)
  , a__length(nil()) -> 0()
  , mark(cons(X1, X2)) -> cons(mark(X1), X2)
  , mark(0()) -> 0()
  , mark(zeros()) -> a__zeros()
  , mark(tt()) -> tt()
  , mark(s(X)) -> s(mark(X))
  , mark(nil()) -> nil()
  , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2))
  , mark(length(X)) -> a__length(mark(X))
  , mark(isNatIList(X)) -> a__isNatIList(X)
  , mark(isNatList(X)) -> a__isNatList(X)
  , mark(isNat(X)) -> a__isNat(X)
  , mark(and(X1, X2)) -> a__and(mark(X1), X2)
  , mark(U11(X1, X2)) -> a__U11(mark(X1), X2)
  , mark(U21(X)) -> a__U21(mark(X))
  , mark(U31(X1, X2, X3, X4)) -> a__U31(mark(X1), X2, X3, X4)
  , a__U21(X) -> U21(X)
  , a__U21(tt()) -> nil()
  , a__U31(X1, X2, X3, X4) -> U31(X1, X2, X3, X4)
  , a__U31(tt(), IL, M, N) -> cons(mark(N), take(M, IL))
  , a__and(X1, X2) -> and(X1, X2)
  , a__and(tt(), X) -> mark(X)
  , a__isNat(X) -> isNat(X)
  , a__isNat(0()) -> tt()
  , a__isNat(s(V1)) -> a__isNat(V1)
  , a__isNat(length(V1)) -> a__isNatList(V1)
  , a__isNatList(X) -> isNatList(X)
  , a__isNatList(cons(V1, V2)) -> a__and(a__isNat(V1), isNatList(V2))
  , a__isNatList(nil()) -> tt()
  , a__isNatList(take(V1, V2)) ->
    a__and(a__isNat(V1), isNatIList(V2))
  , a__isNatIList(V) -> a__isNatList(V)
  , a__isNatIList(X) -> isNatIList(X)
  , a__isNatIList(cons(V1, V2)) ->
    a__and(a__isNat(V1), isNatIList(V2))
  , a__isNatIList(zeros()) -> tt()
  , a__take(X1, X2) -> take(X1, X2)
  , a__take(0(), IL) -> a__U21(a__isNatIList(IL))
  , a__take(s(M), cons(N, IL)) ->
    a__U31(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))),
           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) '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) '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) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed
   due to the following reason:
   
   We add the following weak dependency pairs:
   
   Strict DPs:
     { a__zeros^#() -> c_1()
     , a__zeros^#() -> c_2()
     , a__U11^#(X1, X2) -> c_3(X1, X2)
     , a__U11^#(tt(), L) -> c_4(a__length^#(mark(L)))
     , a__length^#(X) -> c_5(X)
     , a__length^#(cons(N, L)) ->
       c_6(a__U11^#(a__and(a__isNatList(L), isNat(N)), L))
     , a__length^#(nil()) -> c_7()
     , mark^#(cons(X1, X2)) -> c_8(mark^#(X1), X2)
     , mark^#(0()) -> c_9()
     , mark^#(zeros()) -> c_10(a__zeros^#())
     , mark^#(tt()) -> c_11()
     , mark^#(s(X)) -> c_12(mark^#(X))
     , mark^#(nil()) -> c_13()
     , mark^#(take(X1, X2)) -> c_14(a__take^#(mark(X1), mark(X2)))
     , mark^#(length(X)) -> c_15(a__length^#(mark(X)))
     , mark^#(isNatIList(X)) -> c_16(a__isNatIList^#(X))
     , mark^#(isNatList(X)) -> c_17(a__isNatList^#(X))
     , mark^#(isNat(X)) -> c_18(a__isNat^#(X))
     , mark^#(and(X1, X2)) -> c_19(a__and^#(mark(X1), X2))
     , mark^#(U11(X1, X2)) -> c_20(a__U11^#(mark(X1), X2))
     , mark^#(U21(X)) -> c_21(a__U21^#(mark(X)))
     , mark^#(U31(X1, X2, X3, X4)) ->
       c_22(a__U31^#(mark(X1), X2, X3, X4))
     , a__take^#(X1, X2) -> c_41(X1, X2)
     , a__take^#(0(), IL) -> c_42(a__U21^#(a__isNatIList(IL)))
     , a__take^#(s(M), cons(N, IL)) ->
       c_43(a__U31^#(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))),
                     IL,
                     M,
                     N))
     , a__isNatIList^#(V) -> c_37(a__isNatList^#(V))
     , a__isNatIList^#(X) -> c_38(X)
     , a__isNatIList^#(cons(V1, V2)) ->
       c_39(a__and^#(a__isNat(V1), isNatIList(V2)))
     , a__isNatIList^#(zeros()) -> c_40()
     , a__isNatList^#(X) -> c_33(X)
     , a__isNatList^#(cons(V1, V2)) ->
       c_34(a__and^#(a__isNat(V1), isNatList(V2)))
     , a__isNatList^#(nil()) -> c_35()
     , a__isNatList^#(take(V1, V2)) ->
       c_36(a__and^#(a__isNat(V1), isNatIList(V2)))
     , a__isNat^#(X) -> c_29(X)
     , a__isNat^#(0()) -> c_30()
     , a__isNat^#(s(V1)) -> c_31(a__isNat^#(V1))
     , a__isNat^#(length(V1)) -> c_32(a__isNatList^#(V1))
     , a__and^#(X1, X2) -> c_27(X1, X2)
     , a__and^#(tt(), X) -> c_28(mark^#(X))
     , a__U21^#(X) -> c_23(X)
     , a__U21^#(tt()) -> c_24()
     , a__U31^#(X1, X2, X3, X4) -> c_25(X1, X2, X3, X4)
     , a__U31^#(tt(), IL, M, N) -> c_26(mark^#(N), M, IL) }
   
   and mark the set of starting terms.
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { a__zeros^#() -> c_1()
     , a__zeros^#() -> c_2()
     , a__U11^#(X1, X2) -> c_3(X1, X2)
     , a__U11^#(tt(), L) -> c_4(a__length^#(mark(L)))
     , a__length^#(X) -> c_5(X)
     , a__length^#(cons(N, L)) ->
       c_6(a__U11^#(a__and(a__isNatList(L), isNat(N)), L))
     , a__length^#(nil()) -> c_7()
     , mark^#(cons(X1, X2)) -> c_8(mark^#(X1), X2)
     , mark^#(0()) -> c_9()
     , mark^#(zeros()) -> c_10(a__zeros^#())
     , mark^#(tt()) -> c_11()
     , mark^#(s(X)) -> c_12(mark^#(X))
     , mark^#(nil()) -> c_13()
     , mark^#(take(X1, X2)) -> c_14(a__take^#(mark(X1), mark(X2)))
     , mark^#(length(X)) -> c_15(a__length^#(mark(X)))
     , mark^#(isNatIList(X)) -> c_16(a__isNatIList^#(X))
     , mark^#(isNatList(X)) -> c_17(a__isNatList^#(X))
     , mark^#(isNat(X)) -> c_18(a__isNat^#(X))
     , mark^#(and(X1, X2)) -> c_19(a__and^#(mark(X1), X2))
     , mark^#(U11(X1, X2)) -> c_20(a__U11^#(mark(X1), X2))
     , mark^#(U21(X)) -> c_21(a__U21^#(mark(X)))
     , mark^#(U31(X1, X2, X3, X4)) ->
       c_22(a__U31^#(mark(X1), X2, X3, X4))
     , a__take^#(X1, X2) -> c_41(X1, X2)
     , a__take^#(0(), IL) -> c_42(a__U21^#(a__isNatIList(IL)))
     , a__take^#(s(M), cons(N, IL)) ->
       c_43(a__U31^#(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))),
                     IL,
                     M,
                     N))
     , a__isNatIList^#(V) -> c_37(a__isNatList^#(V))
     , a__isNatIList^#(X) -> c_38(X)
     , a__isNatIList^#(cons(V1, V2)) ->
       c_39(a__and^#(a__isNat(V1), isNatIList(V2)))
     , a__isNatIList^#(zeros()) -> c_40()
     , a__isNatList^#(X) -> c_33(X)
     , a__isNatList^#(cons(V1, V2)) ->
       c_34(a__and^#(a__isNat(V1), isNatList(V2)))
     , a__isNatList^#(nil()) -> c_35()
     , a__isNatList^#(take(V1, V2)) ->
       c_36(a__and^#(a__isNat(V1), isNatIList(V2)))
     , a__isNat^#(X) -> c_29(X)
     , a__isNat^#(0()) -> c_30()
     , a__isNat^#(s(V1)) -> c_31(a__isNat^#(V1))
     , a__isNat^#(length(V1)) -> c_32(a__isNatList^#(V1))
     , a__and^#(X1, X2) -> c_27(X1, X2)
     , a__and^#(tt(), X) -> c_28(mark^#(X))
     , a__U21^#(X) -> c_23(X)
     , a__U21^#(tt()) -> c_24()
     , a__U31^#(X1, X2, X3, X4) -> c_25(X1, X2, X3, X4)
     , a__U31^#(tt(), IL, M, N) -> c_26(mark^#(N), M, IL) }
   Strict Trs:
     { a__zeros() -> cons(0(), zeros())
     , a__zeros() -> zeros()
     , a__U11(X1, X2) -> U11(X1, X2)
     , a__U11(tt(), L) -> s(a__length(mark(L)))
     , a__length(X) -> length(X)
     , a__length(cons(N, L)) ->
       a__U11(a__and(a__isNatList(L), isNat(N)), L)
     , a__length(nil()) -> 0()
     , mark(cons(X1, X2)) -> cons(mark(X1), X2)
     , mark(0()) -> 0()
     , mark(zeros()) -> a__zeros()
     , mark(tt()) -> tt()
     , mark(s(X)) -> s(mark(X))
     , mark(nil()) -> nil()
     , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2))
     , mark(length(X)) -> a__length(mark(X))
     , mark(isNatIList(X)) -> a__isNatIList(X)
     , mark(isNatList(X)) -> a__isNatList(X)
     , mark(isNat(X)) -> a__isNat(X)
     , mark(and(X1, X2)) -> a__and(mark(X1), X2)
     , mark(U11(X1, X2)) -> a__U11(mark(X1), X2)
     , mark(U21(X)) -> a__U21(mark(X))
     , mark(U31(X1, X2, X3, X4)) -> a__U31(mark(X1), X2, X3, X4)
     , a__U21(X) -> U21(X)
     , a__U21(tt()) -> nil()
     , a__U31(X1, X2, X3, X4) -> U31(X1, X2, X3, X4)
     , a__U31(tt(), IL, M, N) -> cons(mark(N), take(M, IL))
     , a__and(X1, X2) -> and(X1, X2)
     , a__and(tt(), X) -> mark(X)
     , a__isNat(X) -> isNat(X)
     , a__isNat(0()) -> tt()
     , a__isNat(s(V1)) -> a__isNat(V1)
     , a__isNat(length(V1)) -> a__isNatList(V1)
     , a__isNatList(X) -> isNatList(X)
     , a__isNatList(cons(V1, V2)) -> a__and(a__isNat(V1), isNatList(V2))
     , a__isNatList(nil()) -> tt()
     , a__isNatList(take(V1, V2)) ->
       a__and(a__isNat(V1), isNatIList(V2))
     , a__isNatIList(V) -> a__isNatList(V)
     , a__isNatIList(X) -> isNatIList(X)
     , a__isNatIList(cons(V1, V2)) ->
       a__and(a__isNat(V1), isNatIList(V2))
     , a__isNatIList(zeros()) -> tt()
     , a__take(X1, X2) -> take(X1, X2)
     , a__take(0(), IL) -> a__U21(a__isNatIList(IL))
     , a__take(s(M), cons(N, IL)) ->
       a__U31(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))),
              IL,
              M,
              N) }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of
   {1,2,7,9,11,13,29,32,35,41} by applications of
   Pre({1,2,7,9,11,13,29,32,35,41}) =
   {3,4,5,8,10,12,15,16,17,18,21,23,24,26,27,30,34,36,37,38,39,40,42,43}.
   Here rules are labeled as follows:
   
     DPs:
       { 1: a__zeros^#() -> c_1()
       , 2: a__zeros^#() -> c_2()
       , 3: a__U11^#(X1, X2) -> c_3(X1, X2)
       , 4: a__U11^#(tt(), L) -> c_4(a__length^#(mark(L)))
       , 5: a__length^#(X) -> c_5(X)
       , 6: a__length^#(cons(N, L)) ->
            c_6(a__U11^#(a__and(a__isNatList(L), isNat(N)), L))
       , 7: a__length^#(nil()) -> c_7()
       , 8: mark^#(cons(X1, X2)) -> c_8(mark^#(X1), X2)
       , 9: mark^#(0()) -> c_9()
       , 10: mark^#(zeros()) -> c_10(a__zeros^#())
       , 11: mark^#(tt()) -> c_11()
       , 12: mark^#(s(X)) -> c_12(mark^#(X))
       , 13: mark^#(nil()) -> c_13()
       , 14: mark^#(take(X1, X2)) -> c_14(a__take^#(mark(X1), mark(X2)))
       , 15: mark^#(length(X)) -> c_15(a__length^#(mark(X)))
       , 16: mark^#(isNatIList(X)) -> c_16(a__isNatIList^#(X))
       , 17: mark^#(isNatList(X)) -> c_17(a__isNatList^#(X))
       , 18: mark^#(isNat(X)) -> c_18(a__isNat^#(X))
       , 19: mark^#(and(X1, X2)) -> c_19(a__and^#(mark(X1), X2))
       , 20: mark^#(U11(X1, X2)) -> c_20(a__U11^#(mark(X1), X2))
       , 21: mark^#(U21(X)) -> c_21(a__U21^#(mark(X)))
       , 22: mark^#(U31(X1, X2, X3, X4)) ->
             c_22(a__U31^#(mark(X1), X2, X3, X4))
       , 23: a__take^#(X1, X2) -> c_41(X1, X2)
       , 24: a__take^#(0(), IL) -> c_42(a__U21^#(a__isNatIList(IL)))
       , 25: a__take^#(s(M), cons(N, IL)) ->
             c_43(a__U31^#(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))),
                           IL,
                           M,
                           N))
       , 26: a__isNatIList^#(V) -> c_37(a__isNatList^#(V))
       , 27: a__isNatIList^#(X) -> c_38(X)
       , 28: a__isNatIList^#(cons(V1, V2)) ->
             c_39(a__and^#(a__isNat(V1), isNatIList(V2)))
       , 29: a__isNatIList^#(zeros()) -> c_40()
       , 30: a__isNatList^#(X) -> c_33(X)
       , 31: a__isNatList^#(cons(V1, V2)) ->
             c_34(a__and^#(a__isNat(V1), isNatList(V2)))
       , 32: a__isNatList^#(nil()) -> c_35()
       , 33: a__isNatList^#(take(V1, V2)) ->
             c_36(a__and^#(a__isNat(V1), isNatIList(V2)))
       , 34: a__isNat^#(X) -> c_29(X)
       , 35: a__isNat^#(0()) -> c_30()
       , 36: a__isNat^#(s(V1)) -> c_31(a__isNat^#(V1))
       , 37: a__isNat^#(length(V1)) -> c_32(a__isNatList^#(V1))
       , 38: a__and^#(X1, X2) -> c_27(X1, X2)
       , 39: a__and^#(tt(), X) -> c_28(mark^#(X))
       , 40: a__U21^#(X) -> c_23(X)
       , 41: a__U21^#(tt()) -> c_24()
       , 42: a__U31^#(X1, X2, X3, X4) -> c_25(X1, X2, X3, X4)
       , 43: a__U31^#(tt(), IL, M, N) -> c_26(mark^#(N), M, IL) }
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { a__U11^#(X1, X2) -> c_3(X1, X2)
     , a__U11^#(tt(), L) -> c_4(a__length^#(mark(L)))
     , a__length^#(X) -> c_5(X)
     , a__length^#(cons(N, L)) ->
       c_6(a__U11^#(a__and(a__isNatList(L), isNat(N)), L))
     , mark^#(cons(X1, X2)) -> c_8(mark^#(X1), X2)
     , mark^#(zeros()) -> c_10(a__zeros^#())
     , mark^#(s(X)) -> c_12(mark^#(X))
     , mark^#(take(X1, X2)) -> c_14(a__take^#(mark(X1), mark(X2)))
     , mark^#(length(X)) -> c_15(a__length^#(mark(X)))
     , mark^#(isNatIList(X)) -> c_16(a__isNatIList^#(X))
     , mark^#(isNatList(X)) -> c_17(a__isNatList^#(X))
     , mark^#(isNat(X)) -> c_18(a__isNat^#(X))
     , mark^#(and(X1, X2)) -> c_19(a__and^#(mark(X1), X2))
     , mark^#(U11(X1, X2)) -> c_20(a__U11^#(mark(X1), X2))
     , mark^#(U21(X)) -> c_21(a__U21^#(mark(X)))
     , mark^#(U31(X1, X2, X3, X4)) ->
       c_22(a__U31^#(mark(X1), X2, X3, X4))
     , a__take^#(X1, X2) -> c_41(X1, X2)
     , a__take^#(0(), IL) -> c_42(a__U21^#(a__isNatIList(IL)))
     , a__take^#(s(M), cons(N, IL)) ->
       c_43(a__U31^#(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))),
                     IL,
                     M,
                     N))
     , a__isNatIList^#(V) -> c_37(a__isNatList^#(V))
     , a__isNatIList^#(X) -> c_38(X)
     , a__isNatIList^#(cons(V1, V2)) ->
       c_39(a__and^#(a__isNat(V1), isNatIList(V2)))
     , a__isNatList^#(X) -> c_33(X)
     , a__isNatList^#(cons(V1, V2)) ->
       c_34(a__and^#(a__isNat(V1), isNatList(V2)))
     , a__isNatList^#(take(V1, V2)) ->
       c_36(a__and^#(a__isNat(V1), isNatIList(V2)))
     , a__isNat^#(X) -> c_29(X)
     , a__isNat^#(s(V1)) -> c_31(a__isNat^#(V1))
     , a__isNat^#(length(V1)) -> c_32(a__isNatList^#(V1))
     , a__and^#(X1, X2) -> c_27(X1, X2)
     , a__and^#(tt(), X) -> c_28(mark^#(X))
     , a__U21^#(X) -> c_23(X)
     , a__U31^#(X1, X2, X3, X4) -> c_25(X1, X2, X3, X4)
     , a__U31^#(tt(), IL, M, N) -> c_26(mark^#(N), M, IL) }
   Strict Trs:
     { a__zeros() -> cons(0(), zeros())
     , a__zeros() -> zeros()
     , a__U11(X1, X2) -> U11(X1, X2)
     , a__U11(tt(), L) -> s(a__length(mark(L)))
     , a__length(X) -> length(X)
     , a__length(cons(N, L)) ->
       a__U11(a__and(a__isNatList(L), isNat(N)), L)
     , a__length(nil()) -> 0()
     , mark(cons(X1, X2)) -> cons(mark(X1), X2)
     , mark(0()) -> 0()
     , mark(zeros()) -> a__zeros()
     , mark(tt()) -> tt()
     , mark(s(X)) -> s(mark(X))
     , mark(nil()) -> nil()
     , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2))
     , mark(length(X)) -> a__length(mark(X))
     , mark(isNatIList(X)) -> a__isNatIList(X)
     , mark(isNatList(X)) -> a__isNatList(X)
     , mark(isNat(X)) -> a__isNat(X)
     , mark(and(X1, X2)) -> a__and(mark(X1), X2)
     , mark(U11(X1, X2)) -> a__U11(mark(X1), X2)
     , mark(U21(X)) -> a__U21(mark(X))
     , mark(U31(X1, X2, X3, X4)) -> a__U31(mark(X1), X2, X3, X4)
     , a__U21(X) -> U21(X)
     , a__U21(tt()) -> nil()
     , a__U31(X1, X2, X3, X4) -> U31(X1, X2, X3, X4)
     , a__U31(tt(), IL, M, N) -> cons(mark(N), take(M, IL))
     , a__and(X1, X2) -> and(X1, X2)
     , a__and(tt(), X) -> mark(X)
     , a__isNat(X) -> isNat(X)
     , a__isNat(0()) -> tt()
     , a__isNat(s(V1)) -> a__isNat(V1)
     , a__isNat(length(V1)) -> a__isNatList(V1)
     , a__isNatList(X) -> isNatList(X)
     , a__isNatList(cons(V1, V2)) -> a__and(a__isNat(V1), isNatList(V2))
     , a__isNatList(nil()) -> tt()
     , a__isNatList(take(V1, V2)) ->
       a__and(a__isNat(V1), isNatIList(V2))
     , a__isNatIList(V) -> a__isNatList(V)
     , a__isNatIList(X) -> isNatIList(X)
     , a__isNatIList(cons(V1, V2)) ->
       a__and(a__isNat(V1), isNatIList(V2))
     , a__isNatIList(zeros()) -> tt()
     , a__take(X1, X2) -> take(X1, X2)
     , a__take(0(), IL) -> a__U21(a__isNatIList(IL))
     , a__take(s(M), cons(N, IL)) ->
       a__U31(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))),
              IL,
              M,
              N) }
   Weak DPs:
     { a__zeros^#() -> c_1()
     , a__zeros^#() -> c_2()
     , a__length^#(nil()) -> c_7()
     , mark^#(0()) -> c_9()
     , mark^#(tt()) -> c_11()
     , mark^#(nil()) -> c_13()
     , a__isNatIList^#(zeros()) -> c_40()
     , a__isNatList^#(nil()) -> c_35()
     , a__isNat^#(0()) -> c_30()
     , a__U21^#(tt()) -> c_24() }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of {6} by applications of
   Pre({6}) = {1,3,5,7,17,21,23,26,29,30,31,32,33}. Here rules are
   labeled as follows:
   
     DPs:
       { 1: a__U11^#(X1, X2) -> c_3(X1, X2)
       , 2: a__U11^#(tt(), L) -> c_4(a__length^#(mark(L)))
       , 3: a__length^#(X) -> c_5(X)
       , 4: a__length^#(cons(N, L)) ->
            c_6(a__U11^#(a__and(a__isNatList(L), isNat(N)), L))
       , 5: mark^#(cons(X1, X2)) -> c_8(mark^#(X1), X2)
       , 6: mark^#(zeros()) -> c_10(a__zeros^#())
       , 7: mark^#(s(X)) -> c_12(mark^#(X))
       , 8: mark^#(take(X1, X2)) -> c_14(a__take^#(mark(X1), mark(X2)))
       , 9: mark^#(length(X)) -> c_15(a__length^#(mark(X)))
       , 10: mark^#(isNatIList(X)) -> c_16(a__isNatIList^#(X))
       , 11: mark^#(isNatList(X)) -> c_17(a__isNatList^#(X))
       , 12: mark^#(isNat(X)) -> c_18(a__isNat^#(X))
       , 13: mark^#(and(X1, X2)) -> c_19(a__and^#(mark(X1), X2))
       , 14: mark^#(U11(X1, X2)) -> c_20(a__U11^#(mark(X1), X2))
       , 15: mark^#(U21(X)) -> c_21(a__U21^#(mark(X)))
       , 16: mark^#(U31(X1, X2, X3, X4)) ->
             c_22(a__U31^#(mark(X1), X2, X3, X4))
       , 17: a__take^#(X1, X2) -> c_41(X1, X2)
       , 18: a__take^#(0(), IL) -> c_42(a__U21^#(a__isNatIList(IL)))
       , 19: a__take^#(s(M), cons(N, IL)) ->
             c_43(a__U31^#(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))),
                           IL,
                           M,
                           N))
       , 20: a__isNatIList^#(V) -> c_37(a__isNatList^#(V))
       , 21: a__isNatIList^#(X) -> c_38(X)
       , 22: a__isNatIList^#(cons(V1, V2)) ->
             c_39(a__and^#(a__isNat(V1), isNatIList(V2)))
       , 23: a__isNatList^#(X) -> c_33(X)
       , 24: a__isNatList^#(cons(V1, V2)) ->
             c_34(a__and^#(a__isNat(V1), isNatList(V2)))
       , 25: a__isNatList^#(take(V1, V2)) ->
             c_36(a__and^#(a__isNat(V1), isNatIList(V2)))
       , 26: a__isNat^#(X) -> c_29(X)
       , 27: a__isNat^#(s(V1)) -> c_31(a__isNat^#(V1))
       , 28: a__isNat^#(length(V1)) -> c_32(a__isNatList^#(V1))
       , 29: a__and^#(X1, X2) -> c_27(X1, X2)
       , 30: a__and^#(tt(), X) -> c_28(mark^#(X))
       , 31: a__U21^#(X) -> c_23(X)
       , 32: a__U31^#(X1, X2, X3, X4) -> c_25(X1, X2, X3, X4)
       , 33: a__U31^#(tt(), IL, M, N) -> c_26(mark^#(N), M, IL)
       , 34: a__zeros^#() -> c_1()
       , 35: a__zeros^#() -> c_2()
       , 36: a__length^#(nil()) -> c_7()
       , 37: mark^#(0()) -> c_9()
       , 38: mark^#(tt()) -> c_11()
       , 39: mark^#(nil()) -> c_13()
       , 40: a__isNatIList^#(zeros()) -> c_40()
       , 41: a__isNatList^#(nil()) -> c_35()
       , 42: a__isNat^#(0()) -> c_30()
       , 43: a__U21^#(tt()) -> c_24() }
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { a__U11^#(X1, X2) -> c_3(X1, X2)
     , a__U11^#(tt(), L) -> c_4(a__length^#(mark(L)))
     , a__length^#(X) -> c_5(X)
     , a__length^#(cons(N, L)) ->
       c_6(a__U11^#(a__and(a__isNatList(L), isNat(N)), L))
     , mark^#(cons(X1, X2)) -> c_8(mark^#(X1), X2)
     , mark^#(s(X)) -> c_12(mark^#(X))
     , mark^#(take(X1, X2)) -> c_14(a__take^#(mark(X1), mark(X2)))
     , mark^#(length(X)) -> c_15(a__length^#(mark(X)))
     , mark^#(isNatIList(X)) -> c_16(a__isNatIList^#(X))
     , mark^#(isNatList(X)) -> c_17(a__isNatList^#(X))
     , mark^#(isNat(X)) -> c_18(a__isNat^#(X))
     , mark^#(and(X1, X2)) -> c_19(a__and^#(mark(X1), X2))
     , mark^#(U11(X1, X2)) -> c_20(a__U11^#(mark(X1), X2))
     , mark^#(U21(X)) -> c_21(a__U21^#(mark(X)))
     , mark^#(U31(X1, X2, X3, X4)) ->
       c_22(a__U31^#(mark(X1), X2, X3, X4))
     , a__take^#(X1, X2) -> c_41(X1, X2)
     , a__take^#(0(), IL) -> c_42(a__U21^#(a__isNatIList(IL)))
     , a__take^#(s(M), cons(N, IL)) ->
       c_43(a__U31^#(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))),
                     IL,
                     M,
                     N))
     , a__isNatIList^#(V) -> c_37(a__isNatList^#(V))
     , a__isNatIList^#(X) -> c_38(X)
     , a__isNatIList^#(cons(V1, V2)) ->
       c_39(a__and^#(a__isNat(V1), isNatIList(V2)))
     , a__isNatList^#(X) -> c_33(X)
     , a__isNatList^#(cons(V1, V2)) ->
       c_34(a__and^#(a__isNat(V1), isNatList(V2)))
     , a__isNatList^#(take(V1, V2)) ->
       c_36(a__and^#(a__isNat(V1), isNatIList(V2)))
     , a__isNat^#(X) -> c_29(X)
     , a__isNat^#(s(V1)) -> c_31(a__isNat^#(V1))
     , a__isNat^#(length(V1)) -> c_32(a__isNatList^#(V1))
     , a__and^#(X1, X2) -> c_27(X1, X2)
     , a__and^#(tt(), X) -> c_28(mark^#(X))
     , a__U21^#(X) -> c_23(X)
     , a__U31^#(X1, X2, X3, X4) -> c_25(X1, X2, X3, X4)
     , a__U31^#(tt(), IL, M, N) -> c_26(mark^#(N), M, IL) }
   Strict Trs:
     { a__zeros() -> cons(0(), zeros())
     , a__zeros() -> zeros()
     , a__U11(X1, X2) -> U11(X1, X2)
     , a__U11(tt(), L) -> s(a__length(mark(L)))
     , a__length(X) -> length(X)
     , a__length(cons(N, L)) ->
       a__U11(a__and(a__isNatList(L), isNat(N)), L)
     , a__length(nil()) -> 0()
     , mark(cons(X1, X2)) -> cons(mark(X1), X2)
     , mark(0()) -> 0()
     , mark(zeros()) -> a__zeros()
     , mark(tt()) -> tt()
     , mark(s(X)) -> s(mark(X))
     , mark(nil()) -> nil()
     , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2))
     , mark(length(X)) -> a__length(mark(X))
     , mark(isNatIList(X)) -> a__isNatIList(X)
     , mark(isNatList(X)) -> a__isNatList(X)
     , mark(isNat(X)) -> a__isNat(X)
     , mark(and(X1, X2)) -> a__and(mark(X1), X2)
     , mark(U11(X1, X2)) -> a__U11(mark(X1), X2)
     , mark(U21(X)) -> a__U21(mark(X))
     , mark(U31(X1, X2, X3, X4)) -> a__U31(mark(X1), X2, X3, X4)
     , a__U21(X) -> U21(X)
     , a__U21(tt()) -> nil()
     , a__U31(X1, X2, X3, X4) -> U31(X1, X2, X3, X4)
     , a__U31(tt(), IL, M, N) -> cons(mark(N), take(M, IL))
     , a__and(X1, X2) -> and(X1, X2)
     , a__and(tt(), X) -> mark(X)
     , a__isNat(X) -> isNat(X)
     , a__isNat(0()) -> tt()
     , a__isNat(s(V1)) -> a__isNat(V1)
     , a__isNat(length(V1)) -> a__isNatList(V1)
     , a__isNatList(X) -> isNatList(X)
     , a__isNatList(cons(V1, V2)) -> a__and(a__isNat(V1), isNatList(V2))
     , a__isNatList(nil()) -> tt()
     , a__isNatList(take(V1, V2)) ->
       a__and(a__isNat(V1), isNatIList(V2))
     , a__isNatIList(V) -> a__isNatList(V)
     , a__isNatIList(X) -> isNatIList(X)
     , a__isNatIList(cons(V1, V2)) ->
       a__and(a__isNat(V1), isNatIList(V2))
     , a__isNatIList(zeros()) -> tt()
     , a__take(X1, X2) -> take(X1, X2)
     , a__take(0(), IL) -> a__U21(a__isNatIList(IL))
     , a__take(s(M), cons(N, IL)) ->
       a__U31(a__and(a__isNatIList(IL), and(isNat(M), isNat(N))),
              IL,
              M,
              N) }
   Weak DPs:
     { a__zeros^#() -> c_1()
     , a__zeros^#() -> c_2()
     , a__length^#(nil()) -> c_7()
     , mark^#(0()) -> c_9()
     , mark^#(zeros()) -> c_10(a__zeros^#())
     , mark^#(tt()) -> c_11()
     , mark^#(nil()) -> c_13()
     , a__isNatIList^#(zeros()) -> c_40()
     , a__isNatList^#(nil()) -> c_35()
     , a__isNat^#(0()) -> c_30()
     , a__U21^#(tt()) -> c_24() }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   Empty strict component of the problem is NOT empty.


Arrrr..