MAYBE

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

Strict Trs:
  { zeros() -> cons(0(), n__zeros())
  , zeros() -> n__zeros()
  , and(tt(), X) -> activate(X)
  , activate(X) -> X
  , activate(n__zeros()) -> zeros()
  , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2))
  , length(cons(N, L)) -> s(length(activate(L)))
  , length(nil()) -> 0()
  , take(X1, X2) -> n__take(X1, X2)
  , take(0(), IL) -> nil()
  , take(s(M), cons(N, IL)) -> cons(N, n__take(M, activate(IL))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { zeros^#() -> c_1()
  , zeros^#() -> c_2()
  , and^#(tt(), X) -> c_3(activate^#(X))
  , activate^#(X) -> c_4()
  , activate^#(n__zeros()) -> c_5(zeros^#())
  , activate^#(n__take(X1, X2)) ->
    c_6(take^#(activate(X1), activate(X2)),
        activate^#(X1),
        activate^#(X2))
  , take^#(X1, X2) -> c_9()
  , take^#(0(), IL) -> c_10()
  , take^#(s(M), cons(N, IL)) -> c_11(activate^#(IL))
  , length^#(cons(N, L)) -> c_7(length^#(activate(L)), activate^#(L))
  , length^#(nil()) -> c_8() }

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()
  , zeros^#() -> c_2()
  , and^#(tt(), X) -> c_3(activate^#(X))
  , activate^#(X) -> c_4()
  , activate^#(n__zeros()) -> c_5(zeros^#())
  , activate^#(n__take(X1, X2)) ->
    c_6(take^#(activate(X1), activate(X2)),
        activate^#(X1),
        activate^#(X2))
  , take^#(X1, X2) -> c_9()
  , take^#(0(), IL) -> c_10()
  , take^#(s(M), cons(N, IL)) -> c_11(activate^#(IL))
  , length^#(cons(N, L)) -> c_7(length^#(activate(L)), activate^#(L))
  , length^#(nil()) -> c_8() }
Weak Trs:
  { zeros() -> cons(0(), n__zeros())
  , zeros() -> n__zeros()
  , and(tt(), X) -> activate(X)
  , activate(X) -> X
  , activate(n__zeros()) -> zeros()
  , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2))
  , length(cons(N, L)) -> s(length(activate(L)))
  , length(nil()) -> 0()
  , take(X1, X2) -> n__take(X1, X2)
  , take(0(), IL) -> nil()
  , take(s(M), cons(N, IL)) -> cons(N, n__take(M, activate(IL))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We estimate the number of application of {1,2,4,7,8,11} by
applications of Pre({1,2,4,7,8,11}) = {3,5,6,9,10}. Here rules are
labeled as follows:

  DPs:
    { 1: zeros^#() -> c_1()
    , 2: zeros^#() -> c_2()
    , 3: and^#(tt(), X) -> c_3(activate^#(X))
    , 4: activate^#(X) -> c_4()
    , 5: activate^#(n__zeros()) -> c_5(zeros^#())
    , 6: activate^#(n__take(X1, X2)) ->
         c_6(take^#(activate(X1), activate(X2)),
             activate^#(X1),
             activate^#(X2))
    , 7: take^#(X1, X2) -> c_9()
    , 8: take^#(0(), IL) -> c_10()
    , 9: take^#(s(M), cons(N, IL)) -> c_11(activate^#(IL))
    , 10: length^#(cons(N, L)) ->
          c_7(length^#(activate(L)), activate^#(L))
    , 11: length^#(nil()) -> c_8() }

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

Strict DPs:
  { and^#(tt(), X) -> c_3(activate^#(X))
  , activate^#(n__zeros()) -> c_5(zeros^#())
  , activate^#(n__take(X1, X2)) ->
    c_6(take^#(activate(X1), activate(X2)),
        activate^#(X1),
        activate^#(X2))
  , take^#(s(M), cons(N, IL)) -> c_11(activate^#(IL))
  , length^#(cons(N, L)) ->
    c_7(length^#(activate(L)), activate^#(L)) }
Weak DPs:
  { zeros^#() -> c_1()
  , zeros^#() -> c_2()
  , activate^#(X) -> c_4()
  , take^#(X1, X2) -> c_9()
  , take^#(0(), IL) -> c_10()
  , length^#(nil()) -> c_8() }
Weak Trs:
  { zeros() -> cons(0(), n__zeros())
  , zeros() -> n__zeros()
  , and(tt(), X) -> activate(X)
  , activate(X) -> X
  , activate(n__zeros()) -> zeros()
  , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2))
  , length(cons(N, L)) -> s(length(activate(L)))
  , length(nil()) -> 0()
  , take(X1, X2) -> n__take(X1, X2)
  , take(0(), IL) -> nil()
  , take(s(M), cons(N, IL)) -> cons(N, n__take(M, activate(IL))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We estimate the number of application of {2} by applications of
Pre({2}) = {1,3,4,5}. Here rules are labeled as follows:

  DPs:
    { 1: and^#(tt(), X) -> c_3(activate^#(X))
    , 2: activate^#(n__zeros()) -> c_5(zeros^#())
    , 3: activate^#(n__take(X1, X2)) ->
         c_6(take^#(activate(X1), activate(X2)),
             activate^#(X1),
             activate^#(X2))
    , 4: take^#(s(M), cons(N, IL)) -> c_11(activate^#(IL))
    , 5: length^#(cons(N, L)) ->
         c_7(length^#(activate(L)), activate^#(L))
    , 6: zeros^#() -> c_1()
    , 7: zeros^#() -> c_2()
    , 8: activate^#(X) -> c_4()
    , 9: take^#(X1, X2) -> c_9()
    , 10: take^#(0(), IL) -> c_10()
    , 11: length^#(nil()) -> c_8() }

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

Strict DPs:
  { and^#(tt(), X) -> c_3(activate^#(X))
  , activate^#(n__take(X1, X2)) ->
    c_6(take^#(activate(X1), activate(X2)),
        activate^#(X1),
        activate^#(X2))
  , take^#(s(M), cons(N, IL)) -> c_11(activate^#(IL))
  , length^#(cons(N, L)) ->
    c_7(length^#(activate(L)), activate^#(L)) }
Weak DPs:
  { zeros^#() -> c_1()
  , zeros^#() -> c_2()
  , activate^#(X) -> c_4()
  , activate^#(n__zeros()) -> c_5(zeros^#())
  , take^#(X1, X2) -> c_9()
  , take^#(0(), IL) -> c_10()
  , length^#(nil()) -> c_8() }
Weak Trs:
  { zeros() -> cons(0(), n__zeros())
  , zeros() -> n__zeros()
  , and(tt(), X) -> activate(X)
  , activate(X) -> X
  , activate(n__zeros()) -> zeros()
  , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2))
  , length(cons(N, L)) -> s(length(activate(L)))
  , length(nil()) -> 0()
  , take(X1, X2) -> n__take(X1, X2)
  , take(0(), IL) -> nil()
  , take(s(M), cons(N, IL)) -> cons(N, n__take(M, activate(IL))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ zeros^#() -> c_1()
, zeros^#() -> c_2()
, activate^#(X) -> c_4()
, activate^#(n__zeros()) -> c_5(zeros^#())
, take^#(X1, X2) -> c_9()
, take^#(0(), IL) -> c_10()
, length^#(nil()) -> c_8() }

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

Strict DPs:
  { and^#(tt(), X) -> c_3(activate^#(X))
  , activate^#(n__take(X1, X2)) ->
    c_6(take^#(activate(X1), activate(X2)),
        activate^#(X1),
        activate^#(X2))
  , take^#(s(M), cons(N, IL)) -> c_11(activate^#(IL))
  , length^#(cons(N, L)) ->
    c_7(length^#(activate(L)), activate^#(L)) }
Weak Trs:
  { zeros() -> cons(0(), n__zeros())
  , zeros() -> n__zeros()
  , and(tt(), X) -> activate(X)
  , activate(X) -> X
  , activate(n__zeros()) -> zeros()
  , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2))
  , length(cons(N, L)) -> s(length(activate(L)))
  , length(nil()) -> 0()
  , take(X1, X2) -> n__take(X1, X2)
  , take(0(), IL) -> nil()
  , take(s(M), cons(N, IL)) -> cons(N, n__take(M, activate(IL))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

Consider the dependency graph

  1: and^#(tt(), X) -> c_3(activate^#(X))
     -->_1 activate^#(n__take(X1, X2)) ->
           c_6(take^#(activate(X1), activate(X2)),
               activate^#(X1),
               activate^#(X2)) :2
  
  2: activate^#(n__take(X1, X2)) ->
     c_6(take^#(activate(X1), activate(X2)),
         activate^#(X1),
         activate^#(X2))
     -->_1 take^#(s(M), cons(N, IL)) -> c_11(activate^#(IL)) :3
     -->_3 activate^#(n__take(X1, X2)) ->
           c_6(take^#(activate(X1), activate(X2)),
               activate^#(X1),
               activate^#(X2)) :2
     -->_2 activate^#(n__take(X1, X2)) ->
           c_6(take^#(activate(X1), activate(X2)),
               activate^#(X1),
               activate^#(X2)) :2
  
  3: take^#(s(M), cons(N, IL)) -> c_11(activate^#(IL))
     -->_1 activate^#(n__take(X1, X2)) ->
           c_6(take^#(activate(X1), activate(X2)),
               activate^#(X1),
               activate^#(X2)) :2
  
  4: length^#(cons(N, L)) ->
     c_7(length^#(activate(L)), activate^#(L))
     -->_1 length^#(cons(N, L)) ->
           c_7(length^#(activate(L)), activate^#(L)) :4
     -->_2 activate^#(n__take(X1, X2)) ->
           c_6(take^#(activate(X1), activate(X2)),
               activate^#(X1),
               activate^#(X2)) :2
  

Following roots of the dependency graph are removed, as the
considered set of starting terms is closed under reduction with
respect to these rules (modulo compound contexts).

  { and^#(tt(), X) -> c_3(activate^#(X)) }


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

Strict DPs:
  { activate^#(n__take(X1, X2)) ->
    c_6(take^#(activate(X1), activate(X2)),
        activate^#(X1),
        activate^#(X2))
  , take^#(s(M), cons(N, IL)) -> c_11(activate^#(IL))
  , length^#(cons(N, L)) ->
    c_7(length^#(activate(L)), activate^#(L)) }
Weak Trs:
  { zeros() -> cons(0(), n__zeros())
  , zeros() -> n__zeros()
  , and(tt(), X) -> activate(X)
  , activate(X) -> X
  , activate(n__zeros()) -> zeros()
  , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2))
  , length(cons(N, L)) -> s(length(activate(L)))
  , length(nil()) -> 0()
  , take(X1, X2) -> n__take(X1, X2)
  , take(0(), IL) -> nil()
  , take(s(M), cons(N, IL)) -> cons(N, n__take(M, activate(IL))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { zeros() -> cons(0(), n__zeros())
    , zeros() -> n__zeros()
    , activate(X) -> X
    , activate(n__zeros()) -> zeros()
    , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2))
    , take(X1, X2) -> n__take(X1, X2)
    , take(0(), IL) -> nil()
    , take(s(M), cons(N, IL)) -> cons(N, n__take(M, activate(IL))) }

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

Strict DPs:
  { activate^#(n__take(X1, X2)) ->
    c_6(take^#(activate(X1), activate(X2)),
        activate^#(X1),
        activate^#(X2))
  , take^#(s(M), cons(N, IL)) -> c_11(activate^#(IL))
  , length^#(cons(N, L)) ->
    c_7(length^#(activate(L)), activate^#(L)) }
Weak Trs:
  { zeros() -> cons(0(), n__zeros())
  , zeros() -> n__zeros()
  , activate(X) -> X
  , activate(n__zeros()) -> zeros()
  , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2))
  , take(X1, X2) -> n__take(X1, X2)
  , take(0(), IL) -> nil()
  , take(s(M), cons(N, IL)) -> cons(N, n__take(M, activate(IL))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..