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