MAYBE

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

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

We add following dependency tuples:

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

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

  DPs:
    { 1: zeros^#() -> c_1()
    , 2: zeros^#() -> c_2()
    , 3: U11^#(tt(), L) -> c_3(U12^#(tt(), activate(L)), activate^#(L))
    , 4: U12^#(tt(), L) -> c_4(length^#(activate(L)), activate^#(L))
    , 5: activate^#(X) -> c_5()
    , 6: activate^#(n__zeros()) -> c_6(zeros^#())
    , 7: activate^#(n__take(X1, X2)) ->
         c_7(take^#(activate(X1), activate(X2)),
             activate^#(X1),
             activate^#(X2))
    , 8: length^#(cons(N, L)) ->
         c_8(U11^#(tt(), activate(L)), activate^#(L))
    , 9: length^#(nil()) -> c_9()
    , 10: take^#(X1, X2) -> c_13()
    , 11: take^#(0(), IL) -> c_14()
    , 12: take^#(s(M), cons(N, IL)) ->
          c_15(U21^#(tt(), activate(IL), M, N), activate^#(IL))
    , 13: U21^#(tt(), IL, M, N) ->
          c_10(U22^#(tt(), activate(IL), activate(M), activate(N)),
               activate^#(IL),
               activate^#(M),
               activate^#(N))
    , 14: U22^#(tt(), IL, M, N) ->
          c_11(U23^#(tt(), activate(IL), activate(M), activate(N)),
               activate^#(IL),
               activate^#(M),
               activate^#(N))
    , 15: U23^#(tt(), IL, M, N) ->
          c_12(activate^#(N), activate^#(M), activate^#(IL)) }

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

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

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

  DPs:
    { 1: U11^#(tt(), L) -> c_3(U12^#(tt(), activate(L)), activate^#(L))
    , 2: U12^#(tt(), L) -> c_4(length^#(activate(L)), activate^#(L))
    , 3: activate^#(n__zeros()) -> c_6(zeros^#())
    , 4: activate^#(n__take(X1, X2)) ->
         c_7(take^#(activate(X1), activate(X2)),
             activate^#(X1),
             activate^#(X2))
    , 5: length^#(cons(N, L)) ->
         c_8(U11^#(tt(), activate(L)), activate^#(L))
    , 6: take^#(s(M), cons(N, IL)) ->
         c_15(U21^#(tt(), activate(IL), M, N), activate^#(IL))
    , 7: U21^#(tt(), IL, M, N) ->
         c_10(U22^#(tt(), activate(IL), activate(M), activate(N)),
              activate^#(IL),
              activate^#(M),
              activate^#(N))
    , 8: U22^#(tt(), IL, M, N) ->
         c_11(U23^#(tt(), activate(IL), activate(M), activate(N)),
              activate^#(IL),
              activate^#(M),
              activate^#(N))
    , 9: U23^#(tt(), IL, M, N) ->
         c_12(activate^#(N), activate^#(M), activate^#(IL))
    , 10: zeros^#() -> c_1()
    , 11: zeros^#() -> c_2()
    , 12: activate^#(X) -> c_5()
    , 13: length^#(nil()) -> c_9()
    , 14: take^#(X1, X2) -> c_13()
    , 15: take^#(0(), IL) -> c_14() }

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

Strict DPs:
  { U11^#(tt(), L) -> c_3(U12^#(tt(), activate(L)), activate^#(L))
  , U12^#(tt(), L) -> c_4(length^#(activate(L)), activate^#(L))
  , activate^#(n__take(X1, X2)) ->
    c_7(take^#(activate(X1), activate(X2)),
        activate^#(X1),
        activate^#(X2))
  , length^#(cons(N, L)) ->
    c_8(U11^#(tt(), activate(L)), activate^#(L))
  , take^#(s(M), cons(N, IL)) ->
    c_15(U21^#(tt(), activate(IL), M, N), activate^#(IL))
  , U21^#(tt(), IL, M, N) ->
    c_10(U22^#(tt(), activate(IL), activate(M), activate(N)),
         activate^#(IL),
         activate^#(M),
         activate^#(N))
  , U22^#(tt(), IL, M, N) ->
    c_11(U23^#(tt(), activate(IL), activate(M), activate(N)),
         activate^#(IL),
         activate^#(M),
         activate^#(N))
  , U23^#(tt(), IL, M, N) ->
    c_12(activate^#(N), activate^#(M), activate^#(IL)) }
Weak DPs:
  { zeros^#() -> c_1()
  , zeros^#() -> c_2()
  , activate^#(X) -> c_5()
  , activate^#(n__zeros()) -> c_6(zeros^#())
  , length^#(nil()) -> c_9()
  , take^#(X1, X2) -> c_13()
  , take^#(0(), IL) -> c_14() }
Weak Trs:
  { zeros() -> cons(0(), n__zeros())
  , zeros() -> n__zeros()
  , U11(tt(), L) -> U12(tt(), activate(L))
  , U12(tt(), L) -> s(length(activate(L)))
  , activate(X) -> X
  , activate(n__zeros()) -> zeros()
  , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2))
  , length(cons(N, L)) -> U11(tt(), activate(L))
  , length(nil()) -> 0()
  , U21(tt(), IL, M, N) ->
    U22(tt(), activate(IL), activate(M), activate(N))
  , U22(tt(), IL, M, N) ->
    U23(tt(), activate(IL), activate(M), activate(N))
  , U23(tt(), IL, M, N) ->
    cons(activate(N), n__take(activate(M), activate(IL)))
  , take(X1, X2) -> n__take(X1, X2)
  , take(0(), IL) -> nil()
  , take(s(M), cons(N, IL)) -> U21(tt(), activate(IL), M, N) }
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_5()
, activate^#(n__zeros()) -> c_6(zeros^#())
, length^#(nil()) -> c_9()
, take^#(X1, X2) -> c_13()
, take^#(0(), IL) -> c_14() }

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

Strict DPs:
  { U11^#(tt(), L) -> c_3(U12^#(tt(), activate(L)), activate^#(L))
  , U12^#(tt(), L) -> c_4(length^#(activate(L)), activate^#(L))
  , activate^#(n__take(X1, X2)) ->
    c_7(take^#(activate(X1), activate(X2)),
        activate^#(X1),
        activate^#(X2))
  , length^#(cons(N, L)) ->
    c_8(U11^#(tt(), activate(L)), activate^#(L))
  , take^#(s(M), cons(N, IL)) ->
    c_15(U21^#(tt(), activate(IL), M, N), activate^#(IL))
  , U21^#(tt(), IL, M, N) ->
    c_10(U22^#(tt(), activate(IL), activate(M), activate(N)),
         activate^#(IL),
         activate^#(M),
         activate^#(N))
  , U22^#(tt(), IL, M, N) ->
    c_11(U23^#(tt(), activate(IL), activate(M), activate(N)),
         activate^#(IL),
         activate^#(M),
         activate^#(N))
  , U23^#(tt(), IL, M, N) ->
    c_12(activate^#(N), activate^#(M), activate^#(IL)) }
Weak Trs:
  { zeros() -> cons(0(), n__zeros())
  , zeros() -> n__zeros()
  , U11(tt(), L) -> U12(tt(), activate(L))
  , U12(tt(), L) -> s(length(activate(L)))
  , activate(X) -> X
  , activate(n__zeros()) -> zeros()
  , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2))
  , length(cons(N, L)) -> U11(tt(), activate(L))
  , length(nil()) -> 0()
  , U21(tt(), IL, M, N) ->
    U22(tt(), activate(IL), activate(M), activate(N))
  , U22(tt(), IL, M, N) ->
    U23(tt(), activate(IL), activate(M), activate(N))
  , U23(tt(), IL, M, N) ->
    cons(activate(N), n__take(activate(M), activate(IL)))
  , take(X1, X2) -> n__take(X1, X2)
  , take(0(), IL) -> nil()
  , take(s(M), cons(N, IL)) -> U21(tt(), activate(IL), M, N) }
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))
    , U21(tt(), IL, M, N) ->
      U22(tt(), activate(IL), activate(M), activate(N))
    , U22(tt(), IL, M, N) ->
      U23(tt(), activate(IL), activate(M), activate(N))
    , U23(tt(), IL, M, N) ->
      cons(activate(N), n__take(activate(M), activate(IL)))
    , take(X1, X2) -> n__take(X1, X2)
    , take(0(), IL) -> nil()
    , take(s(M), cons(N, IL)) -> U21(tt(), activate(IL), M, N) }

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

Strict DPs:
  { U11^#(tt(), L) -> c_3(U12^#(tt(), activate(L)), activate^#(L))
  , U12^#(tt(), L) -> c_4(length^#(activate(L)), activate^#(L))
  , activate^#(n__take(X1, X2)) ->
    c_7(take^#(activate(X1), activate(X2)),
        activate^#(X1),
        activate^#(X2))
  , length^#(cons(N, L)) ->
    c_8(U11^#(tt(), activate(L)), activate^#(L))
  , take^#(s(M), cons(N, IL)) ->
    c_15(U21^#(tt(), activate(IL), M, N), activate^#(IL))
  , U21^#(tt(), IL, M, N) ->
    c_10(U22^#(tt(), activate(IL), activate(M), activate(N)),
         activate^#(IL),
         activate^#(M),
         activate^#(N))
  , U22^#(tt(), IL, M, N) ->
    c_11(U23^#(tt(), activate(IL), activate(M), activate(N)),
         activate^#(IL),
         activate^#(M),
         activate^#(N))
  , U23^#(tt(), IL, M, N) ->
    c_12(activate^#(N), activate^#(M), activate^#(IL)) }
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))
  , U21(tt(), IL, M, N) ->
    U22(tt(), activate(IL), activate(M), activate(N))
  , U22(tt(), IL, M, N) ->
    U23(tt(), activate(IL), activate(M), activate(N))
  , U23(tt(), IL, M, N) ->
    cons(activate(N), n__take(activate(M), activate(IL)))
  , take(X1, X2) -> n__take(X1, X2)
  , take(0(), IL) -> nil()
  , take(s(M), cons(N, IL)) -> U21(tt(), activate(IL), M, N) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..