MAYBE

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

Strict Trs:
  { from(X) -> cons(X, n__from(s(X)))
  , from(X) -> n__from(X)
  , cons(X1, X2) -> n__cons(X1, X2)
  , length(n__nil()) -> 0()
  , length(n__cons(X, Y)) -> s(length1(activate(Y)))
  , length1(X) -> length(activate(X))
  , activate(X) -> X
  , activate(n__from(X)) -> from(X)
  , activate(n__nil()) -> nil()
  , activate(n__cons(X1, X2)) -> cons(X1, X2)
  , nil() -> n__nil() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { from^#(X) -> c_1(cons^#(X, n__from(s(X))))
  , from^#(X) -> c_2()
  , cons^#(X1, X2) -> c_3()
  , length^#(n__nil()) -> c_4()
  , length^#(n__cons(X, Y)) ->
    c_5(length1^#(activate(Y)), activate^#(Y))
  , length1^#(X) -> c_6(length^#(activate(X)), activate^#(X))
  , activate^#(X) -> c_7()
  , activate^#(n__from(X)) -> c_8(from^#(X))
  , activate^#(n__nil()) -> c_9(nil^#())
  , activate^#(n__cons(X1, X2)) -> c_10(cons^#(X1, X2))
  , nil^#() -> c_11() }

and mark the set of starting terms.

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

Strict DPs:
  { from^#(X) -> c_1(cons^#(X, n__from(s(X))))
  , from^#(X) -> c_2()
  , cons^#(X1, X2) -> c_3()
  , length^#(n__nil()) -> c_4()
  , length^#(n__cons(X, Y)) ->
    c_5(length1^#(activate(Y)), activate^#(Y))
  , length1^#(X) -> c_6(length^#(activate(X)), activate^#(X))
  , activate^#(X) -> c_7()
  , activate^#(n__from(X)) -> c_8(from^#(X))
  , activate^#(n__nil()) -> c_9(nil^#())
  , activate^#(n__cons(X1, X2)) -> c_10(cons^#(X1, X2))
  , nil^#() -> c_11() }
Weak Trs:
  { from(X) -> cons(X, n__from(s(X)))
  , from(X) -> n__from(X)
  , cons(X1, X2) -> n__cons(X1, X2)
  , length(n__nil()) -> 0()
  , length(n__cons(X, Y)) -> s(length1(activate(Y)))
  , length1(X) -> length(activate(X))
  , activate(X) -> X
  , activate(n__from(X)) -> from(X)
  , activate(n__nil()) -> nil()
  , activate(n__cons(X1, X2)) -> cons(X1, X2)
  , nil() -> n__nil() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: from^#(X) -> c_1(cons^#(X, n__from(s(X))))
    , 2: from^#(X) -> c_2()
    , 3: cons^#(X1, X2) -> c_3()
    , 4: length^#(n__nil()) -> c_4()
    , 5: length^#(n__cons(X, Y)) ->
         c_5(length1^#(activate(Y)), activate^#(Y))
    , 6: length1^#(X) -> c_6(length^#(activate(X)), activate^#(X))
    , 7: activate^#(X) -> c_7()
    , 8: activate^#(n__from(X)) -> c_8(from^#(X))
    , 9: activate^#(n__nil()) -> c_9(nil^#())
    , 10: activate^#(n__cons(X1, X2)) -> c_10(cons^#(X1, X2))
    , 11: nil^#() -> c_11() }

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

Strict DPs:
  { from^#(X) -> c_1(cons^#(X, n__from(s(X))))
  , length^#(n__cons(X, Y)) ->
    c_5(length1^#(activate(Y)), activate^#(Y))
  , length1^#(X) -> c_6(length^#(activate(X)), activate^#(X))
  , activate^#(n__from(X)) -> c_8(from^#(X))
  , activate^#(n__nil()) -> c_9(nil^#())
  , activate^#(n__cons(X1, X2)) -> c_10(cons^#(X1, X2)) }
Weak DPs:
  { from^#(X) -> c_2()
  , cons^#(X1, X2) -> c_3()
  , length^#(n__nil()) -> c_4()
  , activate^#(X) -> c_7()
  , nil^#() -> c_11() }
Weak Trs:
  { from(X) -> cons(X, n__from(s(X)))
  , from(X) -> n__from(X)
  , cons(X1, X2) -> n__cons(X1, X2)
  , length(n__nil()) -> 0()
  , length(n__cons(X, Y)) -> s(length1(activate(Y)))
  , length1(X) -> length(activate(X))
  , activate(X) -> X
  , activate(n__from(X)) -> from(X)
  , activate(n__nil()) -> nil()
  , activate(n__cons(X1, X2)) -> cons(X1, X2)
  , nil() -> n__nil() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: from^#(X) -> c_1(cons^#(X, n__from(s(X))))
    , 2: length^#(n__cons(X, Y)) ->
         c_5(length1^#(activate(Y)), activate^#(Y))
    , 3: length1^#(X) -> c_6(length^#(activate(X)), activate^#(X))
    , 4: activate^#(n__from(X)) -> c_8(from^#(X))
    , 5: activate^#(n__nil()) -> c_9(nil^#())
    , 6: activate^#(n__cons(X1, X2)) -> c_10(cons^#(X1, X2))
    , 7: from^#(X) -> c_2()
    , 8: cons^#(X1, X2) -> c_3()
    , 9: length^#(n__nil()) -> c_4()
    , 10: activate^#(X) -> c_7()
    , 11: nil^#() -> c_11() }

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

Strict DPs:
  { length^#(n__cons(X, Y)) ->
    c_5(length1^#(activate(Y)), activate^#(Y))
  , length1^#(X) -> c_6(length^#(activate(X)), activate^#(X))
  , activate^#(n__from(X)) -> c_8(from^#(X)) }
Weak DPs:
  { from^#(X) -> c_1(cons^#(X, n__from(s(X))))
  , from^#(X) -> c_2()
  , cons^#(X1, X2) -> c_3()
  , length^#(n__nil()) -> c_4()
  , activate^#(X) -> c_7()
  , activate^#(n__nil()) -> c_9(nil^#())
  , activate^#(n__cons(X1, X2)) -> c_10(cons^#(X1, X2))
  , nil^#() -> c_11() }
Weak Trs:
  { from(X) -> cons(X, n__from(s(X)))
  , from(X) -> n__from(X)
  , cons(X1, X2) -> n__cons(X1, X2)
  , length(n__nil()) -> 0()
  , length(n__cons(X, Y)) -> s(length1(activate(Y)))
  , length1(X) -> length(activate(X))
  , activate(X) -> X
  , activate(n__from(X)) -> from(X)
  , activate(n__nil()) -> nil()
  , activate(n__cons(X1, X2)) -> cons(X1, X2)
  , nil() -> n__nil() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  DPs:
    { 1: length^#(n__cons(X, Y)) ->
         c_5(length1^#(activate(Y)), activate^#(Y))
    , 2: length1^#(X) -> c_6(length^#(activate(X)), activate^#(X))
    , 3: activate^#(n__from(X)) -> c_8(from^#(X))
    , 4: from^#(X) -> c_1(cons^#(X, n__from(s(X))))
    , 5: from^#(X) -> c_2()
    , 6: cons^#(X1, X2) -> c_3()
    , 7: length^#(n__nil()) -> c_4()
    , 8: activate^#(X) -> c_7()
    , 9: activate^#(n__nil()) -> c_9(nil^#())
    , 10: activate^#(n__cons(X1, X2)) -> c_10(cons^#(X1, X2))
    , 11: nil^#() -> c_11() }

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

Strict DPs:
  { length^#(n__cons(X, Y)) ->
    c_5(length1^#(activate(Y)), activate^#(Y))
  , length1^#(X) -> c_6(length^#(activate(X)), activate^#(X)) }
Weak DPs:
  { from^#(X) -> c_1(cons^#(X, n__from(s(X))))
  , from^#(X) -> c_2()
  , cons^#(X1, X2) -> c_3()
  , length^#(n__nil()) -> c_4()
  , activate^#(X) -> c_7()
  , activate^#(n__from(X)) -> c_8(from^#(X))
  , activate^#(n__nil()) -> c_9(nil^#())
  , activate^#(n__cons(X1, X2)) -> c_10(cons^#(X1, X2))
  , nil^#() -> c_11() }
Weak Trs:
  { from(X) -> cons(X, n__from(s(X)))
  , from(X) -> n__from(X)
  , cons(X1, X2) -> n__cons(X1, X2)
  , length(n__nil()) -> 0()
  , length(n__cons(X, Y)) -> s(length1(activate(Y)))
  , length1(X) -> length(activate(X))
  , activate(X) -> X
  , activate(n__from(X)) -> from(X)
  , activate(n__nil()) -> nil()
  , activate(n__cons(X1, X2)) -> cons(X1, X2)
  , nil() -> n__nil() }
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.

{ from^#(X) -> c_1(cons^#(X, n__from(s(X))))
, from^#(X) -> c_2()
, cons^#(X1, X2) -> c_3()
, length^#(n__nil()) -> c_4()
, activate^#(X) -> c_7()
, activate^#(n__from(X)) -> c_8(from^#(X))
, activate^#(n__nil()) -> c_9(nil^#())
, activate^#(n__cons(X1, X2)) -> c_10(cons^#(X1, X2))
, nil^#() -> c_11() }

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

Strict DPs:
  { length^#(n__cons(X, Y)) ->
    c_5(length1^#(activate(Y)), activate^#(Y))
  , length1^#(X) -> c_6(length^#(activate(X)), activate^#(X)) }
Weak Trs:
  { from(X) -> cons(X, n__from(s(X)))
  , from(X) -> n__from(X)
  , cons(X1, X2) -> n__cons(X1, X2)
  , length(n__nil()) -> 0()
  , length(n__cons(X, Y)) -> s(length1(activate(Y)))
  , length1(X) -> length(activate(X))
  , activate(X) -> X
  , activate(n__from(X)) -> from(X)
  , activate(n__nil()) -> nil()
  , activate(n__cons(X1, X2)) -> cons(X1, X2)
  , nil() -> n__nil() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:

  { length^#(n__cons(X, Y)) ->
    c_5(length1^#(activate(Y)), activate^#(Y))
  , length1^#(X) -> c_6(length^#(activate(X)), activate^#(X)) }

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

Strict DPs:
  { length^#(n__cons(X, Y)) -> c_1(length1^#(activate(Y)))
  , length1^#(X) -> c_2(length^#(activate(X))) }
Weak Trs:
  { from(X) -> cons(X, n__from(s(X)))
  , from(X) -> n__from(X)
  , cons(X1, X2) -> n__cons(X1, X2)
  , length(n__nil()) -> 0()
  , length(n__cons(X, Y)) -> s(length1(activate(Y)))
  , length1(X) -> length(activate(X))
  , activate(X) -> X
  , activate(n__from(X)) -> from(X)
  , activate(n__nil()) -> nil()
  , activate(n__cons(X1, X2)) -> cons(X1, X2)
  , nil() -> n__nil() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { from(X) -> cons(X, n__from(s(X)))
    , from(X) -> n__from(X)
    , cons(X1, X2) -> n__cons(X1, X2)
    , activate(X) -> X
    , activate(n__from(X)) -> from(X)
    , activate(n__nil()) -> nil()
    , activate(n__cons(X1, X2)) -> cons(X1, X2)
    , nil() -> n__nil() }

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

Strict DPs:
  { length^#(n__cons(X, Y)) -> c_1(length1^#(activate(Y)))
  , length1^#(X) -> c_2(length^#(activate(X))) }
Weak Trs:
  { from(X) -> cons(X, n__from(s(X)))
  , from(X) -> n__from(X)
  , cons(X1, X2) -> n__cons(X1, X2)
  , activate(X) -> X
  , activate(n__from(X)) -> from(X)
  , activate(n__nil()) -> nil()
  , activate(n__cons(X1, X2)) -> cons(X1, X2)
  , nil() -> n__nil() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..