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