MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { a__eq(X, Y) -> false() , a__eq(X1, X2) -> eq(X1, X2) , a__eq(0(), 0()) -> true() , a__eq(s(X), s(Y)) -> a__eq(X, Y) , a__inf(X) -> cons(X, inf(s(X))) , a__inf(X) -> inf(X) , a__take(X1, X2) -> take(X1, X2) , a__take(0(), X) -> nil() , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L)) , a__length(X) -> length(X) , a__length(cons(X, L)) -> s(length(L)) , a__length(nil()) -> 0() , mark(0()) -> 0() , mark(true()) -> true() , mark(s(X)) -> s(X) , mark(false()) -> false() , mark(cons(X1, X2)) -> cons(X1, X2) , mark(inf(X)) -> a__inf(mark(X)) , mark(nil()) -> nil() , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) , mark(length(X)) -> a__length(mark(X)) , mark(eq(X1, X2)) -> a__eq(X1, X2) } 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 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) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { a__eq^#(X, Y) -> c_1() , a__eq^#(X1, X2) -> c_2(X1, X2) , a__eq^#(0(), 0()) -> c_3() , a__eq^#(s(X), s(Y)) -> c_4(a__eq^#(X, Y)) , a__inf^#(X) -> c_5(X, X) , a__inf^#(X) -> c_6(X) , a__take^#(X1, X2) -> c_7(X1, X2) , a__take^#(0(), X) -> c_8() , a__take^#(s(X), cons(Y, L)) -> c_9(Y, X, L) , a__length^#(X) -> c_10(X) , a__length^#(cons(X, L)) -> c_11(L) , a__length^#(nil()) -> c_12() , mark^#(0()) -> c_13() , mark^#(true()) -> c_14() , mark^#(s(X)) -> c_15(X) , mark^#(false()) -> c_16() , mark^#(cons(X1, X2)) -> c_17(X1, X2) , mark^#(inf(X)) -> c_18(a__inf^#(mark(X))) , mark^#(nil()) -> c_19() , mark^#(take(X1, X2)) -> c_20(a__take^#(mark(X1), mark(X2))) , mark^#(length(X)) -> c_21(a__length^#(mark(X))) , mark^#(eq(X1, X2)) -> c_22(a__eq^#(X1, X2)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { a__eq^#(X, Y) -> c_1() , a__eq^#(X1, X2) -> c_2(X1, X2) , a__eq^#(0(), 0()) -> c_3() , a__eq^#(s(X), s(Y)) -> c_4(a__eq^#(X, Y)) , a__inf^#(X) -> c_5(X, X) , a__inf^#(X) -> c_6(X) , a__take^#(X1, X2) -> c_7(X1, X2) , a__take^#(0(), X) -> c_8() , a__take^#(s(X), cons(Y, L)) -> c_9(Y, X, L) , a__length^#(X) -> c_10(X) , a__length^#(cons(X, L)) -> c_11(L) , a__length^#(nil()) -> c_12() , mark^#(0()) -> c_13() , mark^#(true()) -> c_14() , mark^#(s(X)) -> c_15(X) , mark^#(false()) -> c_16() , mark^#(cons(X1, X2)) -> c_17(X1, X2) , mark^#(inf(X)) -> c_18(a__inf^#(mark(X))) , mark^#(nil()) -> c_19() , mark^#(take(X1, X2)) -> c_20(a__take^#(mark(X1), mark(X2))) , mark^#(length(X)) -> c_21(a__length^#(mark(X))) , mark^#(eq(X1, X2)) -> c_22(a__eq^#(X1, X2)) } Strict Trs: { a__eq(X, Y) -> false() , a__eq(X1, X2) -> eq(X1, X2) , a__eq(0(), 0()) -> true() , a__eq(s(X), s(Y)) -> a__eq(X, Y) , a__inf(X) -> cons(X, inf(s(X))) , a__inf(X) -> inf(X) , a__take(X1, X2) -> take(X1, X2) , a__take(0(), X) -> nil() , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L)) , a__length(X) -> length(X) , a__length(cons(X, L)) -> s(length(L)) , a__length(nil()) -> 0() , mark(0()) -> 0() , mark(true()) -> true() , mark(s(X)) -> s(X) , mark(false()) -> false() , mark(cons(X1, X2)) -> cons(X1, X2) , mark(inf(X)) -> a__inf(mark(X)) , mark(nil()) -> nil() , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) , mark(length(X)) -> a__length(mark(X)) , mark(eq(X1, X2)) -> a__eq(X1, X2) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {1,3,8,12,13,14,16,19} by applications of Pre({1,3,8,12,13,14,16,19}) = {2,4,5,6,7,9,10,11,15,17,20,21,22}. Here rules are labeled as follows: DPs: { 1: a__eq^#(X, Y) -> c_1() , 2: a__eq^#(X1, X2) -> c_2(X1, X2) , 3: a__eq^#(0(), 0()) -> c_3() , 4: a__eq^#(s(X), s(Y)) -> c_4(a__eq^#(X, Y)) , 5: a__inf^#(X) -> c_5(X, X) , 6: a__inf^#(X) -> c_6(X) , 7: a__take^#(X1, X2) -> c_7(X1, X2) , 8: a__take^#(0(), X) -> c_8() , 9: a__take^#(s(X), cons(Y, L)) -> c_9(Y, X, L) , 10: a__length^#(X) -> c_10(X) , 11: a__length^#(cons(X, L)) -> c_11(L) , 12: a__length^#(nil()) -> c_12() , 13: mark^#(0()) -> c_13() , 14: mark^#(true()) -> c_14() , 15: mark^#(s(X)) -> c_15(X) , 16: mark^#(false()) -> c_16() , 17: mark^#(cons(X1, X2)) -> c_17(X1, X2) , 18: mark^#(inf(X)) -> c_18(a__inf^#(mark(X))) , 19: mark^#(nil()) -> c_19() , 20: mark^#(take(X1, X2)) -> c_20(a__take^#(mark(X1), mark(X2))) , 21: mark^#(length(X)) -> c_21(a__length^#(mark(X))) , 22: mark^#(eq(X1, X2)) -> c_22(a__eq^#(X1, X2)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { a__eq^#(X1, X2) -> c_2(X1, X2) , a__eq^#(s(X), s(Y)) -> c_4(a__eq^#(X, Y)) , a__inf^#(X) -> c_5(X, X) , a__inf^#(X) -> c_6(X) , a__take^#(X1, X2) -> c_7(X1, X2) , a__take^#(s(X), cons(Y, L)) -> c_9(Y, X, L) , a__length^#(X) -> c_10(X) , a__length^#(cons(X, L)) -> c_11(L) , mark^#(s(X)) -> c_15(X) , mark^#(cons(X1, X2)) -> c_17(X1, X2) , mark^#(inf(X)) -> c_18(a__inf^#(mark(X))) , mark^#(take(X1, X2)) -> c_20(a__take^#(mark(X1), mark(X2))) , mark^#(length(X)) -> c_21(a__length^#(mark(X))) , mark^#(eq(X1, X2)) -> c_22(a__eq^#(X1, X2)) } Strict Trs: { a__eq(X, Y) -> false() , a__eq(X1, X2) -> eq(X1, X2) , a__eq(0(), 0()) -> true() , a__eq(s(X), s(Y)) -> a__eq(X, Y) , a__inf(X) -> cons(X, inf(s(X))) , a__inf(X) -> inf(X) , a__take(X1, X2) -> take(X1, X2) , a__take(0(), X) -> nil() , a__take(s(X), cons(Y, L)) -> cons(Y, take(X, L)) , a__length(X) -> length(X) , a__length(cons(X, L)) -> s(length(L)) , a__length(nil()) -> 0() , mark(0()) -> 0() , mark(true()) -> true() , mark(s(X)) -> s(X) , mark(false()) -> false() , mark(cons(X1, X2)) -> cons(X1, X2) , mark(inf(X)) -> a__inf(mark(X)) , mark(nil()) -> nil() , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) , mark(length(X)) -> a__length(mark(X)) , mark(eq(X1, X2)) -> a__eq(X1, X2) } Weak DPs: { a__eq^#(X, Y) -> c_1() , a__eq^#(0(), 0()) -> c_3() , a__take^#(0(), X) -> c_8() , a__length^#(nil()) -> c_12() , mark^#(0()) -> c_13() , mark^#(true()) -> c_14() , mark^#(false()) -> c_16() , mark^#(nil()) -> c_19() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..