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: 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) '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) '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: { from^#(X) -> c_1(cons^#(X, n__from(s(X)))) , from^#(X) -> c_2(X) , cons^#(X1, X2) -> c_3(X1, X2) , length^#(n__nil()) -> c_4() , length^#(n__cons(X, Y)) -> c_5(length1^#(activate(Y))) , length1^#(X) -> c_6(length^#(activate(X))) , activate^#(X) -> c_7(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)) , 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(X) , cons^#(X1, X2) -> c_3(X1, X2) , length^#(n__nil()) -> c_4() , length^#(n__cons(X, Y)) -> c_5(length1^#(activate(Y))) , length1^#(X) -> c_6(length^#(activate(X))) , activate^#(X) -> c_7(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)) , nil^#() -> c_11() } 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: runtime complexity Answer: MAYBE We estimate the number of application of {4,11} by applications of Pre({4,11}) = {2,3,6,7,9}. Here rules are labeled as follows: DPs: { 1: from^#(X) -> c_1(cons^#(X, n__from(s(X)))) , 2: from^#(X) -> c_2(X) , 3: cons^#(X1, X2) -> c_3(X1, X2) , 4: length^#(n__nil()) -> c_4() , 5: length^#(n__cons(X, Y)) -> c_5(length1^#(activate(Y))) , 6: length1^#(X) -> c_6(length^#(activate(X))) , 7: activate^#(X) -> c_7(X) , 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)))) , from^#(X) -> c_2(X) , cons^#(X1, X2) -> c_3(X1, X2) , length^#(n__cons(X, Y)) -> c_5(length1^#(activate(Y))) , length1^#(X) -> c_6(length^#(activate(X))) , activate^#(X) -> c_7(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)) } 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() } Weak DPs: { length^#(n__nil()) -> c_4() , nil^#() -> c_11() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {8} by applications of Pre({8}) = {2,3,6}. Here rules are labeled as follows: DPs: { 1: from^#(X) -> c_1(cons^#(X, n__from(s(X)))) , 2: from^#(X) -> c_2(X) , 3: cons^#(X1, X2) -> c_3(X1, X2) , 4: length^#(n__cons(X, Y)) -> c_5(length1^#(activate(Y))) , 5: length1^#(X) -> c_6(length^#(activate(X))) , 6: activate^#(X) -> c_7(X) , 7: activate^#(n__from(X)) -> c_8(from^#(X)) , 8: activate^#(n__nil()) -> c_9(nil^#()) , 9: activate^#(n__cons(X1, X2)) -> c_10(cons^#(X1, X2)) , 10: length^#(n__nil()) -> c_4() , 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)))) , from^#(X) -> c_2(X) , cons^#(X1, X2) -> c_3(X1, X2) , length^#(n__cons(X, Y)) -> c_5(length1^#(activate(Y))) , length1^#(X) -> c_6(length^#(activate(X))) , activate^#(X) -> c_7(X) , activate^#(n__from(X)) -> c_8(from^#(X)) , activate^#(n__cons(X1, X2)) -> c_10(cons^#(X1, X2)) } 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() } Weak DPs: { length^#(n__nil()) -> c_4() , activate^#(n__nil()) -> c_9(nil^#()) , nil^#() -> c_11() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..