MAYBE 1055.44/297.03 MAYBE 1055.44/297.03 1055.44/297.03 We are left with following problem, upon which TcT provides the 1055.44/297.03 certificate MAYBE. 1055.44/297.03 1055.44/297.03 Strict Trs: 1055.44/297.03 { active(from(X)) -> from(active(X)) 1055.44/297.03 , active(from(X)) -> mark(cons(X, from(s(X)))) 1055.44/297.03 , active(cons(X1, X2)) -> cons(active(X1), X2) 1055.44/297.03 , active(s(X)) -> s(active(X)) 1055.44/297.03 , active(first(X1, X2)) -> first(X1, active(X2)) 1055.44/297.03 , active(first(X1, X2)) -> first(active(X1), X2) 1055.44/297.03 , active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))) 1055.44/297.03 , active(first(0(), Z)) -> mark(nil()) 1055.44/297.03 , active(sel(X1, X2)) -> sel(X1, active(X2)) 1055.44/297.03 , active(sel(X1, X2)) -> sel(active(X1), X2) 1055.44/297.03 , active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)) 1055.44/297.03 , active(sel(0(), cons(X, Z))) -> mark(X) 1055.44/297.03 , from(mark(X)) -> mark(from(X)) 1055.44/297.03 , from(ok(X)) -> ok(from(X)) 1055.44/297.03 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 1055.44/297.03 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 1055.44/297.03 , s(mark(X)) -> mark(s(X)) 1055.44/297.03 , s(ok(X)) -> ok(s(X)) 1055.44/297.03 , first(X1, mark(X2)) -> mark(first(X1, X2)) 1055.44/297.03 , first(mark(X1), X2) -> mark(first(X1, X2)) 1055.44/297.03 , first(ok(X1), ok(X2)) -> ok(first(X1, X2)) 1055.44/297.03 , sel(X1, mark(X2)) -> mark(sel(X1, X2)) 1055.44/297.03 , sel(mark(X1), X2) -> mark(sel(X1, X2)) 1055.44/297.03 , sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)) 1055.44/297.03 , proper(from(X)) -> from(proper(X)) 1055.44/297.03 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 1055.44/297.03 , proper(s(X)) -> s(proper(X)) 1055.44/297.03 , proper(first(X1, X2)) -> first(proper(X1), proper(X2)) 1055.44/297.03 , proper(0()) -> ok(0()) 1055.44/297.03 , proper(nil()) -> ok(nil()) 1055.44/297.03 , proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)) 1055.44/297.03 , top(mark(X)) -> top(proper(X)) 1055.44/297.03 , top(ok(X)) -> top(active(X)) } 1055.44/297.03 Obligation: 1055.44/297.03 runtime complexity 1055.44/297.03 Answer: 1055.44/297.03 MAYBE 1055.44/297.03 1055.44/297.03 None of the processors succeeded. 1055.44/297.03 1055.44/297.03 Details of failed attempt(s): 1055.44/297.03 ----------------------------- 1055.44/297.03 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1055.44/297.03 following reason: 1055.44/297.03 1055.44/297.03 Computation stopped due to timeout after 297.0 seconds. 1055.44/297.03 1055.44/297.03 2) 'Best' failed due to the following reason: 1055.44/297.03 1055.44/297.03 None of the processors succeeded. 1055.44/297.03 1055.44/297.03 Details of failed attempt(s): 1055.44/297.03 ----------------------------- 1055.44/297.03 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1055.44/297.03 seconds)' failed due to the following reason: 1055.44/297.03 1055.44/297.03 Computation stopped due to timeout after 148.0 seconds. 1055.44/297.03 1055.44/297.03 2) 'Best' failed due to the following reason: 1055.44/297.03 1055.44/297.03 None of the processors succeeded. 1055.44/297.03 1055.44/297.03 Details of failed attempt(s): 1055.44/297.03 ----------------------------- 1055.44/297.03 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1055.44/297.03 following reason: 1055.44/297.03 1055.44/297.03 The processor is inapplicable, reason: 1055.44/297.03 Processor only applicable for innermost runtime complexity analysis 1055.44/297.03 1055.44/297.03 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1055.44/297.03 to the following reason: 1055.44/297.03 1055.44/297.03 The processor is inapplicable, reason: 1055.44/297.03 Processor only applicable for innermost runtime complexity analysis 1055.44/297.03 1055.44/297.03 1055.44/297.03 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1055.44/297.03 failed due to the following reason: 1055.44/297.03 1055.44/297.03 None of the processors succeeded. 1055.44/297.03 1055.44/297.03 Details of failed attempt(s): 1055.44/297.03 ----------------------------- 1055.44/297.03 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1055.44/297.03 failed due to the following reason: 1055.44/297.03 1055.44/297.03 match-boundness of the problem could not be verified. 1055.44/297.03 1055.44/297.03 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1055.44/297.03 failed due to the following reason: 1055.44/297.03 1055.44/297.03 match-boundness of the problem could not be verified. 1055.44/297.03 1055.44/297.03 1055.44/297.03 1055.44/297.03 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1055.44/297.03 the following reason: 1055.44/297.03 1055.44/297.03 We add the following weak dependency pairs: 1055.44/297.03 1055.44/297.03 Strict DPs: 1055.44/297.03 { active^#(from(X)) -> c_1(from^#(active(X))) 1055.44/297.03 , active^#(from(X)) -> c_2(cons^#(X, from(s(X)))) 1055.44/297.03 , active^#(cons(X1, X2)) -> c_3(cons^#(active(X1), X2)) 1055.44/297.03 , active^#(s(X)) -> c_4(s^#(active(X))) 1055.44/297.03 , active^#(first(X1, X2)) -> c_5(first^#(X1, active(X2))) 1055.44/297.03 , active^#(first(X1, X2)) -> c_6(first^#(active(X1), X2)) 1055.44/297.03 , active^#(first(s(X), cons(Y, Z))) -> c_7(cons^#(Y, first(X, Z))) 1055.44/297.03 , active^#(first(0(), Z)) -> c_8() 1055.44/297.03 , active^#(sel(X1, X2)) -> c_9(sel^#(X1, active(X2))) 1055.44/297.03 , active^#(sel(X1, X2)) -> c_10(sel^#(active(X1), X2)) 1055.44/297.03 , active^#(sel(s(X), cons(Y, Z))) -> c_11(sel^#(X, Z)) 1055.44/297.03 , active^#(sel(0(), cons(X, Z))) -> c_12(X) 1055.44/297.03 , from^#(mark(X)) -> c_13(from^#(X)) 1055.44/297.03 , from^#(ok(X)) -> c_14(from^#(X)) 1055.44/297.03 , cons^#(mark(X1), X2) -> c_15(cons^#(X1, X2)) 1055.44/297.03 , cons^#(ok(X1), ok(X2)) -> c_16(cons^#(X1, X2)) 1055.44/297.03 , s^#(mark(X)) -> c_17(s^#(X)) 1055.44/297.03 , s^#(ok(X)) -> c_18(s^#(X)) 1055.44/297.03 , first^#(X1, mark(X2)) -> c_19(first^#(X1, X2)) 1055.44/297.03 , first^#(mark(X1), X2) -> c_20(first^#(X1, X2)) 1055.44/297.03 , first^#(ok(X1), ok(X2)) -> c_21(first^#(X1, X2)) 1055.44/297.03 , sel^#(X1, mark(X2)) -> c_22(sel^#(X1, X2)) 1055.44/297.03 , sel^#(mark(X1), X2) -> c_23(sel^#(X1, X2)) 1055.44/297.03 , sel^#(ok(X1), ok(X2)) -> c_24(sel^#(X1, X2)) 1055.44/297.03 , proper^#(from(X)) -> c_25(from^#(proper(X))) 1055.44/297.03 , proper^#(cons(X1, X2)) -> c_26(cons^#(proper(X1), proper(X2))) 1055.44/297.03 , proper^#(s(X)) -> c_27(s^#(proper(X))) 1055.44/297.03 , proper^#(first(X1, X2)) -> c_28(first^#(proper(X1), proper(X2))) 1055.44/297.03 , proper^#(0()) -> c_29() 1055.44/297.03 , proper^#(nil()) -> c_30() 1055.44/297.03 , proper^#(sel(X1, X2)) -> c_31(sel^#(proper(X1), proper(X2))) 1055.44/297.03 , top^#(mark(X)) -> c_32(top^#(proper(X))) 1055.44/297.03 , top^#(ok(X)) -> c_33(top^#(active(X))) } 1055.44/297.03 1055.44/297.03 and mark the set of starting terms. 1055.44/297.03 1055.44/297.03 We are left with following problem, upon which TcT provides the 1055.44/297.03 certificate MAYBE. 1055.44/297.03 1055.44/297.03 Strict DPs: 1055.44/297.03 { active^#(from(X)) -> c_1(from^#(active(X))) 1055.44/297.03 , active^#(from(X)) -> c_2(cons^#(X, from(s(X)))) 1055.44/297.03 , active^#(cons(X1, X2)) -> c_3(cons^#(active(X1), X2)) 1055.44/297.03 , active^#(s(X)) -> c_4(s^#(active(X))) 1055.44/297.03 , active^#(first(X1, X2)) -> c_5(first^#(X1, active(X2))) 1055.44/297.03 , active^#(first(X1, X2)) -> c_6(first^#(active(X1), X2)) 1055.44/297.03 , active^#(first(s(X), cons(Y, Z))) -> c_7(cons^#(Y, first(X, Z))) 1055.44/297.03 , active^#(first(0(), Z)) -> c_8() 1055.44/297.03 , active^#(sel(X1, X2)) -> c_9(sel^#(X1, active(X2))) 1055.44/297.03 , active^#(sel(X1, X2)) -> c_10(sel^#(active(X1), X2)) 1055.44/297.03 , active^#(sel(s(X), cons(Y, Z))) -> c_11(sel^#(X, Z)) 1055.44/297.03 , active^#(sel(0(), cons(X, Z))) -> c_12(X) 1055.44/297.03 , from^#(mark(X)) -> c_13(from^#(X)) 1055.44/297.03 , from^#(ok(X)) -> c_14(from^#(X)) 1055.44/297.03 , cons^#(mark(X1), X2) -> c_15(cons^#(X1, X2)) 1055.44/297.03 , cons^#(ok(X1), ok(X2)) -> c_16(cons^#(X1, X2)) 1055.44/297.03 , s^#(mark(X)) -> c_17(s^#(X)) 1055.44/297.03 , s^#(ok(X)) -> c_18(s^#(X)) 1055.44/297.03 , first^#(X1, mark(X2)) -> c_19(first^#(X1, X2)) 1055.44/297.03 , first^#(mark(X1), X2) -> c_20(first^#(X1, X2)) 1055.44/297.03 , first^#(ok(X1), ok(X2)) -> c_21(first^#(X1, X2)) 1055.44/297.03 , sel^#(X1, mark(X2)) -> c_22(sel^#(X1, X2)) 1055.44/297.03 , sel^#(mark(X1), X2) -> c_23(sel^#(X1, X2)) 1055.44/297.03 , sel^#(ok(X1), ok(X2)) -> c_24(sel^#(X1, X2)) 1055.44/297.03 , proper^#(from(X)) -> c_25(from^#(proper(X))) 1055.44/297.03 , proper^#(cons(X1, X2)) -> c_26(cons^#(proper(X1), proper(X2))) 1055.44/297.03 , proper^#(s(X)) -> c_27(s^#(proper(X))) 1055.44/297.03 , proper^#(first(X1, X2)) -> c_28(first^#(proper(X1), proper(X2))) 1055.44/297.03 , proper^#(0()) -> c_29() 1055.44/297.03 , proper^#(nil()) -> c_30() 1055.44/297.03 , proper^#(sel(X1, X2)) -> c_31(sel^#(proper(X1), proper(X2))) 1055.44/297.03 , top^#(mark(X)) -> c_32(top^#(proper(X))) 1055.44/297.03 , top^#(ok(X)) -> c_33(top^#(active(X))) } 1055.44/297.03 Strict Trs: 1055.44/297.03 { active(from(X)) -> from(active(X)) 1055.44/297.03 , active(from(X)) -> mark(cons(X, from(s(X)))) 1055.44/297.03 , active(cons(X1, X2)) -> cons(active(X1), X2) 1055.44/297.03 , active(s(X)) -> s(active(X)) 1055.44/297.03 , active(first(X1, X2)) -> first(X1, active(X2)) 1055.44/297.03 , active(first(X1, X2)) -> first(active(X1), X2) 1055.44/297.03 , active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))) 1055.44/297.03 , active(first(0(), Z)) -> mark(nil()) 1055.44/297.03 , active(sel(X1, X2)) -> sel(X1, active(X2)) 1055.44/297.03 , active(sel(X1, X2)) -> sel(active(X1), X2) 1055.44/297.03 , active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)) 1055.44/297.03 , active(sel(0(), cons(X, Z))) -> mark(X) 1055.44/297.03 , from(mark(X)) -> mark(from(X)) 1055.44/297.03 , from(ok(X)) -> ok(from(X)) 1055.44/297.03 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 1055.44/297.03 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 1055.44/297.03 , s(mark(X)) -> mark(s(X)) 1055.44/297.03 , s(ok(X)) -> ok(s(X)) 1055.44/297.03 , first(X1, mark(X2)) -> mark(first(X1, X2)) 1055.44/297.03 , first(mark(X1), X2) -> mark(first(X1, X2)) 1055.44/297.03 , first(ok(X1), ok(X2)) -> ok(first(X1, X2)) 1055.44/297.03 , sel(X1, mark(X2)) -> mark(sel(X1, X2)) 1055.44/297.03 , sel(mark(X1), X2) -> mark(sel(X1, X2)) 1055.44/297.03 , sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)) 1055.44/297.03 , proper(from(X)) -> from(proper(X)) 1055.44/297.03 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 1055.44/297.03 , proper(s(X)) -> s(proper(X)) 1055.44/297.03 , proper(first(X1, X2)) -> first(proper(X1), proper(X2)) 1055.44/297.03 , proper(0()) -> ok(0()) 1055.44/297.03 , proper(nil()) -> ok(nil()) 1055.44/297.03 , proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)) 1055.44/297.03 , top(mark(X)) -> top(proper(X)) 1055.44/297.03 , top(ok(X)) -> top(active(X)) } 1055.44/297.03 Obligation: 1055.44/297.03 runtime complexity 1055.44/297.03 Answer: 1055.44/297.03 MAYBE 1055.44/297.03 1055.44/297.03 Consider the dependency graph: 1055.44/297.03 1055.44/297.03 1: active^#(from(X)) -> c_1(from^#(active(X))) 1055.44/297.03 -->_1 from^#(ok(X)) -> c_14(from^#(X)) :14 1055.44/297.03 -->_1 from^#(mark(X)) -> c_13(from^#(X)) :13 1055.44/297.03 1055.44/297.03 2: active^#(from(X)) -> c_2(cons^#(X, from(s(X)))) 1055.44/297.03 -->_1 cons^#(ok(X1), ok(X2)) -> c_16(cons^#(X1, X2)) :16 1055.44/297.03 -->_1 cons^#(mark(X1), X2) -> c_15(cons^#(X1, X2)) :15 1055.44/297.03 1055.44/297.03 3: active^#(cons(X1, X2)) -> c_3(cons^#(active(X1), X2)) 1055.44/297.03 -->_1 cons^#(ok(X1), ok(X2)) -> c_16(cons^#(X1, X2)) :16 1055.44/297.03 -->_1 cons^#(mark(X1), X2) -> c_15(cons^#(X1, X2)) :15 1055.44/297.03 1055.44/297.03 4: active^#(s(X)) -> c_4(s^#(active(X))) 1055.44/297.03 -->_1 s^#(ok(X)) -> c_18(s^#(X)) :18 1055.44/297.03 -->_1 s^#(mark(X)) -> c_17(s^#(X)) :17 1055.44/297.03 1055.44/297.03 5: active^#(first(X1, X2)) -> c_5(first^#(X1, active(X2))) 1055.44/297.03 -->_1 first^#(ok(X1), ok(X2)) -> c_21(first^#(X1, X2)) :21 1055.44/297.03 -->_1 first^#(mark(X1), X2) -> c_20(first^#(X1, X2)) :20 1055.44/297.03 -->_1 first^#(X1, mark(X2)) -> c_19(first^#(X1, X2)) :19 1055.44/297.03 1055.44/297.03 6: active^#(first(X1, X2)) -> c_6(first^#(active(X1), X2)) 1055.44/297.03 -->_1 first^#(ok(X1), ok(X2)) -> c_21(first^#(X1, X2)) :21 1055.44/297.03 -->_1 first^#(mark(X1), X2) -> c_20(first^#(X1, X2)) :20 1055.44/297.03 -->_1 first^#(X1, mark(X2)) -> c_19(first^#(X1, X2)) :19 1055.44/297.03 1055.44/297.03 7: active^#(first(s(X), cons(Y, Z))) -> c_7(cons^#(Y, first(X, Z))) 1055.44/297.03 -->_1 cons^#(ok(X1), ok(X2)) -> c_16(cons^#(X1, X2)) :16 1055.44/297.03 -->_1 cons^#(mark(X1), X2) -> c_15(cons^#(X1, X2)) :15 1055.44/297.03 1055.44/297.03 8: active^#(first(0(), Z)) -> c_8() 1055.44/297.03 1055.44/297.03 9: active^#(sel(X1, X2)) -> c_9(sel^#(X1, active(X2))) 1055.44/297.03 -->_1 sel^#(ok(X1), ok(X2)) -> c_24(sel^#(X1, X2)) :24 1055.44/297.03 -->_1 sel^#(mark(X1), X2) -> c_23(sel^#(X1, X2)) :23 1055.44/297.03 -->_1 sel^#(X1, mark(X2)) -> c_22(sel^#(X1, X2)) :22 1055.44/297.03 1055.44/297.03 10: active^#(sel(X1, X2)) -> c_10(sel^#(active(X1), X2)) 1055.44/297.03 -->_1 sel^#(ok(X1), ok(X2)) -> c_24(sel^#(X1, X2)) :24 1055.44/297.03 -->_1 sel^#(mark(X1), X2) -> c_23(sel^#(X1, X2)) :23 1055.44/297.03 -->_1 sel^#(X1, mark(X2)) -> c_22(sel^#(X1, X2)) :22 1055.44/297.03 1055.44/297.03 11: active^#(sel(s(X), cons(Y, Z))) -> c_11(sel^#(X, Z)) 1055.44/297.03 -->_1 sel^#(ok(X1), ok(X2)) -> c_24(sel^#(X1, X2)) :24 1055.44/297.03 -->_1 sel^#(mark(X1), X2) -> c_23(sel^#(X1, X2)) :23 1055.44/297.03 -->_1 sel^#(X1, mark(X2)) -> c_22(sel^#(X1, X2)) :22 1055.44/297.03 1055.44/297.03 12: active^#(sel(0(), cons(X, Z))) -> c_12(X) 1055.44/297.03 -->_1 top^#(ok(X)) -> c_33(top^#(active(X))) :33 1055.44/297.03 -->_1 top^#(mark(X)) -> c_32(top^#(proper(X))) :32 1055.44/297.03 -->_1 proper^#(sel(X1, X2)) -> 1055.44/297.03 c_31(sel^#(proper(X1), proper(X2))) :31 1055.44/297.03 -->_1 proper^#(first(X1, X2)) -> 1055.44/297.03 c_28(first^#(proper(X1), proper(X2))) :28 1055.44/297.03 -->_1 proper^#(s(X)) -> c_27(s^#(proper(X))) :27 1055.44/297.03 -->_1 proper^#(cons(X1, X2)) -> 1055.44/297.03 c_26(cons^#(proper(X1), proper(X2))) :26 1055.44/297.03 -->_1 proper^#(from(X)) -> c_25(from^#(proper(X))) :25 1055.44/297.03 -->_1 sel^#(ok(X1), ok(X2)) -> c_24(sel^#(X1, X2)) :24 1055.44/297.03 -->_1 sel^#(mark(X1), X2) -> c_23(sel^#(X1, X2)) :23 1055.44/297.03 -->_1 sel^#(X1, mark(X2)) -> c_22(sel^#(X1, X2)) :22 1055.44/297.03 -->_1 first^#(ok(X1), ok(X2)) -> c_21(first^#(X1, X2)) :21 1055.44/297.03 -->_1 first^#(mark(X1), X2) -> c_20(first^#(X1, X2)) :20 1055.44/297.03 -->_1 first^#(X1, mark(X2)) -> c_19(first^#(X1, X2)) :19 1055.44/297.03 -->_1 s^#(ok(X)) -> c_18(s^#(X)) :18 1055.44/297.03 -->_1 s^#(mark(X)) -> c_17(s^#(X)) :17 1055.44/297.03 -->_1 cons^#(ok(X1), ok(X2)) -> c_16(cons^#(X1, X2)) :16 1055.44/297.03 -->_1 cons^#(mark(X1), X2) -> c_15(cons^#(X1, X2)) :15 1055.44/297.03 -->_1 from^#(ok(X)) -> c_14(from^#(X)) :14 1055.44/297.03 -->_1 from^#(mark(X)) -> c_13(from^#(X)) :13 1055.44/297.03 -->_1 proper^#(nil()) -> c_30() :30 1055.44/297.03 -->_1 proper^#(0()) -> c_29() :29 1055.44/297.03 -->_1 active^#(sel(0(), cons(X, Z))) -> c_12(X) :12 1055.44/297.03 -->_1 active^#(sel(s(X), cons(Y, Z))) -> c_11(sel^#(X, Z)) :11 1055.44/297.03 -->_1 active^#(sel(X1, X2)) -> c_10(sel^#(active(X1), X2)) :10 1055.44/297.03 -->_1 active^#(sel(X1, X2)) -> c_9(sel^#(X1, active(X2))) :9 1055.44/297.03 -->_1 active^#(first(0(), Z)) -> c_8() :8 1055.44/297.03 -->_1 active^#(first(s(X), cons(Y, Z))) -> 1055.44/297.03 c_7(cons^#(Y, first(X, Z))) :7 1055.44/297.03 -->_1 active^#(first(X1, X2)) -> c_6(first^#(active(X1), X2)) :6 1055.44/297.03 -->_1 active^#(first(X1, X2)) -> c_5(first^#(X1, active(X2))) :5 1055.44/297.03 -->_1 active^#(s(X)) -> c_4(s^#(active(X))) :4 1055.44/297.03 -->_1 active^#(cons(X1, X2)) -> c_3(cons^#(active(X1), X2)) :3 1055.44/297.03 -->_1 active^#(from(X)) -> c_2(cons^#(X, from(s(X)))) :2 1055.44/297.03 -->_1 active^#(from(X)) -> c_1(from^#(active(X))) :1 1055.44/297.03 1055.44/297.03 13: from^#(mark(X)) -> c_13(from^#(X)) 1055.44/297.03 -->_1 from^#(ok(X)) -> c_14(from^#(X)) :14 1055.44/297.03 -->_1 from^#(mark(X)) -> c_13(from^#(X)) :13 1055.44/297.03 1055.44/297.03 14: from^#(ok(X)) -> c_14(from^#(X)) 1055.44/297.03 -->_1 from^#(ok(X)) -> c_14(from^#(X)) :14 1055.44/297.03 -->_1 from^#(mark(X)) -> c_13(from^#(X)) :13 1055.44/297.03 1055.44/297.03 15: cons^#(mark(X1), X2) -> c_15(cons^#(X1, X2)) 1055.44/297.03 -->_1 cons^#(ok(X1), ok(X2)) -> c_16(cons^#(X1, X2)) :16 1055.44/297.03 -->_1 cons^#(mark(X1), X2) -> c_15(cons^#(X1, X2)) :15 1055.44/297.03 1055.44/297.03 16: cons^#(ok(X1), ok(X2)) -> c_16(cons^#(X1, X2)) 1055.44/297.03 -->_1 cons^#(ok(X1), ok(X2)) -> c_16(cons^#(X1, X2)) :16 1055.44/297.03 -->_1 cons^#(mark(X1), X2) -> c_15(cons^#(X1, X2)) :15 1055.44/297.03 1055.44/297.03 17: s^#(mark(X)) -> c_17(s^#(X)) 1055.44/297.03 -->_1 s^#(ok(X)) -> c_18(s^#(X)) :18 1055.44/297.03 -->_1 s^#(mark(X)) -> c_17(s^#(X)) :17 1055.44/297.03 1055.44/297.03 18: s^#(ok(X)) -> c_18(s^#(X)) 1055.44/297.03 -->_1 s^#(ok(X)) -> c_18(s^#(X)) :18 1055.44/297.03 -->_1 s^#(mark(X)) -> c_17(s^#(X)) :17 1055.44/297.03 1055.44/297.03 19: first^#(X1, mark(X2)) -> c_19(first^#(X1, X2)) 1055.44/297.03 -->_1 first^#(ok(X1), ok(X2)) -> c_21(first^#(X1, X2)) :21 1055.44/297.03 -->_1 first^#(mark(X1), X2) -> c_20(first^#(X1, X2)) :20 1055.44/297.03 -->_1 first^#(X1, mark(X2)) -> c_19(first^#(X1, X2)) :19 1055.44/297.03 1055.44/297.03 20: first^#(mark(X1), X2) -> c_20(first^#(X1, X2)) 1055.44/297.03 -->_1 first^#(ok(X1), ok(X2)) -> c_21(first^#(X1, X2)) :21 1055.44/297.03 -->_1 first^#(mark(X1), X2) -> c_20(first^#(X1, X2)) :20 1055.44/297.03 -->_1 first^#(X1, mark(X2)) -> c_19(first^#(X1, X2)) :19 1055.44/297.03 1055.44/297.03 21: first^#(ok(X1), ok(X2)) -> c_21(first^#(X1, X2)) 1055.44/297.03 -->_1 first^#(ok(X1), ok(X2)) -> c_21(first^#(X1, X2)) :21 1055.44/297.03 -->_1 first^#(mark(X1), X2) -> c_20(first^#(X1, X2)) :20 1055.44/297.03 -->_1 first^#(X1, mark(X2)) -> c_19(first^#(X1, X2)) :19 1055.44/297.03 1055.44/297.03 22: sel^#(X1, mark(X2)) -> c_22(sel^#(X1, X2)) 1055.44/297.03 -->_1 sel^#(ok(X1), ok(X2)) -> c_24(sel^#(X1, X2)) :24 1055.44/297.03 -->_1 sel^#(mark(X1), X2) -> c_23(sel^#(X1, X2)) :23 1055.44/297.03 -->_1 sel^#(X1, mark(X2)) -> c_22(sel^#(X1, X2)) :22 1055.44/297.03 1055.44/297.03 23: sel^#(mark(X1), X2) -> c_23(sel^#(X1, X2)) 1055.44/297.03 -->_1 sel^#(ok(X1), ok(X2)) -> c_24(sel^#(X1, X2)) :24 1055.44/297.03 -->_1 sel^#(mark(X1), X2) -> c_23(sel^#(X1, X2)) :23 1055.44/297.03 -->_1 sel^#(X1, mark(X2)) -> c_22(sel^#(X1, X2)) :22 1055.44/297.03 1055.44/297.03 24: sel^#(ok(X1), ok(X2)) -> c_24(sel^#(X1, X2)) 1055.44/297.03 -->_1 sel^#(ok(X1), ok(X2)) -> c_24(sel^#(X1, X2)) :24 1055.44/297.03 -->_1 sel^#(mark(X1), X2) -> c_23(sel^#(X1, X2)) :23 1055.44/297.03 -->_1 sel^#(X1, mark(X2)) -> c_22(sel^#(X1, X2)) :22 1055.44/297.03 1055.44/297.03 25: proper^#(from(X)) -> c_25(from^#(proper(X))) 1055.44/297.03 -->_1 from^#(ok(X)) -> c_14(from^#(X)) :14 1055.44/297.03 -->_1 from^#(mark(X)) -> c_13(from^#(X)) :13 1055.44/297.03 1055.44/297.03 26: proper^#(cons(X1, X2)) -> c_26(cons^#(proper(X1), proper(X2))) 1055.44/297.03 -->_1 cons^#(ok(X1), ok(X2)) -> c_16(cons^#(X1, X2)) :16 1055.44/297.03 -->_1 cons^#(mark(X1), X2) -> c_15(cons^#(X1, X2)) :15 1055.44/297.03 1055.44/297.03 27: proper^#(s(X)) -> c_27(s^#(proper(X))) 1055.44/297.03 -->_1 s^#(ok(X)) -> c_18(s^#(X)) :18 1055.44/297.04 -->_1 s^#(mark(X)) -> c_17(s^#(X)) :17 1055.44/297.04 1055.44/297.04 28: proper^#(first(X1, X2)) -> 1055.44/297.04 c_28(first^#(proper(X1), proper(X2))) 1055.44/297.04 -->_1 first^#(ok(X1), ok(X2)) -> c_21(first^#(X1, X2)) :21 1055.44/297.04 -->_1 first^#(mark(X1), X2) -> c_20(first^#(X1, X2)) :20 1055.44/297.04 -->_1 first^#(X1, mark(X2)) -> c_19(first^#(X1, X2)) :19 1055.44/297.04 1055.44/297.04 29: proper^#(0()) -> c_29() 1055.44/297.04 1055.44/297.04 30: proper^#(nil()) -> c_30() 1055.44/297.04 1055.44/297.04 31: proper^#(sel(X1, X2)) -> c_31(sel^#(proper(X1), proper(X2))) 1055.44/297.04 -->_1 sel^#(ok(X1), ok(X2)) -> c_24(sel^#(X1, X2)) :24 1055.44/297.04 -->_1 sel^#(mark(X1), X2) -> c_23(sel^#(X1, X2)) :23 1055.44/297.04 -->_1 sel^#(X1, mark(X2)) -> c_22(sel^#(X1, X2)) :22 1055.44/297.04 1055.44/297.04 32: top^#(mark(X)) -> c_32(top^#(proper(X))) 1055.44/297.04 -->_1 top^#(ok(X)) -> c_33(top^#(active(X))) :33 1055.44/297.04 -->_1 top^#(mark(X)) -> c_32(top^#(proper(X))) :32 1055.44/297.04 1055.44/297.04 33: top^#(ok(X)) -> c_33(top^#(active(X))) 1055.44/297.04 -->_1 top^#(ok(X)) -> c_33(top^#(active(X))) :33 1055.44/297.04 -->_1 top^#(mark(X)) -> c_32(top^#(proper(X))) :32 1055.44/297.04 1055.44/297.04 1055.44/297.04 Only the nodes {13,14,15,16,17,18,19,21,20,22,24,23,29,30,32,33} 1055.44/297.04 are reachable from nodes 1055.44/297.04 {13,14,15,16,17,18,19,20,21,22,23,24,29,30,32,33} that start 1055.44/297.04 derivation from marked basic terms. The nodes not reachable are 1055.44/297.04 removed from the problem. 1055.44/297.04 1055.44/297.04 We are left with following problem, upon which TcT provides the 1055.44/297.04 certificate MAYBE. 1055.44/297.04 1055.44/297.04 Strict DPs: 1055.44/297.04 { from^#(mark(X)) -> c_13(from^#(X)) 1055.44/297.04 , from^#(ok(X)) -> c_14(from^#(X)) 1055.44/297.04 , cons^#(mark(X1), X2) -> c_15(cons^#(X1, X2)) 1055.44/297.04 , cons^#(ok(X1), ok(X2)) -> c_16(cons^#(X1, X2)) 1055.44/297.04 , s^#(mark(X)) -> c_17(s^#(X)) 1055.44/297.04 , s^#(ok(X)) -> c_18(s^#(X)) 1055.44/297.04 , first^#(X1, mark(X2)) -> c_19(first^#(X1, X2)) 1055.44/297.04 , first^#(mark(X1), X2) -> c_20(first^#(X1, X2)) 1055.44/297.04 , first^#(ok(X1), ok(X2)) -> c_21(first^#(X1, X2)) 1055.44/297.04 , sel^#(X1, mark(X2)) -> c_22(sel^#(X1, X2)) 1055.44/297.04 , sel^#(mark(X1), X2) -> c_23(sel^#(X1, X2)) 1055.44/297.04 , sel^#(ok(X1), ok(X2)) -> c_24(sel^#(X1, X2)) 1055.44/297.04 , proper^#(0()) -> c_29() 1055.44/297.04 , proper^#(nil()) -> c_30() 1055.44/297.04 , top^#(mark(X)) -> c_32(top^#(proper(X))) 1055.44/297.04 , top^#(ok(X)) -> c_33(top^#(active(X))) } 1055.44/297.04 Strict Trs: 1055.44/297.04 { active(from(X)) -> from(active(X)) 1055.44/297.04 , active(from(X)) -> mark(cons(X, from(s(X)))) 1055.44/297.04 , active(cons(X1, X2)) -> cons(active(X1), X2) 1055.44/297.04 , active(s(X)) -> s(active(X)) 1055.44/297.04 , active(first(X1, X2)) -> first(X1, active(X2)) 1055.44/297.04 , active(first(X1, X2)) -> first(active(X1), X2) 1055.44/297.04 , active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))) 1055.44/297.04 , active(first(0(), Z)) -> mark(nil()) 1055.44/297.04 , active(sel(X1, X2)) -> sel(X1, active(X2)) 1055.44/297.04 , active(sel(X1, X2)) -> sel(active(X1), X2) 1055.44/297.04 , active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)) 1055.44/297.04 , active(sel(0(), cons(X, Z))) -> mark(X) 1055.44/297.04 , from(mark(X)) -> mark(from(X)) 1055.44/297.04 , from(ok(X)) -> ok(from(X)) 1055.44/297.04 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 1055.44/297.04 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 1055.44/297.04 , s(mark(X)) -> mark(s(X)) 1055.44/297.04 , s(ok(X)) -> ok(s(X)) 1055.44/297.04 , first(X1, mark(X2)) -> mark(first(X1, X2)) 1055.44/297.04 , first(mark(X1), X2) -> mark(first(X1, X2)) 1055.44/297.04 , first(ok(X1), ok(X2)) -> ok(first(X1, X2)) 1055.44/297.04 , sel(X1, mark(X2)) -> mark(sel(X1, X2)) 1055.44/297.04 , sel(mark(X1), X2) -> mark(sel(X1, X2)) 1055.44/297.04 , sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)) 1055.44/297.04 , proper(from(X)) -> from(proper(X)) 1055.44/297.04 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 1055.44/297.04 , proper(s(X)) -> s(proper(X)) 1055.44/297.04 , proper(first(X1, X2)) -> first(proper(X1), proper(X2)) 1055.44/297.04 , proper(0()) -> ok(0()) 1055.44/297.04 , proper(nil()) -> ok(nil()) 1055.44/297.04 , proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)) 1055.44/297.04 , top(mark(X)) -> top(proper(X)) 1055.44/297.04 , top(ok(X)) -> top(active(X)) } 1055.44/297.04 Obligation: 1055.44/297.04 runtime complexity 1055.44/297.04 Answer: 1055.44/297.04 MAYBE 1055.44/297.04 1055.44/297.04 We estimate the number of application of {13,14} by applications of 1055.44/297.04 Pre({13,14}) = {}. Here rules are labeled as follows: 1055.44/297.04 1055.44/297.04 DPs: 1055.44/297.04 { 1: from^#(mark(X)) -> c_13(from^#(X)) 1055.44/297.04 , 2: from^#(ok(X)) -> c_14(from^#(X)) 1055.44/297.04 , 3: cons^#(mark(X1), X2) -> c_15(cons^#(X1, X2)) 1055.44/297.04 , 4: cons^#(ok(X1), ok(X2)) -> c_16(cons^#(X1, X2)) 1055.44/297.04 , 5: s^#(mark(X)) -> c_17(s^#(X)) 1055.44/297.04 , 6: s^#(ok(X)) -> c_18(s^#(X)) 1055.44/297.04 , 7: first^#(X1, mark(X2)) -> c_19(first^#(X1, X2)) 1055.44/297.04 , 8: first^#(mark(X1), X2) -> c_20(first^#(X1, X2)) 1055.44/297.04 , 9: first^#(ok(X1), ok(X2)) -> c_21(first^#(X1, X2)) 1055.44/297.04 , 10: sel^#(X1, mark(X2)) -> c_22(sel^#(X1, X2)) 1055.44/297.04 , 11: sel^#(mark(X1), X2) -> c_23(sel^#(X1, X2)) 1055.44/297.04 , 12: sel^#(ok(X1), ok(X2)) -> c_24(sel^#(X1, X2)) 1055.44/297.04 , 13: proper^#(0()) -> c_29() 1055.44/297.04 , 14: proper^#(nil()) -> c_30() 1055.44/297.04 , 15: top^#(mark(X)) -> c_32(top^#(proper(X))) 1055.44/297.04 , 16: top^#(ok(X)) -> c_33(top^#(active(X))) } 1055.44/297.04 1055.44/297.04 We are left with following problem, upon which TcT provides the 1055.44/297.04 certificate MAYBE. 1055.44/297.04 1055.44/297.04 Strict DPs: 1055.44/297.04 { from^#(mark(X)) -> c_13(from^#(X)) 1055.44/297.04 , from^#(ok(X)) -> c_14(from^#(X)) 1055.44/297.04 , cons^#(mark(X1), X2) -> c_15(cons^#(X1, X2)) 1055.44/297.04 , cons^#(ok(X1), ok(X2)) -> c_16(cons^#(X1, X2)) 1055.44/297.04 , s^#(mark(X)) -> c_17(s^#(X)) 1055.44/297.04 , s^#(ok(X)) -> c_18(s^#(X)) 1055.44/297.04 , first^#(X1, mark(X2)) -> c_19(first^#(X1, X2)) 1055.44/297.04 , first^#(mark(X1), X2) -> c_20(first^#(X1, X2)) 1055.44/297.04 , first^#(ok(X1), ok(X2)) -> c_21(first^#(X1, X2)) 1055.44/297.04 , sel^#(X1, mark(X2)) -> c_22(sel^#(X1, X2)) 1055.44/297.04 , sel^#(mark(X1), X2) -> c_23(sel^#(X1, X2)) 1055.44/297.04 , sel^#(ok(X1), ok(X2)) -> c_24(sel^#(X1, X2)) 1055.44/297.04 , top^#(mark(X)) -> c_32(top^#(proper(X))) 1055.44/297.04 , top^#(ok(X)) -> c_33(top^#(active(X))) } 1055.44/297.04 Strict Trs: 1055.44/297.04 { active(from(X)) -> from(active(X)) 1055.44/297.04 , active(from(X)) -> mark(cons(X, from(s(X)))) 1055.44/297.04 , active(cons(X1, X2)) -> cons(active(X1), X2) 1055.44/297.04 , active(s(X)) -> s(active(X)) 1055.44/297.04 , active(first(X1, X2)) -> first(X1, active(X2)) 1055.44/297.04 , active(first(X1, X2)) -> first(active(X1), X2) 1055.44/297.04 , active(first(s(X), cons(Y, Z))) -> mark(cons(Y, first(X, Z))) 1055.44/297.04 , active(first(0(), Z)) -> mark(nil()) 1055.44/297.04 , active(sel(X1, X2)) -> sel(X1, active(X2)) 1055.44/297.04 , active(sel(X1, X2)) -> sel(active(X1), X2) 1055.44/297.04 , active(sel(s(X), cons(Y, Z))) -> mark(sel(X, Z)) 1055.44/297.04 , active(sel(0(), cons(X, Z))) -> mark(X) 1055.44/297.04 , from(mark(X)) -> mark(from(X)) 1055.44/297.04 , from(ok(X)) -> ok(from(X)) 1055.44/297.04 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 1055.44/297.04 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 1055.44/297.04 , s(mark(X)) -> mark(s(X)) 1055.44/297.04 , s(ok(X)) -> ok(s(X)) 1055.44/297.04 , first(X1, mark(X2)) -> mark(first(X1, X2)) 1055.44/297.04 , first(mark(X1), X2) -> mark(first(X1, X2)) 1055.44/297.04 , first(ok(X1), ok(X2)) -> ok(first(X1, X2)) 1055.44/297.04 , sel(X1, mark(X2)) -> mark(sel(X1, X2)) 1055.44/297.04 , sel(mark(X1), X2) -> mark(sel(X1, X2)) 1055.44/297.04 , sel(ok(X1), ok(X2)) -> ok(sel(X1, X2)) 1055.44/297.04 , proper(from(X)) -> from(proper(X)) 1055.44/297.04 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 1055.44/297.04 , proper(s(X)) -> s(proper(X)) 1055.44/297.04 , proper(first(X1, X2)) -> first(proper(X1), proper(X2)) 1055.44/297.04 , proper(0()) -> ok(0()) 1055.44/297.04 , proper(nil()) -> ok(nil()) 1055.44/297.04 , proper(sel(X1, X2)) -> sel(proper(X1), proper(X2)) 1055.44/297.04 , top(mark(X)) -> top(proper(X)) 1055.44/297.04 , top(ok(X)) -> top(active(X)) } 1055.44/297.04 Weak DPs: 1055.44/297.04 { proper^#(0()) -> c_29() 1055.44/297.04 , proper^#(nil()) -> c_30() } 1055.44/297.04 Obligation: 1055.44/297.04 runtime complexity 1055.44/297.04 Answer: 1055.44/297.04 MAYBE 1055.44/297.04 1055.44/297.04 Empty strict component of the problem is NOT empty. 1055.44/297.04 1055.44/297.04 1055.44/297.04 Arrrr.. 1055.73/297.25 EOF