MAYBE
1091.05/297.07	MAYBE
1091.05/297.07	
1091.05/297.07	We are left with following problem, upon which TcT provides the
1091.05/297.07	certificate MAYBE.
1091.05/297.07	
1091.05/297.07	Strict Trs:
1091.05/297.07	  { primes() -> sieve(from(s(s(0()))))
1091.05/297.07	  , sieve(X) -> n__sieve(X)
1091.05/297.07	  , sieve(cons(X, Y)) -> cons(X, n__filter(X, n__sieve(activate(Y))))
1091.05/297.07	  , from(X) -> cons(X, n__from(n__s(X)))
1091.05/297.07	  , from(X) -> n__from(X)
1091.05/297.07	  , s(X) -> n__s(X)
1091.05/297.07	  , cons(X1, X2) -> n__cons(X1, X2)
1091.05/297.07	  , head(cons(X, Y)) -> X
1091.05/297.07	  , tail(cons(X, Y)) -> activate(Y)
1091.05/297.07	  , activate(X) -> X
1091.05/297.07	  , activate(n__from(X)) -> from(activate(X))
1091.05/297.07	  , activate(n__s(X)) -> s(activate(X))
1091.05/297.07	  , activate(n__filter(X1, X2)) -> filter(activate(X1), activate(X2))
1091.05/297.07	  , activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
1091.05/297.07	  , activate(n__sieve(X)) -> sieve(activate(X))
1091.05/297.07	  , if(true(), X, Y) -> activate(X)
1091.05/297.07	  , if(false(), X, Y) -> activate(Y)
1091.05/297.07	  , filter(X1, X2) -> n__filter(X1, X2)
1091.05/297.07	  , filter(s(s(X)), cons(Y, Z)) ->
1091.05/297.07	    if(divides(s(s(X)), Y),
1091.05/297.07	       n__filter(n__s(n__s(X)), activate(Z)),
1091.05/297.07	       n__cons(Y, n__filter(X, n__sieve(Y)))) }
1091.05/297.07	Obligation:
1091.05/297.07	  runtime complexity
1091.05/297.07	Answer:
1091.05/297.07	  MAYBE
1091.05/297.07	
1091.05/297.07	None of the processors succeeded.
1091.05/297.07	
1091.05/297.07	Details of failed attempt(s):
1091.05/297.07	-----------------------------
1091.05/297.07	1) 'With Problem ... (timeout of 297 seconds)' failed due to the
1091.05/297.07	   following reason:
1091.05/297.07	   
1091.05/297.07	   Computation stopped due to timeout after 297.0 seconds.
1091.05/297.07	
1091.05/297.07	2) 'Best' failed due to the following reason:
1091.05/297.07	   
1091.05/297.07	   None of the processors succeeded.
1091.05/297.07	   
1091.05/297.07	   Details of failed attempt(s):
1091.05/297.07	   -----------------------------
1091.05/297.07	   1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
1091.05/297.07	      seconds)' failed due to the following reason:
1091.05/297.07	      
1091.05/297.07	      Computation stopped due to timeout after 148.0 seconds.
1091.05/297.07	   
1091.05/297.07	   2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
1091.05/297.07	      failed due to the following reason:
1091.05/297.07	      
1091.05/297.07	      None of the processors succeeded.
1091.05/297.07	      
1091.05/297.07	      Details of failed attempt(s):
1091.05/297.07	      -----------------------------
1091.05/297.07	      1) 'Bounds with perSymbol-enrichment and initial automaton 'match''
1091.05/297.07	         failed due to the following reason:
1091.05/297.07	         
1091.05/297.07	         match-boundness of the problem could not be verified.
1091.05/297.07	      
1091.05/297.07	      2) 'Bounds with minimal-enrichment and initial automaton 'match''
1091.05/297.07	         failed due to the following reason:
1091.05/297.07	         
1091.05/297.07	         match-boundness of the problem could not be verified.
1091.05/297.07	      
1091.05/297.07	   
1091.05/297.07	   3) 'Best' failed due to the following reason:
1091.05/297.07	      
1091.05/297.07	      None of the processors succeeded.
1091.05/297.07	      
1091.05/297.07	      Details of failed attempt(s):
1091.05/297.07	      -----------------------------
1091.05/297.07	      1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
1091.05/297.07	         following reason:
1091.05/297.07	         
1091.05/297.07	         The processor is inapplicable, reason:
1091.05/297.07	           Processor only applicable for innermost runtime complexity analysis
1091.05/297.07	      
1091.05/297.07	      2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
1091.05/297.07	         to the following reason:
1091.05/297.07	         
1091.05/297.07	         The processor is inapplicable, reason:
1091.05/297.07	           Processor only applicable for innermost runtime complexity analysis
1091.05/297.07	      
1091.05/297.07	   
1091.05/297.07	
1091.05/297.07	3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to
1091.05/297.07	   the following reason:
1091.05/297.07	   
1091.05/297.07	   We add the following weak dependency pairs:
1091.05/297.07	   
1091.05/297.07	   Strict DPs:
1091.05/297.07	     { primes^#() -> c_1(sieve^#(from(s(s(0())))))
1091.05/297.07	     , sieve^#(X) -> c_2(X)
1091.05/297.07	     , sieve^#(cons(X, Y)) ->
1091.05/297.07	       c_3(cons^#(X, n__filter(X, n__sieve(activate(Y)))))
1091.05/297.07	     , cons^#(X1, X2) -> c_7(X1, X2)
1091.05/297.07	     , from^#(X) -> c_4(cons^#(X, n__from(n__s(X))))
1091.05/297.07	     , from^#(X) -> c_5(X)
1091.05/297.07	     , s^#(X) -> c_6(X)
1091.05/297.07	     , head^#(cons(X, Y)) -> c_8(X)
1091.05/297.07	     , tail^#(cons(X, Y)) -> c_9(activate^#(Y))
1091.05/297.07	     , activate^#(X) -> c_10(X)
1091.05/297.07	     , activate^#(n__from(X)) -> c_11(from^#(activate(X)))
1091.05/297.07	     , activate^#(n__s(X)) -> c_12(s^#(activate(X)))
1091.05/297.07	     , activate^#(n__filter(X1, X2)) ->
1091.05/297.07	       c_13(filter^#(activate(X1), activate(X2)))
1091.05/297.07	     , activate^#(n__cons(X1, X2)) -> c_14(cons^#(activate(X1), X2))
1091.05/297.07	     , activate^#(n__sieve(X)) -> c_15(sieve^#(activate(X)))
1091.05/297.07	     , filter^#(X1, X2) -> c_18(X1, X2)
1091.05/297.07	     , filter^#(s(s(X)), cons(Y, Z)) ->
1091.05/297.07	       c_19(if^#(divides(s(s(X)), Y),
1091.05/297.07	                 n__filter(n__s(n__s(X)), activate(Z)),
1091.05/297.07	                 n__cons(Y, n__filter(X, n__sieve(Y)))))
1091.05/297.07	     , if^#(true(), X, Y) -> c_16(activate^#(X))
1091.05/297.07	     , if^#(false(), X, Y) -> c_17(activate^#(Y)) }
1091.05/297.07	   
1091.05/297.07	   and mark the set of starting terms.
1091.05/297.07	   
1091.05/297.07	   We are left with following problem, upon which TcT provides the
1091.05/297.07	   certificate MAYBE.
1091.05/297.07	   
1091.05/297.07	   Strict DPs:
1091.05/297.07	     { primes^#() -> c_1(sieve^#(from(s(s(0())))))
1091.05/297.07	     , sieve^#(X) -> c_2(X)
1091.05/297.07	     , sieve^#(cons(X, Y)) ->
1091.05/297.07	       c_3(cons^#(X, n__filter(X, n__sieve(activate(Y)))))
1091.05/297.07	     , cons^#(X1, X2) -> c_7(X1, X2)
1091.05/297.07	     , from^#(X) -> c_4(cons^#(X, n__from(n__s(X))))
1091.05/297.07	     , from^#(X) -> c_5(X)
1091.05/297.07	     , s^#(X) -> c_6(X)
1091.05/297.07	     , head^#(cons(X, Y)) -> c_8(X)
1091.05/297.07	     , tail^#(cons(X, Y)) -> c_9(activate^#(Y))
1091.05/297.07	     , activate^#(X) -> c_10(X)
1091.05/297.07	     , activate^#(n__from(X)) -> c_11(from^#(activate(X)))
1091.05/297.07	     , activate^#(n__s(X)) -> c_12(s^#(activate(X)))
1091.05/297.07	     , activate^#(n__filter(X1, X2)) ->
1091.05/297.07	       c_13(filter^#(activate(X1), activate(X2)))
1091.05/297.07	     , activate^#(n__cons(X1, X2)) -> c_14(cons^#(activate(X1), X2))
1091.05/297.07	     , activate^#(n__sieve(X)) -> c_15(sieve^#(activate(X)))
1091.05/297.07	     , filter^#(X1, X2) -> c_18(X1, X2)
1091.05/297.07	     , filter^#(s(s(X)), cons(Y, Z)) ->
1091.05/297.07	       c_19(if^#(divides(s(s(X)), Y),
1091.05/297.07	                 n__filter(n__s(n__s(X)), activate(Z)),
1091.05/297.07	                 n__cons(Y, n__filter(X, n__sieve(Y)))))
1091.05/297.07	     , if^#(true(), X, Y) -> c_16(activate^#(X))
1091.05/297.07	     , if^#(false(), X, Y) -> c_17(activate^#(Y)) }
1091.05/297.07	   Strict Trs:
1091.05/297.07	     { primes() -> sieve(from(s(s(0()))))
1091.05/297.07	     , sieve(X) -> n__sieve(X)
1091.05/297.07	     , sieve(cons(X, Y)) -> cons(X, n__filter(X, n__sieve(activate(Y))))
1091.05/297.07	     , from(X) -> cons(X, n__from(n__s(X)))
1091.05/297.07	     , from(X) -> n__from(X)
1091.05/297.07	     , s(X) -> n__s(X)
1091.05/297.07	     , cons(X1, X2) -> n__cons(X1, X2)
1091.05/297.07	     , head(cons(X, Y)) -> X
1091.05/297.07	     , tail(cons(X, Y)) -> activate(Y)
1091.05/297.07	     , activate(X) -> X
1091.05/297.07	     , activate(n__from(X)) -> from(activate(X))
1091.05/297.07	     , activate(n__s(X)) -> s(activate(X))
1091.05/297.07	     , activate(n__filter(X1, X2)) -> filter(activate(X1), activate(X2))
1091.05/297.07	     , activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
1091.05/297.07	     , activate(n__sieve(X)) -> sieve(activate(X))
1091.05/297.07	     , if(true(), X, Y) -> activate(X)
1091.05/297.07	     , if(false(), X, Y) -> activate(Y)
1091.05/297.07	     , filter(X1, X2) -> n__filter(X1, X2)
1091.05/297.07	     , filter(s(s(X)), cons(Y, Z)) ->
1091.05/297.07	       if(divides(s(s(X)), Y),
1091.05/297.07	          n__filter(n__s(n__s(X)), activate(Z)),
1091.05/297.07	          n__cons(Y, n__filter(X, n__sieve(Y)))) }
1091.05/297.07	   Obligation:
1091.05/297.07	     runtime complexity
1091.05/297.07	   Answer:
1091.05/297.07	     MAYBE
1091.05/297.07	   
1091.05/297.07	   We estimate the number of application of {17} by applications of
1091.05/297.07	   Pre({17}) = {2,4,6,7,8,10,13,16}. Here rules are labeled as
1091.05/297.07	   follows:
1091.05/297.07	   
1091.05/297.07	     DPs:
1091.05/297.07	       { 1: primes^#() -> c_1(sieve^#(from(s(s(0())))))
1091.05/297.07	       , 2: sieve^#(X) -> c_2(X)
1091.05/297.07	       , 3: sieve^#(cons(X, Y)) ->
1091.05/297.07	            c_3(cons^#(X, n__filter(X, n__sieve(activate(Y)))))
1091.05/297.07	       , 4: cons^#(X1, X2) -> c_7(X1, X2)
1091.05/297.07	       , 5: from^#(X) -> c_4(cons^#(X, n__from(n__s(X))))
1091.05/297.07	       , 6: from^#(X) -> c_5(X)
1091.05/297.07	       , 7: s^#(X) -> c_6(X)
1091.05/297.07	       , 8: head^#(cons(X, Y)) -> c_8(X)
1091.05/297.07	       , 9: tail^#(cons(X, Y)) -> c_9(activate^#(Y))
1091.05/297.07	       , 10: activate^#(X) -> c_10(X)
1091.05/297.07	       , 11: activate^#(n__from(X)) -> c_11(from^#(activate(X)))
1091.05/297.07	       , 12: activate^#(n__s(X)) -> c_12(s^#(activate(X)))
1091.05/297.07	       , 13: activate^#(n__filter(X1, X2)) ->
1091.05/297.07	             c_13(filter^#(activate(X1), activate(X2)))
1091.05/297.07	       , 14: activate^#(n__cons(X1, X2)) -> c_14(cons^#(activate(X1), X2))
1091.05/297.07	       , 15: activate^#(n__sieve(X)) -> c_15(sieve^#(activate(X)))
1091.05/297.07	       , 16: filter^#(X1, X2) -> c_18(X1, X2)
1091.05/297.07	       , 17: filter^#(s(s(X)), cons(Y, Z)) ->
1091.05/297.07	             c_19(if^#(divides(s(s(X)), Y),
1091.05/297.07	                       n__filter(n__s(n__s(X)), activate(Z)),
1091.05/297.07	                       n__cons(Y, n__filter(X, n__sieve(Y)))))
1091.05/297.07	       , 18: if^#(true(), X, Y) -> c_16(activate^#(X))
1091.05/297.07	       , 19: if^#(false(), X, Y) -> c_17(activate^#(Y)) }
1091.05/297.07	   
1091.05/297.07	   We are left with following problem, upon which TcT provides the
1091.05/297.07	   certificate MAYBE.
1091.05/297.07	   
1091.05/297.07	   Strict DPs:
1091.05/297.07	     { primes^#() -> c_1(sieve^#(from(s(s(0())))))
1091.05/297.07	     , sieve^#(X) -> c_2(X)
1091.05/297.07	     , sieve^#(cons(X, Y)) ->
1091.05/297.07	       c_3(cons^#(X, n__filter(X, n__sieve(activate(Y)))))
1091.05/297.08	     , cons^#(X1, X2) -> c_7(X1, X2)
1091.05/297.08	     , from^#(X) -> c_4(cons^#(X, n__from(n__s(X))))
1091.05/297.08	     , from^#(X) -> c_5(X)
1091.05/297.08	     , s^#(X) -> c_6(X)
1091.05/297.08	     , head^#(cons(X, Y)) -> c_8(X)
1091.05/297.08	     , tail^#(cons(X, Y)) -> c_9(activate^#(Y))
1091.05/297.08	     , activate^#(X) -> c_10(X)
1091.05/297.08	     , activate^#(n__from(X)) -> c_11(from^#(activate(X)))
1091.05/297.08	     , activate^#(n__s(X)) -> c_12(s^#(activate(X)))
1091.05/297.08	     , activate^#(n__filter(X1, X2)) ->
1091.05/297.08	       c_13(filter^#(activate(X1), activate(X2)))
1091.05/297.08	     , activate^#(n__cons(X1, X2)) -> c_14(cons^#(activate(X1), X2))
1091.05/297.08	     , activate^#(n__sieve(X)) -> c_15(sieve^#(activate(X)))
1091.05/297.08	     , filter^#(X1, X2) -> c_18(X1, X2)
1091.05/297.08	     , if^#(true(), X, Y) -> c_16(activate^#(X))
1091.05/297.08	     , if^#(false(), X, Y) -> c_17(activate^#(Y)) }
1091.05/297.08	   Strict Trs:
1091.05/297.08	     { primes() -> sieve(from(s(s(0()))))
1091.05/297.08	     , sieve(X) -> n__sieve(X)
1091.05/297.08	     , sieve(cons(X, Y)) -> cons(X, n__filter(X, n__sieve(activate(Y))))
1091.05/297.08	     , from(X) -> cons(X, n__from(n__s(X)))
1091.05/297.08	     , from(X) -> n__from(X)
1091.05/297.08	     , s(X) -> n__s(X)
1091.05/297.08	     , cons(X1, X2) -> n__cons(X1, X2)
1091.05/297.08	     , head(cons(X, Y)) -> X
1091.05/297.08	     , tail(cons(X, Y)) -> activate(Y)
1091.05/297.08	     , activate(X) -> X
1091.05/297.08	     , activate(n__from(X)) -> from(activate(X))
1091.05/297.08	     , activate(n__s(X)) -> s(activate(X))
1091.05/297.08	     , activate(n__filter(X1, X2)) -> filter(activate(X1), activate(X2))
1091.05/297.08	     , activate(n__cons(X1, X2)) -> cons(activate(X1), X2)
1091.05/297.08	     , activate(n__sieve(X)) -> sieve(activate(X))
1091.05/297.08	     , if(true(), X, Y) -> activate(X)
1091.05/297.08	     , if(false(), X, Y) -> activate(Y)
1091.05/297.08	     , filter(X1, X2) -> n__filter(X1, X2)
1091.05/297.08	     , filter(s(s(X)), cons(Y, Z)) ->
1091.05/297.08	       if(divides(s(s(X)), Y),
1091.05/297.08	          n__filter(n__s(n__s(X)), activate(Z)),
1091.05/297.08	          n__cons(Y, n__filter(X, n__sieve(Y)))) }
1091.05/297.08	   Weak DPs:
1091.05/297.08	     { filter^#(s(s(X)), cons(Y, Z)) ->
1091.05/297.08	       c_19(if^#(divides(s(s(X)), Y),
1091.05/297.08	                 n__filter(n__s(n__s(X)), activate(Z)),
1091.05/297.08	                 n__cons(Y, n__filter(X, n__sieve(Y))))) }
1091.05/297.08	   Obligation:
1091.05/297.08	     runtime complexity
1091.05/297.08	   Answer:
1091.05/297.08	     MAYBE
1091.05/297.08	   
1091.05/297.08	   Empty strict component of the problem is NOT empty.
1091.05/297.08	
1091.05/297.08	
1091.05/297.08	Arrrr..
1092.13/298.00	EOF