MAYBE

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

Strict Trs:
  { a__and(X1, X2) -> and(X1, X2)
  , a__and(tt(), T) -> mark(T)
  , mark(tt()) -> tt()
  , mark(0()) -> 0()
  , mark(s(X)) -> s(mark(X))
  , mark(length(X)) -> a__length(mark(X))
  , mark(zeros()) -> a__zeros()
  , mark(cons(X1, X2)) -> cons(mark(X1), X2)
  , mark(nil()) -> nil()
  , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2))
  , mark(and(X1, X2)) -> a__and(mark(X1), mark(X2))
  , mark(isNatIList(X)) -> a__isNatIList(X)
  , mark(isNatList(X)) -> a__isNatList(X)
  , mark(isNat(X)) -> a__isNat(X)
  , mark(uTake1(X)) -> a__uTake1(mark(X))
  , mark(uTake2(X1, X2, X3, X4)) -> a__uTake2(mark(X1), X2, X3, X4)
  , mark(uLength(X1, X2)) -> a__uLength(mark(X1), X2)
  , a__isNatIList(IL) -> a__isNatList(IL)
  , a__isNatIList(X) -> isNatIList(X)
  , a__isNatIList(zeros()) -> tt()
  , a__isNatIList(cons(N, IL)) ->
    a__and(a__isNat(N), a__isNatIList(IL))
  , a__isNatList(X) -> isNatList(X)
  , a__isNatList(cons(N, L)) -> a__and(a__isNat(N), a__isNatList(L))
  , a__isNatList(nil()) -> tt()
  , a__isNatList(take(N, IL)) ->
    a__and(a__isNat(N), a__isNatIList(IL))
  , a__isNat(X) -> isNat(X)
  , a__isNat(0()) -> tt()
  , a__isNat(s(N)) -> a__isNat(N)
  , a__isNat(length(L)) -> a__isNatList(L)
  , a__zeros() -> zeros()
  , a__zeros() -> cons(0(), zeros())
  , a__take(X1, X2) -> take(X1, X2)
  , a__take(0(), IL) -> a__uTake1(a__isNatIList(IL))
  , a__take(s(M), cons(N, IL)) ->
    a__uTake2(a__and(a__isNat(M),
                     a__and(a__isNat(N), a__isNatIList(IL))),
              M,
              N,
              IL)
  , a__uTake1(X) -> uTake1(X)
  , a__uTake1(tt()) -> nil()
  , a__uTake2(X1, X2, X3, X4) -> uTake2(X1, X2, X3, X4)
  , a__uTake2(tt(), M, N, IL) -> cons(mark(N), take(M, IL))
  , a__length(X) -> length(X)
  , a__length(cons(N, L)) ->
    a__uLength(a__and(a__isNat(N), a__isNatList(L)), L)
  , a__uLength(X1, X2) -> uLength(X1, X2)
  , a__uLength(tt(), L) -> s(a__length(mark(L))) }
Obligation:
  runtime complexity
Answer:
  MAYBE

None of the processors succeeded.

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

