MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { active(primes()) -> mark(sieve(from(s(s(0()))))) , active(sieve(X)) -> sieve(active(X)) , active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))) , active(from(X)) -> mark(cons(X, from(s(X)))) , active(from(X)) -> from(active(X)) , active(s(X)) -> s(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(head(X)) -> head(active(X)) , active(head(cons(X, Y))) -> mark(X) , active(tail(X)) -> tail(active(X)) , active(tail(cons(X, Y))) -> mark(Y) , active(if(X1, X2, X3)) -> if(active(X1), X2, X3) , active(if(true(), X, Y)) -> mark(X) , active(if(false(), X, Y)) -> mark(Y) , active(filter(X1, X2)) -> filter(X1, active(X2)) , active(filter(X1, X2)) -> filter(active(X1), X2) , active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) , active(divides(X1, X2)) -> divides(X1, active(X2)) , active(divides(X1, X2)) -> divides(active(X1), X2) , sieve(mark(X)) -> mark(sieve(X)) , sieve(ok(X)) -> ok(sieve(X)) , from(mark(X)) -> mark(from(X)) , from(ok(X)) -> ok(from(X)) , s(mark(X)) -> mark(s(X)) , s(ok(X)) -> ok(s(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , head(mark(X)) -> mark(head(X)) , head(ok(X)) -> ok(head(X)) , tail(mark(X)) -> mark(tail(X)) , tail(ok(X)) -> ok(tail(X)) , if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)) , if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)) , filter(X1, mark(X2)) -> mark(filter(X1, X2)) , filter(mark(X1), X2) -> mark(filter(X1, X2)) , filter(ok(X1), ok(X2)) -> ok(filter(X1, X2)) , divides(X1, mark(X2)) -> mark(divides(X1, X2)) , divides(mark(X1), X2) -> mark(divides(X1, X2)) , divides(ok(X1), ok(X2)) -> ok(divides(X1, X2)) , proper(primes()) -> ok(primes()) , proper(sieve(X)) -> sieve(proper(X)) , proper(from(X)) -> from(proper(X)) , proper(s(X)) -> s(proper(X)) , proper(0()) -> ok(0()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(head(X)) -> head(proper(X)) , proper(tail(X)) -> tail(proper(X)) , proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)) , proper(true()) -> ok(true()) , proper(false()) -> ok(false()) , proper(filter(X1, X2)) -> filter(proper(X1), proper(X2)) , proper(divides(X1, X2)) -> divides(proper(X1), proper(X2)) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X)) } 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) '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 2) '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 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 perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with minimal-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: { active^#(primes()) -> c_1(sieve^#(from(s(s(0()))))) , active^#(sieve(X)) -> c_2(sieve^#(active(X))) , active^#(sieve(cons(X, Y))) -> c_3(cons^#(X, filter(X, sieve(Y)))) , active^#(from(X)) -> c_4(cons^#(X, from(s(X)))) , active^#(from(X)) -> c_5(from^#(active(X))) , active^#(s(X)) -> c_6(s^#(active(X))) , active^#(cons(X1, X2)) -> c_7(cons^#(active(X1), X2)) , active^#(head(X)) -> c_8(head^#(active(X))) , active^#(head(cons(X, Y))) -> c_9(X) , active^#(tail(X)) -> c_10(tail^#(active(X))) , active^#(tail(cons(X, Y))) -> c_11(Y) , active^#(if(X1, X2, X3)) -> c_12(if^#(active(X1), X2, X3)) , active^#(if(true(), X, Y)) -> c_13(X) , active^#(if(false(), X, Y)) -> c_14(Y) , active^#(filter(X1, X2)) -> c_15(filter^#(X1, active(X2))) , active^#(filter(X1, X2)) -> c_16(filter^#(active(X1), X2)) , active^#(filter(s(s(X)), cons(Y, Z))) -> c_17(if^#(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) , active^#(divides(X1, X2)) -> c_18(divides^#(X1, active(X2))) , active^#(divides(X1, X2)) -> c_19(divides^#(active(X1), X2)) , sieve^#(mark(X)) -> c_20(sieve^#(X)) , sieve^#(ok(X)) -> c_21(sieve^#(X)) , cons^#(mark(X1), X2) -> c_26(cons^#(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_27(cons^#(X1, X2)) , from^#(mark(X)) -> c_22(from^#(X)) , from^#(ok(X)) -> c_23(from^#(X)) , s^#(mark(X)) -> c_24(s^#(X)) , s^#(ok(X)) -> c_25(s^#(X)) , head^#(mark(X)) -> c_28(head^#(X)) , head^#(ok(X)) -> c_29(head^#(X)) , tail^#(mark(X)) -> c_30(tail^#(X)) , tail^#(ok(X)) -> c_31(tail^#(X)) , if^#(mark(X1), X2, X3) -> c_32(if^#(X1, X2, X3)) , if^#(ok(X1), ok(X2), ok(X3)) -> c_33(if^#(X1, X2, X3)) , filter^#(X1, mark(X2)) -> c_34(filter^#(X1, X2)) , filter^#(mark(X1), X2) -> c_35(filter^#(X1, X2)) , filter^#(ok(X1), ok(X2)) -> c_36(filter^#(X1, X2)) , divides^#(X1, mark(X2)) -> c_37(divides^#(X1, X2)) , divides^#(mark(X1), X2) -> c_38(divides^#(X1, X2)) , divides^#(ok(X1), ok(X2)) -> c_39(divides^#(X1, X2)) , proper^#(primes()) -> c_40() , proper^#(sieve(X)) -> c_41(sieve^#(proper(X))) , proper^#(from(X)) -> c_42(from^#(proper(X))) , proper^#(s(X)) -> c_43(s^#(proper(X))) , proper^#(0()) -> c_44() , proper^#(cons(X1, X2)) -> c_45(cons^#(proper(X1), proper(X2))) , proper^#(head(X)) -> c_46(head^#(proper(X))) , proper^#(tail(X)) -> c_47(tail^#(proper(X))) , proper^#(if(X1, X2, X3)) -> c_48(if^#(proper(X1), proper(X2), proper(X3))) , proper^#(true()) -> c_49() , proper^#(false()) -> c_50() , proper^#(filter(X1, X2)) -> c_51(filter^#(proper(X1), proper(X2))) , proper^#(divides(X1, X2)) -> c_52(divides^#(proper(X1), proper(X2))) , top^#(mark(X)) -> c_53(top^#(proper(X))) , top^#(ok(X)) -> c_54(top^#(active(X))) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { active^#(primes()) -> c_1(sieve^#(from(s(s(0()))))) , active^#(sieve(X)) -> c_2(sieve^#(active(X))) , active^#(sieve(cons(X, Y))) -> c_3(cons^#(X, filter(X, sieve(Y)))) , active^#(from(X)) -> c_4(cons^#(X, from(s(X)))) , active^#(from(X)) -> c_5(from^#(active(X))) , active^#(s(X)) -> c_6(s^#(active(X))) , active^#(cons(X1, X2)) -> c_7(cons^#(active(X1), X2)) , active^#(head(X)) -> c_8(head^#(active(X))) , active^#(head(cons(X, Y))) -> c_9(X) , active^#(tail(X)) -> c_10(tail^#(active(X))) , active^#(tail(cons(X, Y))) -> c_11(Y) , active^#(if(X1, X2, X3)) -> c_12(if^#(active(X1), X2, X3)) , active^#(if(true(), X, Y)) -> c_13(X) , active^#(if(false(), X, Y)) -> c_14(Y) , active^#(filter(X1, X2)) -> c_15(filter^#(X1, active(X2))) , active^#(filter(X1, X2)) -> c_16(filter^#(active(X1), X2)) , active^#(filter(s(s(X)), cons(Y, Z))) -> c_17(if^#(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) , active^#(divides(X1, X2)) -> c_18(divides^#(X1, active(X2))) , active^#(divides(X1, X2)) -> c_19(divides^#(active(X1), X2)) , sieve^#(mark(X)) -> c_20(sieve^#(X)) , sieve^#(ok(X)) -> c_21(sieve^#(X)) , cons^#(mark(X1), X2) -> c_26(cons^#(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_27(cons^#(X1, X2)) , from^#(mark(X)) -> c_22(from^#(X)) , from^#(ok(X)) -> c_23(from^#(X)) , s^#(mark(X)) -> c_24(s^#(X)) , s^#(ok(X)) -> c_25(s^#(X)) , head^#(mark(X)) -> c_28(head^#(X)) , head^#(ok(X)) -> c_29(head^#(X)) , tail^#(mark(X)) -> c_30(tail^#(X)) , tail^#(ok(X)) -> c_31(tail^#(X)) , if^#(mark(X1), X2, X3) -> c_32(if^#(X1, X2, X3)) , if^#(ok(X1), ok(X2), ok(X3)) -> c_33(if^#(X1, X2, X3)) , filter^#(X1, mark(X2)) -> c_34(filter^#(X1, X2)) , filter^#(mark(X1), X2) -> c_35(filter^#(X1, X2)) , filter^#(ok(X1), ok(X2)) -> c_36(filter^#(X1, X2)) , divides^#(X1, mark(X2)) -> c_37(divides^#(X1, X2)) , divides^#(mark(X1), X2) -> c_38(divides^#(X1, X2)) , divides^#(ok(X1), ok(X2)) -> c_39(divides^#(X1, X2)) , proper^#(primes()) -> c_40() , proper^#(sieve(X)) -> c_41(sieve^#(proper(X))) , proper^#(from(X)) -> c_42(from^#(proper(X))) , proper^#(s(X)) -> c_43(s^#(proper(X))) , proper^#(0()) -> c_44() , proper^#(cons(X1, X2)) -> c_45(cons^#(proper(X1), proper(X2))) , proper^#(head(X)) -> c_46(head^#(proper(X))) , proper^#(tail(X)) -> c_47(tail^#(proper(X))) , proper^#(if(X1, X2, X3)) -> c_48(if^#(proper(X1), proper(X2), proper(X3))) , proper^#(true()) -> c_49() , proper^#(false()) -> c_50() , proper^#(filter(X1, X2)) -> c_51(filter^#(proper(X1), proper(X2))) , proper^#(divides(X1, X2)) -> c_52(divides^#(proper(X1), proper(X2))) , top^#(mark(X)) -> c_53(top^#(proper(X))) , top^#(ok(X)) -> c_54(top^#(active(X))) } Strict Trs: { active(primes()) -> mark(sieve(from(s(s(0()))))) , active(sieve(X)) -> sieve(active(X)) , active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))) , active(from(X)) -> mark(cons(X, from(s(X)))) , active(from(X)) -> from(active(X)) , active(s(X)) -> s(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(head(X)) -> head(active(X)) , active(head(cons(X, Y))) -> mark(X) , active(tail(X)) -> tail(active(X)) , active(tail(cons(X, Y))) -> mark(Y) , active(if(X1, X2, X3)) -> if(active(X1), X2, X3) , active(if(true(), X, Y)) -> mark(X) , active(if(false(), X, Y)) -> mark(Y) , active(filter(X1, X2)) -> filter(X1, active(X2)) , active(filter(X1, X2)) -> filter(active(X1), X2) , active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) , active(divides(X1, X2)) -> divides(X1, active(X2)) , active(divides(X1, X2)) -> divides(active(X1), X2) , sieve(mark(X)) -> mark(sieve(X)) , sieve(ok(X)) -> ok(sieve(X)) , from(mark(X)) -> mark(from(X)) , from(ok(X)) -> ok(from(X)) , s(mark(X)) -> mark(s(X)) , s(ok(X)) -> ok(s(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , head(mark(X)) -> mark(head(X)) , head(ok(X)) -> ok(head(X)) , tail(mark(X)) -> mark(tail(X)) , tail(ok(X)) -> ok(tail(X)) , if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)) , if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)) , filter(X1, mark(X2)) -> mark(filter(X1, X2)) , filter(mark(X1), X2) -> mark(filter(X1, X2)) , filter(ok(X1), ok(X2)) -> ok(filter(X1, X2)) , divides(X1, mark(X2)) -> mark(divides(X1, X2)) , divides(mark(X1), X2) -> mark(divides(X1, X2)) , divides(ok(X1), ok(X2)) -> ok(divides(X1, X2)) , proper(primes()) -> ok(primes()) , proper(sieve(X)) -> sieve(proper(X)) , proper(from(X)) -> from(proper(X)) , proper(s(X)) -> s(proper(X)) , proper(0()) -> ok(0()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(head(X)) -> head(proper(X)) , proper(tail(X)) -> tail(proper(X)) , proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)) , proper(true()) -> ok(true()) , proper(false()) -> ok(false()) , proper(filter(X1, X2)) -> filter(proper(X1), proper(X2)) , proper(divides(X1, X2)) -> divides(proper(X1), proper(X2)) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X)) } Obligation: runtime complexity Answer: MAYBE Consider the dependency graph: 1: active^#(primes()) -> c_1(sieve^#(from(s(s(0()))))) 2: active^#(sieve(X)) -> c_2(sieve^#(active(X))) -->_1 sieve^#(ok(X)) -> c_21(sieve^#(X)) :21 -->_1 sieve^#(mark(X)) -> c_20(sieve^#(X)) :20 3: active^#(sieve(cons(X, Y))) -> c_3(cons^#(X, filter(X, sieve(Y)))) -->_1 cons^#(ok(X1), ok(X2)) -> c_27(cons^#(X1, X2)) :23 -->_1 cons^#(mark(X1), X2) -> c_26(cons^#(X1, X2)) :22 4: active^#(from(X)) -> c_4(cons^#(X, from(s(X)))) -->_1 cons^#(ok(X1), ok(X2)) -> c_27(cons^#(X1, X2)) :23 -->_1 cons^#(mark(X1), X2) -> c_26(cons^#(X1, X2)) :22 5: active^#(from(X)) -> c_5(from^#(active(X))) -->_1 from^#(ok(X)) -> c_23(from^#(X)) :25 -->_1 from^#(mark(X)) -> c_22(from^#(X)) :24 6: active^#(s(X)) -> c_6(s^#(active(X))) -->_1 s^#(ok(X)) -> c_25(s^#(X)) :27 -->_1 s^#(mark(X)) -> c_24(s^#(X)) :26 7: active^#(cons(X1, X2)) -> c_7(cons^#(active(X1), X2)) -->_1 cons^#(ok(X1), ok(X2)) -> c_27(cons^#(X1, X2)) :23 -->_1 cons^#(mark(X1), X2) -> c_26(cons^#(X1, X2)) :22 8: active^#(head(X)) -> c_8(head^#(active(X))) -->_1 head^#(ok(X)) -> c_29(head^#(X)) :29 -->_1 head^#(mark(X)) -> c_28(head^#(X)) :28 9: active^#(head(cons(X, Y))) -> c_9(X) -->_1 top^#(ok(X)) -> c_54(top^#(active(X))) :54 -->_1 top^#(mark(X)) -> c_53(top^#(proper(X))) :53 -->_1 proper^#(divides(X1, X2)) -> c_52(divides^#(proper(X1), proper(X2))) :52 -->_1 proper^#(filter(X1, X2)) -> c_51(filter^#(proper(X1), proper(X2))) :51 -->_1 proper^#(if(X1, X2, X3)) -> c_48(if^#(proper(X1), proper(X2), proper(X3))) :48 -->_1 proper^#(tail(X)) -> c_47(tail^#(proper(X))) :47 -->_1 proper^#(head(X)) -> c_46(head^#(proper(X))) :46 -->_1 proper^#(cons(X1, X2)) -> c_45(cons^#(proper(X1), proper(X2))) :45 -->_1 proper^#(s(X)) -> c_43(s^#(proper(X))) :43 -->_1 proper^#(from(X)) -> c_42(from^#(proper(X))) :42 -->_1 proper^#(sieve(X)) -> c_41(sieve^#(proper(X))) :41 -->_1 divides^#(ok(X1), ok(X2)) -> c_39(divides^#(X1, X2)) :39 -->_1 divides^#(mark(X1), X2) -> c_38(divides^#(X1, X2)) :38 -->_1 divides^#(X1, mark(X2)) -> c_37(divides^#(X1, X2)) :37 -->_1 filter^#(ok(X1), ok(X2)) -> c_36(filter^#(X1, X2)) :36 -->_1 filter^#(mark(X1), X2) -> c_35(filter^#(X1, X2)) :35 -->_1 filter^#(X1, mark(X2)) -> c_34(filter^#(X1, X2)) :34 -->_1 if^#(ok(X1), ok(X2), ok(X3)) -> c_33(if^#(X1, X2, X3)) :33 -->_1 if^#(mark(X1), X2, X3) -> c_32(if^#(X1, X2, X3)) :32 -->_1 tail^#(ok(X)) -> c_31(tail^#(X)) :31 -->_1 tail^#(mark(X)) -> c_30(tail^#(X)) :30 -->_1 head^#(ok(X)) -> c_29(head^#(X)) :29 -->_1 head^#(mark(X)) -> c_28(head^#(X)) :28 -->_1 s^#(ok(X)) -> c_25(s^#(X)) :27 -->_1 s^#(mark(X)) -> c_24(s^#(X)) :26 -->_1 from^#(ok(X)) -> c_23(from^#(X)) :25 -->_1 from^#(mark(X)) -> c_22(from^#(X)) :24 -->_1 cons^#(ok(X1), ok(X2)) -> c_27(cons^#(X1, X2)) :23 -->_1 cons^#(mark(X1), X2) -> c_26(cons^#(X1, X2)) :22 -->_1 sieve^#(ok(X)) -> c_21(sieve^#(X)) :21 -->_1 sieve^#(mark(X)) -> c_20(sieve^#(X)) :20 -->_1 active^#(divides(X1, X2)) -> c_19(divides^#(active(X1), X2)) :19 -->_1 active^#(divides(X1, X2)) -> c_18(divides^#(X1, active(X2))) :18 -->_1 active^#(filter(s(s(X)), cons(Y, Z))) -> c_17(if^#(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) :17 -->_1 active^#(filter(X1, X2)) -> c_16(filter^#(active(X1), X2)) :16 -->_1 active^#(filter(X1, X2)) -> c_15(filter^#(X1, active(X2))) :15 -->_1 active^#(if(false(), X, Y)) -> c_14(Y) :14 -->_1 active^#(if(true(), X, Y)) -> c_13(X) :13 -->_1 active^#(if(X1, X2, X3)) -> c_12(if^#(active(X1), X2, X3)) :12 -->_1 active^#(tail(cons(X, Y))) -> c_11(Y) :11 -->_1 active^#(tail(X)) -> c_10(tail^#(active(X))) :10 -->_1 proper^#(false()) -> c_50() :50 -->_1 proper^#(true()) -> c_49() :49 -->_1 proper^#(0()) -> c_44() :44 -->_1 proper^#(primes()) -> c_40() :40 -->_1 active^#(head(cons(X, Y))) -> c_9(X) :9 -->_1 active^#(head(X)) -> c_8(head^#(active(X))) :8 -->_1 active^#(cons(X1, X2)) -> c_7(cons^#(active(X1), X2)) :7 -->_1 active^#(s(X)) -> c_6(s^#(active(X))) :6 -->_1 active^#(from(X)) -> c_5(from^#(active(X))) :5 -->_1 active^#(from(X)) -> c_4(cons^#(X, from(s(X)))) :4 -->_1 active^#(sieve(cons(X, Y))) -> c_3(cons^#(X, filter(X, sieve(Y)))) :3 -->_1 active^#(sieve(X)) -> c_2(sieve^#(active(X))) :2 -->_1 active^#(primes()) -> c_1(sieve^#(from(s(s(0()))))) :1 10: active^#(tail(X)) -> c_10(tail^#(active(X))) -->_1 tail^#(ok(X)) -> c_31(tail^#(X)) :31 -->_1 tail^#(mark(X)) -> c_30(tail^#(X)) :30 11: active^#(tail(cons(X, Y))) -> c_11(Y) -->_1 top^#(ok(X)) -> c_54(top^#(active(X))) :54 -->_1 top^#(mark(X)) -> c_53(top^#(proper(X))) :53 -->_1 proper^#(divides(X1, X2)) -> c_52(divides^#(proper(X1), proper(X2))) :52 -->_1 proper^#(filter(X1, X2)) -> c_51(filter^#(proper(X1), proper(X2))) :51 -->_1 proper^#(if(X1, X2, X3)) -> c_48(if^#(proper(X1), proper(X2), proper(X3))) :48 -->_1 proper^#(tail(X)) -> c_47(tail^#(proper(X))) :47 -->_1 proper^#(head(X)) -> c_46(head^#(proper(X))) :46 -->_1 proper^#(cons(X1, X2)) -> c_45(cons^#(proper(X1), proper(X2))) :45 -->_1 proper^#(s(X)) -> c_43(s^#(proper(X))) :43 -->_1 proper^#(from(X)) -> c_42(from^#(proper(X))) :42 -->_1 proper^#(sieve(X)) -> c_41(sieve^#(proper(X))) :41 -->_1 divides^#(ok(X1), ok(X2)) -> c_39(divides^#(X1, X2)) :39 -->_1 divides^#(mark(X1), X2) -> c_38(divides^#(X1, X2)) :38 -->_1 divides^#(X1, mark(X2)) -> c_37(divides^#(X1, X2)) :37 -->_1 filter^#(ok(X1), ok(X2)) -> c_36(filter^#(X1, X2)) :36 -->_1 filter^#(mark(X1), X2) -> c_35(filter^#(X1, X2)) :35 -->_1 filter^#(X1, mark(X2)) -> c_34(filter^#(X1, X2)) :34 -->_1 if^#(ok(X1), ok(X2), ok(X3)) -> c_33(if^#(X1, X2, X3)) :33 -->_1 if^#(mark(X1), X2, X3) -> c_32(if^#(X1, X2, X3)) :32 -->_1 tail^#(ok(X)) -> c_31(tail^#(X)) :31 -->_1 tail^#(mark(X)) -> c_30(tail^#(X)) :30 -->_1 head^#(ok(X)) -> c_29(head^#(X)) :29 -->_1 head^#(mark(X)) -> c_28(head^#(X)) :28 -->_1 s^#(ok(X)) -> c_25(s^#(X)) :27 -->_1 s^#(mark(X)) -> c_24(s^#(X)) :26 -->_1 from^#(ok(X)) -> c_23(from^#(X)) :25 -->_1 from^#(mark(X)) -> c_22(from^#(X)) :24 -->_1 cons^#(ok(X1), ok(X2)) -> c_27(cons^#(X1, X2)) :23 -->_1 cons^#(mark(X1), X2) -> c_26(cons^#(X1, X2)) :22 -->_1 sieve^#(ok(X)) -> c_21(sieve^#(X)) :21 -->_1 sieve^#(mark(X)) -> c_20(sieve^#(X)) :20 -->_1 active^#(divides(X1, X2)) -> c_19(divides^#(active(X1), X2)) :19 -->_1 active^#(divides(X1, X2)) -> c_18(divides^#(X1, active(X2))) :18 -->_1 active^#(filter(s(s(X)), cons(Y, Z))) -> c_17(if^#(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) :17 -->_1 active^#(filter(X1, X2)) -> c_16(filter^#(active(X1), X2)) :16 -->_1 active^#(filter(X1, X2)) -> c_15(filter^#(X1, active(X2))) :15 -->_1 active^#(if(false(), X, Y)) -> c_14(Y) :14 -->_1 active^#(if(true(), X, Y)) -> c_13(X) :13 -->_1 active^#(if(X1, X2, X3)) -> c_12(if^#(active(X1), X2, X3)) :12 -->_1 proper^#(false()) -> c_50() :50 -->_1 proper^#(true()) -> c_49() :49 -->_1 proper^#(0()) -> c_44() :44 -->_1 proper^#(primes()) -> c_40() :40 -->_1 active^#(tail(cons(X, Y))) -> c_11(Y) :11 -->_1 active^#(tail(X)) -> c_10(tail^#(active(X))) :10 -->_1 active^#(head(cons(X, Y))) -> c_9(X) :9 -->_1 active^#(head(X)) -> c_8(head^#(active(X))) :8 -->_1 active^#(cons(X1, X2)) -> c_7(cons^#(active(X1), X2)) :7 -->_1 active^#(s(X)) -> c_6(s^#(active(X))) :6 -->_1 active^#(from(X)) -> c_5(from^#(active(X))) :5 -->_1 active^#(from(X)) -> c_4(cons^#(X, from(s(X)))) :4 -->_1 active^#(sieve(cons(X, Y))) -> c_3(cons^#(X, filter(X, sieve(Y)))) :3 -->_1 active^#(sieve(X)) -> c_2(sieve^#(active(X))) :2 -->_1 active^#(primes()) -> c_1(sieve^#(from(s(s(0()))))) :1 12: active^#(if(X1, X2, X3)) -> c_12(if^#(active(X1), X2, X3)) -->_1 if^#(ok(X1), ok(X2), ok(X3)) -> c_33(if^#(X1, X2, X3)) :33 -->_1 if^#(mark(X1), X2, X3) -> c_32(if^#(X1, X2, X3)) :32 13: active^#(if(true(), X, Y)) -> c_13(X) -->_1 top^#(ok(X)) -> c_54(top^#(active(X))) :54 -->_1 top^#(mark(X)) -> c_53(top^#(proper(X))) :53 -->_1 proper^#(divides(X1, X2)) -> c_52(divides^#(proper(X1), proper(X2))) :52 -->_1 proper^#(filter(X1, X2)) -> c_51(filter^#(proper(X1), proper(X2))) :51 -->_1 proper^#(if(X1, X2, X3)) -> c_48(if^#(proper(X1), proper(X2), proper(X3))) :48 -->_1 proper^#(tail(X)) -> c_47(tail^#(proper(X))) :47 -->_1 proper^#(head(X)) -> c_46(head^#(proper(X))) :46 -->_1 proper^#(cons(X1, X2)) -> c_45(cons^#(proper(X1), proper(X2))) :45 -->_1 proper^#(s(X)) -> c_43(s^#(proper(X))) :43 -->_1 proper^#(from(X)) -> c_42(from^#(proper(X))) :42 -->_1 proper^#(sieve(X)) -> c_41(sieve^#(proper(X))) :41 -->_1 divides^#(ok(X1), ok(X2)) -> c_39(divides^#(X1, X2)) :39 -->_1 divides^#(mark(X1), X2) -> c_38(divides^#(X1, X2)) :38 -->_1 divides^#(X1, mark(X2)) -> c_37(divides^#(X1, X2)) :37 -->_1 filter^#(ok(X1), ok(X2)) -> c_36(filter^#(X1, X2)) :36 -->_1 filter^#(mark(X1), X2) -> c_35(filter^#(X1, X2)) :35 -->_1 filter^#(X1, mark(X2)) -> c_34(filter^#(X1, X2)) :34 -->_1 if^#(ok(X1), ok(X2), ok(X3)) -> c_33(if^#(X1, X2, X3)) :33 -->_1 if^#(mark(X1), X2, X3) -> c_32(if^#(X1, X2, X3)) :32 -->_1 tail^#(ok(X)) -> c_31(tail^#(X)) :31 -->_1 tail^#(mark(X)) -> c_30(tail^#(X)) :30 -->_1 head^#(ok(X)) -> c_29(head^#(X)) :29 -->_1 head^#(mark(X)) -> c_28(head^#(X)) :28 -->_1 s^#(ok(X)) -> c_25(s^#(X)) :27 -->_1 s^#(mark(X)) -> c_24(s^#(X)) :26 -->_1 from^#(ok(X)) -> c_23(from^#(X)) :25 -->_1 from^#(mark(X)) -> c_22(from^#(X)) :24 -->_1 cons^#(ok(X1), ok(X2)) -> c_27(cons^#(X1, X2)) :23 -->_1 cons^#(mark(X1), X2) -> c_26(cons^#(X1, X2)) :22 -->_1 sieve^#(ok(X)) -> c_21(sieve^#(X)) :21 -->_1 sieve^#(mark(X)) -> c_20(sieve^#(X)) :20 -->_1 active^#(divides(X1, X2)) -> c_19(divides^#(active(X1), X2)) :19 -->_1 active^#(divides(X1, X2)) -> c_18(divides^#(X1, active(X2))) :18 -->_1 active^#(filter(s(s(X)), cons(Y, Z))) -> c_17(if^#(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) :17 -->_1 active^#(filter(X1, X2)) -> c_16(filter^#(active(X1), X2)) :16 -->_1 active^#(filter(X1, X2)) -> c_15(filter^#(X1, active(X2))) :15 -->_1 active^#(if(false(), X, Y)) -> c_14(Y) :14 -->_1 proper^#(false()) -> c_50() :50 -->_1 proper^#(true()) -> c_49() :49 -->_1 proper^#(0()) -> c_44() :44 -->_1 proper^#(primes()) -> c_40() :40 -->_1 active^#(if(true(), X, Y)) -> c_13(X) :13 -->_1 active^#(if(X1, X2, X3)) -> c_12(if^#(active(X1), X2, X3)) :12 -->_1 active^#(tail(cons(X, Y))) -> c_11(Y) :11 -->_1 active^#(tail(X)) -> c_10(tail^#(active(X))) :10 -->_1 active^#(head(cons(X, Y))) -> c_9(X) :9 -->_1 active^#(head(X)) -> c_8(head^#(active(X))) :8 -->_1 active^#(cons(X1, X2)) -> c_7(cons^#(active(X1), X2)) :7 -->_1 active^#(s(X)) -> c_6(s^#(active(X))) :6 -->_1 active^#(from(X)) -> c_5(from^#(active(X))) :5 -->_1 active^#(from(X)) -> c_4(cons^#(X, from(s(X)))) :4 -->_1 active^#(sieve(cons(X, Y))) -> c_3(cons^#(X, filter(X, sieve(Y)))) :3 -->_1 active^#(sieve(X)) -> c_2(sieve^#(active(X))) :2 -->_1 active^#(primes()) -> c_1(sieve^#(from(s(s(0()))))) :1 14: active^#(if(false(), X, Y)) -> c_14(Y) -->_1 top^#(ok(X)) -> c_54(top^#(active(X))) :54 -->_1 top^#(mark(X)) -> c_53(top^#(proper(X))) :53 -->_1 proper^#(divides(X1, X2)) -> c_52(divides^#(proper(X1), proper(X2))) :52 -->_1 proper^#(filter(X1, X2)) -> c_51(filter^#(proper(X1), proper(X2))) :51 -->_1 proper^#(if(X1, X2, X3)) -> c_48(if^#(proper(X1), proper(X2), proper(X3))) :48 -->_1 proper^#(tail(X)) -> c_47(tail^#(proper(X))) :47 -->_1 proper^#(head(X)) -> c_46(head^#(proper(X))) :46 -->_1 proper^#(cons(X1, X2)) -> c_45(cons^#(proper(X1), proper(X2))) :45 -->_1 proper^#(s(X)) -> c_43(s^#(proper(X))) :43 -->_1 proper^#(from(X)) -> c_42(from^#(proper(X))) :42 -->_1 proper^#(sieve(X)) -> c_41(sieve^#(proper(X))) :41 -->_1 divides^#(ok(X1), ok(X2)) -> c_39(divides^#(X1, X2)) :39 -->_1 divides^#(mark(X1), X2) -> c_38(divides^#(X1, X2)) :38 -->_1 divides^#(X1, mark(X2)) -> c_37(divides^#(X1, X2)) :37 -->_1 filter^#(ok(X1), ok(X2)) -> c_36(filter^#(X1, X2)) :36 -->_1 filter^#(mark(X1), X2) -> c_35(filter^#(X1, X2)) :35 -->_1 filter^#(X1, mark(X2)) -> c_34(filter^#(X1, X2)) :34 -->_1 if^#(ok(X1), ok(X2), ok(X3)) -> c_33(if^#(X1, X2, X3)) :33 -->_1 if^#(mark(X1), X2, X3) -> c_32(if^#(X1, X2, X3)) :32 -->_1 tail^#(ok(X)) -> c_31(tail^#(X)) :31 -->_1 tail^#(mark(X)) -> c_30(tail^#(X)) :30 -->_1 head^#(ok(X)) -> c_29(head^#(X)) :29 -->_1 head^#(mark(X)) -> c_28(head^#(X)) :28 -->_1 s^#(ok(X)) -> c_25(s^#(X)) :27 -->_1 s^#(mark(X)) -> c_24(s^#(X)) :26 -->_1 from^#(ok(X)) -> c_23(from^#(X)) :25 -->_1 from^#(mark(X)) -> c_22(from^#(X)) :24 -->_1 cons^#(ok(X1), ok(X2)) -> c_27(cons^#(X1, X2)) :23 -->_1 cons^#(mark(X1), X2) -> c_26(cons^#(X1, X2)) :22 -->_1 sieve^#(ok(X)) -> c_21(sieve^#(X)) :21 -->_1 sieve^#(mark(X)) -> c_20(sieve^#(X)) :20 -->_1 active^#(divides(X1, X2)) -> c_19(divides^#(active(X1), X2)) :19 -->_1 active^#(divides(X1, X2)) -> c_18(divides^#(X1, active(X2))) :18 -->_1 active^#(filter(s(s(X)), cons(Y, Z))) -> c_17(if^#(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) :17 -->_1 active^#(filter(X1, X2)) -> c_16(filter^#(active(X1), X2)) :16 -->_1 active^#(filter(X1, X2)) -> c_15(filter^#(X1, active(X2))) :15 -->_1 proper^#(false()) -> c_50() :50 -->_1 proper^#(true()) -> c_49() :49 -->_1 proper^#(0()) -> c_44() :44 -->_1 proper^#(primes()) -> c_40() :40 -->_1 active^#(if(false(), X, Y)) -> c_14(Y) :14 -->_1 active^#(if(true(), X, Y)) -> c_13(X) :13 -->_1 active^#(if(X1, X2, X3)) -> c_12(if^#(active(X1), X2, X3)) :12 -->_1 active^#(tail(cons(X, Y))) -> c_11(Y) :11 -->_1 active^#(tail(X)) -> c_10(tail^#(active(X))) :10 -->_1 active^#(head(cons(X, Y))) -> c_9(X) :9 -->_1 active^#(head(X)) -> c_8(head^#(active(X))) :8 -->_1 active^#(cons(X1, X2)) -> c_7(cons^#(active(X1), X2)) :7 -->_1 active^#(s(X)) -> c_6(s^#(active(X))) :6 -->_1 active^#(from(X)) -> c_5(from^#(active(X))) :5 -->_1 active^#(from(X)) -> c_4(cons^#(X, from(s(X)))) :4 -->_1 active^#(sieve(cons(X, Y))) -> c_3(cons^#(X, filter(X, sieve(Y)))) :3 -->_1 active^#(sieve(X)) -> c_2(sieve^#(active(X))) :2 -->_1 active^#(primes()) -> c_1(sieve^#(from(s(s(0()))))) :1 15: active^#(filter(X1, X2)) -> c_15(filter^#(X1, active(X2))) -->_1 filter^#(ok(X1), ok(X2)) -> c_36(filter^#(X1, X2)) :36 -->_1 filter^#(mark(X1), X2) -> c_35(filter^#(X1, X2)) :35 -->_1 filter^#(X1, mark(X2)) -> c_34(filter^#(X1, X2)) :34 16: active^#(filter(X1, X2)) -> c_16(filter^#(active(X1), X2)) -->_1 filter^#(ok(X1), ok(X2)) -> c_36(filter^#(X1, X2)) :36 -->_1 filter^#(mark(X1), X2) -> c_35(filter^#(X1, X2)) :35 -->_1 filter^#(X1, mark(X2)) -> c_34(filter^#(X1, X2)) :34 17: active^#(filter(s(s(X)), cons(Y, Z))) -> c_17(if^#(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) -->_1 if^#(ok(X1), ok(X2), ok(X3)) -> c_33(if^#(X1, X2, X3)) :33 -->_1 if^#(mark(X1), X2, X3) -> c_32(if^#(X1, X2, X3)) :32 18: active^#(divides(X1, X2)) -> c_18(divides^#(X1, active(X2))) -->_1 divides^#(ok(X1), ok(X2)) -> c_39(divides^#(X1, X2)) :39 -->_1 divides^#(mark(X1), X2) -> c_38(divides^#(X1, X2)) :38 -->_1 divides^#(X1, mark(X2)) -> c_37(divides^#(X1, X2)) :37 19: active^#(divides(X1, X2)) -> c_19(divides^#(active(X1), X2)) -->_1 divides^#(ok(X1), ok(X2)) -> c_39(divides^#(X1, X2)) :39 -->_1 divides^#(mark(X1), X2) -> c_38(divides^#(X1, X2)) :38 -->_1 divides^#(X1, mark(X2)) -> c_37(divides^#(X1, X2)) :37 20: sieve^#(mark(X)) -> c_20(sieve^#(X)) -->_1 sieve^#(ok(X)) -> c_21(sieve^#(X)) :21 -->_1 sieve^#(mark(X)) -> c_20(sieve^#(X)) :20 21: sieve^#(ok(X)) -> c_21(sieve^#(X)) -->_1 sieve^#(ok(X)) -> c_21(sieve^#(X)) :21 -->_1 sieve^#(mark(X)) -> c_20(sieve^#(X)) :20 22: cons^#(mark(X1), X2) -> c_26(cons^#(X1, X2)) -->_1 cons^#(ok(X1), ok(X2)) -> c_27(cons^#(X1, X2)) :23 -->_1 cons^#(mark(X1), X2) -> c_26(cons^#(X1, X2)) :22 23: cons^#(ok(X1), ok(X2)) -> c_27(cons^#(X1, X2)) -->_1 cons^#(ok(X1), ok(X2)) -> c_27(cons^#(X1, X2)) :23 -->_1 cons^#(mark(X1), X2) -> c_26(cons^#(X1, X2)) :22 24: from^#(mark(X)) -> c_22(from^#(X)) -->_1 from^#(ok(X)) -> c_23(from^#(X)) :25 -->_1 from^#(mark(X)) -> c_22(from^#(X)) :24 25: from^#(ok(X)) -> c_23(from^#(X)) -->_1 from^#(ok(X)) -> c_23(from^#(X)) :25 -->_1 from^#(mark(X)) -> c_22(from^#(X)) :24 26: s^#(mark(X)) -> c_24(s^#(X)) -->_1 s^#(ok(X)) -> c_25(s^#(X)) :27 -->_1 s^#(mark(X)) -> c_24(s^#(X)) :26 27: s^#(ok(X)) -> c_25(s^#(X)) -->_1 s^#(ok(X)) -> c_25(s^#(X)) :27 -->_1 s^#(mark(X)) -> c_24(s^#(X)) :26 28: head^#(mark(X)) -> c_28(head^#(X)) -->_1 head^#(ok(X)) -> c_29(head^#(X)) :29 -->_1 head^#(mark(X)) -> c_28(head^#(X)) :28 29: head^#(ok(X)) -> c_29(head^#(X)) -->_1 head^#(ok(X)) -> c_29(head^#(X)) :29 -->_1 head^#(mark(X)) -> c_28(head^#(X)) :28 30: tail^#(mark(X)) -> c_30(tail^#(X)) -->_1 tail^#(ok(X)) -> c_31(tail^#(X)) :31 -->_1 tail^#(mark(X)) -> c_30(tail^#(X)) :30 31: tail^#(ok(X)) -> c_31(tail^#(X)) -->_1 tail^#(ok(X)) -> c_31(tail^#(X)) :31 -->_1 tail^#(mark(X)) -> c_30(tail^#(X)) :30 32: if^#(mark(X1), X2, X3) -> c_32(if^#(X1, X2, X3)) -->_1 if^#(ok(X1), ok(X2), ok(X3)) -> c_33(if^#(X1, X2, X3)) :33 -->_1 if^#(mark(X1), X2, X3) -> c_32(if^#(X1, X2, X3)) :32 33: if^#(ok(X1), ok(X2), ok(X3)) -> c_33(if^#(X1, X2, X3)) -->_1 if^#(ok(X1), ok(X2), ok(X3)) -> c_33(if^#(X1, X2, X3)) :33 -->_1 if^#(mark(X1), X2, X3) -> c_32(if^#(X1, X2, X3)) :32 34: filter^#(X1, mark(X2)) -> c_34(filter^#(X1, X2)) -->_1 filter^#(ok(X1), ok(X2)) -> c_36(filter^#(X1, X2)) :36 -->_1 filter^#(mark(X1), X2) -> c_35(filter^#(X1, X2)) :35 -->_1 filter^#(X1, mark(X2)) -> c_34(filter^#(X1, X2)) :34 35: filter^#(mark(X1), X2) -> c_35(filter^#(X1, X2)) -->_1 filter^#(ok(X1), ok(X2)) -> c_36(filter^#(X1, X2)) :36 -->_1 filter^#(mark(X1), X2) -> c_35(filter^#(X1, X2)) :35 -->_1 filter^#(X1, mark(X2)) -> c_34(filter^#(X1, X2)) :34 36: filter^#(ok(X1), ok(X2)) -> c_36(filter^#(X1, X2)) -->_1 filter^#(ok(X1), ok(X2)) -> c_36(filter^#(X1, X2)) :36 -->_1 filter^#(mark(X1), X2) -> c_35(filter^#(X1, X2)) :35 -->_1 filter^#(X1, mark(X2)) -> c_34(filter^#(X1, X2)) :34 37: divides^#(X1, mark(X2)) -> c_37(divides^#(X1, X2)) -->_1 divides^#(ok(X1), ok(X2)) -> c_39(divides^#(X1, X2)) :39 -->_1 divides^#(mark(X1), X2) -> c_38(divides^#(X1, X2)) :38 -->_1 divides^#(X1, mark(X2)) -> c_37(divides^#(X1, X2)) :37 38: divides^#(mark(X1), X2) -> c_38(divides^#(X1, X2)) -->_1 divides^#(ok(X1), ok(X2)) -> c_39(divides^#(X1, X2)) :39 -->_1 divides^#(mark(X1), X2) -> c_38(divides^#(X1, X2)) :38 -->_1 divides^#(X1, mark(X2)) -> c_37(divides^#(X1, X2)) :37 39: divides^#(ok(X1), ok(X2)) -> c_39(divides^#(X1, X2)) -->_1 divides^#(ok(X1), ok(X2)) -> c_39(divides^#(X1, X2)) :39 -->_1 divides^#(mark(X1), X2) -> c_38(divides^#(X1, X2)) :38 -->_1 divides^#(X1, mark(X2)) -> c_37(divides^#(X1, X2)) :37 40: proper^#(primes()) -> c_40() 41: proper^#(sieve(X)) -> c_41(sieve^#(proper(X))) -->_1 sieve^#(ok(X)) -> c_21(sieve^#(X)) :21 -->_1 sieve^#(mark(X)) -> c_20(sieve^#(X)) :20 42: proper^#(from(X)) -> c_42(from^#(proper(X))) -->_1 from^#(ok(X)) -> c_23(from^#(X)) :25 -->_1 from^#(mark(X)) -> c_22(from^#(X)) :24 43: proper^#(s(X)) -> c_43(s^#(proper(X))) -->_1 s^#(ok(X)) -> c_25(s^#(X)) :27 -->_1 s^#(mark(X)) -> c_24(s^#(X)) :26 44: proper^#(0()) -> c_44() 45: proper^#(cons(X1, X2)) -> c_45(cons^#(proper(X1), proper(X2))) -->_1 cons^#(ok(X1), ok(X2)) -> c_27(cons^#(X1, X2)) :23 -->_1 cons^#(mark(X1), X2) -> c_26(cons^#(X1, X2)) :22 46: proper^#(head(X)) -> c_46(head^#(proper(X))) -->_1 head^#(ok(X)) -> c_29(head^#(X)) :29 -->_1 head^#(mark(X)) -> c_28(head^#(X)) :28 47: proper^#(tail(X)) -> c_47(tail^#(proper(X))) -->_1 tail^#(ok(X)) -> c_31(tail^#(X)) :31 -->_1 tail^#(mark(X)) -> c_30(tail^#(X)) :30 48: proper^#(if(X1, X2, X3)) -> c_48(if^#(proper(X1), proper(X2), proper(X3))) -->_1 if^#(ok(X1), ok(X2), ok(X3)) -> c_33(if^#(X1, X2, X3)) :33 -->_1 if^#(mark(X1), X2, X3) -> c_32(if^#(X1, X2, X3)) :32 49: proper^#(true()) -> c_49() 50: proper^#(false()) -> c_50() 51: proper^#(filter(X1, X2)) -> c_51(filter^#(proper(X1), proper(X2))) -->_1 filter^#(ok(X1), ok(X2)) -> c_36(filter^#(X1, X2)) :36 -->_1 filter^#(mark(X1), X2) -> c_35(filter^#(X1, X2)) :35 -->_1 filter^#(X1, mark(X2)) -> c_34(filter^#(X1, X2)) :34 52: proper^#(divides(X1, X2)) -> c_52(divides^#(proper(X1), proper(X2))) -->_1 divides^#(ok(X1), ok(X2)) -> c_39(divides^#(X1, X2)) :39 -->_1 divides^#(mark(X1), X2) -> c_38(divides^#(X1, X2)) :38 -->_1 divides^#(X1, mark(X2)) -> c_37(divides^#(X1, X2)) :37 53: top^#(mark(X)) -> c_53(top^#(proper(X))) -->_1 top^#(ok(X)) -> c_54(top^#(active(X))) :54 -->_1 top^#(mark(X)) -> c_53(top^#(proper(X))) :53 54: top^#(ok(X)) -> c_54(top^#(active(X))) -->_1 top^#(ok(X)) -> c_54(top^#(active(X))) :54 -->_1 top^#(mark(X)) -> c_53(top^#(proper(X))) :53 Only the nodes {1,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,36,35,37,39,38,40,44,49,50,53,54} are reachable from nodes {1,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,44,49,50,53,54} that start derivation from marked basic terms. The nodes not reachable are removed from the problem. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { active^#(primes()) -> c_1(sieve^#(from(s(s(0()))))) , sieve^#(mark(X)) -> c_20(sieve^#(X)) , sieve^#(ok(X)) -> c_21(sieve^#(X)) , cons^#(mark(X1), X2) -> c_26(cons^#(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_27(cons^#(X1, X2)) , from^#(mark(X)) -> c_22(from^#(X)) , from^#(ok(X)) -> c_23(from^#(X)) , s^#(mark(X)) -> c_24(s^#(X)) , s^#(ok(X)) -> c_25(s^#(X)) , head^#(mark(X)) -> c_28(head^#(X)) , head^#(ok(X)) -> c_29(head^#(X)) , tail^#(mark(X)) -> c_30(tail^#(X)) , tail^#(ok(X)) -> c_31(tail^#(X)) , if^#(mark(X1), X2, X3) -> c_32(if^#(X1, X2, X3)) , if^#(ok(X1), ok(X2), ok(X3)) -> c_33(if^#(X1, X2, X3)) , filter^#(X1, mark(X2)) -> c_34(filter^#(X1, X2)) , filter^#(mark(X1), X2) -> c_35(filter^#(X1, X2)) , filter^#(ok(X1), ok(X2)) -> c_36(filter^#(X1, X2)) , divides^#(X1, mark(X2)) -> c_37(divides^#(X1, X2)) , divides^#(mark(X1), X2) -> c_38(divides^#(X1, X2)) , divides^#(ok(X1), ok(X2)) -> c_39(divides^#(X1, X2)) , proper^#(primes()) -> c_40() , proper^#(0()) -> c_44() , proper^#(true()) -> c_49() , proper^#(false()) -> c_50() , top^#(mark(X)) -> c_53(top^#(proper(X))) , top^#(ok(X)) -> c_54(top^#(active(X))) } Strict Trs: { active(primes()) -> mark(sieve(from(s(s(0()))))) , active(sieve(X)) -> sieve(active(X)) , active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))) , active(from(X)) -> mark(cons(X, from(s(X)))) , active(from(X)) -> from(active(X)) , active(s(X)) -> s(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(head(X)) -> head(active(X)) , active(head(cons(X, Y))) -> mark(X) , active(tail(X)) -> tail(active(X)) , active(tail(cons(X, Y))) -> mark(Y) , active(if(X1, X2, X3)) -> if(active(X1), X2, X3) , active(if(true(), X, Y)) -> mark(X) , active(if(false(), X, Y)) -> mark(Y) , active(filter(X1, X2)) -> filter(X1, active(X2)) , active(filter(X1, X2)) -> filter(active(X1), X2) , active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) , active(divides(X1, X2)) -> divides(X1, active(X2)) , active(divides(X1, X2)) -> divides(active(X1), X2) , sieve(mark(X)) -> mark(sieve(X)) , sieve(ok(X)) -> ok(sieve(X)) , from(mark(X)) -> mark(from(X)) , from(ok(X)) -> ok(from(X)) , s(mark(X)) -> mark(s(X)) , s(ok(X)) -> ok(s(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , head(mark(X)) -> mark(head(X)) , head(ok(X)) -> ok(head(X)) , tail(mark(X)) -> mark(tail(X)) , tail(ok(X)) -> ok(tail(X)) , if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)) , if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)) , filter(X1, mark(X2)) -> mark(filter(X1, X2)) , filter(mark(X1), X2) -> mark(filter(X1, X2)) , filter(ok(X1), ok(X2)) -> ok(filter(X1, X2)) , divides(X1, mark(X2)) -> mark(divides(X1, X2)) , divides(mark(X1), X2) -> mark(divides(X1, X2)) , divides(ok(X1), ok(X2)) -> ok(divides(X1, X2)) , proper(primes()) -> ok(primes()) , proper(sieve(X)) -> sieve(proper(X)) , proper(from(X)) -> from(proper(X)) , proper(s(X)) -> s(proper(X)) , proper(0()) -> ok(0()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(head(X)) -> head(proper(X)) , proper(tail(X)) -> tail(proper(X)) , proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)) , proper(true()) -> ok(true()) , proper(false()) -> ok(false()) , proper(filter(X1, X2)) -> filter(proper(X1), proper(X2)) , proper(divides(X1, X2)) -> divides(proper(X1), proper(X2)) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X)) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {1,22,23,24,25} by applications of Pre({1,22,23,24,25}) = {}. Here rules are labeled as follows: DPs: { 1: active^#(primes()) -> c_1(sieve^#(from(s(s(0()))))) , 2: sieve^#(mark(X)) -> c_20(sieve^#(X)) , 3: sieve^#(ok(X)) -> c_21(sieve^#(X)) , 4: cons^#(mark(X1), X2) -> c_26(cons^#(X1, X2)) , 5: cons^#(ok(X1), ok(X2)) -> c_27(cons^#(X1, X2)) , 6: from^#(mark(X)) -> c_22(from^#(X)) , 7: from^#(ok(X)) -> c_23(from^#(X)) , 8: s^#(mark(X)) -> c_24(s^#(X)) , 9: s^#(ok(X)) -> c_25(s^#(X)) , 10: head^#(mark(X)) -> c_28(head^#(X)) , 11: head^#(ok(X)) -> c_29(head^#(X)) , 12: tail^#(mark(X)) -> c_30(tail^#(X)) , 13: tail^#(ok(X)) -> c_31(tail^#(X)) , 14: if^#(mark(X1), X2, X3) -> c_32(if^#(X1, X2, X3)) , 15: if^#(ok(X1), ok(X2), ok(X3)) -> c_33(if^#(X1, X2, X3)) , 16: filter^#(X1, mark(X2)) -> c_34(filter^#(X1, X2)) , 17: filter^#(mark(X1), X2) -> c_35(filter^#(X1, X2)) , 18: filter^#(ok(X1), ok(X2)) -> c_36(filter^#(X1, X2)) , 19: divides^#(X1, mark(X2)) -> c_37(divides^#(X1, X2)) , 20: divides^#(mark(X1), X2) -> c_38(divides^#(X1, X2)) , 21: divides^#(ok(X1), ok(X2)) -> c_39(divides^#(X1, X2)) , 22: proper^#(primes()) -> c_40() , 23: proper^#(0()) -> c_44() , 24: proper^#(true()) -> c_49() , 25: proper^#(false()) -> c_50() , 26: top^#(mark(X)) -> c_53(top^#(proper(X))) , 27: top^#(ok(X)) -> c_54(top^#(active(X))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { sieve^#(mark(X)) -> c_20(sieve^#(X)) , sieve^#(ok(X)) -> c_21(sieve^#(X)) , cons^#(mark(X1), X2) -> c_26(cons^#(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_27(cons^#(X1, X2)) , from^#(mark(X)) -> c_22(from^#(X)) , from^#(ok(X)) -> c_23(from^#(X)) , s^#(mark(X)) -> c_24(s^#(X)) , s^#(ok(X)) -> c_25(s^#(X)) , head^#(mark(X)) -> c_28(head^#(X)) , head^#(ok(X)) -> c_29(head^#(X)) , tail^#(mark(X)) -> c_30(tail^#(X)) , tail^#(ok(X)) -> c_31(tail^#(X)) , if^#(mark(X1), X2, X3) -> c_32(if^#(X1, X2, X3)) , if^#(ok(X1), ok(X2), ok(X3)) -> c_33(if^#(X1, X2, X3)) , filter^#(X1, mark(X2)) -> c_34(filter^#(X1, X2)) , filter^#(mark(X1), X2) -> c_35(filter^#(X1, X2)) , filter^#(ok(X1), ok(X2)) -> c_36(filter^#(X1, X2)) , divides^#(X1, mark(X2)) -> c_37(divides^#(X1, X2)) , divides^#(mark(X1), X2) -> c_38(divides^#(X1, X2)) , divides^#(ok(X1), ok(X2)) -> c_39(divides^#(X1, X2)) , top^#(mark(X)) -> c_53(top^#(proper(X))) , top^#(ok(X)) -> c_54(top^#(active(X))) } Strict Trs: { active(primes()) -> mark(sieve(from(s(s(0()))))) , active(sieve(X)) -> sieve(active(X)) , active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))) , active(from(X)) -> mark(cons(X, from(s(X)))) , active(from(X)) -> from(active(X)) , active(s(X)) -> s(active(X)) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(head(X)) -> head(active(X)) , active(head(cons(X, Y))) -> mark(X) , active(tail(X)) -> tail(active(X)) , active(tail(cons(X, Y))) -> mark(Y) , active(if(X1, X2, X3)) -> if(active(X1), X2, X3) , active(if(true(), X, Y)) -> mark(X) , active(if(false(), X, Y)) -> mark(Y) , active(filter(X1, X2)) -> filter(X1, active(X2)) , active(filter(X1, X2)) -> filter(active(X1), X2) , active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) , active(divides(X1, X2)) -> divides(X1, active(X2)) , active(divides(X1, X2)) -> divides(active(X1), X2) , sieve(mark(X)) -> mark(sieve(X)) , sieve(ok(X)) -> ok(sieve(X)) , from(mark(X)) -> mark(from(X)) , from(ok(X)) -> ok(from(X)) , s(mark(X)) -> mark(s(X)) , s(ok(X)) -> ok(s(X)) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , head(mark(X)) -> mark(head(X)) , head(ok(X)) -> ok(head(X)) , tail(mark(X)) -> mark(tail(X)) , tail(ok(X)) -> ok(tail(X)) , if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)) , if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)) , filter(X1, mark(X2)) -> mark(filter(X1, X2)) , filter(mark(X1), X2) -> mark(filter(X1, X2)) , filter(ok(X1), ok(X2)) -> ok(filter(X1, X2)) , divides(X1, mark(X2)) -> mark(divides(X1, X2)) , divides(mark(X1), X2) -> mark(divides(X1, X2)) , divides(ok(X1), ok(X2)) -> ok(divides(X1, X2)) , proper(primes()) -> ok(primes()) , proper(sieve(X)) -> sieve(proper(X)) , proper(from(X)) -> from(proper(X)) , proper(s(X)) -> s(proper(X)) , proper(0()) -> ok(0()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(head(X)) -> head(proper(X)) , proper(tail(X)) -> tail(proper(X)) , proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)) , proper(true()) -> ok(true()) , proper(false()) -> ok(false()) , proper(filter(X1, X2)) -> filter(proper(X1), proper(X2)) , proper(divides(X1, X2)) -> divides(proper(X1), proper(X2)) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X)) } Weak DPs: { active^#(primes()) -> c_1(sieve^#(from(s(s(0()))))) , proper^#(primes()) -> c_40() , proper^#(0()) -> c_44() , proper^#(true()) -> c_49() , proper^#(false()) -> c_50() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..