MAYBE
908.45/297.04	MAYBE
908.45/297.04	
908.45/297.04	We are left with following problem, upon which TcT provides the
908.45/297.04	certificate MAYBE.
908.45/297.04	
908.45/297.04	Strict Trs:
908.45/297.04	  { active(filter(X1, X2, X3)) -> filter(X1, X2, active(X3))
908.45/297.04	  , active(filter(X1, X2, X3)) -> filter(X1, active(X2), X3)
908.45/297.04	  , active(filter(X1, X2, X3)) -> filter(active(X1), X2, X3)
908.45/297.04	  , active(filter(cons(X, Y), 0(), M)) ->
908.45/297.04	    mark(cons(0(), filter(Y, M, M)))
908.45/297.04	  , active(filter(cons(X, Y), s(N), M)) ->
908.45/297.04	    mark(cons(X, filter(Y, N, M)))
908.45/297.04	  , active(cons(X1, X2)) -> cons(active(X1), X2)
908.45/297.04	  , active(s(X)) -> s(active(X))
908.45/297.04	  , active(sieve(X)) -> sieve(active(X))
908.45/297.04	  , active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y)))
908.45/297.04	  , active(sieve(cons(s(N), Y))) ->
908.45/297.04	    mark(cons(s(N), sieve(filter(Y, N, N))))
908.45/297.04	  , active(nats(N)) -> mark(cons(N, nats(s(N))))
908.45/297.04	  , active(nats(X)) -> nats(active(X))
908.45/297.04	  , active(zprimes()) -> mark(sieve(nats(s(s(0())))))
908.45/297.04	  , filter(X1, X2, mark(X3)) -> mark(filter(X1, X2, X3))
908.45/297.04	  , filter(X1, mark(X2), X3) -> mark(filter(X1, X2, X3))
908.45/297.04	  , filter(mark(X1), X2, X3) -> mark(filter(X1, X2, X3))
908.45/297.04	  , filter(ok(X1), ok(X2), ok(X3)) -> ok(filter(X1, X2, X3))
908.45/297.04	  , cons(mark(X1), X2) -> mark(cons(X1, X2))
908.45/297.04	  , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
908.45/297.04	  , s(mark(X)) -> mark(s(X))
908.45/297.04	  , s(ok(X)) -> ok(s(X))
908.45/297.04	  , sieve(mark(X)) -> mark(sieve(X))
908.45/297.04	  , sieve(ok(X)) -> ok(sieve(X))
908.45/297.04	  , nats(mark(X)) -> mark(nats(X))
908.45/297.04	  , nats(ok(X)) -> ok(nats(X))
908.45/297.04	  , proper(filter(X1, X2, X3)) ->
908.45/297.04	    filter(proper(X1), proper(X2), proper(X3))
908.45/297.04	  , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
908.45/297.04	  , proper(0()) -> ok(0())
908.45/297.04	  , proper(s(X)) -> s(proper(X))
908.45/297.04	  , proper(sieve(X)) -> sieve(proper(X))
908.45/297.04	  , proper(nats(X)) -> nats(proper(X))
908.45/297.04	  , proper(zprimes()) -> ok(zprimes())
908.45/297.04	  , top(mark(X)) -> top(proper(X))
908.45/297.04	  , top(ok(X)) -> top(active(X)) }
908.45/297.04	Obligation:
908.45/297.04	  runtime complexity
908.45/297.04	Answer:
908.45/297.04	  MAYBE
908.45/297.04	
908.45/297.04	None of the processors succeeded.
908.45/297.04	
908.45/297.04	Details of failed attempt(s):
908.45/297.04	-----------------------------
908.45/297.04	1) 'With Problem ... (timeout of 297 seconds)' failed due to the
908.45/297.04	   following reason:
908.45/297.04	   
908.45/297.04	   Computation stopped due to timeout after 297.0 seconds.
908.45/297.04	
908.45/297.04	2) 'Best' failed due to the following reason:
908.45/297.04	   
908.45/297.04	   None of the processors succeeded.
908.45/297.04	   
908.45/297.04	   Details of failed attempt(s):
908.45/297.04	   -----------------------------
908.45/297.04	   1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
908.45/297.04	      seconds)' failed due to the following reason:
908.45/297.04	      
908.45/297.04	      Computation stopped due to timeout after 148.0 seconds.
908.45/297.04	   
908.45/297.04	   2) 'Best' failed due to the following reason:
908.45/297.04	      
908.45/297.04	      None of the processors succeeded.
908.45/297.04	      
908.45/297.04	      Details of failed attempt(s):
908.45/297.04	      -----------------------------
908.45/297.04	      1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
908.45/297.04	         following reason:
908.45/297.04	         
908.45/297.04	         The processor is inapplicable, reason:
908.45/297.04	           Processor only applicable for innermost runtime complexity analysis
908.45/297.04	      
908.45/297.04	      2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
908.45/297.04	         to the following reason:
908.45/297.04	         
908.45/297.04	         The processor is inapplicable, reason:
908.45/297.04	           Processor only applicable for innermost runtime complexity analysis
908.45/297.04	      
908.45/297.04	   
908.45/297.04	   3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
908.45/297.04	      failed due to the following reason:
908.45/297.04	      
908.45/297.04	      None of the processors succeeded.
908.45/297.04	      
908.45/297.04	      Details of failed attempt(s):
908.45/297.04	      -----------------------------
908.45/297.04	      1) 'Bounds with minimal-enrichment and initial automaton 'match''
908.45/297.04	         failed due to the following reason:
908.45/297.04	         
908.45/297.04	         match-boundness of the problem could not be verified.
908.45/297.04	      
908.45/297.04	      2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
908.45/297.04	         failed due to the following reason:
908.45/297.04	         
908.45/297.04	         match-boundness of the problem could not be verified.
908.45/297.04	      
908.45/297.04	   
908.45/297.04	
908.45/297.04	3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to
908.45/297.04	   the following reason:
908.45/297.04	   
908.45/297.04	   We add the following weak dependency pairs:
908.45/297.04	   
908.45/297.04	   Strict DPs:
908.45/297.04	     { active^#(filter(X1, X2, X3)) -> c_1(filter^#(X1, X2, active(X3)))
908.45/297.04	     , active^#(filter(X1, X2, X3)) -> c_2(filter^#(X1, active(X2), X3))
908.45/297.04	     , active^#(filter(X1, X2, X3)) -> c_3(filter^#(active(X1), X2, X3))
908.45/297.04	     , active^#(filter(cons(X, Y), 0(), M)) ->
908.45/297.04	       c_4(cons^#(0(), filter(Y, M, M)))
908.45/297.04	     , active^#(filter(cons(X, Y), s(N), M)) ->
908.45/297.04	       c_5(cons^#(X, filter(Y, N, M)))
908.45/297.04	     , active^#(cons(X1, X2)) -> c_6(cons^#(active(X1), X2))
908.45/297.04	     , active^#(s(X)) -> c_7(s^#(active(X)))
908.45/297.04	     , active^#(sieve(X)) -> c_8(sieve^#(active(X)))
908.45/297.04	     , active^#(sieve(cons(0(), Y))) -> c_9(cons^#(0(), sieve(Y)))
908.45/297.04	     , active^#(sieve(cons(s(N), Y))) ->
908.45/297.04	       c_10(cons^#(s(N), sieve(filter(Y, N, N))))
908.45/297.04	     , active^#(nats(N)) -> c_11(cons^#(N, nats(s(N))))
908.45/297.04	     , active^#(nats(X)) -> c_12(nats^#(active(X)))
908.45/297.04	     , active^#(zprimes()) -> c_13(sieve^#(nats(s(s(0())))))
908.45/297.04	     , filter^#(X1, X2, mark(X3)) -> c_14(filter^#(X1, X2, X3))
908.45/297.04	     , filter^#(X1, mark(X2), X3) -> c_15(filter^#(X1, X2, X3))
908.45/297.04	     , filter^#(mark(X1), X2, X3) -> c_16(filter^#(X1, X2, X3))
908.45/297.04	     , filter^#(ok(X1), ok(X2), ok(X3)) -> c_17(filter^#(X1, X2, X3))
908.45/297.04	     , cons^#(mark(X1), X2) -> c_18(cons^#(X1, X2))
908.45/297.04	     , cons^#(ok(X1), ok(X2)) -> c_19(cons^#(X1, X2))
908.45/297.04	     , s^#(mark(X)) -> c_20(s^#(X))
908.45/297.04	     , s^#(ok(X)) -> c_21(s^#(X))
908.45/297.04	     , sieve^#(mark(X)) -> c_22(sieve^#(X))
908.45/297.04	     , sieve^#(ok(X)) -> c_23(sieve^#(X))
908.45/297.04	     , nats^#(mark(X)) -> c_24(nats^#(X))
908.45/297.04	     , nats^#(ok(X)) -> c_25(nats^#(X))
908.45/297.04	     , proper^#(filter(X1, X2, X3)) ->
908.45/297.04	       c_26(filter^#(proper(X1), proper(X2), proper(X3)))
908.45/297.04	     , proper^#(cons(X1, X2)) -> c_27(cons^#(proper(X1), proper(X2)))
908.45/297.04	     , proper^#(0()) -> c_28()
908.45/297.04	     , proper^#(s(X)) -> c_29(s^#(proper(X)))
908.45/297.04	     , proper^#(sieve(X)) -> c_30(sieve^#(proper(X)))
908.45/297.04	     , proper^#(nats(X)) -> c_31(nats^#(proper(X)))
908.45/297.04	     , proper^#(zprimes()) -> c_32()
908.45/297.04	     , top^#(mark(X)) -> c_33(top^#(proper(X)))
908.45/297.04	     , top^#(ok(X)) -> c_34(top^#(active(X))) }
908.45/297.04	   
908.45/297.04	   and mark the set of starting terms.
908.45/297.04	   
908.45/297.04	   We are left with following problem, upon which TcT provides the
908.45/297.04	   certificate MAYBE.
908.45/297.04	   
908.45/297.04	   Strict DPs:
908.45/297.04	     { active^#(filter(X1, X2, X3)) -> c_1(filter^#(X1, X2, active(X3)))
908.45/297.04	     , active^#(filter(X1, X2, X3)) -> c_2(filter^#(X1, active(X2), X3))
908.45/297.04	     , active^#(filter(X1, X2, X3)) -> c_3(filter^#(active(X1), X2, X3))
908.45/297.04	     , active^#(filter(cons(X, Y), 0(), M)) ->
908.45/297.04	       c_4(cons^#(0(), filter(Y, M, M)))
908.45/297.04	     , active^#(filter(cons(X, Y), s(N), M)) ->
908.45/297.04	       c_5(cons^#(X, filter(Y, N, M)))
908.45/297.04	     , active^#(cons(X1, X2)) -> c_6(cons^#(active(X1), X2))
908.45/297.04	     , active^#(s(X)) -> c_7(s^#(active(X)))
908.45/297.04	     , active^#(sieve(X)) -> c_8(sieve^#(active(X)))
908.45/297.04	     , active^#(sieve(cons(0(), Y))) -> c_9(cons^#(0(), sieve(Y)))
908.45/297.04	     , active^#(sieve(cons(s(N), Y))) ->
908.45/297.04	       c_10(cons^#(s(N), sieve(filter(Y, N, N))))
908.45/297.04	     , active^#(nats(N)) -> c_11(cons^#(N, nats(s(N))))
908.45/297.04	     , active^#(nats(X)) -> c_12(nats^#(active(X)))
908.45/297.04	     , active^#(zprimes()) -> c_13(sieve^#(nats(s(s(0())))))
908.45/297.04	     , filter^#(X1, X2, mark(X3)) -> c_14(filter^#(X1, X2, X3))
908.45/297.04	     , filter^#(X1, mark(X2), X3) -> c_15(filter^#(X1, X2, X3))
908.45/297.04	     , filter^#(mark(X1), X2, X3) -> c_16(filter^#(X1, X2, X3))
908.45/297.04	     , filter^#(ok(X1), ok(X2), ok(X3)) -> c_17(filter^#(X1, X2, X3))
908.45/297.04	     , cons^#(mark(X1), X2) -> c_18(cons^#(X1, X2))
908.45/297.04	     , cons^#(ok(X1), ok(X2)) -> c_19(cons^#(X1, X2))
908.45/297.04	     , s^#(mark(X)) -> c_20(s^#(X))
908.45/297.04	     , s^#(ok(X)) -> c_21(s^#(X))
908.45/297.04	     , sieve^#(mark(X)) -> c_22(sieve^#(X))
908.45/297.04	     , sieve^#(ok(X)) -> c_23(sieve^#(X))
908.45/297.04	     , nats^#(mark(X)) -> c_24(nats^#(X))
908.45/297.04	     , nats^#(ok(X)) -> c_25(nats^#(X))
908.45/297.04	     , proper^#(filter(X1, X2, X3)) ->
908.45/297.04	       c_26(filter^#(proper(X1), proper(X2), proper(X3)))
908.45/297.04	     , proper^#(cons(X1, X2)) -> c_27(cons^#(proper(X1), proper(X2)))
908.45/297.04	     , proper^#(0()) -> c_28()
908.45/297.04	     , proper^#(s(X)) -> c_29(s^#(proper(X)))
908.45/297.04	     , proper^#(sieve(X)) -> c_30(sieve^#(proper(X)))
908.45/297.04	     , proper^#(nats(X)) -> c_31(nats^#(proper(X)))
908.45/297.04	     , proper^#(zprimes()) -> c_32()
908.45/297.04	     , top^#(mark(X)) -> c_33(top^#(proper(X)))
908.45/297.04	     , top^#(ok(X)) -> c_34(top^#(active(X))) }
908.45/297.04	   Strict Trs:
908.45/297.04	     { active(filter(X1, X2, X3)) -> filter(X1, X2, active(X3))
908.45/297.04	     , active(filter(X1, X2, X3)) -> filter(X1, active(X2), X3)
908.45/297.04	     , active(filter(X1, X2, X3)) -> filter(active(X1), X2, X3)
908.45/297.04	     , active(filter(cons(X, Y), 0(), M)) ->
908.45/297.04	       mark(cons(0(), filter(Y, M, M)))
908.45/297.04	     , active(filter(cons(X, Y), s(N), M)) ->
908.45/297.04	       mark(cons(X, filter(Y, N, M)))
908.45/297.04	     , active(cons(X1, X2)) -> cons(active(X1), X2)
908.45/297.04	     , active(s(X)) -> s(active(X))
908.45/297.04	     , active(sieve(X)) -> sieve(active(X))
908.45/297.04	     , active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y)))
908.45/297.04	     , active(sieve(cons(s(N), Y))) ->
908.45/297.04	       mark(cons(s(N), sieve(filter(Y, N, N))))
908.45/297.04	     , active(nats(N)) -> mark(cons(N, nats(s(N))))
908.45/297.04	     , active(nats(X)) -> nats(active(X))
908.45/297.04	     , active(zprimes()) -> mark(sieve(nats(s(s(0())))))
908.45/297.04	     , filter(X1, X2, mark(X3)) -> mark(filter(X1, X2, X3))
908.45/297.04	     , filter(X1, mark(X2), X3) -> mark(filter(X1, X2, X3))
908.45/297.04	     , filter(mark(X1), X2, X3) -> mark(filter(X1, X2, X3))
908.45/297.04	     , filter(ok(X1), ok(X2), ok(X3)) -> ok(filter(X1, X2, X3))
908.45/297.04	     , cons(mark(X1), X2) -> mark(cons(X1, X2))
908.45/297.04	     , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
908.45/297.04	     , s(mark(X)) -> mark(s(X))
908.45/297.04	     , s(ok(X)) -> ok(s(X))
908.45/297.04	     , sieve(mark(X)) -> mark(sieve(X))
908.45/297.04	     , sieve(ok(X)) -> ok(sieve(X))
908.45/297.04	     , nats(mark(X)) -> mark(nats(X))
908.45/297.04	     , nats(ok(X)) -> ok(nats(X))
908.45/297.04	     , proper(filter(X1, X2, X3)) ->
908.45/297.04	       filter(proper(X1), proper(X2), proper(X3))
908.45/297.04	     , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
908.45/297.04	     , proper(0()) -> ok(0())
908.45/297.04	     , proper(s(X)) -> s(proper(X))
908.45/297.04	     , proper(sieve(X)) -> sieve(proper(X))
908.45/297.04	     , proper(nats(X)) -> nats(proper(X))
908.45/297.04	     , proper(zprimes()) -> ok(zprimes())
908.45/297.04	     , top(mark(X)) -> top(proper(X))
908.45/297.04	     , top(ok(X)) -> top(active(X)) }
908.45/297.04	   Obligation:
908.45/297.04	     runtime complexity
908.45/297.04	   Answer:
908.45/297.04	     MAYBE
908.45/297.04	   
908.45/297.04	   Consider the dependency graph:
908.45/297.04	   
908.45/297.04	     1: active^#(filter(X1, X2, X3)) ->
908.45/297.04	        c_1(filter^#(X1, X2, active(X3)))
908.45/297.04	        -->_1 filter^#(ok(X1), ok(X2), ok(X3)) ->
908.45/297.04	              c_17(filter^#(X1, X2, X3)) :17
908.45/297.04	        -->_1 filter^#(mark(X1), X2, X3) -> c_16(filter^#(X1, X2, X3)) :16
908.45/297.04	        -->_1 filter^#(X1, mark(X2), X3) -> c_15(filter^#(X1, X2, X3)) :15
908.45/297.05	        -->_1 filter^#(X1, X2, mark(X3)) -> c_14(filter^#(X1, X2, X3)) :14
908.45/297.05	     
908.45/297.05	     2: active^#(filter(X1, X2, X3)) ->
908.45/297.05	        c_2(filter^#(X1, active(X2), X3))
908.45/297.05	        -->_1 filter^#(ok(X1), ok(X2), ok(X3)) ->
908.45/297.05	              c_17(filter^#(X1, X2, X3)) :17
908.45/297.05	        -->_1 filter^#(mark(X1), X2, X3) -> c_16(filter^#(X1, X2, X3)) :16
908.45/297.05	        -->_1 filter^#(X1, mark(X2), X3) -> c_15(filter^#(X1, X2, X3)) :15
908.45/297.05	        -->_1 filter^#(X1, X2, mark(X3)) -> c_14(filter^#(X1, X2, X3)) :14
908.45/297.05	     
908.45/297.05	     3: active^#(filter(X1, X2, X3)) ->
908.45/297.05	        c_3(filter^#(active(X1), X2, X3))
908.45/297.05	        -->_1 filter^#(ok(X1), ok(X2), ok(X3)) ->
908.45/297.05	              c_17(filter^#(X1, X2, X3)) :17
908.45/297.05	        -->_1 filter^#(mark(X1), X2, X3) -> c_16(filter^#(X1, X2, X3)) :16
908.45/297.05	        -->_1 filter^#(X1, mark(X2), X3) -> c_15(filter^#(X1, X2, X3)) :15
908.45/297.05	        -->_1 filter^#(X1, X2, mark(X3)) -> c_14(filter^#(X1, X2, X3)) :14
908.45/297.05	     
908.45/297.05	     4: active^#(filter(cons(X, Y), 0(), M)) ->
908.45/297.05	        c_4(cons^#(0(), filter(Y, M, M)))
908.45/297.05	     
908.45/297.05	     5: active^#(filter(cons(X, Y), s(N), M)) ->
908.45/297.05	        c_5(cons^#(X, filter(Y, N, M)))
908.45/297.05	        -->_1 cons^#(ok(X1), ok(X2)) -> c_19(cons^#(X1, X2)) :19
908.45/297.05	        -->_1 cons^#(mark(X1), X2) -> c_18(cons^#(X1, X2)) :18
908.45/297.05	     
908.45/297.05	     6: active^#(cons(X1, X2)) -> c_6(cons^#(active(X1), X2))
908.45/297.05	        -->_1 cons^#(ok(X1), ok(X2)) -> c_19(cons^#(X1, X2)) :19
908.45/297.05	        -->_1 cons^#(mark(X1), X2) -> c_18(cons^#(X1, X2)) :18
908.45/297.05	     
908.45/297.05	     7: active^#(s(X)) -> c_7(s^#(active(X)))
908.45/297.05	        -->_1 s^#(ok(X)) -> c_21(s^#(X)) :21
908.45/297.05	        -->_1 s^#(mark(X)) -> c_20(s^#(X)) :20
908.45/297.05	     
908.45/297.05	     8: active^#(sieve(X)) -> c_8(sieve^#(active(X)))
908.45/297.05	        -->_1 sieve^#(ok(X)) -> c_23(sieve^#(X)) :23
908.45/297.05	        -->_1 sieve^#(mark(X)) -> c_22(sieve^#(X)) :22
908.45/297.05	     
908.45/297.05	     9: active^#(sieve(cons(0(), Y))) -> c_9(cons^#(0(), sieve(Y)))
908.45/297.05	     
908.45/297.05	     10: active^#(sieve(cons(s(N), Y))) ->
908.45/297.05	         c_10(cons^#(s(N), sieve(filter(Y, N, N))))
908.45/297.05	        -->_1 cons^#(ok(X1), ok(X2)) -> c_19(cons^#(X1, X2)) :19
908.45/297.05	        -->_1 cons^#(mark(X1), X2) -> c_18(cons^#(X1, X2)) :18
908.45/297.05	     
908.45/297.05	     11: active^#(nats(N)) -> c_11(cons^#(N, nats(s(N))))
908.45/297.05	        -->_1 cons^#(ok(X1), ok(X2)) -> c_19(cons^#(X1, X2)) :19
908.45/297.05	        -->_1 cons^#(mark(X1), X2) -> c_18(cons^#(X1, X2)) :18
908.45/297.05	     
908.45/297.05	     12: active^#(nats(X)) -> c_12(nats^#(active(X)))
908.45/297.05	        -->_1 nats^#(ok(X)) -> c_25(nats^#(X)) :25
908.45/297.05	        -->_1 nats^#(mark(X)) -> c_24(nats^#(X)) :24
908.45/297.05	     
908.45/297.05	     13: active^#(zprimes()) -> c_13(sieve^#(nats(s(s(0())))))
908.45/297.05	     
908.45/297.05	     14: filter^#(X1, X2, mark(X3)) -> c_14(filter^#(X1, X2, X3))
908.45/297.05	        -->_1 filter^#(ok(X1), ok(X2), ok(X3)) ->
908.45/297.05	              c_17(filter^#(X1, X2, X3)) :17
908.45/297.05	        -->_1 filter^#(mark(X1), X2, X3) -> c_16(filter^#(X1, X2, X3)) :16
908.45/297.05	        -->_1 filter^#(X1, mark(X2), X3) -> c_15(filter^#(X1, X2, X3)) :15
908.45/297.05	        -->_1 filter^#(X1, X2, mark(X3)) -> c_14(filter^#(X1, X2, X3)) :14
908.45/297.05	     
908.45/297.05	     15: filter^#(X1, mark(X2), X3) -> c_15(filter^#(X1, X2, X3))
908.45/297.05	        -->_1 filter^#(ok(X1), ok(X2), ok(X3)) ->
908.45/297.05	              c_17(filter^#(X1, X2, X3)) :17
908.45/297.05	        -->_1 filter^#(mark(X1), X2, X3) -> c_16(filter^#(X1, X2, X3)) :16
908.45/297.05	        -->_1 filter^#(X1, mark(X2), X3) -> c_15(filter^#(X1, X2, X3)) :15
908.45/297.05	        -->_1 filter^#(X1, X2, mark(X3)) -> c_14(filter^#(X1, X2, X3)) :14
908.45/297.05	     
908.45/297.05	     16: filter^#(mark(X1), X2, X3) -> c_16(filter^#(X1, X2, X3))
908.45/297.05	        -->_1 filter^#(ok(X1), ok(X2), ok(X3)) ->
908.45/297.05	              c_17(filter^#(X1, X2, X3)) :17
908.45/297.05	        -->_1 filter^#(mark(X1), X2, X3) -> c_16(filter^#(X1, X2, X3)) :16
908.45/297.05	        -->_1 filter^#(X1, mark(X2), X3) -> c_15(filter^#(X1, X2, X3)) :15
908.45/297.05	        -->_1 filter^#(X1, X2, mark(X3)) -> c_14(filter^#(X1, X2, X3)) :14
908.45/297.05	     
908.45/297.05	     17: filter^#(ok(X1), ok(X2), ok(X3)) -> c_17(filter^#(X1, X2, X3))
908.45/297.05	        -->_1 filter^#(ok(X1), ok(X2), ok(X3)) ->
908.45/297.05	              c_17(filter^#(X1, X2, X3)) :17
908.45/297.05	        -->_1 filter^#(mark(X1), X2, X3) -> c_16(filter^#(X1, X2, X3)) :16
908.45/297.05	        -->_1 filter^#(X1, mark(X2), X3) -> c_15(filter^#(X1, X2, X3)) :15
908.45/297.05	        -->_1 filter^#(X1, X2, mark(X3)) -> c_14(filter^#(X1, X2, X3)) :14
908.45/297.05	     
908.45/297.05	     18: cons^#(mark(X1), X2) -> c_18(cons^#(X1, X2))
908.45/297.05	        -->_1 cons^#(ok(X1), ok(X2)) -> c_19(cons^#(X1, X2)) :19
908.45/297.05	        -->_1 cons^#(mark(X1), X2) -> c_18(cons^#(X1, X2)) :18
908.45/297.05	     
908.45/297.05	     19: cons^#(ok(X1), ok(X2)) -> c_19(cons^#(X1, X2))
908.45/297.05	        -->_1 cons^#(ok(X1), ok(X2)) -> c_19(cons^#(X1, X2)) :19
908.45/297.05	        -->_1 cons^#(mark(X1), X2) -> c_18(cons^#(X1, X2)) :18
908.45/297.05	     
908.45/297.05	     20: s^#(mark(X)) -> c_20(s^#(X))
908.45/297.05	        -->_1 s^#(ok(X)) -> c_21(s^#(X)) :21
908.45/297.05	        -->_1 s^#(mark(X)) -> c_20(s^#(X)) :20
908.45/297.05	     
908.45/297.05	     21: s^#(ok(X)) -> c_21(s^#(X))
908.45/297.05	        -->_1 s^#(ok(X)) -> c_21(s^#(X)) :21
908.45/297.05	        -->_1 s^#(mark(X)) -> c_20(s^#(X)) :20
908.45/297.05	     
908.45/297.05	     22: sieve^#(mark(X)) -> c_22(sieve^#(X))
908.45/297.05	        -->_1 sieve^#(ok(X)) -> c_23(sieve^#(X)) :23
908.45/297.05	        -->_1 sieve^#(mark(X)) -> c_22(sieve^#(X)) :22
908.45/297.05	     
908.45/297.05	     23: sieve^#(ok(X)) -> c_23(sieve^#(X))
908.45/297.05	        -->_1 sieve^#(ok(X)) -> c_23(sieve^#(X)) :23
908.45/297.05	        -->_1 sieve^#(mark(X)) -> c_22(sieve^#(X)) :22
908.45/297.05	     
908.45/297.05	     24: nats^#(mark(X)) -> c_24(nats^#(X))
908.45/297.05	        -->_1 nats^#(ok(X)) -> c_25(nats^#(X)) :25
908.45/297.05	        -->_1 nats^#(mark(X)) -> c_24(nats^#(X)) :24
908.45/297.05	     
908.45/297.05	     25: nats^#(ok(X)) -> c_25(nats^#(X))
908.45/297.05	        -->_1 nats^#(ok(X)) -> c_25(nats^#(X)) :25
908.45/297.05	        -->_1 nats^#(mark(X)) -> c_24(nats^#(X)) :24
908.45/297.05	     
908.45/297.05	     26: proper^#(filter(X1, X2, X3)) ->
908.45/297.05	         c_26(filter^#(proper(X1), proper(X2), proper(X3)))
908.45/297.05	        -->_1 filter^#(ok(X1), ok(X2), ok(X3)) ->
908.45/297.05	              c_17(filter^#(X1, X2, X3)) :17
908.45/297.05	        -->_1 filter^#(mark(X1), X2, X3) -> c_16(filter^#(X1, X2, X3)) :16
908.45/297.05	        -->_1 filter^#(X1, mark(X2), X3) -> c_15(filter^#(X1, X2, X3)) :15
908.45/297.05	        -->_1 filter^#(X1, X2, mark(X3)) -> c_14(filter^#(X1, X2, X3)) :14
908.45/297.05	     
908.45/297.05	     27: proper^#(cons(X1, X2)) -> c_27(cons^#(proper(X1), proper(X2)))
908.45/297.05	        -->_1 cons^#(ok(X1), ok(X2)) -> c_19(cons^#(X1, X2)) :19
908.45/297.05	        -->_1 cons^#(mark(X1), X2) -> c_18(cons^#(X1, X2)) :18
908.45/297.05	     
908.45/297.05	     28: proper^#(0()) -> c_28()
908.45/297.05	     
908.45/297.05	     29: proper^#(s(X)) -> c_29(s^#(proper(X)))
908.45/297.05	        -->_1 s^#(ok(X)) -> c_21(s^#(X)) :21
908.45/297.05	        -->_1 s^#(mark(X)) -> c_20(s^#(X)) :20
908.45/297.05	     
908.45/297.05	     30: proper^#(sieve(X)) -> c_30(sieve^#(proper(X)))
908.45/297.05	        -->_1 sieve^#(ok(X)) -> c_23(sieve^#(X)) :23
908.45/297.05	        -->_1 sieve^#(mark(X)) -> c_22(sieve^#(X)) :22
908.45/297.05	     
908.45/297.05	     31: proper^#(nats(X)) -> c_31(nats^#(proper(X)))
908.45/297.05	        -->_1 nats^#(ok(X)) -> c_25(nats^#(X)) :25
908.45/297.05	        -->_1 nats^#(mark(X)) -> c_24(nats^#(X)) :24
908.45/297.05	     
908.45/297.05	     32: proper^#(zprimes()) -> c_32()
908.45/297.05	     
908.45/297.05	     33: top^#(mark(X)) -> c_33(top^#(proper(X)))
908.45/297.05	        -->_1 top^#(ok(X)) -> c_34(top^#(active(X))) :34
908.45/297.05	        -->_1 top^#(mark(X)) -> c_33(top^#(proper(X))) :33
908.45/297.05	     
908.45/297.05	     34: top^#(ok(X)) -> c_34(top^#(active(X)))
908.45/297.05	        -->_1 top^#(ok(X)) -> c_34(top^#(active(X))) :34
908.45/297.05	        -->_1 top^#(mark(X)) -> c_33(top^#(proper(X))) :33
908.45/297.05	     
908.45/297.05	   
908.45/297.05	   Only the nodes {13,14,17,16,15,18,19,20,21,22,23,24,25,28,32,33,34}
908.45/297.05	   are reachable from nodes
908.45/297.05	   {13,14,15,16,17,18,19,20,21,22,23,24,25,28,32,33,34} that start
908.45/297.05	   derivation from marked basic terms. The nodes not reachable are
908.45/297.05	   removed from the problem.
908.45/297.05	   
908.45/297.05	   We are left with following problem, upon which TcT provides the
908.45/297.05	   certificate MAYBE.
908.45/297.05	   
908.45/297.05	   Strict DPs:
908.45/297.05	     { active^#(zprimes()) -> c_13(sieve^#(nats(s(s(0())))))
908.45/297.05	     , filter^#(X1, X2, mark(X3)) -> c_14(filter^#(X1, X2, X3))
908.45/297.05	     , filter^#(X1, mark(X2), X3) -> c_15(filter^#(X1, X2, X3))
908.45/297.05	     , filter^#(mark(X1), X2, X3) -> c_16(filter^#(X1, X2, X3))
908.45/297.05	     , filter^#(ok(X1), ok(X2), ok(X3)) -> c_17(filter^#(X1, X2, X3))
908.45/297.05	     , cons^#(mark(X1), X2) -> c_18(cons^#(X1, X2))
908.45/297.05	     , cons^#(ok(X1), ok(X2)) -> c_19(cons^#(X1, X2))
908.45/297.05	     , s^#(mark(X)) -> c_20(s^#(X))
908.45/297.05	     , s^#(ok(X)) -> c_21(s^#(X))
908.45/297.05	     , sieve^#(mark(X)) -> c_22(sieve^#(X))
908.45/297.05	     , sieve^#(ok(X)) -> c_23(sieve^#(X))
908.45/297.05	     , nats^#(mark(X)) -> c_24(nats^#(X))
908.45/297.05	     , nats^#(ok(X)) -> c_25(nats^#(X))
908.45/297.05	     , proper^#(0()) -> c_28()
908.45/297.05	     , proper^#(zprimes()) -> c_32()
908.45/297.05	     , top^#(mark(X)) -> c_33(top^#(proper(X)))
908.45/297.05	     , top^#(ok(X)) -> c_34(top^#(active(X))) }
908.45/297.05	   Strict Trs:
908.45/297.05	     { active(filter(X1, X2, X3)) -> filter(X1, X2, active(X3))
908.45/297.05	     , active(filter(X1, X2, X3)) -> filter(X1, active(X2), X3)
908.45/297.05	     , active(filter(X1, X2, X3)) -> filter(active(X1), X2, X3)
908.45/297.05	     , active(filter(cons(X, Y), 0(), M)) ->
908.45/297.05	       mark(cons(0(), filter(Y, M, M)))
908.45/297.05	     , active(filter(cons(X, Y), s(N), M)) ->
908.45/297.05	       mark(cons(X, filter(Y, N, M)))
908.45/297.05	     , active(cons(X1, X2)) -> cons(active(X1), X2)
908.45/297.05	     , active(s(X)) -> s(active(X))
908.45/297.05	     , active(sieve(X)) -> sieve(active(X))
908.45/297.05	     , active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y)))
908.45/297.05	     , active(sieve(cons(s(N), Y))) ->
908.45/297.05	       mark(cons(s(N), sieve(filter(Y, N, N))))
908.45/297.05	     , active(nats(N)) -> mark(cons(N, nats(s(N))))
908.45/297.05	     , active(nats(X)) -> nats(active(X))
908.45/297.05	     , active(zprimes()) -> mark(sieve(nats(s(s(0())))))
908.45/297.05	     , filter(X1, X2, mark(X3)) -> mark(filter(X1, X2, X3))
908.45/297.05	     , filter(X1, mark(X2), X3) -> mark(filter(X1, X2, X3))
908.45/297.05	     , filter(mark(X1), X2, X3) -> mark(filter(X1, X2, X3))
908.45/297.05	     , filter(ok(X1), ok(X2), ok(X3)) -> ok(filter(X1, X2, X3))
908.45/297.05	     , cons(mark(X1), X2) -> mark(cons(X1, X2))
908.45/297.05	     , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
908.45/297.05	     , s(mark(X)) -> mark(s(X))
908.45/297.05	     , s(ok(X)) -> ok(s(X))
908.45/297.05	     , sieve(mark(X)) -> mark(sieve(X))
908.45/297.05	     , sieve(ok(X)) -> ok(sieve(X))
908.45/297.05	     , nats(mark(X)) -> mark(nats(X))
908.45/297.05	     , nats(ok(X)) -> ok(nats(X))
908.45/297.05	     , proper(filter(X1, X2, X3)) ->
908.45/297.05	       filter(proper(X1), proper(X2), proper(X3))
908.45/297.05	     , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
908.45/297.05	     , proper(0()) -> ok(0())
908.45/297.05	     , proper(s(X)) -> s(proper(X))
908.45/297.05	     , proper(sieve(X)) -> sieve(proper(X))
908.45/297.05	     , proper(nats(X)) -> nats(proper(X))
908.45/297.05	     , proper(zprimes()) -> ok(zprimes())
908.45/297.05	     , top(mark(X)) -> top(proper(X))
908.45/297.05	     , top(ok(X)) -> top(active(X)) }
908.45/297.05	   Obligation:
908.45/297.05	     runtime complexity
908.45/297.05	   Answer:
908.45/297.05	     MAYBE
908.45/297.05	   
908.45/297.05	   We estimate the number of application of {1,14,15} by applications
908.45/297.05	   of Pre({1,14,15}) = {}. Here rules are labeled as follows:
908.45/297.05	   
908.45/297.05	     DPs:
908.45/297.05	       { 1: active^#(zprimes()) -> c_13(sieve^#(nats(s(s(0())))))
908.45/297.05	       , 2: filter^#(X1, X2, mark(X3)) -> c_14(filter^#(X1, X2, X3))
908.45/297.05	       , 3: filter^#(X1, mark(X2), X3) -> c_15(filter^#(X1, X2, X3))
908.45/297.05	       , 4: filter^#(mark(X1), X2, X3) -> c_16(filter^#(X1, X2, X3))
908.45/297.05	       , 5: filter^#(ok(X1), ok(X2), ok(X3)) -> c_17(filter^#(X1, X2, X3))
908.45/297.05	       , 6: cons^#(mark(X1), X2) -> c_18(cons^#(X1, X2))
908.45/297.05	       , 7: cons^#(ok(X1), ok(X2)) -> c_19(cons^#(X1, X2))
908.45/297.05	       , 8: s^#(mark(X)) -> c_20(s^#(X))
908.45/297.05	       , 9: s^#(ok(X)) -> c_21(s^#(X))
908.45/297.05	       , 10: sieve^#(mark(X)) -> c_22(sieve^#(X))
908.45/297.05	       , 11: sieve^#(ok(X)) -> c_23(sieve^#(X))
908.45/297.05	       , 12: nats^#(mark(X)) -> c_24(nats^#(X))
908.45/297.05	       , 13: nats^#(ok(X)) -> c_25(nats^#(X))
908.45/297.05	       , 14: proper^#(0()) -> c_28()
908.45/297.05	       , 15: proper^#(zprimes()) -> c_32()
908.45/297.05	       , 16: top^#(mark(X)) -> c_33(top^#(proper(X)))
908.45/297.05	       , 17: top^#(ok(X)) -> c_34(top^#(active(X))) }
908.45/297.05	   
908.45/297.05	   We are left with following problem, upon which TcT provides the
908.45/297.05	   certificate MAYBE.
908.45/297.05	   
908.45/297.05	   Strict DPs:
908.45/297.05	     { filter^#(X1, X2, mark(X3)) -> c_14(filter^#(X1, X2, X3))
908.45/297.05	     , filter^#(X1, mark(X2), X3) -> c_15(filter^#(X1, X2, X3))
908.45/297.05	     , filter^#(mark(X1), X2, X3) -> c_16(filter^#(X1, X2, X3))
908.45/297.05	     , filter^#(ok(X1), ok(X2), ok(X3)) -> c_17(filter^#(X1, X2, X3))
908.45/297.05	     , cons^#(mark(X1), X2) -> c_18(cons^#(X1, X2))
908.45/297.05	     , cons^#(ok(X1), ok(X2)) -> c_19(cons^#(X1, X2))
908.45/297.05	     , s^#(mark(X)) -> c_20(s^#(X))
908.45/297.05	     , s^#(ok(X)) -> c_21(s^#(X))
908.45/297.05	     , sieve^#(mark(X)) -> c_22(sieve^#(X))
908.45/297.05	     , sieve^#(ok(X)) -> c_23(sieve^#(X))
908.45/297.05	     , nats^#(mark(X)) -> c_24(nats^#(X))
908.45/297.05	     , nats^#(ok(X)) -> c_25(nats^#(X))
908.45/297.05	     , top^#(mark(X)) -> c_33(top^#(proper(X)))
908.45/297.05	     , top^#(ok(X)) -> c_34(top^#(active(X))) }
908.45/297.05	   Strict Trs:
908.45/297.05	     { active(filter(X1, X2, X3)) -> filter(X1, X2, active(X3))
908.45/297.05	     , active(filter(X1, X2, X3)) -> filter(X1, active(X2), X3)
908.45/297.05	     , active(filter(X1, X2, X3)) -> filter(active(X1), X2, X3)
908.45/297.05	     , active(filter(cons(X, Y), 0(), M)) ->
908.45/297.05	       mark(cons(0(), filter(Y, M, M)))
908.45/297.05	     , active(filter(cons(X, Y), s(N), M)) ->
908.45/297.05	       mark(cons(X, filter(Y, N, M)))
908.45/297.05	     , active(cons(X1, X2)) -> cons(active(X1), X2)
908.45/297.05	     , active(s(X)) -> s(active(X))
908.45/297.05	     , active(sieve(X)) -> sieve(active(X))
908.45/297.05	     , active(sieve(cons(0(), Y))) -> mark(cons(0(), sieve(Y)))
908.45/297.05	     , active(sieve(cons(s(N), Y))) ->
908.45/297.05	       mark(cons(s(N), sieve(filter(Y, N, N))))
908.45/297.05	     , active(nats(N)) -> mark(cons(N, nats(s(N))))
908.45/297.05	     , active(nats(X)) -> nats(active(X))
908.45/297.05	     , active(zprimes()) -> mark(sieve(nats(s(s(0())))))
908.45/297.05	     , filter(X1, X2, mark(X3)) -> mark(filter(X1, X2, X3))
908.45/297.05	     , filter(X1, mark(X2), X3) -> mark(filter(X1, X2, X3))
908.45/297.05	     , filter(mark(X1), X2, X3) -> mark(filter(X1, X2, X3))
908.45/297.05	     , filter(ok(X1), ok(X2), ok(X3)) -> ok(filter(X1, X2, X3))
908.45/297.05	     , cons(mark(X1), X2) -> mark(cons(X1, X2))
908.45/297.05	     , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
908.45/297.05	     , s(mark(X)) -> mark(s(X))
908.45/297.05	     , s(ok(X)) -> ok(s(X))
908.45/297.05	     , sieve(mark(X)) -> mark(sieve(X))
908.45/297.05	     , sieve(ok(X)) -> ok(sieve(X))
908.45/297.05	     , nats(mark(X)) -> mark(nats(X))
908.45/297.05	     , nats(ok(X)) -> ok(nats(X))
908.45/297.05	     , proper(filter(X1, X2, X3)) ->
908.45/297.05	       filter(proper(X1), proper(X2), proper(X3))
908.45/297.05	     , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
908.45/297.05	     , proper(0()) -> ok(0())
908.45/297.05	     , proper(s(X)) -> s(proper(X))
908.45/297.05	     , proper(sieve(X)) -> sieve(proper(X))
908.45/297.05	     , proper(nats(X)) -> nats(proper(X))
908.45/297.05	     , proper(zprimes()) -> ok(zprimes())
908.45/297.05	     , top(mark(X)) -> top(proper(X))
908.45/297.05	     , top(ok(X)) -> top(active(X)) }
908.45/297.05	   Weak DPs:
908.45/297.05	     { active^#(zprimes()) -> c_13(sieve^#(nats(s(s(0())))))
908.45/297.05	     , proper^#(0()) -> c_28()
908.45/297.05	     , proper^#(zprimes()) -> c_32() }
908.45/297.05	   Obligation:
908.45/297.05	     runtime complexity
908.45/297.05	   Answer:
908.45/297.05	     MAYBE
908.45/297.05	   
908.45/297.05	   Empty strict component of the problem is NOT empty.
908.45/297.05	
908.45/297.05	
908.45/297.05	Arrrr..
908.69/297.29	EOF