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