MAYBE TRS: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} DP: Strict: { mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> sieve#(mark(X)), mark#(sieve(X)) -> active#(sieve(mark(X))), mark#(from(X)) -> mark#(X), mark#(from(X)) -> from#(mark(X)), mark#(from(X)) -> active#(from(mark(X))), mark#(s(X)) -> mark#(X), mark#(s(X)) -> s#(mark(X)), mark#(s(X)) -> active#(s(mark(X))), mark#(0()) -> active#(0()), mark#(primes()) -> active#(primes()), mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), mark#(cons(X1, X2)) -> cons#(mark(X1), X2), mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X))), mark#(head(X)) -> head#(mark(X)), mark#(tail(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X))), mark#(tail(X)) -> tail#(mark(X)), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3), mark#(true()) -> active#(true()), mark#(false()) -> active#(false()), mark#(divides(X1, X2)) -> mark#(X1), mark#(divides(X1, X2)) -> mark#(X2), mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2))), mark#(divides(X1, X2)) -> divides#(mark(X1), mark(X2)), mark#(filter(X1, X2)) -> mark#(X1), mark#(filter(X1, X2)) -> mark#(X2), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), mark#(filter(X1, X2)) -> filter#(mark(X1), mark(X2)), sieve#(mark(X)) -> sieve#(X), sieve#(active(X)) -> sieve#(X), from#(mark(X)) -> from#(X), from#(active(X)) -> from#(X), s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X), active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), active#(sieve(cons(X, Y))) -> sieve#(Y), active#(sieve(cons(X, Y))) -> cons#(X, filter(X, sieve(Y))), active#(sieve(cons(X, Y))) -> filter#(X, sieve(Y)), active#(from(X)) -> mark#(cons(X, from(s(X)))), active#(from(X)) -> from#(s(X)), active#(from(X)) -> s#(X), active#(from(X)) -> cons#(X, from(s(X))), active#(primes()) -> mark#(sieve(from(s(s(0()))))), active#(primes()) -> sieve#(from(s(s(0())))), active#(primes()) -> from#(s(s(0()))), active#(primes()) -> s#(s(0())), active#(primes()) -> s#(0()), active#(head(cons(X, Y))) -> mark#(X), active#(tail(cons(X, Y))) -> mark#(Y), active#(if(true(), X, Y)) -> mark#(X), active#(if(false(), X, Y)) -> mark#(Y), active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), active#(filter(s(s(X)), cons(Y, Z))) -> sieve#(Y), active#(filter(s(s(X)), cons(Y, Z))) -> cons#(Y, filter(X, sieve(Y))), active#(filter(s(s(X)), cons(Y, Z))) -> if#(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))), active#(filter(s(s(X)), cons(Y, Z))) -> divides#(s(s(X)), Y), active#(filter(s(s(X)), cons(Y, Z))) -> filter#(X, sieve(Y)), active#(filter(s(s(X)), cons(Y, Z))) -> filter#(s(s(X)), Z), cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2), head#(mark(X)) -> head#(X), head#(active(X)) -> head#(X), tail#(mark(X)) -> tail#(X), tail#(active(X)) -> tail#(X), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(active(X1), X2, X3) -> if#(X1, X2, X3), divides#(X1, mark(X2)) -> divides#(X1, X2), divides#(X1, active(X2)) -> divides#(X1, X2), divides#(mark(X1), X2) -> divides#(X1, X2), divides#(active(X1), X2) -> divides#(X1, X2), filter#(X1, mark(X2)) -> filter#(X1, X2), filter#(X1, active(X2)) -> filter#(X1, X2), filter#(mark(X1), X2) -> filter#(X1, X2), filter#(active(X1), X2) -> filter#(X1, X2)} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} EDG: { (active#(filter(s(s(X)), cons(Y, Z))) -> cons#(Y, filter(X, sieve(Y))), cons#(active(X1), X2) -> cons#(X1, X2)) (active#(filter(s(s(X)), cons(Y, Z))) -> cons#(Y, filter(X, sieve(Y))), cons#(mark(X1), X2) -> cons#(X1, X2)) (active#(filter(s(s(X)), cons(Y, Z))) -> cons#(Y, filter(X, sieve(Y))), cons#(X1, active(X2)) -> cons#(X1, X2)) (active#(filter(s(s(X)), cons(Y, Z))) -> cons#(Y, filter(X, sieve(Y))), cons#(X1, mark(X2)) -> cons#(X1, X2)) (mark#(primes()) -> active#(primes()), active#(primes()) -> s#(0())) (mark#(primes()) -> active#(primes()), active#(primes()) -> s#(s(0()))) (mark#(primes()) -> active#(primes()), active#(primes()) -> from#(s(s(0())))) (mark#(primes()) -> active#(primes()), active#(primes()) -> sieve#(from(s(s(0()))))) (mark#(primes()) -> active#(primes()), active#(primes()) -> mark#(sieve(from(s(s(0())))))) (mark#(sieve(X)) -> sieve#(mark(X)), sieve#(active(X)) -> sieve#(X)) (mark#(sieve(X)) -> sieve#(mark(X)), sieve#(mark(X)) -> sieve#(X)) (mark#(s(X)) -> s#(mark(X)), s#(active(X)) -> s#(X)) (mark#(s(X)) -> s#(mark(X)), s#(mark(X)) -> s#(X)) (mark#(tail(X)) -> tail#(mark(X)), tail#(active(X)) -> tail#(X)) (mark#(tail(X)) -> tail#(mark(X)), tail#(mark(X)) -> tail#(X)) (active#(sieve(cons(X, Y))) -> sieve#(Y), sieve#(active(X)) -> sieve#(X)) (active#(sieve(cons(X, Y))) -> sieve#(Y), sieve#(mark(X)) -> sieve#(X)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(filter(X1, X2)) -> filter#(mark(X1), mark(X2))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(filter(X1, X2)) -> mark#(X2)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(filter(X1, X2)) -> mark#(X1)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(divides(X1, X2)) -> divides#(mark(X1), mark(X2))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2)))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(divides(X1, X2)) -> mark#(X2)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(divides(X1, X2)) -> mark#(X1)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(false()) -> active#(false())) (active#(if(false(), X, Y)) -> mark#(Y), mark#(true()) -> active#(true())) (active#(if(false(), X, Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(tail(X)) -> tail#(mark(X))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(tail(X)) -> active#(tail(mark(X)))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(tail(X)) -> mark#(X)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(head(X)) -> head#(mark(X))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(head(X)) -> active#(head(mark(X)))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(head(X)) -> mark#(X)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(cons(X1, X2)) -> mark#(X1)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(primes()) -> active#(primes())) (active#(if(false(), X, Y)) -> mark#(Y), mark#(0()) -> active#(0())) (active#(if(false(), X, Y)) -> mark#(Y), mark#(s(X)) -> active#(s(mark(X)))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(s(X)) -> s#(mark(X))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(s(X)) -> mark#(X)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(from(X)) -> active#(from(mark(X)))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(from(X)) -> from#(mark(X))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(from(X)) -> mark#(X)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(sieve(X)) -> sieve#(mark(X))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(sieve(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(filter(s(s(X)), cons(Y, Z))) -> filter#(s(s(X)), Z)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(filter(s(s(X)), cons(Y, Z))) -> filter#(X, sieve(Y))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(filter(s(s(X)), cons(Y, Z))) -> divides#(s(s(X)), Y)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(filter(s(s(X)), cons(Y, Z))) -> if#(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(filter(s(s(X)), cons(Y, Z))) -> cons#(Y, filter(X, sieve(Y)))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(filter(s(s(X)), cons(Y, Z))) -> sieve#(Y)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(tail(cons(X, Y))) -> mark#(Y)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(head(cons(X, Y))) -> mark#(X)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(from(X)) -> cons#(X, from(s(X)))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(from(X)) -> s#(X)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(from(X)) -> from#(s(X))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(from(X)) -> mark#(cons(X, from(s(X))))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(sieve(cons(X, Y))) -> filter#(X, sieve(Y))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(sieve(cons(X, Y))) -> cons#(X, filter(X, sieve(Y)))) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(sieve(cons(X, Y))) -> sieve#(Y)) (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y))))) (mark#(filter(X1, X2)) -> filter#(mark(X1), mark(X2)), filter#(active(X1), X2) -> filter#(X1, X2)) (mark#(filter(X1, X2)) -> filter#(mark(X1), mark(X2)), filter#(mark(X1), X2) -> filter#(X1, X2)) (mark#(filter(X1, X2)) -> filter#(mark(X1), mark(X2)), filter#(X1, active(X2)) -> filter#(X1, X2)) (mark#(filter(X1, X2)) -> filter#(mark(X1), mark(X2)), filter#(X1, mark(X2)) -> filter#(X1, X2)) (active#(filter(s(s(X)), cons(Y, Z))) -> filter#(X, sieve(Y)), filter#(active(X1), X2) -> filter#(X1, X2)) (active#(filter(s(s(X)), cons(Y, Z))) -> filter#(X, sieve(Y)), filter#(mark(X1), X2) -> filter#(X1, X2)) (active#(filter(s(s(X)), cons(Y, Z))) -> filter#(X, sieve(Y)), filter#(X1, active(X2)) -> filter#(X1, X2)) (active#(filter(s(s(X)), cons(Y, Z))) -> filter#(X, sieve(Y)), filter#(X1, mark(X2)) -> filter#(X1, X2)) (mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3), if#(active(X1), X2, X3) -> if#(X1, X2, X3)) (mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(active(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(active(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(active(X1), X2, X3) -> if#(X1, X2, X3), if#(active(X1), X2, X3) -> if#(X1, X2, X3)) (if#(active(X1), X2, X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(active(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(active(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(active(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(active(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(filter(X1, X2)) -> filter#(mark(X1), mark(X2))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(filter(X1, X2)) -> mark#(X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(filter(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(divides(X1, X2)) -> divides#(mark(X1), mark(X2))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(divides(X1, X2)) -> mark#(X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(divides(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(false()) -> active#(false())) (mark#(cons(X1, X2)) -> mark#(X1), mark#(true()) -> active#(true())) (mark#(cons(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(tail(X)) -> tail#(mark(X))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(tail(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(head(X)) -> head#(mark(X))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(head(X)) -> active#(head(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(head(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(primes()) -> active#(primes())) (mark#(cons(X1, X2)) -> mark#(X1), mark#(0()) -> active#(0())) (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> s#(mark(X))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> from#(mark(X))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sieve(X)) -> sieve#(mark(X))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sieve(X)) -> mark#(X)) (mark#(divides(X1, X2)) -> mark#(X1), mark#(filter(X1, X2)) -> filter#(mark(X1), mark(X2))) (mark#(divides(X1, X2)) -> mark#(X1), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (mark#(divides(X1, X2)) -> mark#(X1), mark#(filter(X1, X2)) -> mark#(X2)) (mark#(divides(X1, X2)) -> mark#(X1), mark#(filter(X1, X2)) -> mark#(X1)) (mark#(divides(X1, X2)) -> mark#(X1), mark#(divides(X1, X2)) -> divides#(mark(X1), mark(X2))) (mark#(divides(X1, X2)) -> mark#(X1), mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2)))) (mark#(divides(X1, X2)) -> mark#(X1), mark#(divides(X1, X2)) -> mark#(X2)) (mark#(divides(X1, X2)) -> mark#(X1), mark#(divides(X1, X2)) -> mark#(X1)) (mark#(divides(X1, X2)) -> mark#(X1), mark#(false()) -> active#(false())) (mark#(divides(X1, X2)) -> mark#(X1), mark#(true()) -> active#(true())) (mark#(divides(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (mark#(divides(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(divides(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(divides(X1, X2)) -> mark#(X1), mark#(tail(X)) -> tail#(mark(X))) (mark#(divides(X1, X2)) -> mark#(X1), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(divides(X1, X2)) -> mark#(X1), mark#(tail(X)) -> mark#(X)) (mark#(divides(X1, X2)) -> mark#(X1), mark#(head(X)) -> head#(mark(X))) (mark#(divides(X1, X2)) -> mark#(X1), mark#(head(X)) -> active#(head(mark(X)))) (mark#(divides(X1, X2)) -> mark#(X1), mark#(head(X)) -> mark#(X)) (mark#(divides(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(divides(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(divides(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(divides(X1, X2)) -> mark#(X1), mark#(primes()) -> active#(primes())) (mark#(divides(X1, X2)) -> mark#(X1), mark#(0()) -> active#(0())) (mark#(divides(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(mark(X)))) (mark#(divides(X1, X2)) -> mark#(X1), mark#(s(X)) -> s#(mark(X))) (mark#(divides(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(divides(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X)))) (mark#(divides(X1, X2)) -> mark#(X1), mark#(from(X)) -> from#(mark(X))) (mark#(divides(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X)) (mark#(divides(X1, X2)) -> mark#(X1), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(divides(X1, X2)) -> mark#(X1), mark#(sieve(X)) -> sieve#(mark(X))) (mark#(divides(X1, X2)) -> mark#(X1), mark#(sieve(X)) -> mark#(X)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)) (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)) (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (divides#(X1, mark(X2)) -> divides#(X1, X2), divides#(active(X1), X2) -> divides#(X1, X2)) (divides#(X1, mark(X2)) -> divides#(X1, X2), divides#(mark(X1), X2) -> divides#(X1, X2)) (divides#(X1, mark(X2)) -> divides#(X1, X2), divides#(X1, active(X2)) -> divides#(X1, X2)) (divides#(X1, mark(X2)) -> divides#(X1, X2), divides#(X1, mark(X2)) -> divides#(X1, X2)) (divides#(mark(X1), X2) -> divides#(X1, X2), divides#(active(X1), X2) -> divides#(X1, X2)) (divides#(mark(X1), X2) -> divides#(X1, X2), divides#(mark(X1), X2) -> divides#(X1, X2)) (divides#(mark(X1), X2) -> divides#(X1, X2), divides#(X1, active(X2)) -> divides#(X1, X2)) (divides#(mark(X1), X2) -> divides#(X1, X2), divides#(X1, mark(X2)) -> divides#(X1, X2)) (filter#(X1, mark(X2)) -> filter#(X1, X2), filter#(active(X1), X2) -> filter#(X1, X2)) (filter#(X1, mark(X2)) -> filter#(X1, X2), filter#(mark(X1), X2) -> filter#(X1, X2)) (filter#(X1, mark(X2)) -> filter#(X1, X2), filter#(X1, active(X2)) -> filter#(X1, X2)) (filter#(X1, mark(X2)) -> filter#(X1, X2), filter#(X1, mark(X2)) -> filter#(X1, X2)) (filter#(mark(X1), X2) -> filter#(X1, X2), filter#(active(X1), X2) -> filter#(X1, X2)) (filter#(mark(X1), X2) -> filter#(X1, X2), filter#(mark(X1), X2) -> filter#(X1, X2)) (filter#(mark(X1), X2) -> filter#(X1, X2), filter#(X1, active(X2)) -> filter#(X1, X2)) (filter#(mark(X1), X2) -> filter#(X1, X2), filter#(X1, mark(X2)) -> filter#(X1, X2)) (mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2))), active#(filter(s(s(X)), cons(Y, Z))) -> filter#(s(s(X)), Z)) (mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2))), active#(filter(s(s(X)), cons(Y, Z))) -> filter#(X, sieve(Y))) (mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2))), active#(filter(s(s(X)), cons(Y, Z))) -> divides#(s(s(X)), Y)) (mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2))), active#(filter(s(s(X)), cons(Y, Z))) -> if#(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) (mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2))), active#(filter(s(s(X)), cons(Y, Z))) -> cons#(Y, filter(X, sieve(Y)))) (mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2))), active#(filter(s(s(X)), cons(Y, Z))) -> sieve#(Y)) (mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2))), active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))))) (mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2))), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2))), active#(if(true(), X, Y)) -> mark#(X)) (mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2))), active#(tail(cons(X, Y))) -> mark#(Y)) (mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2))), active#(head(cons(X, Y))) -> mark#(X)) (mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2))), active#(from(X)) -> cons#(X, from(s(X)))) (mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2))), active#(from(X)) -> s#(X)) (mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2))), active#(from(X)) -> from#(s(X))) (mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2))), active#(from(X)) -> mark#(cons(X, from(s(X))))) (mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2))), active#(sieve(cons(X, Y))) -> filter#(X, sieve(Y))) (mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2))), active#(sieve(cons(X, Y))) -> cons#(X, filter(X, sieve(Y)))) (mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2))), active#(sieve(cons(X, Y))) -> sieve#(Y)) (mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2))), active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y))))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(filter(X1, X2)) -> filter#(mark(X1), mark(X2))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(filter(X1, X2)) -> mark#(X2)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(filter(X1, X2)) -> mark#(X1)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(divides(X1, X2)) -> divides#(mark(X1), mark(X2))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2)))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(divides(X1, X2)) -> mark#(X2)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(divides(X1, X2)) -> mark#(X1)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(tail(X)) -> tail#(mark(X))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(tail(X)) -> active#(tail(mark(X)))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(tail(X)) -> mark#(X)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(head(X)) -> head#(mark(X))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(head(X)) -> active#(head(mark(X)))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(head(X)) -> mark#(X)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(s(X)) -> active#(s(mark(X)))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(s(X)) -> s#(mark(X))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(s(X)) -> mark#(X)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(from(X)) -> active#(from(mark(X)))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(from(X)) -> from#(mark(X))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(from(X)) -> mark#(X)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(sieve(X)) -> sieve#(mark(X))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(sieve(X)) -> mark#(X)) (mark#(from(X)) -> mark#(X), mark#(filter(X1, X2)) -> filter#(mark(X1), mark(X2))) (mark#(from(X)) -> mark#(X), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (mark#(from(X)) -> mark#(X), mark#(filter(X1, X2)) -> mark#(X2)) (mark#(from(X)) -> mark#(X), mark#(filter(X1, X2)) -> mark#(X1)) (mark#(from(X)) -> mark#(X), mark#(divides(X1, X2)) -> divides#(mark(X1), mark(X2))) (mark#(from(X)) -> mark#(X), mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2)))) (mark#(from(X)) -> mark#(X), mark#(divides(X1, X2)) -> mark#(X2)) (mark#(from(X)) -> mark#(X), mark#(divides(X1, X2)) -> mark#(X1)) (mark#(from(X)) -> mark#(X), mark#(false()) -> active#(false())) (mark#(from(X)) -> mark#(X), mark#(true()) -> active#(true())) (mark#(from(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (mark#(from(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(from(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(from(X)) -> mark#(X), mark#(tail(X)) -> tail#(mark(X))) (mark#(from(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(from(X)) -> mark#(X), mark#(tail(X)) -> mark#(X)) (mark#(from(X)) -> mark#(X), mark#(head(X)) -> head#(mark(X))) (mark#(from(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(from(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(from(X)) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(from(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(from(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(from(X)) -> mark#(X), mark#(primes()) -> active#(primes())) (mark#(from(X)) -> mark#(X), mark#(0()) -> active#(0())) (mark#(from(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (mark#(from(X)) -> mark#(X), mark#(s(X)) -> s#(mark(X))) (mark#(from(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(from(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X)))) (mark#(from(X)) -> mark#(X), mark#(from(X)) -> from#(mark(X))) (mark#(from(X)) -> mark#(X), mark#(from(X)) -> mark#(X)) (mark#(from(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(from(X)) -> mark#(X), mark#(sieve(X)) -> sieve#(mark(X))) (mark#(from(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(filter(X1, X2)) -> filter#(mark(X1), mark(X2))) (mark#(head(X)) -> mark#(X), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (mark#(head(X)) -> mark#(X), mark#(filter(X1, X2)) -> mark#(X2)) (mark#(head(X)) -> mark#(X), mark#(filter(X1, X2)) -> mark#(X1)) (mark#(head(X)) -> mark#(X), mark#(divides(X1, X2)) -> divides#(mark(X1), mark(X2))) (mark#(head(X)) -> mark#(X), mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2)))) (mark#(head(X)) -> mark#(X), mark#(divides(X1, X2)) -> mark#(X2)) (mark#(head(X)) -> mark#(X), mark#(divides(X1, X2)) -> mark#(X1)) (mark#(head(X)) -> mark#(X), mark#(false()) -> active#(false())) (mark#(head(X)) -> mark#(X), mark#(true()) -> active#(true())) (mark#(head(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (mark#(head(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(head(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(head(X)) -> mark#(X), mark#(tail(X)) -> tail#(mark(X))) (mark#(head(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(head(X)) -> mark#(X), mark#(tail(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(head(X)) -> head#(mark(X))) (mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(head(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(head(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(head(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(head(X)) -> mark#(X), mark#(primes()) -> active#(primes())) (mark#(head(X)) -> mark#(X), mark#(0()) -> active#(0())) (mark#(head(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (mark#(head(X)) -> mark#(X), mark#(s(X)) -> s#(mark(X))) (mark#(head(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X)))) (mark#(head(X)) -> mark#(X), mark#(from(X)) -> from#(mark(X))) (mark#(head(X)) -> mark#(X), mark#(from(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(head(X)) -> mark#(X), mark#(sieve(X)) -> sieve#(mark(X))) (mark#(head(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X)) (sieve#(mark(X)) -> sieve#(X), sieve#(active(X)) -> sieve#(X)) (sieve#(mark(X)) -> sieve#(X), sieve#(mark(X)) -> sieve#(X)) (from#(mark(X)) -> from#(X), from#(active(X)) -> from#(X)) (from#(mark(X)) -> from#(X), from#(mark(X)) -> from#(X)) (s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X)) (s#(mark(X)) -> s#(X), s#(mark(X)) -> s#(X)) (active#(from(X)) -> s#(X), s#(active(X)) -> s#(X)) (active#(from(X)) -> s#(X), s#(mark(X)) -> s#(X)) (active#(if(true(), X, Y)) -> mark#(X), mark#(filter(X1, X2)) -> filter#(mark(X1), mark(X2))) (active#(if(true(), X, Y)) -> mark#(X), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (active#(if(true(), X, Y)) -> mark#(X), mark#(filter(X1, X2)) -> mark#(X2)) (active#(if(true(), X, Y)) -> mark#(X), mark#(filter(X1, X2)) -> mark#(X1)) (active#(if(true(), X, Y)) -> mark#(X), mark#(divides(X1, X2)) -> divides#(mark(X1), mark(X2))) (active#(if(true(), X, Y)) -> mark#(X), mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2)))) (active#(if(true(), X, Y)) -> mark#(X), mark#(divides(X1, X2)) -> mark#(X2)) (active#(if(true(), X, Y)) -> mark#(X), mark#(divides(X1, X2)) -> mark#(X1)) (active#(if(true(), X, Y)) -> mark#(X), mark#(false()) -> active#(false())) (active#(if(true(), X, Y)) -> mark#(X), mark#(true()) -> active#(true())) (active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(if(true(), X, Y)) -> mark#(X), mark#(tail(X)) -> tail#(mark(X))) (active#(if(true(), X, Y)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X)))) (active#(if(true(), X, Y)) -> mark#(X), mark#(tail(X)) -> mark#(X)) (active#(if(true(), X, Y)) -> mark#(X), mark#(head(X)) -> head#(mark(X))) (active#(if(true(), X, Y)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (active#(if(true(), X, Y)) -> mark#(X), mark#(head(X)) -> mark#(X)) (active#(if(true(), X, Y)) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (active#(if(true(), X, Y)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (active#(if(true(), X, Y)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (active#(if(true(), X, Y)) -> mark#(X), mark#(primes()) -> active#(primes())) (active#(if(true(), X, Y)) -> mark#(X), mark#(0()) -> active#(0())) (active#(if(true(), X, Y)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (active#(if(true(), X, Y)) -> mark#(X), mark#(s(X)) -> s#(mark(X))) (active#(if(true(), X, Y)) -> mark#(X), mark#(s(X)) -> mark#(X)) (active#(if(true(), X, Y)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X)))) (active#(if(true(), X, Y)) -> mark#(X), mark#(from(X)) -> from#(mark(X))) (active#(if(true(), X, Y)) -> mark#(X), mark#(from(X)) -> mark#(X)) (active#(if(true(), X, Y)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(if(true(), X, Y)) -> mark#(X), mark#(sieve(X)) -> sieve#(mark(X))) (active#(if(true(), X, Y)) -> mark#(X), mark#(sieve(X)) -> mark#(X)) (head#(active(X)) -> head#(X), head#(active(X)) -> head#(X)) (head#(active(X)) -> head#(X), head#(mark(X)) -> head#(X)) (tail#(active(X)) -> tail#(X), tail#(active(X)) -> tail#(X)) (tail#(active(X)) -> tail#(X), tail#(mark(X)) -> tail#(X)) (active#(filter(s(s(X)), cons(Y, Z))) -> divides#(s(s(X)), Y), divides#(active(X1), X2) -> divides#(X1, X2)) (active#(filter(s(s(X)), cons(Y, Z))) -> divides#(s(s(X)), Y), divides#(mark(X1), X2) -> divides#(X1, X2)) (active#(filter(s(s(X)), cons(Y, Z))) -> divides#(s(s(X)), Y), divides#(X1, active(X2)) -> divides#(X1, X2)) (active#(filter(s(s(X)), cons(Y, Z))) -> divides#(s(s(X)), Y), divides#(X1, mark(X2)) -> divides#(X1, X2)) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> filter#(s(s(X)), Z)) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> filter#(X, sieve(Y))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> divides#(s(s(X)), Y)) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> if#(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> cons#(Y, filter(X, sieve(Y)))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> sieve#(Y)) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(if(true(), X, Y)) -> mark#(X)) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(tail(cons(X, Y))) -> mark#(Y)) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(head(cons(X, Y))) -> mark#(X)) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(from(X)) -> cons#(X, from(s(X)))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(from(X)) -> s#(X)) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(from(X)) -> from#(s(X))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(from(X)) -> mark#(cons(X, from(s(X))))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(sieve(cons(X, Y))) -> filter#(X, sieve(Y))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(sieve(cons(X, Y))) -> cons#(X, filter(X, sieve(Y)))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(sieve(cons(X, Y))) -> sieve#(Y)) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y))))) (mark#(s(X)) -> active#(s(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> filter#(s(s(X)), Z)) (mark#(s(X)) -> active#(s(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> filter#(X, sieve(Y))) (mark#(s(X)) -> active#(s(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> divides#(s(s(X)), Y)) (mark#(s(X)) -> active#(s(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> if#(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) (mark#(s(X)) -> active#(s(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> cons#(Y, filter(X, sieve(Y)))) (mark#(s(X)) -> active#(s(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> sieve#(Y)) (mark#(s(X)) -> active#(s(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))))) (mark#(s(X)) -> active#(s(mark(X))), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(s(X)) -> active#(s(mark(X))), active#(if(true(), X, Y)) -> mark#(X)) (mark#(s(X)) -> active#(s(mark(X))), active#(tail(cons(X, Y))) -> mark#(Y)) (mark#(s(X)) -> active#(s(mark(X))), active#(head(cons(X, Y))) -> mark#(X)) (mark#(s(X)) -> active#(s(mark(X))), active#(from(X)) -> cons#(X, from(s(X)))) (mark#(s(X)) -> active#(s(mark(X))), active#(from(X)) -> s#(X)) (mark#(s(X)) -> active#(s(mark(X))), active#(from(X)) -> from#(s(X))) (mark#(s(X)) -> active#(s(mark(X))), active#(from(X)) -> mark#(cons(X, from(s(X))))) (mark#(s(X)) -> active#(s(mark(X))), active#(sieve(cons(X, Y))) -> filter#(X, sieve(Y))) (mark#(s(X)) -> active#(s(mark(X))), active#(sieve(cons(X, Y))) -> cons#(X, filter(X, sieve(Y)))) (mark#(s(X)) -> active#(s(mark(X))), active#(sieve(cons(X, Y))) -> sieve#(Y)) (mark#(s(X)) -> active#(s(mark(X))), active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y))))) (mark#(tail(X)) -> active#(tail(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> filter#(s(s(X)), Z)) (mark#(tail(X)) -> active#(tail(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> filter#(X, sieve(Y))) (mark#(tail(X)) -> active#(tail(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> divides#(s(s(X)), Y)) (mark#(tail(X)) -> active#(tail(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> if#(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) (mark#(tail(X)) -> active#(tail(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> cons#(Y, filter(X, sieve(Y)))) (mark#(tail(X)) -> active#(tail(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> sieve#(Y)) (mark#(tail(X)) -> active#(tail(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))))) (mark#(tail(X)) -> active#(tail(mark(X))), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(tail(X)) -> active#(tail(mark(X))), active#(if(true(), X, Y)) -> mark#(X)) (mark#(tail(X)) -> active#(tail(mark(X))), active#(tail(cons(X, Y))) -> mark#(Y)) (mark#(tail(X)) -> active#(tail(mark(X))), active#(head(cons(X, Y))) -> mark#(X)) (mark#(tail(X)) -> active#(tail(mark(X))), active#(from(X)) -> cons#(X, from(s(X)))) (mark#(tail(X)) -> active#(tail(mark(X))), active#(from(X)) -> s#(X)) (mark#(tail(X)) -> active#(tail(mark(X))), active#(from(X)) -> from#(s(X))) (mark#(tail(X)) -> active#(tail(mark(X))), active#(from(X)) -> mark#(cons(X, from(s(X))))) (mark#(tail(X)) -> active#(tail(mark(X))), active#(sieve(cons(X, Y))) -> filter#(X, sieve(Y))) (mark#(tail(X)) -> active#(tail(mark(X))), active#(sieve(cons(X, Y))) -> cons#(X, filter(X, sieve(Y)))) (mark#(tail(X)) -> active#(tail(mark(X))), active#(sieve(cons(X, Y))) -> sieve#(Y)) (mark#(tail(X)) -> active#(tail(mark(X))), active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y))))) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(filter(X1, X2)) -> filter#(mark(X1), mark(X2))) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(filter(X1, X2)) -> mark#(X2)) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(filter(X1, X2)) -> mark#(X1)) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(divides(X1, X2)) -> divides#(mark(X1), mark(X2))) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2)))) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(divides(X1, X2)) -> mark#(X2)) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(divides(X1, X2)) -> mark#(X1)) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(tail(X)) -> tail#(mark(X))) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(tail(X)) -> active#(tail(mark(X)))) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(tail(X)) -> mark#(X)) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(head(X)) -> head#(mark(X))) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(head(X)) -> active#(head(mark(X)))) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(head(X)) -> mark#(X)) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(s(X)) -> active#(s(mark(X)))) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(s(X)) -> s#(mark(X))) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(s(X)) -> mark#(X)) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(from(X)) -> active#(from(mark(X)))) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(from(X)) -> from#(mark(X))) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(from(X)) -> mark#(X)) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(sieve(X)) -> sieve#(mark(X))) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(sieve(X)) -> mark#(X)) (mark#(filter(X1, X2)) -> mark#(X2), mark#(filter(X1, X2)) -> filter#(mark(X1), mark(X2))) (mark#(filter(X1, X2)) -> mark#(X2), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (mark#(filter(X1, X2)) -> mark#(X2), mark#(filter(X1, X2)) -> mark#(X2)) (mark#(filter(X1, X2)) -> mark#(X2), mark#(filter(X1, X2)) -> mark#(X1)) (mark#(filter(X1, X2)) -> mark#(X2), mark#(divides(X1, X2)) -> divides#(mark(X1), mark(X2))) (mark#(filter(X1, X2)) -> mark#(X2), mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2)))) (mark#(filter(X1, X2)) -> mark#(X2), mark#(divides(X1, X2)) -> mark#(X2)) (mark#(filter(X1, X2)) -> mark#(X2), mark#(divides(X1, X2)) -> mark#(X1)) (mark#(filter(X1, X2)) -> mark#(X2), mark#(false()) -> active#(false())) (mark#(filter(X1, X2)) -> mark#(X2), mark#(true()) -> active#(true())) (mark#(filter(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (mark#(filter(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(filter(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(filter(X1, X2)) -> mark#(X2), mark#(tail(X)) -> tail#(mark(X))) (mark#(filter(X1, X2)) -> mark#(X2), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(filter(X1, X2)) -> mark#(X2), mark#(tail(X)) -> mark#(X)) (mark#(filter(X1, X2)) -> mark#(X2), mark#(head(X)) -> head#(mark(X))) (mark#(filter(X1, X2)) -> mark#(X2), mark#(head(X)) -> active#(head(mark(X)))) (mark#(filter(X1, X2)) -> mark#(X2), mark#(head(X)) -> mark#(X)) (mark#(filter(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(filter(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(filter(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(filter(X1, X2)) -> mark#(X2), mark#(primes()) -> active#(primes())) (mark#(filter(X1, X2)) -> mark#(X2), mark#(0()) -> active#(0())) (mark#(filter(X1, X2)) -> mark#(X2), mark#(s(X)) -> active#(s(mark(X)))) (mark#(filter(X1, X2)) -> mark#(X2), mark#(s(X)) -> s#(mark(X))) (mark#(filter(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X)) (mark#(filter(X1, X2)) -> mark#(X2), mark#(from(X)) -> active#(from(mark(X)))) (mark#(filter(X1, X2)) -> mark#(X2), mark#(from(X)) -> from#(mark(X))) (mark#(filter(X1, X2)) -> mark#(X2), mark#(from(X)) -> mark#(X)) (mark#(filter(X1, X2)) -> mark#(X2), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(filter(X1, X2)) -> mark#(X2), mark#(sieve(X)) -> sieve#(mark(X))) (mark#(filter(X1, X2)) -> mark#(X2), mark#(sieve(X)) -> mark#(X)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y))))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(sieve(cons(X, Y))) -> sieve#(Y)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(sieve(cons(X, Y))) -> cons#(X, filter(X, sieve(Y)))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(sieve(cons(X, Y))) -> filter#(X, sieve(Y))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(from(X)) -> mark#(cons(X, from(s(X))))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(from(X)) -> from#(s(X))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(from(X)) -> s#(X)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(from(X)) -> cons#(X, from(s(X)))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(head(cons(X, Y))) -> mark#(X)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(tail(cons(X, Y))) -> mark#(Y)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(filter(s(s(X)), cons(Y, Z))) -> sieve#(Y)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(filter(s(s(X)), cons(Y, Z))) -> cons#(Y, filter(X, sieve(Y)))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(filter(s(s(X)), cons(Y, Z))) -> if#(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(filter(s(s(X)), cons(Y, Z))) -> divides#(s(s(X)), Y)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(filter(s(s(X)), cons(Y, Z))) -> filter#(X, sieve(Y))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(filter(s(s(X)), cons(Y, Z))) -> filter#(s(s(X)), Z)) (mark#(divides(X1, X2)) -> mark#(X2), mark#(sieve(X)) -> mark#(X)) (mark#(divides(X1, X2)) -> mark#(X2), mark#(sieve(X)) -> sieve#(mark(X))) (mark#(divides(X1, X2)) -> mark#(X2), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(divides(X1, X2)) -> mark#(X2), mark#(from(X)) -> mark#(X)) (mark#(divides(X1, X2)) -> mark#(X2), mark#(from(X)) -> from#(mark(X))) (mark#(divides(X1, X2)) -> mark#(X2), mark#(from(X)) -> active#(from(mark(X)))) (mark#(divides(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X)) (mark#(divides(X1, X2)) -> mark#(X2), mark#(s(X)) -> s#(mark(X))) (mark#(divides(X1, X2)) -> mark#(X2), mark#(s(X)) -> active#(s(mark(X)))) (mark#(divides(X1, X2)) -> mark#(X2), mark#(0()) -> active#(0())) (mark#(divides(X1, X2)) -> mark#(X2), mark#(primes()) -> active#(primes())) (mark#(divides(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(divides(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(divides(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(divides(X1, X2)) -> mark#(X2), mark#(head(X)) -> mark#(X)) (mark#(divides(X1, X2)) -> mark#(X2), mark#(head(X)) -> active#(head(mark(X)))) (mark#(divides(X1, X2)) -> mark#(X2), mark#(head(X)) -> head#(mark(X))) (mark#(divides(X1, X2)) -> mark#(X2), mark#(tail(X)) -> mark#(X)) (mark#(divides(X1, X2)) -> mark#(X2), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(divides(X1, X2)) -> mark#(X2), mark#(tail(X)) -> tail#(mark(X))) (mark#(divides(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(divides(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(divides(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (mark#(divides(X1, X2)) -> mark#(X2), mark#(true()) -> active#(true())) (mark#(divides(X1, X2)) -> mark#(X2), mark#(false()) -> active#(false())) (mark#(divides(X1, X2)) -> mark#(X2), mark#(divides(X1, X2)) -> mark#(X1)) (mark#(divides(X1, X2)) -> mark#(X2), mark#(divides(X1, X2)) -> mark#(X2)) (mark#(divides(X1, X2)) -> mark#(X2), mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2)))) (mark#(divides(X1, X2)) -> mark#(X2), mark#(divides(X1, X2)) -> divides#(mark(X1), mark(X2))) (mark#(divides(X1, X2)) -> mark#(X2), mark#(filter(X1, X2)) -> mark#(X1)) (mark#(divides(X1, X2)) -> mark#(X2), mark#(filter(X1, X2)) -> mark#(X2)) (mark#(divides(X1, X2)) -> mark#(X2), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (mark#(divides(X1, X2)) -> mark#(X2), mark#(filter(X1, X2)) -> filter#(mark(X1), mark(X2))) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(sieve(X)) -> mark#(X)) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(sieve(X)) -> sieve#(mark(X))) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(from(X)) -> mark#(X)) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(from(X)) -> from#(mark(X))) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(from(X)) -> active#(from(mark(X)))) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(s(X)) -> mark#(X)) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(s(X)) -> s#(mark(X))) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(s(X)) -> active#(s(mark(X)))) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(head(X)) -> mark#(X)) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(head(X)) -> active#(head(mark(X)))) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(head(X)) -> head#(mark(X))) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(tail(X)) -> mark#(X)) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(tail(X)) -> active#(tail(mark(X)))) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(tail(X)) -> tail#(mark(X))) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(divides(X1, X2)) -> mark#(X1)) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(divides(X1, X2)) -> mark#(X2)) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2)))) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(divides(X1, X2)) -> divides#(mark(X1), mark(X2))) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(filter(X1, X2)) -> mark#(X1)) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(filter(X1, X2)) -> mark#(X2)) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(filter(X1, X2)) -> filter#(mark(X1), mark(X2))) (mark#(head(X)) -> active#(head(mark(X))), active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y))))) (mark#(head(X)) -> active#(head(mark(X))), active#(sieve(cons(X, Y))) -> sieve#(Y)) (mark#(head(X)) -> active#(head(mark(X))), active#(sieve(cons(X, Y))) -> cons#(X, filter(X, sieve(Y)))) (mark#(head(X)) -> active#(head(mark(X))), active#(sieve(cons(X, Y))) -> filter#(X, sieve(Y))) (mark#(head(X)) -> active#(head(mark(X))), active#(from(X)) -> mark#(cons(X, from(s(X))))) (mark#(head(X)) -> active#(head(mark(X))), active#(from(X)) -> from#(s(X))) (mark#(head(X)) -> active#(head(mark(X))), active#(from(X)) -> s#(X)) (mark#(head(X)) -> active#(head(mark(X))), active#(from(X)) -> cons#(X, from(s(X)))) (mark#(head(X)) -> active#(head(mark(X))), active#(head(cons(X, Y))) -> mark#(X)) (mark#(head(X)) -> active#(head(mark(X))), active#(tail(cons(X, Y))) -> mark#(Y)) (mark#(head(X)) -> active#(head(mark(X))), active#(if(true(), X, Y)) -> mark#(X)) (mark#(head(X)) -> active#(head(mark(X))), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(head(X)) -> active#(head(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))))) (mark#(head(X)) -> active#(head(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> sieve#(Y)) (mark#(head(X)) -> active#(head(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> cons#(Y, filter(X, sieve(Y)))) (mark#(head(X)) -> active#(head(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> if#(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) (mark#(head(X)) -> active#(head(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> divides#(s(s(X)), Y)) (mark#(head(X)) -> active#(head(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> filter#(X, sieve(Y))) (mark#(head(X)) -> active#(head(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> filter#(s(s(X)), Z)) (mark#(from(X)) -> active#(from(mark(X))), active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y))))) (mark#(from(X)) -> active#(from(mark(X))), active#(sieve(cons(X, Y))) -> sieve#(Y)) (mark#(from(X)) -> active#(from(mark(X))), active#(sieve(cons(X, Y))) -> cons#(X, filter(X, sieve(Y)))) (mark#(from(X)) -> active#(from(mark(X))), active#(sieve(cons(X, Y))) -> filter#(X, sieve(Y))) (mark#(from(X)) -> active#(from(mark(X))), active#(from(X)) -> mark#(cons(X, from(s(X))))) (mark#(from(X)) -> active#(from(mark(X))), active#(from(X)) -> from#(s(X))) (mark#(from(X)) -> active#(from(mark(X))), active#(from(X)) -> s#(X)) (mark#(from(X)) -> active#(from(mark(X))), active#(from(X)) -> cons#(X, from(s(X)))) (mark#(from(X)) -> active#(from(mark(X))), active#(head(cons(X, Y))) -> mark#(X)) (mark#(from(X)) -> active#(from(mark(X))), active#(tail(cons(X, Y))) -> mark#(Y)) (mark#(from(X)) -> active#(from(mark(X))), active#(if(true(), X, Y)) -> mark#(X)) (mark#(from(X)) -> active#(from(mark(X))), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(from(X)) -> active#(from(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))))) (mark#(from(X)) -> active#(from(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> sieve#(Y)) (mark#(from(X)) -> active#(from(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> cons#(Y, filter(X, sieve(Y)))) (mark#(from(X)) -> active#(from(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> if#(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) (mark#(from(X)) -> active#(from(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> divides#(s(s(X)), Y)) (mark#(from(X)) -> active#(from(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> filter#(X, sieve(Y))) (mark#(from(X)) -> active#(from(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> filter#(s(s(X)), Z)) (active#(primes()) -> mark#(sieve(from(s(s(0()))))), mark#(sieve(X)) -> mark#(X)) (active#(primes()) -> mark#(sieve(from(s(s(0()))))), mark#(sieve(X)) -> sieve#(mark(X))) (active#(primes()) -> mark#(sieve(from(s(s(0()))))), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(from(X)) -> cons#(X, from(s(X))), cons#(X1, mark(X2)) -> cons#(X1, X2)) (active#(from(X)) -> cons#(X, from(s(X))), cons#(X1, active(X2)) -> cons#(X1, X2)) (active#(from(X)) -> cons#(X, from(s(X))), cons#(mark(X1), X2) -> cons#(X1, X2)) (active#(from(X)) -> cons#(X, from(s(X))), cons#(active(X1), X2) -> cons#(X1, X2)) (tail#(mark(X)) -> tail#(X), tail#(mark(X)) -> tail#(X)) (tail#(mark(X)) -> tail#(X), tail#(active(X)) -> tail#(X)) (head#(mark(X)) -> head#(X), head#(mark(X)) -> head#(X)) (head#(mark(X)) -> head#(X), head#(active(X)) -> head#(X)) (active#(head(cons(X, Y))) -> mark#(X), mark#(sieve(X)) -> mark#(X)) (active#(head(cons(X, Y))) -> mark#(X), mark#(sieve(X)) -> sieve#(mark(X))) (active#(head(cons(X, Y))) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(head(cons(X, Y))) -> mark#(X), mark#(from(X)) -> mark#(X)) (active#(head(cons(X, Y))) -> mark#(X), mark#(from(X)) -> from#(mark(X))) (active#(head(cons(X, Y))) -> mark#(X), mark#(from(X)) -> active#(from(mark(X)))) (active#(head(cons(X, Y))) -> mark#(X), mark#(s(X)) -> mark#(X)) (active#(head(cons(X, Y))) -> mark#(X), mark#(s(X)) -> s#(mark(X))) (active#(head(cons(X, Y))) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (active#(head(cons(X, Y))) -> mark#(X), mark#(0()) -> active#(0())) (active#(head(cons(X, Y))) -> mark#(X), mark#(primes()) -> active#(primes())) (active#(head(cons(X, Y))) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (active#(head(cons(X, Y))) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (active#(head(cons(X, Y))) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (active#(head(cons(X, Y))) -> mark#(X), mark#(head(X)) -> mark#(X)) (active#(head(cons(X, Y))) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (active#(head(cons(X, Y))) -> mark#(X), mark#(head(X)) -> head#(mark(X))) (active#(head(cons(X, Y))) -> mark#(X), mark#(tail(X)) -> mark#(X)) (active#(head(cons(X, Y))) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X)))) (active#(head(cons(X, Y))) -> mark#(X), mark#(tail(X)) -> tail#(mark(X))) (active#(head(cons(X, Y))) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(head(cons(X, Y))) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(head(cons(X, Y))) -> mark#(X), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (active#(head(cons(X, Y))) -> mark#(X), mark#(true()) -> active#(true())) (active#(head(cons(X, Y))) -> mark#(X), mark#(false()) -> active#(false())) (active#(head(cons(X, Y))) -> mark#(X), mark#(divides(X1, X2)) -> mark#(X1)) (active#(head(cons(X, Y))) -> mark#(X), mark#(divides(X1, X2)) -> mark#(X2)) (active#(head(cons(X, Y))) -> mark#(X), mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2)))) (active#(head(cons(X, Y))) -> mark#(X), mark#(divides(X1, X2)) -> divides#(mark(X1), mark(X2))) (active#(head(cons(X, Y))) -> mark#(X), mark#(filter(X1, X2)) -> mark#(X1)) (active#(head(cons(X, Y))) -> mark#(X), mark#(filter(X1, X2)) -> mark#(X2)) (active#(head(cons(X, Y))) -> mark#(X), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (active#(head(cons(X, Y))) -> mark#(X), mark#(filter(X1, X2)) -> filter#(mark(X1), mark(X2))) (s#(active(X)) -> s#(X), s#(mark(X)) -> s#(X)) (s#(active(X)) -> s#(X), s#(active(X)) -> s#(X)) (from#(active(X)) -> from#(X), from#(mark(X)) -> from#(X)) (from#(active(X)) -> from#(X), from#(active(X)) -> from#(X)) (sieve#(active(X)) -> sieve#(X), sieve#(mark(X)) -> sieve#(X)) (sieve#(active(X)) -> sieve#(X), sieve#(active(X)) -> sieve#(X)) (mark#(tail(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X)) (mark#(tail(X)) -> mark#(X), mark#(sieve(X)) -> sieve#(mark(X))) (mark#(tail(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(tail(X)) -> mark#(X), mark#(from(X)) -> mark#(X)) (mark#(tail(X)) -> mark#(X), mark#(from(X)) -> from#(mark(X))) (mark#(tail(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X)))) (mark#(tail(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(tail(X)) -> mark#(X), mark#(s(X)) -> s#(mark(X))) (mark#(tail(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (mark#(tail(X)) -> mark#(X), mark#(0()) -> active#(0())) (mark#(tail(X)) -> mark#(X), mark#(primes()) -> active#(primes())) (mark#(tail(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(tail(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(tail(X)) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(tail(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(tail(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(tail(X)) -> mark#(X), mark#(head(X)) -> head#(mark(X))) (mark#(tail(X)) -> mark#(X), mark#(tail(X)) -> mark#(X)) (mark#(tail(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(tail(X)) -> mark#(X), mark#(tail(X)) -> tail#(mark(X))) (mark#(tail(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(tail(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(tail(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (mark#(tail(X)) -> mark#(X), mark#(true()) -> active#(true())) (mark#(tail(X)) -> mark#(X), mark#(false()) -> active#(false())) (mark#(tail(X)) -> mark#(X), mark#(divides(X1, X2)) -> mark#(X1)) (mark#(tail(X)) -> mark#(X), mark#(divides(X1, X2)) -> mark#(X2)) (mark#(tail(X)) -> mark#(X), mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2)))) (mark#(tail(X)) -> mark#(X), mark#(divides(X1, X2)) -> divides#(mark(X1), mark(X2))) (mark#(tail(X)) -> mark#(X), mark#(filter(X1, X2)) -> mark#(X1)) (mark#(tail(X)) -> mark#(X), mark#(filter(X1, X2)) -> mark#(X2)) (mark#(tail(X)) -> mark#(X), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (mark#(tail(X)) -> mark#(X), mark#(filter(X1, X2)) -> filter#(mark(X1), mark(X2))) (mark#(s(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(sieve(X)) -> sieve#(mark(X))) (mark#(s(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(from(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(from(X)) -> from#(mark(X))) (mark#(s(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> s#(mark(X))) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(0()) -> active#(0())) (mark#(s(X)) -> mark#(X), mark#(primes()) -> active#(primes())) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(s(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(head(X)) -> head#(mark(X))) (mark#(s(X)) -> mark#(X), mark#(tail(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(tail(X)) -> tail#(mark(X))) (mark#(s(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(s(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (mark#(s(X)) -> mark#(X), mark#(true()) -> active#(true())) (mark#(s(X)) -> mark#(X), mark#(false()) -> active#(false())) (mark#(s(X)) -> mark#(X), mark#(divides(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(divides(X1, X2)) -> mark#(X2)) (mark#(s(X)) -> mark#(X), mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2)))) (mark#(s(X)) -> mark#(X), mark#(divides(X1, X2)) -> divides#(mark(X1), mark(X2))) (mark#(s(X)) -> mark#(X), mark#(filter(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(filter(X1, X2)) -> mark#(X2)) (mark#(s(X)) -> mark#(X), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (mark#(s(X)) -> mark#(X), mark#(filter(X1, X2)) -> filter#(mark(X1), mark(X2))) (mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X)) (mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> sieve#(mark(X))) (mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(sieve(X)) -> mark#(X), mark#(from(X)) -> mark#(X)) (mark#(sieve(X)) -> mark#(X), mark#(from(X)) -> from#(mark(X))) (mark#(sieve(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X)))) (mark#(sieve(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(sieve(X)) -> mark#(X), mark#(s(X)) -> s#(mark(X))) (mark#(sieve(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X)))) (mark#(sieve(X)) -> mark#(X), mark#(0()) -> active#(0())) (mark#(sieve(X)) -> mark#(X), mark#(primes()) -> active#(primes())) (mark#(sieve(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(sieve(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(sieve(X)) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(sieve(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(sieve(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(sieve(X)) -> mark#(X), mark#(head(X)) -> head#(mark(X))) (mark#(sieve(X)) -> mark#(X), mark#(tail(X)) -> mark#(X)) (mark#(sieve(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(sieve(X)) -> mark#(X), mark#(tail(X)) -> tail#(mark(X))) (mark#(sieve(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(sieve(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(sieve(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (mark#(sieve(X)) -> mark#(X), mark#(true()) -> active#(true())) (mark#(sieve(X)) -> mark#(X), mark#(false()) -> active#(false())) (mark#(sieve(X)) -> mark#(X), mark#(divides(X1, X2)) -> mark#(X1)) (mark#(sieve(X)) -> mark#(X), mark#(divides(X1, X2)) -> mark#(X2)) (mark#(sieve(X)) -> mark#(X), mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2)))) (mark#(sieve(X)) -> mark#(X), mark#(divides(X1, X2)) -> divides#(mark(X1), mark(X2))) (mark#(sieve(X)) -> mark#(X), mark#(filter(X1, X2)) -> mark#(X1)) (mark#(sieve(X)) -> mark#(X), mark#(filter(X1, X2)) -> mark#(X2)) (mark#(sieve(X)) -> mark#(X), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (mark#(sieve(X)) -> mark#(X), mark#(filter(X1, X2)) -> filter#(mark(X1), mark(X2))) (mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y))))) (mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(sieve(cons(X, Y))) -> sieve#(Y)) (mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(sieve(cons(X, Y))) -> cons#(X, filter(X, sieve(Y)))) (mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(sieve(cons(X, Y))) -> filter#(X, sieve(Y))) (mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(from(X)) -> mark#(cons(X, from(s(X))))) (mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(from(X)) -> from#(s(X))) (mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(from(X)) -> s#(X)) (mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(from(X)) -> cons#(X, from(s(X)))) (mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(head(cons(X, Y))) -> mark#(X)) (mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(tail(cons(X, Y))) -> mark#(Y)) (mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(if(true(), X, Y)) -> mark#(X)) (mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))))) (mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(filter(s(s(X)), cons(Y, Z))) -> sieve#(Y)) (mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(filter(s(s(X)), cons(Y, Z))) -> cons#(Y, filter(X, sieve(Y)))) (mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(filter(s(s(X)), cons(Y, Z))) -> if#(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))) (mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(filter(s(s(X)), cons(Y, Z))) -> divides#(s(s(X)), Y)) (mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(filter(s(s(X)), cons(Y, Z))) -> filter#(X, sieve(Y))) (mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(filter(s(s(X)), cons(Y, Z))) -> filter#(s(s(X)), Z)) (active#(filter(s(s(X)), cons(Y, Z))) -> filter#(s(s(X)), Z), filter#(X1, mark(X2)) -> filter#(X1, X2)) (active#(filter(s(s(X)), cons(Y, Z))) -> filter#(s(s(X)), Z), filter#(X1, active(X2)) -> filter#(X1, X2)) (active#(filter(s(s(X)), cons(Y, Z))) -> filter#(s(s(X)), Z), filter#(mark(X1), X2) -> filter#(X1, X2)) (active#(filter(s(s(X)), cons(Y, Z))) -> filter#(s(s(X)), Z), filter#(active(X1), X2) -> filter#(X1, X2)) (filter#(active(X1), X2) -> filter#(X1, X2), filter#(X1, mark(X2)) -> filter#(X1, X2)) (filter#(active(X1), X2) -> filter#(X1, X2), filter#(X1, active(X2)) -> filter#(X1, X2)) (filter#(active(X1), X2) -> filter#(X1, X2), filter#(mark(X1), X2) -> filter#(X1, X2)) (filter#(active(X1), X2) -> filter#(X1, X2), filter#(active(X1), X2) -> filter#(X1, X2)) (filter#(X1, active(X2)) -> filter#(X1, X2), filter#(X1, mark(X2)) -> filter#(X1, X2)) (filter#(X1, active(X2)) -> filter#(X1, X2), filter#(X1, active(X2)) -> filter#(X1, X2)) (filter#(X1, active(X2)) -> filter#(X1, X2), filter#(mark(X1), X2) -> filter#(X1, X2)) (filter#(X1, active(X2)) -> filter#(X1, X2), filter#(active(X1), X2) -> filter#(X1, X2)) (divides#(active(X1), X2) -> divides#(X1, X2), divides#(X1, mark(X2)) -> divides#(X1, X2)) (divides#(active(X1), X2) -> divides#(X1, X2), divides#(X1, active(X2)) -> divides#(X1, X2)) (divides#(active(X1), X2) -> divides#(X1, X2), divides#(mark(X1), X2) -> divides#(X1, X2)) (divides#(active(X1), X2) -> divides#(X1, X2), divides#(active(X1), X2) -> divides#(X1, X2)) (divides#(X1, active(X2)) -> divides#(X1, X2), divides#(X1, mark(X2)) -> divides#(X1, X2)) (divides#(X1, active(X2)) -> divides#(X1, X2), divides#(X1, active(X2)) -> divides#(X1, X2)) (divides#(X1, active(X2)) -> divides#(X1, X2), divides#(mark(X1), X2) -> divides#(X1, X2)) (divides#(X1, active(X2)) -> divides#(X1, X2), divides#(active(X1), X2) -> divides#(X1, X2)) (cons#(active(X1), X2) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(active(X1), X2) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)) (cons#(active(X1), X2) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (cons#(active(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)) (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2)) (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)) (mark#(filter(X1, X2)) -> mark#(X1), mark#(sieve(X)) -> mark#(X)) (mark#(filter(X1, X2)) -> mark#(X1), mark#(sieve(X)) -> sieve#(mark(X))) (mark#(filter(X1, X2)) -> mark#(X1), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(filter(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X)) (mark#(filter(X1, X2)) -> mark#(X1), mark#(from(X)) -> from#(mark(X))) (mark#(filter(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X)))) (mark#(filter(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(filter(X1, X2)) -> mark#(X1), mark#(s(X)) -> s#(mark(X))) (mark#(filter(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(mark(X)))) (mark#(filter(X1, X2)) -> mark#(X1), mark#(0()) -> active#(0())) (mark#(filter(X1, X2)) -> mark#(X1), mark#(primes()) -> active#(primes())) (mark#(filter(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(filter(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(filter(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(filter(X1, X2)) -> mark#(X1), mark#(head(X)) -> mark#(X)) (mark#(filter(X1, X2)) -> mark#(X1), mark#(head(X)) -> active#(head(mark(X)))) (mark#(filter(X1, X2)) -> mark#(X1), mark#(head(X)) -> head#(mark(X))) (mark#(filter(X1, X2)) -> mark#(X1), mark#(tail(X)) -> mark#(X)) (mark#(filter(X1, X2)) -> mark#(X1), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(filter(X1, X2)) -> mark#(X1), mark#(tail(X)) -> tail#(mark(X))) (mark#(filter(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(filter(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(filter(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (mark#(filter(X1, X2)) -> mark#(X1), mark#(true()) -> active#(true())) (mark#(filter(X1, X2)) -> mark#(X1), mark#(false()) -> active#(false())) (mark#(filter(X1, X2)) -> mark#(X1), mark#(divides(X1, X2)) -> mark#(X1)) (mark#(filter(X1, X2)) -> mark#(X1), mark#(divides(X1, X2)) -> mark#(X2)) (mark#(filter(X1, X2)) -> mark#(X1), mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2)))) (mark#(filter(X1, X2)) -> mark#(X1), mark#(divides(X1, X2)) -> divides#(mark(X1), mark(X2))) (mark#(filter(X1, X2)) -> mark#(X1), mark#(filter(X1, X2)) -> mark#(X1)) (mark#(filter(X1, X2)) -> mark#(X1), mark#(filter(X1, X2)) -> mark#(X2)) (mark#(filter(X1, X2)) -> mark#(X1), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (mark#(filter(X1, X2)) -> mark#(X1), mark#(filter(X1, X2)) -> filter#(mark(X1), mark(X2))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(sieve(X)) -> mark#(X)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(sieve(X)) -> sieve#(mark(X))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(from(X)) -> mark#(X)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(from(X)) -> from#(mark(X))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X)))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(s(X)) -> s#(mark(X))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(s(X)) -> active#(s(mark(X)))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(0()) -> active#(0())) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(primes()) -> active#(primes())) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(head(X)) -> mark#(X)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(head(X)) -> active#(head(mark(X)))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(head(X)) -> head#(mark(X))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(tail(X)) -> mark#(X)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(tail(X)) -> tail#(mark(X))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(true()) -> active#(true())) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(false()) -> active#(false())) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(divides(X1, X2)) -> mark#(X1)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(divides(X1, X2)) -> mark#(X2)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2)))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(divides(X1, X2)) -> divides#(mark(X1), mark(X2))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(filter(X1, X2)) -> mark#(X1)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(filter(X1, X2)) -> mark#(X2)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(filter(X1, X2)) -> filter#(mark(X1), mark(X2))) (active#(filter(s(s(X)), cons(Y, Z))) -> if#(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (active#(filter(s(s(X)), cons(Y, Z))) -> if#(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (active#(filter(s(s(X)), cons(Y, Z))) -> if#(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (active#(filter(s(s(X)), cons(Y, Z))) -> if#(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (active#(filter(s(s(X)), cons(Y, Z))) -> if#(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (active#(filter(s(s(X)), cons(Y, Z))) -> if#(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))), if#(active(X1), X2, X3) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(active(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(active(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(active(X1), X2, X3) -> if#(X1, X2, X3)) (mark#(cons(X1, X2)) -> cons#(mark(X1), X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (mark#(cons(X1, X2)) -> cons#(mark(X1), X2), cons#(X1, active(X2)) -> cons#(X1, X2)) (mark#(cons(X1, X2)) -> cons#(mark(X1), X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (mark#(cons(X1, X2)) -> cons#(mark(X1), X2), cons#(active(X1), X2) -> cons#(X1, X2)) (active#(sieve(cons(X, Y))) -> filter#(X, sieve(Y)), filter#(X1, mark(X2)) -> filter#(X1, X2)) (active#(sieve(cons(X, Y))) -> filter#(X, sieve(Y)), filter#(X1, active(X2)) -> filter#(X1, X2)) (active#(sieve(cons(X, Y))) -> filter#(X, sieve(Y)), filter#(mark(X1), X2) -> filter#(X1, X2)) (active#(sieve(cons(X, Y))) -> filter#(X, sieve(Y)), filter#(active(X1), X2) -> filter#(X1, X2)) (mark#(divides(X1, X2)) -> divides#(mark(X1), mark(X2)), divides#(X1, mark(X2)) -> divides#(X1, X2)) (mark#(divides(X1, X2)) -> divides#(mark(X1), mark(X2)), divides#(X1, active(X2)) -> divides#(X1, X2)) (mark#(divides(X1, X2)) -> divides#(mark(X1), mark(X2)), divides#(mark(X1), X2) -> divides#(X1, X2)) (mark#(divides(X1, X2)) -> divides#(mark(X1), mark(X2)), divides#(active(X1), X2) -> divides#(X1, X2)) (active#(filter(s(s(X)), cons(Y, Z))) -> sieve#(Y), sieve#(mark(X)) -> sieve#(X)) (active#(filter(s(s(X)), cons(Y, Z))) -> sieve#(Y), sieve#(active(X)) -> sieve#(X)) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(sieve(X)) -> mark#(X)) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(sieve(X)) -> sieve#(mark(X))) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(from(X)) -> mark#(X)) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(from(X)) -> from#(mark(X))) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(from(X)) -> active#(from(mark(X)))) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(s(X)) -> mark#(X)) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(s(X)) -> s#(mark(X))) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(s(X)) -> active#(s(mark(X)))) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(0()) -> active#(0())) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(primes()) -> active#(primes())) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(cons(X1, X2)) -> mark#(X1)) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2))) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(cons(X1, X2)) -> cons#(mark(X1), X2)) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(head(X)) -> mark#(X)) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(head(X)) -> active#(head(mark(X)))) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(head(X)) -> head#(mark(X))) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(tail(X)) -> mark#(X)) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(tail(X)) -> active#(tail(mark(X)))) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(tail(X)) -> tail#(mark(X))) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(if(X1, X2, X3)) -> if#(mark(X1), X2, X3)) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(true()) -> active#(true())) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(false()) -> active#(false())) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(divides(X1, X2)) -> mark#(X1)) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(divides(X1, X2)) -> mark#(X2)) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2)))) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(divides(X1, X2)) -> divides#(mark(X1), mark(X2))) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(filter(X1, X2)) -> mark#(X1)) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(filter(X1, X2)) -> mark#(X2)) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(filter(X1, X2)) -> filter#(mark(X1), mark(X2))) (active#(from(X)) -> from#(s(X)), from#(mark(X)) -> from#(X)) (active#(from(X)) -> from#(s(X)), from#(active(X)) -> from#(X)) (mark#(head(X)) -> head#(mark(X)), head#(mark(X)) -> head#(X)) (mark#(head(X)) -> head#(mark(X)), head#(active(X)) -> head#(X)) (mark#(from(X)) -> from#(mark(X)), from#(mark(X)) -> from#(X)) (mark#(from(X)) -> from#(mark(X)), from#(active(X)) -> from#(X)) (active#(sieve(cons(X, Y))) -> cons#(X, filter(X, sieve(Y))), cons#(X1, mark(X2)) -> cons#(X1, X2)) (active#(sieve(cons(X, Y))) -> cons#(X, filter(X, sieve(Y))), cons#(X1, active(X2)) -> cons#(X1, X2)) (active#(sieve(cons(X, Y))) -> cons#(X, filter(X, sieve(Y))), cons#(mark(X1), X2) -> cons#(X1, X2)) (active#(sieve(cons(X, Y))) -> cons#(X, filter(X, sieve(Y))), cons#(active(X1), X2) -> cons#(X1, X2)) } SCCS: Scc: { filter#(X1, mark(X2)) -> filter#(X1, X2), filter#(X1, active(X2)) -> filter#(X1, X2), filter#(mark(X1), X2) -> filter#(X1, X2), filter#(active(X1), X2) -> filter#(X1, X2)} Scc: { divides#(X1, mark(X2)) -> divides#(X1, X2), divides#(X1, active(X2)) -> divides#(X1, X2), divides#(mark(X1), X2) -> divides#(X1, X2), divides#(active(X1), X2) -> divides#(X1, X2)} Scc: { if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(active(X1), X2, X3) -> if#(X1, X2, X3)} Scc: { tail#(mark(X)) -> tail#(X), tail#(active(X)) -> tail#(X)} Scc: { head#(mark(X)) -> head#(X), head#(active(X)) -> head#(X)} Scc: { cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)} Scc: { s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X)} Scc: { from#(mark(X)) -> from#(X), from#(active(X)) -> from#(X)} Scc: { sieve#(mark(X)) -> sieve#(X), sieve#(active(X)) -> sieve#(X)} Scc: { mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X))), mark#(from(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X))), mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))), mark#(primes()) -> active#(primes()), mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X))), mark#(tail(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X))), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), mark#(divides(X1, X2)) -> mark#(X1), mark#(divides(X1, X2)) -> mark#(X2), mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2))), mark#(filter(X1, X2)) -> mark#(X1), mark#(filter(X1, X2)) -> mark#(X2), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), active#(from(X)) -> mark#(cons(X, from(s(X)))), active#(primes()) -> mark#(sieve(from(s(s(0()))))), active#(head(cons(X, Y))) -> mark#(X), active#(tail(cons(X, Y))) -> mark#(Y), active#(if(true(), X, Y)) -> mark#(X), active#(if(false(), X, Y)) -> mark#(Y), active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))))} SCC: Strict: { filter#(X1, mark(X2)) -> filter#(X1, X2), filter#(X1, active(X2)) -> filter#(X1, X2), filter#(mark(X1), X2) -> filter#(X1, X2), filter#(active(X1), X2) -> filter#(X1, X2)} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} SPSC: Simple Projection: pi(filter#) = 0 Strict: { filter#(X1, mark(X2)) -> filter#(X1, X2), filter#(X1, active(X2)) -> filter#(X1, X2), filter#(mark(X1), X2) -> filter#(X1, X2)} EDG: {(filter#(X1, active(X2)) -> filter#(X1, X2), filter#(mark(X1), X2) -> filter#(X1, X2)) (filter#(X1, active(X2)) -> filter#(X1, X2), filter#(X1, active(X2)) -> filter#(X1, X2)) (filter#(X1, active(X2)) -> filter#(X1, X2), filter#(X1, mark(X2)) -> filter#(X1, X2)) (filter#(mark(X1), X2) -> filter#(X1, X2), filter#(X1, mark(X2)) -> filter#(X1, X2)) (filter#(mark(X1), X2) -> filter#(X1, X2), filter#(X1, active(X2)) -> filter#(X1, X2)) (filter#(mark(X1), X2) -> filter#(X1, X2), filter#(mark(X1), X2) -> filter#(X1, X2)) (filter#(X1, mark(X2)) -> filter#(X1, X2), filter#(X1, mark(X2)) -> filter#(X1, X2)) (filter#(X1, mark(X2)) -> filter#(X1, X2), filter#(X1, active(X2)) -> filter#(X1, X2)) (filter#(X1, mark(X2)) -> filter#(X1, X2), filter#(mark(X1), X2) -> filter#(X1, X2))} SCCS: Scc: { filter#(X1, mark(X2)) -> filter#(X1, X2), filter#(X1, active(X2)) -> filter#(X1, X2), filter#(mark(X1), X2) -> filter#(X1, X2)} SCC: Strict: { filter#(X1, mark(X2)) -> filter#(X1, X2), filter#(X1, active(X2)) -> filter#(X1, X2), filter#(mark(X1), X2) -> filter#(X1, X2)} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} SPSC: Simple Projection: pi(filter#) = 0 Strict: { filter#(X1, mark(X2)) -> filter#(X1, X2), filter#(X1, active(X2)) -> filter#(X1, X2)} EDG: {(filter#(X1, active(X2)) -> filter#(X1, X2), filter#(X1, active(X2)) -> filter#(X1, X2)) (filter#(X1, active(X2)) -> filter#(X1, X2), filter#(X1, mark(X2)) -> filter#(X1, X2)) (filter#(X1, mark(X2)) -> filter#(X1, X2), filter#(X1, mark(X2)) -> filter#(X1, X2)) (filter#(X1, mark(X2)) -> filter#(X1, X2), filter#(X1, active(X2)) -> filter#(X1, X2))} SCCS: Scc: { filter#(X1, mark(X2)) -> filter#(X1, X2), filter#(X1, active(X2)) -> filter#(X1, X2)} SCC: Strict: { filter#(X1, mark(X2)) -> filter#(X1, X2), filter#(X1, active(X2)) -> filter#(X1, X2)} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} SPSC: Simple Projection: pi(filter#) = 1 Strict: {filter#(X1, active(X2)) -> filter#(X1, X2)} EDG: {(filter#(X1, active(X2)) -> filter#(X1, X2), filter#(X1, active(X2)) -> filter#(X1, X2))} SCCS: Scc: {filter#(X1, active(X2)) -> filter#(X1, X2)} SCC: Strict: {filter#(X1, active(X2)) -> filter#(X1, X2)} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} SPSC: Simple Projection: pi(filter#) = 1 Strict: {} Qed SCC: Strict: { divides#(X1, mark(X2)) -> divides#(X1, X2), divides#(X1, active(X2)) -> divides#(X1, X2), divides#(mark(X1), X2) -> divides#(X1, X2), divides#(active(X1), X2) -> divides#(X1, X2)} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} SPSC: Simple Projection: pi(divides#) = 0 Strict: { divides#(X1, mark(X2)) -> divides#(X1, X2), divides#(X1, active(X2)) -> divides#(X1, X2), divides#(mark(X1), X2) -> divides#(X1, X2)} EDG: {(divides#(X1, active(X2)) -> divides#(X1, X2), divides#(mark(X1), X2) -> divides#(X1, X2)) (divides#(X1, active(X2)) -> divides#(X1, X2), divides#(X1, active(X2)) -> divides#(X1, X2)) (divides#(X1, active(X2)) -> divides#(X1, X2), divides#(X1, mark(X2)) -> divides#(X1, X2)) (divides#(mark(X1), X2) -> divides#(X1, X2), divides#(X1, mark(X2)) -> divides#(X1, X2)) (divides#(mark(X1), X2) -> divides#(X1, X2), divides#(X1, active(X2)) -> divides#(X1, X2)) (divides#(mark(X1), X2) -> divides#(X1, X2), divides#(mark(X1), X2) -> divides#(X1, X2)) (divides#(X1, mark(X2)) -> divides#(X1, X2), divides#(X1, mark(X2)) -> divides#(X1, X2)) (divides#(X1, mark(X2)) -> divides#(X1, X2), divides#(X1, active(X2)) -> divides#(X1, X2)) (divides#(X1, mark(X2)) -> divides#(X1, X2), divides#(mark(X1), X2) -> divides#(X1, X2))} SCCS: Scc: { divides#(X1, mark(X2)) -> divides#(X1, X2), divides#(X1, active(X2)) -> divides#(X1, X2), divides#(mark(X1), X2) -> divides#(X1, X2)} SCC: Strict: { divides#(X1, mark(X2)) -> divides#(X1, X2), divides#(X1, active(X2)) -> divides#(X1, X2), divides#(mark(X1), X2) -> divides#(X1, X2)} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} SPSC: Simple Projection: pi(divides#) = 0 Strict: { divides#(X1, mark(X2)) -> divides#(X1, X2), divides#(X1, active(X2)) -> divides#(X1, X2)} EDG: {(divides#(X1, active(X2)) -> divides#(X1, X2), divides#(X1, active(X2)) -> divides#(X1, X2)) (divides#(X1, active(X2)) -> divides#(X1, X2), divides#(X1, mark(X2)) -> divides#(X1, X2)) (divides#(X1, mark(X2)) -> divides#(X1, X2), divides#(X1, mark(X2)) -> divides#(X1, X2)) (divides#(X1, mark(X2)) -> divides#(X1, X2), divides#(X1, active(X2)) -> divides#(X1, X2))} SCCS: Scc: { divides#(X1, mark(X2)) -> divides#(X1, X2), divides#(X1, active(X2)) -> divides#(X1, X2)} SCC: Strict: { divides#(X1, mark(X2)) -> divides#(X1, X2), divides#(X1, active(X2)) -> divides#(X1, X2)} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} SPSC: Simple Projection: pi(divides#) = 1 Strict: {divides#(X1, active(X2)) -> divides#(X1, X2)} EDG: {(divides#(X1, active(X2)) -> divides#(X1, X2), divides#(X1, active(X2)) -> divides#(X1, X2))} SCCS: Scc: {divides#(X1, active(X2)) -> divides#(X1, X2)} SCC: Strict: {divides#(X1, active(X2)) -> divides#(X1, X2)} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} SPSC: Simple Projection: pi(divides#) = 1 Strict: {} Qed SCC: Strict: { if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(active(X1), X2, X3) -> if#(X1, X2, X3)} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} SPSC: Simple Projection: pi(if#) = 0 Strict: { if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)} EDG: {(if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, mark(X3)) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3))} SCCS: Scc: { if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)} SCC: Strict: { if#(X1, X2, mark(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} SPSC: Simple Projection: pi(if#) = 2 Strict: {if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)} EDG: {(if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3))} SCCS: Scc: {if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)} SCC: Strict: {if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3)} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} SPSC: Simple Projection: pi(if#) = 0 Strict: {if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)} EDG: {(if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, X2, active(X3)) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3))} SCCS: Scc: {if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)} SCC: Strict: {if#(X1, X2, active(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} SPSC: Simple Projection: pi(if#) = 2 Strict: { if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)} EDG: {(if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)) (if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3)) (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3))} SCCS: Scc: { if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)} SCC: Strict: { if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3)} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} SPSC: Simple Projection: pi(if#) = 1 Strict: {if#(X1, active(X2), X3) -> if#(X1, X2, X3)} EDG: {(if#(X1, active(X2), X3) -> if#(X1, X2, X3), if#(X1, active(X2), X3) -> if#(X1, X2, X3))} SCCS: Scc: {if#(X1, active(X2), X3) -> if#(X1, X2, X3)} SCC: Strict: {if#(X1, active(X2), X3) -> if#(X1, X2, X3)} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} SPSC: Simple Projection: pi(if#) = 1 Strict: {} Qed SCC: Strict: { tail#(mark(X)) -> tail#(X), tail#(active(X)) -> tail#(X)} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} SPSC: Simple Projection: pi(tail#) = 0 Strict: {tail#(active(X)) -> tail#(X)} EDG: {(tail#(active(X)) -> tail#(X), tail#(active(X)) -> tail#(X))} SCCS: Scc: {tail#(active(X)) -> tail#(X)} SCC: Strict: {tail#(active(X)) -> tail#(X)} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} SPSC: Simple Projection: pi(tail#) = 0 Strict: {} Qed SCC: Strict: { head#(mark(X)) -> head#(X), head#(active(X)) -> head#(X)} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} SPSC: Simple Projection: pi(head#) = 0 Strict: {head#(active(X)) -> head#(X)} EDG: {(head#(active(X)) -> head#(X), head#(active(X)) -> head#(X))} SCCS: Scc: {head#(active(X)) -> head#(X)} SCC: Strict: {head#(active(X)) -> head#(X)} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} SPSC: Simple Projection: pi(head#) = 0 Strict: {} Qed SCC: Strict: { cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} SPSC: Simple Projection: pi(cons#) = 1 Strict: { cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)} EDG: {(cons#(mark(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)) (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(active(X1), X2) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(active(X1), X2) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (cons#(active(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2))} SCCS: Scc: { cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)} SCC: Strict: { cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} SPSC: Simple Projection: pi(cons#) = 0 Strict: { cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)} EDG: {(cons#(active(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)) (cons#(active(X1), X2) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2)) (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2))} SCCS: Scc: { cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)} SCC: Strict: { cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2)} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} SPSC: Simple Projection: pi(cons#) = 0 Strict: {cons#(X1, mark(X2)) -> cons#(X1, X2)} EDG: {(cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))} SCCS: Scc: {cons#(X1, mark(X2)) -> cons#(X1, X2)} SCC: Strict: {cons#(X1, mark(X2)) -> cons#(X1, X2)} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} SPSC: Simple Projection: pi(cons#) = 1 Strict: {} Qed SCC: Strict: { s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X)} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} SPSC: Simple Projection: pi(s#) = 0 Strict: {s#(active(X)) -> s#(X)} EDG: {(s#(active(X)) -> s#(X), s#(active(X)) -> s#(X))} SCCS: Scc: {s#(active(X)) -> s#(X)} SCC: Strict: {s#(active(X)) -> s#(X)} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} SPSC: Simple Projection: pi(s#) = 0 Strict: {} Qed SCC: Strict: { from#(mark(X)) -> from#(X), from#(active(X)) -> from#(X)} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} SPSC: Simple Projection: pi(from#) = 0 Strict: {from#(active(X)) -> from#(X)} EDG: {(from#(active(X)) -> from#(X), from#(active(X)) -> from#(X))} SCCS: Scc: {from#(active(X)) -> from#(X)} SCC: Strict: {from#(active(X)) -> from#(X)} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} SPSC: Simple Projection: pi(from#) = 0 Strict: {} Qed SCC: Strict: { sieve#(mark(X)) -> sieve#(X), sieve#(active(X)) -> sieve#(X)} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} SPSC: Simple Projection: pi(sieve#) = 0 Strict: {sieve#(active(X)) -> sieve#(X)} EDG: {(sieve#(active(X)) -> sieve#(X), sieve#(active(X)) -> sieve#(X))} SCCS: Scc: {sieve#(active(X)) -> sieve#(X)} SCC: Strict: {sieve#(active(X)) -> sieve#(X)} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} SPSC: Simple Projection: pi(sieve#) = 0 Strict: {} Qed SCC: Strict: { mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X))), mark#(from(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X))), mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))), mark#(primes()) -> active#(primes()), mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X))), mark#(tail(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X))), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), mark#(divides(X1, X2)) -> mark#(X1), mark#(divides(X1, X2)) -> mark#(X2), mark#(divides(X1, X2)) -> active#(divides(mark(X1), mark(X2))), mark#(filter(X1, X2)) -> mark#(X1), mark#(filter(X1, X2)) -> mark#(X2), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), active#(from(X)) -> mark#(cons(X, from(s(X)))), active#(primes()) -> mark#(sieve(from(s(s(0()))))), active#(head(cons(X, Y))) -> mark#(X), active#(tail(cons(X, Y))) -> mark#(Y), active#(if(true(), X, Y)) -> mark#(X), active#(if(false(), X, Y)) -> mark#(Y), active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))))} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} POLY: Argument Filtering: pi(filter) = [], pi(divides) = [], pi(false) = [], pi(true) = [], pi(if) = [], pi(tail) = [], pi(head) = [], pi(cons) = [], pi(primes) = [], pi(active#) = 0, pi(active) = [], pi(0) = [], pi(s) = [], pi(from) = [], pi(sieve) = [], pi(mark#) = [], pi(mark) = [] Usable Rules: {} Interpretation: [mark#] = 1, [if] = 1, [filter] = 1, [divides] = 0, [cons] = 0, [tail] = 1, [head] = 1, [s] = 0, [from] = 1, [sieve] = 1, [primes] = 1 Strict: { mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X))), mark#(from(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X))), mark#(s(X)) -> mark#(X), mark#(primes()) -> active#(primes()), mark#(cons(X1, X2)) -> mark#(X1), mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X))), mark#(tail(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X))), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), mark#(divides(X1, X2)) -> mark#(X1), mark#(divides(X1, X2)) -> mark#(X2), mark#(filter(X1, X2)) -> mark#(X1), mark#(filter(X1, X2)) -> mark#(X2), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), active#(from(X)) -> mark#(cons(X, from(s(X)))), active#(primes()) -> mark#(sieve(from(s(s(0()))))), active#(head(cons(X, Y))) -> mark#(X), active#(tail(cons(X, Y))) -> mark#(Y), active#(if(true(), X, Y)) -> mark#(X), active#(if(false(), X, Y)) -> mark#(Y), active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))))} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} EDG: { (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(filter(X1, X2)) -> mark#(X2)) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(filter(X1, X2)) -> mark#(X1)) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(divides(X1, X2)) -> mark#(X2)) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(divides(X1, X2)) -> mark#(X1)) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(tail(X)) -> active#(tail(mark(X)))) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(tail(X)) -> mark#(X)) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(head(X)) -> active#(head(mark(X)))) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(head(X)) -> mark#(X)) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(s(X)) -> mark#(X)) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(from(X)) -> active#(from(mark(X)))) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(from(X)) -> mark#(X)) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), mark#(sieve(X)) -> mark#(X)) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(filter(X1, X2)) -> mark#(X2)) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(filter(X1, X2)) -> mark#(X1)) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(divides(X1, X2)) -> mark#(X2)) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(divides(X1, X2)) -> mark#(X1)) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(tail(X)) -> active#(tail(mark(X)))) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(tail(X)) -> mark#(X)) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(head(X)) -> active#(head(mark(X)))) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(head(X)) -> mark#(X)) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(cons(X1, X2)) -> mark#(X1)) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(primes()) -> active#(primes())) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(s(X)) -> mark#(X)) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(from(X)) -> active#(from(mark(X)))) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(from(X)) -> mark#(X)) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(tail(cons(X, Y))) -> mark#(Y), mark#(sieve(X)) -> mark#(X)) (active#(primes()) -> mark#(sieve(from(s(s(0()))))), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(primes()) -> mark#(sieve(from(s(s(0()))))), mark#(sieve(X)) -> mark#(X)) (mark#(from(X)) -> active#(from(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))))) (mark#(from(X)) -> active#(from(mark(X))), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(from(X)) -> active#(from(mark(X))), active#(if(true(), X, Y)) -> mark#(X)) (mark#(from(X)) -> active#(from(mark(X))), active#(tail(cons(X, Y))) -> mark#(Y)) (mark#(from(X)) -> active#(from(mark(X))), active#(head(cons(X, Y))) -> mark#(X)) (mark#(from(X)) -> active#(from(mark(X))), active#(from(X)) -> mark#(cons(X, from(s(X))))) (mark#(from(X)) -> active#(from(mark(X))), active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y))))) (mark#(tail(X)) -> active#(tail(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))))) (mark#(tail(X)) -> active#(tail(mark(X))), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(tail(X)) -> active#(tail(mark(X))), active#(if(true(), X, Y)) -> mark#(X)) (mark#(tail(X)) -> active#(tail(mark(X))), active#(tail(cons(X, Y))) -> mark#(Y)) (mark#(tail(X)) -> active#(tail(mark(X))), active#(head(cons(X, Y))) -> mark#(X)) (mark#(tail(X)) -> active#(tail(mark(X))), active#(from(X)) -> mark#(cons(X, from(s(X))))) (mark#(tail(X)) -> active#(tail(mark(X))), active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y))))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(filter(X1, X2)) -> mark#(X2)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(filter(X1, X2)) -> mark#(X1)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(divides(X1, X2)) -> mark#(X2)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(divides(X1, X2)) -> mark#(X1)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(tail(X)) -> mark#(X)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(head(X)) -> active#(head(mark(X)))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(head(X)) -> mark#(X)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(primes()) -> active#(primes())) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X)))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(from(X)) -> mark#(X)) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(if(X1, X2, X3)) -> mark#(X1), mark#(sieve(X)) -> mark#(X)) (mark#(filter(X1, X2)) -> mark#(X1), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (mark#(filter(X1, X2)) -> mark#(X1), mark#(filter(X1, X2)) -> mark#(X2)) (mark#(filter(X1, X2)) -> mark#(X1), mark#(filter(X1, X2)) -> mark#(X1)) (mark#(filter(X1, X2)) -> mark#(X1), mark#(divides(X1, X2)) -> mark#(X2)) (mark#(filter(X1, X2)) -> mark#(X1), mark#(divides(X1, X2)) -> mark#(X1)) (mark#(filter(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(filter(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(filter(X1, X2)) -> mark#(X1), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(filter(X1, X2)) -> mark#(X1), mark#(tail(X)) -> mark#(X)) (mark#(filter(X1, X2)) -> mark#(X1), mark#(head(X)) -> active#(head(mark(X)))) (mark#(filter(X1, X2)) -> mark#(X1), mark#(head(X)) -> mark#(X)) (mark#(filter(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(filter(X1, X2)) -> mark#(X1), mark#(primes()) -> active#(primes())) (mark#(filter(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(filter(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X)))) (mark#(filter(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X)) (mark#(filter(X1, X2)) -> mark#(X1), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(filter(X1, X2)) -> mark#(X1), mark#(sieve(X)) -> mark#(X)) (mark#(from(X)) -> mark#(X), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (mark#(from(X)) -> mark#(X), mark#(filter(X1, X2)) -> mark#(X2)) (mark#(from(X)) -> mark#(X), mark#(filter(X1, X2)) -> mark#(X1)) (mark#(from(X)) -> mark#(X), mark#(divides(X1, X2)) -> mark#(X2)) (mark#(from(X)) -> mark#(X), mark#(divides(X1, X2)) -> mark#(X1)) (mark#(from(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(from(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(from(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(from(X)) -> mark#(X), mark#(tail(X)) -> mark#(X)) (mark#(from(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(from(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(from(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(from(X)) -> mark#(X), mark#(primes()) -> active#(primes())) (mark#(from(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(from(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X)))) (mark#(from(X)) -> mark#(X), mark#(from(X)) -> mark#(X)) (mark#(from(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(from(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (mark#(head(X)) -> mark#(X), mark#(filter(X1, X2)) -> mark#(X2)) (mark#(head(X)) -> mark#(X), mark#(filter(X1, X2)) -> mark#(X1)) (mark#(head(X)) -> mark#(X), mark#(divides(X1, X2)) -> mark#(X2)) (mark#(head(X)) -> mark#(X), mark#(divides(X1, X2)) -> mark#(X1)) (mark#(head(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(head(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(head(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(head(X)) -> mark#(X), mark#(tail(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(head(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(head(X)) -> mark#(X), mark#(primes()) -> active#(primes())) (mark#(head(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X)))) (mark#(head(X)) -> mark#(X), mark#(from(X)) -> mark#(X)) (mark#(head(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(head(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X)) (active#(head(cons(X, Y))) -> mark#(X), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (active#(head(cons(X, Y))) -> mark#(X), mark#(filter(X1, X2)) -> mark#(X2)) (active#(head(cons(X, Y))) -> mark#(X), mark#(filter(X1, X2)) -> mark#(X1)) (active#(head(cons(X, Y))) -> mark#(X), mark#(divides(X1, X2)) -> mark#(X2)) (active#(head(cons(X, Y))) -> mark#(X), mark#(divides(X1, X2)) -> mark#(X1)) (active#(head(cons(X, Y))) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(head(cons(X, Y))) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(head(cons(X, Y))) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X)))) (active#(head(cons(X, Y))) -> mark#(X), mark#(tail(X)) -> mark#(X)) (active#(head(cons(X, Y))) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (active#(head(cons(X, Y))) -> mark#(X), mark#(head(X)) -> mark#(X)) (active#(head(cons(X, Y))) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (active#(head(cons(X, Y))) -> mark#(X), mark#(primes()) -> active#(primes())) (active#(head(cons(X, Y))) -> mark#(X), mark#(s(X)) -> mark#(X)) (active#(head(cons(X, Y))) -> mark#(X), mark#(from(X)) -> active#(from(mark(X)))) (active#(head(cons(X, Y))) -> mark#(X), mark#(from(X)) -> mark#(X)) (active#(head(cons(X, Y))) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(head(cons(X, Y))) -> mark#(X), mark#(sieve(X)) -> mark#(X)) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(filter(X1, X2)) -> mark#(X2)) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(filter(X1, X2)) -> mark#(X1)) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(divides(X1, X2)) -> mark#(X2)) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(divides(X1, X2)) -> mark#(X1)) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(tail(X)) -> active#(tail(mark(X)))) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(tail(X)) -> mark#(X)) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(head(X)) -> active#(head(mark(X)))) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(head(X)) -> mark#(X)) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(s(X)) -> mark#(X)) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(from(X)) -> active#(from(mark(X)))) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(from(X)) -> mark#(X)) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), mark#(sieve(X)) -> mark#(X)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(filter(X1, X2)) -> mark#(X2)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(filter(X1, X2)) -> mark#(X1)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(divides(X1, X2)) -> mark#(X2)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(divides(X1, X2)) -> mark#(X1)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(tail(X)) -> active#(tail(mark(X)))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(tail(X)) -> mark#(X)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(head(X)) -> active#(head(mark(X)))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(head(X)) -> mark#(X)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(cons(X1, X2)) -> mark#(X1)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(s(X)) -> mark#(X)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(from(X)) -> active#(from(mark(X)))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(from(X)) -> mark#(X)) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(from(X)) -> mark#(cons(X, from(s(X)))), mark#(sieve(X)) -> mark#(X)) (mark#(filter(X1, X2)) -> mark#(X2), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (mark#(filter(X1, X2)) -> mark#(X2), mark#(filter(X1, X2)) -> mark#(X2)) (mark#(filter(X1, X2)) -> mark#(X2), mark#(filter(X1, X2)) -> mark#(X1)) (mark#(filter(X1, X2)) -> mark#(X2), mark#(divides(X1, X2)) -> mark#(X2)) (mark#(filter(X1, X2)) -> mark#(X2), mark#(divides(X1, X2)) -> mark#(X1)) (mark#(filter(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(filter(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(filter(X1, X2)) -> mark#(X2), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(filter(X1, X2)) -> mark#(X2), mark#(tail(X)) -> mark#(X)) (mark#(filter(X1, X2)) -> mark#(X2), mark#(head(X)) -> active#(head(mark(X)))) (mark#(filter(X1, X2)) -> mark#(X2), mark#(head(X)) -> mark#(X)) (mark#(filter(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(filter(X1, X2)) -> mark#(X2), mark#(primes()) -> active#(primes())) (mark#(filter(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X)) (mark#(filter(X1, X2)) -> mark#(X2), mark#(from(X)) -> active#(from(mark(X)))) (mark#(filter(X1, X2)) -> mark#(X2), mark#(from(X)) -> mark#(X)) (mark#(filter(X1, X2)) -> mark#(X2), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(filter(X1, X2)) -> mark#(X2), mark#(sieve(X)) -> mark#(X)) (mark#(divides(X1, X2)) -> mark#(X2), mark#(sieve(X)) -> mark#(X)) (mark#(divides(X1, X2)) -> mark#(X2), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(divides(X1, X2)) -> mark#(X2), mark#(from(X)) -> mark#(X)) (mark#(divides(X1, X2)) -> mark#(X2), mark#(from(X)) -> active#(from(mark(X)))) (mark#(divides(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X)) (mark#(divides(X1, X2)) -> mark#(X2), mark#(primes()) -> active#(primes())) (mark#(divides(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(divides(X1, X2)) -> mark#(X2), mark#(head(X)) -> mark#(X)) (mark#(divides(X1, X2)) -> mark#(X2), mark#(head(X)) -> active#(head(mark(X)))) (mark#(divides(X1, X2)) -> mark#(X2), mark#(tail(X)) -> mark#(X)) (mark#(divides(X1, X2)) -> mark#(X2), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(divides(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(divides(X1, X2)) -> mark#(X2), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(divides(X1, X2)) -> mark#(X2), mark#(divides(X1, X2)) -> mark#(X1)) (mark#(divides(X1, X2)) -> mark#(X2), mark#(divides(X1, X2)) -> mark#(X2)) (mark#(divides(X1, X2)) -> mark#(X2), mark#(filter(X1, X2)) -> mark#(X1)) (mark#(divides(X1, X2)) -> mark#(X2), mark#(filter(X1, X2)) -> mark#(X2)) (mark#(divides(X1, X2)) -> mark#(X2), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y))))) (mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(from(X)) -> mark#(cons(X, from(s(X))))) (mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(head(cons(X, Y))) -> mark#(X)) (mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(tail(cons(X, Y))) -> mark#(Y)) (mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(if(true(), X, Y)) -> mark#(X)) (mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))))) (active#(if(true(), X, Y)) -> mark#(X), mark#(sieve(X)) -> mark#(X)) (active#(if(true(), X, Y)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(if(true(), X, Y)) -> mark#(X), mark#(from(X)) -> mark#(X)) (active#(if(true(), X, Y)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X)))) (active#(if(true(), X, Y)) -> mark#(X), mark#(s(X)) -> mark#(X)) (active#(if(true(), X, Y)) -> mark#(X), mark#(primes()) -> active#(primes())) (active#(if(true(), X, Y)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (active#(if(true(), X, Y)) -> mark#(X), mark#(head(X)) -> mark#(X)) (active#(if(true(), X, Y)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (active#(if(true(), X, Y)) -> mark#(X), mark#(tail(X)) -> mark#(X)) (active#(if(true(), X, Y)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X)))) (active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(if(true(), X, Y)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(if(true(), X, Y)) -> mark#(X), mark#(divides(X1, X2)) -> mark#(X1)) (active#(if(true(), X, Y)) -> mark#(X), mark#(divides(X1, X2)) -> mark#(X2)) (active#(if(true(), X, Y)) -> mark#(X), mark#(filter(X1, X2)) -> mark#(X1)) (active#(if(true(), X, Y)) -> mark#(X), mark#(filter(X1, X2)) -> mark#(X2)) (active#(if(true(), X, Y)) -> mark#(X), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (mark#(tail(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X)) (mark#(tail(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(tail(X)) -> mark#(X), mark#(from(X)) -> mark#(X)) (mark#(tail(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X)))) (mark#(tail(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(tail(X)) -> mark#(X), mark#(primes()) -> active#(primes())) (mark#(tail(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(tail(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(tail(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(tail(X)) -> mark#(X), mark#(tail(X)) -> mark#(X)) (mark#(tail(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(tail(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(tail(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(tail(X)) -> mark#(X), mark#(divides(X1, X2)) -> mark#(X1)) (mark#(tail(X)) -> mark#(X), mark#(divides(X1, X2)) -> mark#(X2)) (mark#(tail(X)) -> mark#(X), mark#(filter(X1, X2)) -> mark#(X1)) (mark#(tail(X)) -> mark#(X), mark#(filter(X1, X2)) -> mark#(X2)) (mark#(tail(X)) -> mark#(X), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (mark#(s(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(from(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(primes()) -> active#(primes())) (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(tail(X)) -> mark#(X)) (mark#(s(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(s(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(s(X)) -> mark#(X), mark#(divides(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(divides(X1, X2)) -> mark#(X2)) (mark#(s(X)) -> mark#(X), mark#(filter(X1, X2)) -> mark#(X1)) (mark#(s(X)) -> mark#(X), mark#(filter(X1, X2)) -> mark#(X2)) (mark#(s(X)) -> mark#(X), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> mark#(X)) (mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(sieve(X)) -> mark#(X), mark#(from(X)) -> mark#(X)) (mark#(sieve(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X)))) (mark#(sieve(X)) -> mark#(X), mark#(s(X)) -> mark#(X)) (mark#(sieve(X)) -> mark#(X), mark#(primes()) -> active#(primes())) (mark#(sieve(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(sieve(X)) -> mark#(X), mark#(head(X)) -> mark#(X)) (mark#(sieve(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X)))) (mark#(sieve(X)) -> mark#(X), mark#(tail(X)) -> mark#(X)) (mark#(sieve(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(sieve(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(sieve(X)) -> mark#(X), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(sieve(X)) -> mark#(X), mark#(divides(X1, X2)) -> mark#(X1)) (mark#(sieve(X)) -> mark#(X), mark#(divides(X1, X2)) -> mark#(X2)) (mark#(sieve(X)) -> mark#(X), mark#(filter(X1, X2)) -> mark#(X1)) (mark#(sieve(X)) -> mark#(X), mark#(filter(X1, X2)) -> mark#(X2)) (mark#(sieve(X)) -> mark#(X), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (mark#(divides(X1, X2)) -> mark#(X1), mark#(sieve(X)) -> mark#(X)) (mark#(divides(X1, X2)) -> mark#(X1), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(divides(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X)) (mark#(divides(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X)))) (mark#(divides(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(divides(X1, X2)) -> mark#(X1), mark#(primes()) -> active#(primes())) (mark#(divides(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(divides(X1, X2)) -> mark#(X1), mark#(head(X)) -> mark#(X)) (mark#(divides(X1, X2)) -> mark#(X1), mark#(head(X)) -> active#(head(mark(X)))) (mark#(divides(X1, X2)) -> mark#(X1), mark#(tail(X)) -> mark#(X)) (mark#(divides(X1, X2)) -> mark#(X1), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(divides(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(divides(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(divides(X1, X2)) -> mark#(X1), mark#(divides(X1, X2)) -> mark#(X1)) (mark#(divides(X1, X2)) -> mark#(X1), mark#(divides(X1, X2)) -> mark#(X2)) (mark#(divides(X1, X2)) -> mark#(X1), mark#(filter(X1, X2)) -> mark#(X1)) (mark#(divides(X1, X2)) -> mark#(X1), mark#(filter(X1, X2)) -> mark#(X2)) (mark#(divides(X1, X2)) -> mark#(X1), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sieve(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(sieve(X)) -> active#(sieve(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> active#(from(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(primes()) -> active#(primes())) (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(head(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(head(X)) -> active#(head(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(tail(X)) -> mark#(X)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(tail(X)) -> active#(tail(mark(X)))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (mark#(cons(X1, X2)) -> mark#(X1), mark#(divides(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(divides(X1, X2)) -> mark#(X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(filter(X1, X2)) -> mark#(X1)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(filter(X1, X2)) -> mark#(X2)) (mark#(cons(X1, X2)) -> mark#(X1), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (mark#(head(X)) -> active#(head(mark(X))), active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y))))) (mark#(head(X)) -> active#(head(mark(X))), active#(from(X)) -> mark#(cons(X, from(s(X))))) (mark#(head(X)) -> active#(head(mark(X))), active#(head(cons(X, Y))) -> mark#(X)) (mark#(head(X)) -> active#(head(mark(X))), active#(tail(cons(X, Y))) -> mark#(Y)) (mark#(head(X)) -> active#(head(mark(X))), active#(if(true(), X, Y)) -> mark#(X)) (mark#(head(X)) -> active#(head(mark(X))), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(head(X)) -> active#(head(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y))))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(from(X)) -> mark#(cons(X, from(s(X))))) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(head(cons(X, Y))) -> mark#(X)) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(tail(cons(X, Y))) -> mark#(Y)) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(if(true(), X, Y)) -> mark#(X)) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(sieve(X)) -> active#(sieve(mark(X))), active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(sieve(X)) -> mark#(X)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(sieve(X)) -> active#(sieve(mark(X)))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(from(X)) -> mark#(X)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(from(X)) -> active#(from(mark(X)))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(s(X)) -> mark#(X)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(primes()) -> active#(primes())) (active#(if(false(), X, Y)) -> mark#(Y), mark#(cons(X1, X2)) -> mark#(X1)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(head(X)) -> mark#(X)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(head(X)) -> active#(head(mark(X)))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(tail(X)) -> mark#(X)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(tail(X)) -> active#(tail(mark(X)))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> mark#(X1)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3))) (active#(if(false(), X, Y)) -> mark#(Y), mark#(divides(X1, X2)) -> mark#(X1)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(divides(X1, X2)) -> mark#(X2)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(filter(X1, X2)) -> mark#(X1)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(filter(X1, X2)) -> mark#(X2)) (active#(if(false(), X, Y)) -> mark#(Y), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2)))) (mark#(primes()) -> active#(primes()), active#(primes()) -> mark#(sieve(from(s(s(0())))))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y))))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(from(X)) -> mark#(cons(X, from(s(X))))) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(head(cons(X, Y))) -> mark#(X)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(tail(cons(X, Y))) -> mark#(Y)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(true(), X, Y)) -> mark#(X)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(if(false(), X, Y)) -> mark#(Y)) (mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))))) } SCCS: Scc: { mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X))), mark#(from(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X))), mark#(s(X)) -> mark#(X), mark#(primes()) -> active#(primes()), mark#(cons(X1, X2)) -> mark#(X1), mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X))), mark#(tail(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X))), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), mark#(divides(X1, X2)) -> mark#(X1), mark#(divides(X1, X2)) -> mark#(X2), mark#(filter(X1, X2)) -> mark#(X1), mark#(filter(X1, X2)) -> mark#(X2), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), active#(from(X)) -> mark#(cons(X, from(s(X)))), active#(primes()) -> mark#(sieve(from(s(s(0()))))), active#(head(cons(X, Y))) -> mark#(X), active#(tail(cons(X, Y))) -> mark#(Y), active#(if(true(), X, Y)) -> mark#(X), active#(if(false(), X, Y)) -> mark#(Y), active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))))} SCC: Strict: { mark#(sieve(X)) -> mark#(X), mark#(sieve(X)) -> active#(sieve(mark(X))), mark#(from(X)) -> mark#(X), mark#(from(X)) -> active#(from(mark(X))), mark#(s(X)) -> mark#(X), mark#(primes()) -> active#(primes()), mark#(cons(X1, X2)) -> mark#(X1), mark#(head(X)) -> mark#(X), mark#(head(X)) -> active#(head(mark(X))), mark#(tail(X)) -> mark#(X), mark#(tail(X)) -> active#(tail(mark(X))), mark#(if(X1, X2, X3)) -> mark#(X1), mark#(if(X1, X2, X3)) -> active#(if(mark(X1), X2, X3)), mark#(divides(X1, X2)) -> mark#(X1), mark#(divides(X1, X2)) -> mark#(X2), mark#(filter(X1, X2)) -> mark#(X1), mark#(filter(X1, X2)) -> mark#(X2), mark#(filter(X1, X2)) -> active#(filter(mark(X1), mark(X2))), active#(sieve(cons(X, Y))) -> mark#(cons(X, filter(X, sieve(Y)))), active#(from(X)) -> mark#(cons(X, from(s(X)))), active#(primes()) -> mark#(sieve(from(s(s(0()))))), active#(head(cons(X, Y))) -> mark#(X), active#(tail(cons(X, Y))) -> mark#(Y), active#(if(true(), X, Y)) -> mark#(X), active#(if(false(), X, Y)) -> mark#(Y), active#(filter(s(s(X)), cons(Y, Z))) -> mark#(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y)))))} Weak: { mark(sieve(X)) -> active(sieve(mark(X))), mark(from(X)) -> active(from(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(0()) -> active(0()), mark(primes()) -> active(primes()), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(head(X)) -> active(head(mark(X))), mark(tail(X)) -> active(tail(mark(X))), mark(if(X1, X2, X3)) -> active(if(mark(X1), X2, X3)), mark(true()) -> active(true()), mark(false()) -> active(false()), mark(divides(X1, X2)) -> active(divides(mark(X1), mark(X2))), mark(filter(X1, X2)) -> active(filter(mark(X1), mark(X2))), sieve(mark(X)) -> sieve(X), sieve(active(X)) -> sieve(X), from(mark(X)) -> from(X), from(active(X)) -> from(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), active(sieve(cons(X, Y))) -> mark(cons(X, filter(X, sieve(Y)))), active(from(X)) -> mark(cons(X, from(s(X)))), active(primes()) -> mark(sieve(from(s(s(0()))))), active(head(cons(X, Y))) -> mark(X), active(tail(cons(X, Y))) -> mark(Y), active(if(true(), X, Y)) -> mark(X), active(if(false(), X, Y)) -> mark(Y), active(filter(s(s(X)), cons(Y, Z))) -> mark(if(divides(s(s(X)), Y), filter(s(s(X)), Z), cons(Y, filter(X, sieve(Y))))), cons(X1, mark(X2)) -> cons(X1, X2), cons(X1, active(X2)) -> cons(X1, X2), cons(mark(X1), X2) -> cons(X1, X2), cons(active(X1), X2) -> cons(X1, X2), head(mark(X)) -> head(X), head(active(X)) -> head(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), if(X1, X2, mark(X3)) -> if(X1, X2, X3), if(X1, X2, active(X3)) -> if(X1, X2, X3), if(X1, mark(X2), X3) -> if(X1, X2, X3), if(X1, active(X2), X3) -> if(X1, X2, X3), if(mark(X1), X2, X3) -> if(X1, X2, X3), if(active(X1), X2, X3) -> if(X1, X2, X3), divides(X1, mark(X2)) -> divides(X1, X2), divides(X1, active(X2)) -> divides(X1, X2), divides(mark(X1), X2) -> divides(X1, X2), divides(active(X1), X2) -> divides(X1, X2), filter(X1, mark(X2)) -> filter(X1, X2), filter(X1, active(X2)) -> filter(X1, X2), filter(mark(X1), X2) -> filter(X1, X2), filter(active(X1), X2) -> filter(X1, X2)} Fail