2) 'Best' failed due to the following reason:
   
   None of the processors succeeded.
   
   Details of failed attempt(s):
   -----------------------------
   1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)'
      failed due to the following reason:
      
      Computation stopped due to timeout after 30.0 seconds.
   
   2) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed
      due to the following reason:
      
      None of the processors succeeded.
      
      Details of failed attempt(s):
      -----------------------------
      1) 'Bounds with minimal-enrichment and initial automaton 'match''
         failed due to the following reason:
         
         match-boundness of the problem could not be verified.
      
      2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
         failed due to the following reason:
         
         match-boundness of the problem could not be verified.
      
   
   3) 'Best' failed due to the following reason:
      
      None of the processors succeeded.
      
      Details of failed attempt(s):
      -----------------------------
      1) '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:
     { a__and^#(X1, X2) -> c_1(X1, X2)
     , a__and^#(tt(), T) -> c_2(mark^#(T))
     , mark^#(tt()) -> c_3()
     , mark^#(0()) -> c_4()
     , mark^#(s(X)) -> c_5(mark^#(X))
     , mark^#(length(X)) -> c_6(a__length^#(mark(X)))
     , mark^#(zeros()) -> c_7(a__zeros^#())
     , mark^#(cons(X1, X2)) -> c_8(mark^#(X1), X2)
     , mark^#(nil()) -> c_9()
     , mark^#(take(X1, X2)) -> c_10(a__take^#(mark(X1), mark(X2)))
     , mark^#(and(X1, X2)) -> c_11(a__and^#(mark(X1), mark(X2)))
     , mark^#(isNatIList(X)) -> c_12(a__isNatIList^#(X))
     , mark^#(isNatList(X)) -> c_13(a__isNatList^#(X))
     , mark^#(isNat(X)) -> c_14(a__isNat^#(X))
     , mark^#(uTake1(X)) -> c_15(a__uTake1^#(mark(X)))
     , mark^#(uTake2(X1, X2, X3, X4)) ->
       c_16(a__uTake2^#(mark(X1), X2, X3, X4))
     , mark^#(uLength(X1, X2)) -> c_17(a__uLength^#(mark(X1), X2))
     , a__length^#(X) -> c_39(X)
     , a__length^#(cons(N, L)) ->
       c_40(a__uLength^#(a__and(a__isNat(N), a__isNatList(L)), L))
     , a__zeros^#() -> c_30()
     , a__zeros^#() -> c_31()
     , a__take^#(X1, X2) -> c_32(X1, X2)
     , a__take^#(0(), IL) -> c_33(a__uTake1^#(a__isNatIList(IL)))
     , a__take^#(s(M), cons(N, IL)) ->
       c_34(a__uTake2^#(a__and(a__isNat(M),
                               a__and(a__isNat(N), a__isNatIList(IL))),
                        M,
                        N,
                        IL))
     , a__isNatIList^#(IL) -> c_18(a__isNatList^#(IL))
     , a__isNatIList^#(X) -> c_19(X)
     , a__isNatIList^#(zeros()) -> c_20()
     , a__isNatIList^#(cons(N, IL)) ->
       c_21(a__and^#(a__isNat(N), a__isNatIList(IL)))
     , a__isNatList^#(X) -> c_22(X)
     , a__isNatList^#(cons(N, L)) ->
       c_23(a__and^#(a__isNat(N), a__isNatList(L)))
     , a__isNatList^#(nil()) -> c_24()
     , a__isNatList^#(take(N, IL)) ->
       c_25(a__and^#(a__isNat(N), a__isNatIList(IL)))
     , a__isNat^#(X) -> c_26(X)
     , a__isNat^#(0()) -> c_27()
     , a__isNat^#(s(N)) -> c_28(a__isNat^#(N))
     , a__isNat^#(length(L)) -> c_29(a__isNatList^#(L))
     , a__uTake1^#(X) -> c_35(X)
     , a__uTake1^#(tt()) -> c_36()
     , a__uTake2^#(X1, X2, X3, X4) -> c_37(X1, X2, X3, X4)
     , a__uTake2^#(tt(), M, N, IL) -> c_38(mark^#(N), M, IL)
     , a__uLength^#(X1, X2) -> c_41(X1, X2)
     , a__uLength^#(tt(), L) -> c_42(a__length^#(mark(L))) }
   
   and mark the set of starting terms.
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { a__and^#(X1, X2) -> c_1(X1, X2)
     , a__and^#(tt(), T) -> c_2(mark^#(T))
     , mark^#(tt()) -> c_3()
     , mark^#(0()) -> c_4()
     , mark^#(s(X)) -> c_5(mark^#(X))
     , mark^#(length(X)) -> c_6(a__length^#(mark(X)))
     , mark^#(zeros()) -> c_7(a__zeros^#())
     , mark^#(cons(X1, X2)) -> c_8(mark^#(X1), X2)
     , mark^#(nil()) -> c_9()
     , mark^#(take(X1, X2)) -> c_10(a__take^#(mark(X1), mark(X2)))
     , mark^#(and(X1, X2)) -> c_11(a__and^#(mark(X1), mark(X2)))
     , mark^#(isNatIList(X)) -> c_12(a__isNatIList^#(X))
     , mark^#(isNatList(X)) -> c_13(a__isNatList^#(X))
     , mark^#(isNat(X)) -> c_14(a__isNat^#(X))
     , mark^#(uTake1(X)) -> c_15(a__uTake1^#(mark(X)))
     , mark^#(uTake2(X1, X2, X3, X4)) ->
       c_16(a__uTake2^#(mark(X1), X2, X3, X4))
     , mark^#(uLength(X1, X2)) -> c_17(a__uLength^#(mark(X1), X2))
     , a__length^#(X) -> c_39(X)
     , a__length^#(cons(N, L)) ->
       c_40(a__uLength^#(a__and(a__isNat(N), a__isNatList(L)), L))
     , a__zeros^#() -> c_30()
     , a__zeros^#() -> c_31()
     , a__take^#(X1, X2) -> c_32(X1, X2)
     , a__take^#(0(), IL) -> c_33(a__uTake1^#(a__isNatIList(IL)))
     , a__take^#(s(M), cons(N, IL)) ->
       c_34(a__uTake2^#(a__and(a__isNat(M),
                               a__and(a__isNat(N), a__isNatIList(IL))),
                        M,
                        N,
                        IL))
     , a__isNatIList^#(IL) -> c_18(a__isNatList^#(IL))
     , a__isNatIList^#(X) -> c_19(X)
     , a__isNatIList^#(zeros()) -> c_20()
     , a__isNatIList^#(cons(N, IL)) ->
       c_21(a__and^#(a__isNat(N), a__isNatIList(IL)))
     , a__isNatList^#(X) -> c_22(X)
     , a__isNatList^#(cons(N, L)) ->
       c_23(a__and^#(a__isNat(N), a__isNatList(L)))
     , a__isNatList^#(nil()) -> c_24()
     , a__isNatList^#(take(N, IL)) ->
       c_25(a__and^#(a__isNat(N), a__isNatIList(IL)))
     , a__isNat^#(X) -> c_26(X)
     , a__isNat^#(0()) -> c_27()
     , a__isNat^#(s(N)) -> c_28(a__isNat^#(N))
     , a__isNat^#(length(L)) -> c_29(a__isNatList^#(L))
     , a__uTake1^#(X) -> c_35(X)
     , a__uTake1^#(tt()) -> c_36()
     , a__uTake2^#(X1, X2, X3, X4) -> c_37(X1, X2, X3, X4)
     , a__uTake2^#(tt(), M, N, IL) -> c_38(mark^#(N), M, IL)
     , a__uLength^#(X1, X2) -> c_41(X1, X2)
     , a__uLength^#(tt(), L) -> c_42(a__length^#(mark(L))) }
   Strict Trs:
     { a__and(X1, X2) -> and(X1, X2)
     , a__and(tt(), T) -> mark(T)
     , mark(tt()) -> tt()
     , mark(0()) -> 0()
     , mark(s(X)) -> s(mark(X))
     , mark(length(X)) -> a__length(mark(X))
     , mark(zeros()) -> a__zeros()
     , mark(cons(X1, X2)) -> cons(mark(X1), X2)
     , mark(nil()) -> nil()
     , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2))
     , mark(and(X1, X2)) -> a__and(mark(X1), mark(X2))
     , mark(isNatIList(X)) -> a__isNatIList(X)
     , mark(isNatList(X)) -> a__isNatList(X)
     , mark(isNat(X)) -> a__isNat(X)
     , mark(uTake1(X)) -> a__uTake1(mark(X))
     , mark(uTake2(X1, X2, X3, X4)) -> a__uTake2(mark(X1), X2, X3, X4)
     , mark(uLength(X1, X2)) -> a__uLength(mark(X1), X2)
     , a__isNatIList(IL) -> a__isNatList(IL)
     , a__isNatIList(X) -> isNatIList(X)
     , a__isNatIList(zeros()) -> tt()
     , a__isNatIList(cons(N, IL)) ->
       a__and(a__isNat(N), a__isNatIList(IL))
     , a__isNatList(X) -> isNatList(X)
     , a__isNatList(cons(N, L)) -> a__and(a__isNat(N), a__isNatList(L))
     , a__isNatList(nil()) -> tt()
     , a__isNatList(take(N, IL)) ->
       a__and(a__isNat(N), a__isNatIList(IL))
     , a__isNat(X) -> isNat(X)
     , a__isNat(0()) -> tt()
     , a__isNat(s(N)) -> a__isNat(N)
     , a__isNat(length(L)) -> a__isNatList(L)
     , a__zeros() -> zeros()
     , a__zeros() -> cons(0(), zeros())
     , a__take(X1, X2) -> take(X1, X2)
     , a__take(0(), IL) -> a__uTake1(a__isNatIList(IL))
     , a__take(s(M), cons(N, IL)) ->
       a__uTake2(a__and(a__isNat(M),
                        a__and(a__isNat(N), a__isNatIList(IL))),
                 M,
                 N,
                 IL)
     , a__uTake1(X) -> uTake1(X)
     , a__uTake1(tt()) -> nil()
     , a__uTake2(X1, X2, X3, X4) -> uTake2(X1, X2, X3, X4)
     , a__uTake2(tt(), M, N, IL) -> cons(mark(N), take(M, IL))
     , a__length(X) -> length(X)
     , a__length(cons(N, L)) ->
       a__uLength(a__and(a__isNat(N), a__isNatList(L)), L)
     , a__uLength(X1, X2) -> uLength(X1, X2)
     , a__uLength(tt(), L) -> s(a__length(mark(L))) }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of {3,4,9,20,21,27,31,34,38}
   by applications of Pre({3,4,9,20,21,27,31,34,38}) =
   {1,2,5,7,8,12,13,14,15,18,22,23,25,26,29,33,35,36,37,39,40,41}.
   Here rules are labeled as follows:
   
     DPs:
       { 1: a__and^#(X1, X2) -> c_1(X1, X2)
       , 2: a__and^#(tt(), T) -> c_2(mark^#(T))
       , 3: mark^#(tt()) -> c_3()
       , 4: mark^#(0()) -> c_4()
       , 5: mark^#(s(X)) -> c_5(mark^#(X))
       , 6: mark^#(length(X)) -> c_6(a__length^#(mark(X)))
       , 7: mark^#(zeros()) -> c_7(a__zeros^#())
       , 8: mark^#(cons(X1, X2)) -> c_8(mark^#(X1), X2)
       , 9: mark^#(nil()) -> c_9()
       , 10: mark^#(take(X1, X2)) -> c_10(a__take^#(mark(X1), mark(X2)))
       , 11: mark^#(and(X1, X2)) -> c_11(a__and^#(mark(X1), mark(X2)))
       , 12: mark^#(isNatIList(X)) -> c_12(a__isNatIList^#(X))
       , 13: mark^#(isNatList(X)) -> c_13(a__isNatList^#(X))
       , 14: mark^#(isNat(X)) -> c_14(a__isNat^#(X))
       , 15: mark^#(uTake1(X)) -> c_15(a__uTake1^#(mark(X)))
       , 16: mark^#(uTake2(X1, X2, X3, X4)) ->
             c_16(a__uTake2^#(mark(X1), X2, X3, X4))
       , 17: mark^#(uLength(X1, X2)) -> c_17(a__uLength^#(mark(X1), X2))
       , 18: a__length^#(X) -> c_39(X)
       , 19: a__length^#(cons(N, L)) ->
             c_40(a__uLength^#(a__and(a__isNat(N), a__isNatList(L)), L))
       , 20: a__zeros^#() -> c_30()
       , 21: a__zeros^#() -> c_31()
       , 22: a__take^#(X1, X2) -> c_32(X1, X2)
       , 23: a__take^#(0(), IL) -> c_33(a__uTake1^#(a__isNatIList(IL)))
       , 24: a__take^#(s(M), cons(N, IL)) ->
             c_34(a__uTake2^#(a__and(a__isNat(M),
                                     a__and(a__isNat(N), a__isNatIList(IL))),
                              M,
                              N,
                              IL))
       , 25: a__isNatIList^#(IL) -> c_18(a__isNatList^#(IL))
       , 26: a__isNatIList^#(X) -> c_19(X)
       , 27: a__isNatIList^#(zeros()) -> c_20()
       , 28: a__isNatIList^#(cons(N, IL)) ->
             c_21(a__and^#(a__isNat(N), a__isNatIList(IL)))
       , 29: a__isNatList^#(X) -> c_22(X)
       , 30: a__isNatList^#(cons(N, L)) ->
             c_23(a__and^#(a__isNat(N), a__isNatList(L)))
       , 31: a__isNatList^#(nil()) -> c_24()
       , 32: a__isNatList^#(take(N, IL)) ->
             c_25(a__and^#(a__isNat(N), a__isNatIList(IL)))
       , 33: a__isNat^#(X) -> c_26(X)
       , 34: a__isNat^#(0()) -> c_27()
       , 35: a__isNat^#(s(N)) -> c_28(a__isNat^#(N))
       , 36: a__isNat^#(length(L)) -> c_29(a__isNatList^#(L))
       , 37: a__uTake1^#(X) -> c_35(X)
       , 38: a__uTake1^#(tt()) -> c_36()
       , 39: a__uTake2^#(X1, X2, X3, X4) -> c_37(X1, X2, X3, X4)
       , 40: a__uTake2^#(tt(), M, N, IL) -> c_38(mark^#(N), M, IL)
       , 41: a__uLength^#(X1, X2) -> c_41(X1, X2)
       , 42: a__uLength^#(tt(), L) -> c_42(a__length^#(mark(L))) }
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { a__and^#(X1, X2) -> c_1(X1, X2)
     , a__and^#(tt(), T) -> c_2(mark^#(T))
     , mark^#(s(X)) -> c_5(mark^#(X))
     , mark^#(length(X)) -> c_6(a__length^#(mark(X)))
     , mark^#(zeros()) -> c_7(a__zeros^#())
     , mark^#(cons(X1, X2)) -> c_8(mark^#(X1), X2)
     , mark^#(take(X1, X2)) -> c_10(a__take^#(mark(X1), mark(X2)))
     , mark^#(and(X1, X2)) -> c_11(a__and^#(mark(X1), mark(X2)))
     , mark^#(isNatIList(X)) -> c_12(a__isNatIList^#(X))
     , mark^#(isNatList(X)) -> c_13(a__isNatList^#(X))
     , mark^#(isNat(X)) -> c_14(a__isNat^#(X))
     , mark^#(uTake1(X)) -> c_15(a__uTake1^#(mark(X)))
     , mark^#(uTake2(X1, X2, X3, X4)) ->
       c_16(a__uTake2^#(mark(X1), X2, X3, X4))
     , mark^#(uLength(X1, X2)) -> c_17(a__uLength^#(mark(X1), X2))
     , a__length^#(X) -> c_39(X)
     , a__length^#(cons(N, L)) ->
       c_40(a__uLength^#(a__and(a__isNat(N), a__isNatList(L)), L))
     , a__take^#(X1, X2) -> c_32(X1, X2)
     , a__take^#(0(), IL) -> c_33(a__uTake1^#(a__isNatIList(IL)))
     , a__take^#(s(M), cons(N, IL)) ->
       c_34(a__uTake2^#(a__and(a__isNat(M),
                               a__and(a__isNat(N), a__isNatIList(IL))),
                        M,
                        N,
                        IL))
     , a__isNatIList^#(IL) -> c_18(a__isNatList^#(IL))
     , a__isNatIList^#(X) -> c_19(X)
     , a__isNatIList^#(cons(N, IL)) ->
       c_21(a__and^#(a__isNat(N), a__isNatIList(IL)))
     , a__isNatList^#(X) -> c_22(X)
     , a__isNatList^#(cons(N, L)) ->
       c_23(a__and^#(a__isNat(N), a__isNatList(L)))
     , a__isNatList^#(take(N, IL)) ->
       c_25(a__and^#(a__isNat(N), a__isNatIList(IL)))
     , a__isNat^#(X) -> c_26(X)
     , a__isNat^#(s(N)) -> c_28(a__isNat^#(N))
     , a__isNat^#(length(L)) -> c_29(a__isNatList^#(L))
     , a__uTake1^#(X) -> c_35(X)
     , a__uTake2^#(X1, X2, X3, X4) -> c_37(X1, X2, X3, X4)
     , a__uTake2^#(tt(), M, N, IL) -> c_38(mark^#(N), M, IL)
     , a__uLength^#(X1, X2) -> c_41(X1, X2)
     , a__uLength^#(tt(), L) -> c_42(a__length^#(mark(L))) }
   Strict Trs:
     { a__and(X1, X2) -> and(X1, X2)
     , a__and(tt(), T) -> mark(T)
     , mark(tt()) -> tt()
     , mark(0()) -> 0()
     , mark(s(X)) -> s(mark(X))
     , mark(length(X)) -> a__length(mark(X))
     , mark(zeros()) -> a__zeros()
     , mark(cons(X1, X2)) -> cons(mark(X1), X2)
     , mark(nil()) -> nil()
     , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2))
     , mark(and(X1, X2)) -> a__and(mark(X1), mark(X2))
     , mark(isNatIList(X)) -> a__isNatIList(X)
     , mark(isNatList(X)) -> a__isNatList(X)
     , mark(isNat(X)) -> a__isNat(X)
     , mark(uTake1(X)) -> a__uTake1(mark(X))
     , mark(uTake2(X1, X2, X3, X4)) -> a__uTake2(mark(X1), X2, X3, X4)
     , mark(uLength(X1, X2)) -> a__uLength(mark(X1), X2)
     , a__isNatIList(IL) -> a__isNatList(IL)
     , a__isNatIList(X) -> isNatIList(X)
     , a__isNatIList(zeros()) -> tt()
     , a__isNatIList(cons(N, IL)) ->
       a__and(a__isNat(N), a__isNatIList(IL))
     , a__isNatList(X) -> isNatList(X)
     , a__isNatList(cons(N, L)) -> a__and(a__isNat(N), a__isNatList(L))
     , a__isNatList(nil()) -> tt()
     , a__isNatList(take(N, IL)) ->
       a__and(a__isNat(N), a__isNatIList(IL))
     , a__isNat(X) -> isNat(X)
     , a__isNat(0()) -> tt()
     , a__isNat(s(N)) -> a__isNat(N)
     , a__isNat(length(L)) -> a__isNatList(L)
     , a__zeros() -> zeros()
     , a__zeros() -> cons(0(), zeros())
     , a__take(X1, X2) -> take(X1, X2)
     , a__take(0(), IL) -> a__uTake1(a__isNatIList(IL))
     , a__take(s(M), cons(N, IL)) ->
       a__uTake2(a__and(a__isNat(M),
                        a__and(a__isNat(N), a__isNatIList(IL))),
                 M,
                 N,
                 IL)
     , a__uTake1(X) -> uTake1(X)
     , a__uTake1(tt()) -> nil()
     , a__uTake2(X1, X2, X3, X4) -> uTake2(X1, X2, X3, X4)
     , a__uTake2(tt(), M, N, IL) -> cons(mark(N), take(M, IL))
     , a__length(X) -> length(X)
     , a__length(cons(N, L)) ->
       a__uLength(a__and(a__isNat(N), a__isNatList(L)), L)
     , a__uLength(X1, X2) -> uLength(X1, X2)
     , a__uLength(tt(), L) -> s(a__length(mark(L))) }
   Weak DPs:
     { mark^#(tt()) -> c_3()
     , mark^#(0()) -> c_4()
     , mark^#(nil()) -> c_9()
     , a__zeros^#() -> c_30()
     , a__zeros^#() -> c_31()
     , a__isNatIList^#(zeros()) -> c_20()
     , a__isNatList^#(nil()) -> c_24()
     , a__isNat^#(0()) -> c_27()
     , a__uTake1^#(tt()) -> c_36() }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of {5} by applications of
   Pre({5}) = {1,2,3,6,15,17,21,23,26,29,30,31,32}. Here rules are
   labeled as follows:
   
     DPs:
       { 1: a__and^#(X1, X2) -> c_1(X1, X2)
       , 2: a__and^#(tt(), T) -> c_2(mark^#(T))
       , 3: mark^#(s(X)) -> c_5(mark^#(X))
       , 4: mark^#(length(X)) -> c_6(a__length^#(mark(X)))
       , 5: mark^#(zeros()) -> c_7(a__zeros^#())
       , 6: mark^#(cons(X1, X2)) -> c_8(mark^#(X1), X2)
       , 7: mark^#(take(X1, X2)) -> c_10(a__take^#(mark(X1), mark(X2)))
       , 8: mark^#(and(X1, X2)) -> c_11(a__and^#(mark(X1), mark(X2)))
       , 9: mark^#(isNatIList(X)) -> c_12(a__isNatIList^#(X))
       , 10: mark^#(isNatList(X)) -> c_13(a__isNatList^#(X))
       , 11: mark^#(isNat(X)) -> c_14(a__isNat^#(X))
       , 12: mark^#(uTake1(X)) -> c_15(a__uTake1^#(mark(X)))
       , 13: mark^#(uTake2(X1, X2, X3, X4)) ->
             c_16(a__uTake2^#(mark(X1), X2, X3, X4))
       , 14: mark^#(uLength(X1, X2)) -> c_17(a__uLength^#(mark(X1), X2))
       , 15: a__length^#(X) -> c_39(X)
       , 16: a__length^#(cons(N, L)) ->
             c_40(a__uLength^#(a__and(a__isNat(N), a__isNatList(L)), L))
       , 17: a__take^#(X1, X2) -> c_32(X1, X2)
       , 18: a__take^#(0(), IL) -> c_33(a__uTake1^#(a__isNatIList(IL)))
       , 19: a__take^#(s(M), cons(N, IL)) ->
             c_34(a__uTake2^#(a__and(a__isNat(M),
                                     a__and(a__isNat(N), a__isNatIList(IL))),
                              M,
                              N,
                              IL))
       , 20: a__isNatIList^#(IL) -> c_18(a__isNatList^#(IL))
       , 21: a__isNatIList^#(X) -> c_19(X)
       , 22: a__isNatIList^#(cons(N, IL)) ->
             c_21(a__and^#(a__isNat(N), a__isNatIList(IL)))
       , 23: a__isNatList^#(X) -> c_22(X)
       , 24: a__isNatList^#(cons(N, L)) ->
             c_23(a__and^#(a__isNat(N), a__isNatList(L)))
       , 25: a__isNatList^#(take(N, IL)) ->
             c_25(a__and^#(a__isNat(N), a__isNatIList(IL)))
       , 26: a__isNat^#(X) -> c_26(X)
       , 27: a__isNat^#(s(N)) -> c_28(a__isNat^#(N))
       , 28: a__isNat^#(length(L)) -> c_29(a__isNatList^#(L))
       , 29: a__uTake1^#(X) -> c_35(X)
       , 30: a__uTake2^#(X1, X2, X3, X4) -> c_37(X1, X2, X3, X4)
       , 31: a__uTake2^#(tt(), M, N, IL) -> c_38(mark^#(N), M, IL)
       , 32: a__uLength^#(X1, X2) -> c_41(X1, X2)
       , 33: a__uLength^#(tt(), L) -> c_42(a__length^#(mark(L)))
       , 34: mark^#(tt()) -> c_3()
       , 35: mark^#(0()) -> c_4()
       , 36: mark^#(nil()) -> c_9()
       , 37: a__zeros^#() -> c_30()
       , 38: a__zeros^#() -> c_31()
       , 39: a__isNatIList^#(zeros()) -> c_20()
       , 40: a__isNatList^#(nil()) -> c_24()
       , 41: a__isNat^#(0()) -> c_27()
       , 42: a__uTake1^#(tt()) -> c_36() }
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { a__and^#(X1, X2) -> c_1(X1, X2)
     , a__and^#(tt(), T) -> c_2(mark^#(T))
     , mark^#(s(X)) -> c_5(mark^#(X))
     , mark^#(length(X)) -> c_6(a__length^#(mark(X)))
     , mark^#(cons(X1, X2)) -> c_8(mark^#(X1), X2)
     , mark^#(take(X1, X2)) -> c_10(a__take^#(mark(X1), mark(X2)))
     , mark^#(and(X1, X2)) -> c_11(a__and^#(mark(X1), mark(X2)))
     , mark^#(isNatIList(X)) -> c_12(a__isNatIList^#(X))
     , mark^#(isNatList(X)) -> c_13(a__isNatList^#(X))
     , mark^#(isNat(X)) -> c_14(a__isNat^#(X))
     , mark^#(uTake1(X)) -> c_15(a__uTake1^#(mark(X)))
     , mark^#(uTake2(X1, X2, X3, X4)) ->
       c_16(a__uTake2^#(mark(X1), X2, X3, X4))
     , mark^#(uLength(X1, X2)) -> c_17(a__uLength^#(mark(X1), X2))
     , a__length^#(X) -> c_39(X)
     , a__length^#(cons(N, L)) ->
       c_40(a__uLength^#(a__and(a__isNat(N), a__isNatList(L)), L))
     , a__take^#(X1, X2) -> c_32(X1, X2)
     , a__take^#(0(), IL) -> c_33(a__uTake1^#(a__isNatIList(IL)))
     , a__take^#(s(M), cons(N, IL)) ->
       c_34(a__uTake2^#(a__and(a__isNat(M),
                               a__and(a__isNat(N), a__isNatIList(IL))),
                        M,
                        N,
                        IL))
     , a__isNatIList^#(IL) -> c_18(a__isNatList^#(IL))
     , a__isNatIList^#(X) -> c_19(X)
     , a__isNatIList^#(cons(N, IL)) ->
       c_21(a__and^#(a__isNat(N), a__isNatIList(IL)))
     , a__isNatList^#(X) -> c_22(X)
     , a__isNatList^#(cons(N, L)) ->
       c_23(a__and^#(a__isNat(N), a__isNatList(L)))
     , a__isNatList^#(take(N, IL)) ->
       c_25(a__and^#(a__isNat(N), a__isNatIList(IL)))
     , a__isNat^#(X) -> c_26(X)
     , a__isNat^#(s(N)) -> c_28(a__isNat^#(N))
     , a__isNat^#(length(L)) -> c_29(a__isNatList^#(L))
     , a__uTake1^#(X) -> c_35(X)
     , a__uTake2^#(X1, X2, X3, X4) -> c_37(X1, X2, X3, X4)
     , a__uTake2^#(tt(), M, N, IL) -> c_38(mark^#(N), M, IL)
     , a__uLength^#(X1, X2) -> c_41(X1, X2)
     , a__uLength^#(tt(), L) -> c_42(a__length^#(mark(L))) }
   Strict Trs:
     { a__and(X1, X2) -> and(X1, X2)
     , a__and(tt(), T) -> mark(T)
     , mark(tt()) -> tt()
     , mark(0()) -> 0()
     , mark(s(X)) -> s(mark(X))
     , mark(length(X)) -> a__length(mark(X))
     , mark(zeros()) -> a__zeros()
     , mark(cons(X1, X2)) -> cons(mark(X1), X2)
     , mark(nil()) -> nil()
     , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2))
     , mark(and(X1, X2)) -> a__and(mark(X1), mark(X2))
     , mark(isNatIList(X)) -> a__isNatIList(X)
     , mark(isNatList(X)) -> a__isNatList(X)
     , mark(isNat(X)) -> a__isNat(X)
     , mark(uTake1(X)) -> a__uTake1(mark(X))
     , mark(uTake2(X1, X2, X3, X4)) -> a__uTake2(mark(X1), X2, X3, X4)
     , mark(uLength(X1, X2)) -> a__uLength(mark(X1), X2)
     , a__isNatIList(IL) -> a__isNatList(IL)
     , a__isNatIList(X) -> isNatIList(X)
     , a__isNatIList(zeros()) -> tt()
     , a__isNatIList(cons(N, IL)) ->
       a__and(a__isNat(N), a__isNatIList(IL))
     , a__isNatList(X) -> isNatList(X)
     , a__isNatList(cons(N, L)) -> a__and(a__isNat(N), a__isNatList(L))
     , a__isNatList(nil()) -> tt()
     , a__isNatList(take(N, IL)) ->
       a__and(a__isNat(N), a__isNatIList(IL))
     , a__isNat(X) -> isNat(X)
     , a__isNat(0()) -> tt()
     , a__isNat(s(N)) -> a__isNat(N)
     , a__isNat(length(L)) -> a__isNatList(L)
     , a__zeros() -> zeros()
     , a__zeros() -> cons(0(), zeros())
     , a__take(X1, X2) -> take(X1, X2)
     , a__take(0(), IL) -> a__uTake1(a__isNatIList(IL))
     , a__take(s(M), cons(N, IL)) ->
       a__uTake2(a__and(a__isNat(M),
                        a__and(a__isNat(N), a__isNatIList(IL))),
                 M,
                 N,
                 IL)
     , a__uTake1(X) -> uTake1(X)
     , a__uTake1(tt()) -> nil()
     , a__uTake2(X1, X2, X3, X4) -> uTake2(X1, X2, X3, X4)
     , a__uTake2(tt(), M, N, IL) -> cons(mark(N), take(M, IL))
     , a__length(X) -> length(X)
     , a__length(cons(N, L)) ->
       a__uLength(a__and(a__isNat(N), a__isNatList(L)), L)
     , a__uLength(X1, X2) -> uLength(X1, X2)
     , a__uLength(tt(), L) -> s(a__length(mark(L))) }
   Weak DPs:
     { mark^#(tt()) -> c_3()
     , mark^#(0()) -> c_4()
     , mark^#(zeros()) -> c_7(a__zeros^#())
     , mark^#(nil()) -> c_9()
     , a__zeros^#() -> c_30()
     , a__zeros^#() -> c_31()
     , a__isNatIList^#(zeros()) -> c_20()
     , a__isNatList^#(nil()) -> c_24()
     , a__isNat^#(0()) -> c_27()
     , a__uTake1^#(tt()) -> c_36() }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   Empty strict component of the problem is NOT empty.


Arrrr..