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