MAYBE

Problem:
 active(primes()) -> mark(sieve(from(s(s(0())))))
 active(from(X)) -> mark(cons(X,from(s(X))))
 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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
 mark(primes()) -> active(primes())
 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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
 mark(divides(X1,X2)) -> active(divides(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)
 cons(mark(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)
 head(mark(X)) -> head(X)
 head(active(X)) -> head(X)
 tail(mark(X)) -> tail(X)
 tail(active(X)) -> tail(X)
 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(active(X1),X2,X3) -> if(X1,X2,X3)
 if(X1,active(X2),X3) -> if(X1,X2,X3)
 if(X1,X2,active(X3)) -> if(X1,X2,X3)
 filter(mark(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)
 divides(mark(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)

Proof:
 DP Processor:
  DPs:
   active#(primes()) -> s#(0())
   active#(primes()) -> s#(s(0()))
   active#(primes()) -> from#(s(s(0())))
   active#(primes()) -> sieve#(from(s(s(0()))))
   active#(primes()) -> mark#(sieve(from(s(s(0())))))
   active#(from(X)) -> s#(X)
   active#(from(X)) -> from#(s(X))
   active#(from(X)) -> cons#(X,from(s(X)))
   active#(from(X)) -> mark#(cons(X,from(s(X))))
   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))) -> sieve#(Y)
   active#(filter(s(s(X)),cons(Y,Z))) -> filter#(X,sieve(Y))
   active#(filter(s(s(X)),cons(Y,Z))) -> cons#(Y,filter(X,sieve(Y)))
   active#(filter(s(s(X)),cons(Y,Z))) -> filter#(s(s(X)),Z)
   active#(filter(s(s(X)),cons(Y,Z))) -> divides#(s(s(X)),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))) ->
   mark#(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))))
   active#(sieve(cons(X,Y))) -> sieve#(Y)
   active#(sieve(cons(X,Y))) -> filter#(X,sieve(Y))
   active#(sieve(cons(X,Y))) -> cons#(X,filter(X,sieve(Y)))
   active#(sieve(cons(X,Y))) -> mark#(cons(X,filter(X,sieve(Y))))
   mark#(primes()) -> active#(primes())
   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#(cons(X1,X2)) -> mark#(X1)
   mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
   mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
   mark#(head(X)) -> mark#(X)
   mark#(head(X)) -> head#(mark(X))
   mark#(head(X)) -> active#(head(mark(X)))
   mark#(tail(X)) -> mark#(X)
   mark#(tail(X)) -> tail#(mark(X))
   mark#(tail(X)) -> active#(tail(mark(X)))
   mark#(if(X1,X2,X3)) -> mark#(X1)
   mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
   mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
   mark#(true()) -> active#(true())
   mark#(false()) -> active#(false())
   mark#(filter(X1,X2)) -> mark#(X2)
   mark#(filter(X1,X2)) -> mark#(X1)
   mark#(filter(X1,X2)) -> filter#(mark(X1),mark(X2))
   mark#(filter(X1,X2)) -> active#(filter(mark(X1),mark(X2)))
   mark#(divides(X1,X2)) -> mark#(X2)
   mark#(divides(X1,X2)) -> mark#(X1)
   mark#(divides(X1,X2)) -> divides#(mark(X1),mark(X2))
   mark#(divides(X1,X2)) -> active#(divides(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)
   cons#(mark(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)
   head#(mark(X)) -> head#(X)
   head#(active(X)) -> head#(X)
   tail#(mark(X)) -> tail#(X)
   tail#(active(X)) -> tail#(X)
   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#(active(X1),X2,X3) -> if#(X1,X2,X3)
   if#(X1,active(X2),X3) -> if#(X1,X2,X3)
   if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
   filter#(mark(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)
   divides#(mark(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)
  TRS:
   active(primes()) -> mark(sieve(from(s(s(0())))))
   active(from(X)) -> mark(cons(X,from(s(X))))
   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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
   mark(primes()) -> active(primes())
   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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
   mark(divides(X1,X2)) -> active(divides(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)
   cons(mark(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)
   head(mark(X)) -> head(X)
   head(active(X)) -> head(X)
   tail(mark(X)) -> tail(X)
   tail(active(X)) -> tail(X)
   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(active(X1),X2,X3) -> if(X1,X2,X3)
   if(X1,active(X2),X3) -> if(X1,X2,X3)
   if(X1,X2,active(X3)) -> if(X1,X2,X3)
   filter(mark(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)
   divides(mark(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)
  TDG Processor:
   DPs:
    active#(primes()) -> s#(0())
    active#(primes()) -> s#(s(0()))
    active#(primes()) -> from#(s(s(0())))
    active#(primes()) -> sieve#(from(s(s(0()))))
    active#(primes()) -> mark#(sieve(from(s(s(0())))))
    active#(from(X)) -> s#(X)
    active#(from(X)) -> from#(s(X))
    active#(from(X)) -> cons#(X,from(s(X)))
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    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))) -> sieve#(Y)
    active#(filter(s(s(X)),cons(Y,Z))) -> filter#(X,sieve(Y))
    active#(filter(s(s(X)),cons(Y,Z))) -> cons#(Y,filter(X,sieve(Y)))
    active#(filter(s(s(X)),cons(Y,Z))) -> filter#(s(s(X)),Z)
    active#(filter(s(s(X)),cons(Y,Z))) -> divides#(s(s(X)),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))) ->
    mark#(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))))
    active#(sieve(cons(X,Y))) -> sieve#(Y)
    active#(sieve(cons(X,Y))) -> filter#(X,sieve(Y))
    active#(sieve(cons(X,Y))) -> cons#(X,filter(X,sieve(Y)))
    active#(sieve(cons(X,Y))) -> mark#(cons(X,filter(X,sieve(Y))))
    mark#(primes()) -> active#(primes())
    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#(cons(X1,X2)) -> mark#(X1)
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(head(X)) -> mark#(X)
    mark#(head(X)) -> head#(mark(X))
    mark#(head(X)) -> active#(head(mark(X)))
    mark#(tail(X)) -> mark#(X)
    mark#(tail(X)) -> tail#(mark(X))
    mark#(tail(X)) -> active#(tail(mark(X)))
    mark#(if(X1,X2,X3)) -> mark#(X1)
    mark#(if(X1,X2,X3)) -> if#(mark(X1),X2,X3)
    mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
    mark#(true()) -> active#(true())
    mark#(false()) -> active#(false())
    mark#(filter(X1,X2)) -> mark#(X2)
    mark#(filter(X1,X2)) -> mark#(X1)
    mark#(filter(X1,X2)) -> filter#(mark(X1),mark(X2))
    mark#(filter(X1,X2)) -> active#(filter(mark(X1),mark(X2)))
    mark#(divides(X1,X2)) -> mark#(X2)
    mark#(divides(X1,X2)) -> mark#(X1)
    mark#(divides(X1,X2)) -> divides#(mark(X1),mark(X2))
    mark#(divides(X1,X2)) -> active#(divides(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)
    cons#(mark(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)
    head#(mark(X)) -> head#(X)
    head#(active(X)) -> head#(X)
    tail#(mark(X)) -> tail#(X)
    tail#(active(X)) -> tail#(X)
    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#(active(X1),X2,X3) -> if#(X1,X2,X3)
    if#(X1,active(X2),X3) -> if#(X1,X2,X3)
    if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
    filter#(mark(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)
    divides#(mark(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)
   TRS:
    active(primes()) -> mark(sieve(from(s(s(0())))))
    active(from(X)) -> mark(cons(X,from(s(X))))
    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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
    mark(primes()) -> active(primes())
    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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
    mark(divides(X1,X2)) -> active(divides(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)
    cons(mark(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)
    head(mark(X)) -> head(X)
    head(active(X)) -> head(X)
    tail(mark(X)) -> tail(X)
    tail(active(X)) -> tail(X)
    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(active(X1),X2,X3) -> if(X1,X2,X3)
    if(X1,active(X2),X3) -> if(X1,X2,X3)
    if(X1,X2,active(X3)) -> if(X1,X2,X3)
    filter(mark(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)
    divides(mark(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)
   graph:
    ...
   SCC Processor:
    #sccs: 10
    #rules: 60
    #arcs: 1121/7225
    DPs:
     mark#(divides(X1,X2)) -> mark#(X2)
     mark#(primes()) -> active#(primes())
     active#(primes()) -> mark#(sieve(from(s(s(0())))))
     mark#(sieve(X)) -> mark#(X)
     mark#(sieve(X)) -> active#(sieve(mark(X)))
     active#(from(X)) -> mark#(cons(X,from(s(X))))
     mark#(from(X)) -> mark#(X)
     mark#(from(X)) -> active#(from(mark(X)))
     active#(head(cons(X,Y))) -> mark#(X)
     mark#(s(X)) -> mark#(X)
     mark#(s(X)) -> active#(s(mark(X)))
     active#(tail(cons(X,Y))) -> mark#(Y)
     mark#(0()) -> active#(0())
     active#(if(true(),X,Y)) -> mark#(X)
     mark#(cons(X1,X2)) -> mark#(X1)
     mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
     active#(if(false(),X,Y)) -> mark#(Y)
     mark#(head(X)) -> mark#(X)
     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#(tail(X)) -> mark#(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#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
     mark#(true()) -> active#(true())
     mark#(false()) -> active#(false())
     mark#(filter(X1,X2)) -> mark#(X2)
     mark#(filter(X1,X2)) -> mark#(X1)
     mark#(filter(X1,X2)) -> active#(filter(mark(X1),mark(X2)))
     mark#(divides(X1,X2)) -> mark#(X1)
     mark#(divides(X1,X2)) -> active#(divides(mark(X1),mark(X2)))
    TRS:
     active(primes()) -> mark(sieve(from(s(s(0())))))
     active(from(X)) -> mark(cons(X,from(s(X))))
     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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
     mark(primes()) -> active(primes())
     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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
     mark(divides(X1,X2)) -> active(divides(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)
     cons(mark(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)
     head(mark(X)) -> head(X)
     head(active(X)) -> head(X)
     tail(mark(X)) -> tail(X)
     tail(active(X)) -> tail(X)
     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(active(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,active(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,active(X3)) -> if(X1,X2,X3)
     filter(mark(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)
     divides(mark(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)
    EDG Processor:
     DPs:
      mark#(divides(X1,X2)) -> mark#(X2)
      mark#(primes()) -> active#(primes())
      active#(primes()) -> mark#(sieve(from(s(s(0())))))
      mark#(sieve(X)) -> mark#(X)
      mark#(sieve(X)) -> active#(sieve(mark(X)))
      active#(from(X)) -> mark#(cons(X,from(s(X))))
      mark#(from(X)) -> mark#(X)
      mark#(from(X)) -> active#(from(mark(X)))
      active#(head(cons(X,Y))) -> mark#(X)
      mark#(s(X)) -> mark#(X)
      mark#(s(X)) -> active#(s(mark(X)))
      active#(tail(cons(X,Y))) -> mark#(Y)
      mark#(0()) -> active#(0())
      active#(if(true(),X,Y)) -> mark#(X)
      mark#(cons(X1,X2)) -> mark#(X1)
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      active#(if(false(),X,Y)) -> mark#(Y)
      mark#(head(X)) -> mark#(X)
      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#(tail(X)) -> mark#(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#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      mark#(true()) -> active#(true())
      mark#(false()) -> active#(false())
      mark#(filter(X1,X2)) -> mark#(X2)
      mark#(filter(X1,X2)) -> mark#(X1)
      mark#(filter(X1,X2)) -> active#(filter(mark(X1),mark(X2)))
      mark#(divides(X1,X2)) -> mark#(X1)
      mark#(divides(X1,X2)) -> active#(divides(mark(X1),mark(X2)))
     TRS:
      active(primes()) -> mark(sieve(from(s(s(0())))))
      active(from(X)) -> mark(cons(X,from(s(X))))
      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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
      mark(primes()) -> active(primes())
      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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
      mark(divides(X1,X2)) -> active(divides(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)
      cons(mark(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)
      head(mark(X)) -> head(X)
      head(active(X)) -> head(X)
      tail(mark(X)) -> tail(X)
      tail(active(X)) -> tail(X)
      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(active(X1),X2,X3) -> if(X1,X2,X3)
      if(X1,active(X2),X3) -> if(X1,X2,X3)
      if(X1,X2,active(X3)) -> if(X1,X2,X3)
      filter(mark(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)
      divides(mark(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)
     graph:
      mark#(divides(X1,X2)) -> mark#(X2) ->
      mark#(primes()) -> active#(primes())
      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#(s(X)) -> active#(s(mark(X)))
      mark#(divides(X1,X2)) -> mark#(X2) ->
      mark#(0()) -> active#(0())
      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#(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#(true()) -> active#(true())
      mark#(divides(X1,X2)) -> mark#(X2) ->
      mark#(false()) -> active#(false())
      mark#(divides(X1,X2)) -> mark#(X2) ->
      mark#(filter(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)) -> active#(filter(mark(X1),mark(X2)))
      mark#(divides(X1,X2)) -> mark#(X2) ->
      mark#(divides(X1,X2)) -> mark#(X2)
      mark#(divides(X1,X2)) -> mark#(X2) ->
      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)) -> mark#(X1) ->
      mark#(primes()) -> active#(primes())
      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#(s(X)) -> active#(s(mark(X)))
      mark#(divides(X1,X2)) -> mark#(X1) ->
      mark#(0()) -> active#(0())
      mark#(divides(X1,X2)) -> mark#(X1) ->
      mark#(cons(X1,X2)) -> mark#(X1)
      mark#(divides(X1,X2)) -> mark#(X1) ->
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      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#(true()) -> active#(true())
      mark#(divides(X1,X2)) -> mark#(X1) ->
      mark#(false()) -> active#(false())
      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#(filter(X1,X2)) -> active#(filter(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#(divides(X1,X2)) -> active#(divides(mark(X1),mark(X2)))
      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#(head(cons(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#(if(true(),X,Y)) -> mark#(X)
      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#(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#(sieve(cons(X,Y))) -> mark#(cons(X,filter(X,sieve(Y))))
      mark#(filter(X1,X2)) -> mark#(X2) ->
      mark#(primes()) -> active#(primes())
      mark#(filter(X1,X2)) -> mark#(X2) ->
      mark#(sieve(X)) -> mark#(X)
      mark#(filter(X1,X2)) -> mark#(X2) ->
      mark#(sieve(X)) -> active#(sieve(mark(X)))
      mark#(filter(X1,X2)) -> mark#(X2) ->
      mark#(from(X)) -> mark#(X)
      mark#(filter(X1,X2)) -> mark#(X2) ->
      mark#(from(X)) -> active#(from(mark(X)))
      mark#(filter(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> mark#(X)
      mark#(filter(X1,X2)) -> mark#(X2) ->
      mark#(s(X)) -> active#(s(mark(X)))
      mark#(filter(X1,X2)) -> mark#(X2) ->
      mark#(0()) -> active#(0())
      mark#(filter(X1,X2)) -> mark#(X2) ->
      mark#(cons(X1,X2)) -> mark#(X1)
      mark#(filter(X1,X2)) -> mark#(X2) ->
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      mark#(filter(X1,X2)) -> mark#(X2) ->
      mark#(head(X)) -> mark#(X)
      mark#(filter(X1,X2)) -> mark#(X2) ->
      mark#(head(X)) -> active#(head(mark(X)))
      mark#(filter(X1,X2)) -> mark#(X2) ->
      mark#(tail(X)) -> mark#(X)
      mark#(filter(X1,X2)) -> mark#(X2) ->
      mark#(tail(X)) -> active#(tail(mark(X)))
      mark#(filter(X1,X2)) -> mark#(X2) ->
      mark#(if(X1,X2,X3)) -> 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#(true()) -> active#(true())
      mark#(filter(X1,X2)) -> mark#(X2) ->
      mark#(false()) -> active#(false())
      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#(filter(X1,X2)) -> active#(filter(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#(divides(X1,X2)) -> active#(divides(mark(X1),mark(X2)))
      mark#(filter(X1,X2)) -> mark#(X1) ->
      mark#(primes()) -> active#(primes())
      mark#(filter(X1,X2)) -> mark#(X1) ->
      mark#(sieve(X)) -> 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)) -> active#(from(mark(X)))
      mark#(filter(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> 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#(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#(head(X)) -> mark#(X)
      mark#(filter(X1,X2)) -> mark#(X1) ->
      mark#(head(X)) -> active#(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#(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#(true()) -> active#(true())
      mark#(filter(X1,X2)) -> mark#(X1) ->
      mark#(false()) -> active#(false())
      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#(filter(X1,X2)) -> active#(filter(mark(X1),mark(X2)))
      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#(divides(X1,X2)) -> active#(divides(mark(X1),mark(X2)))
      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)))))
      mark#(filter(X1,X2)) -> active#(filter(mark(X1),mark(X2))) ->
      active#(sieve(cons(X,Y))) -> mark#(cons(X,filter(X,sieve(Y))))
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(primes()) -> active#(primes())
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(sieve(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#(from(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#(s(X)) -> 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#(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#(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#(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#(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#(true()) -> active#(true())
      mark#(if(X1,X2,X3)) -> mark#(X1) ->
      mark#(false()) -> active#(false())
      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#(filter(X1,X2)) -> active#(filter(mark(X1),mark(X2)))
      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#(divides(X1,X2)) -> active#(divides(mark(X1),mark(X2)))
      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)))))
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3)) ->
      active#(sieve(cons(X,Y))) -> mark#(cons(X,filter(X,sieve(Y))))
      mark#(tail(X)) -> mark#(X) -> mark#(primes()) -> active#(primes())
      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#(s(X)) -> active#(s(mark(X)))
      mark#(tail(X)) -> mark#(X) -> mark#(0()) -> active#(0())
      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#(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#(true()) -> active#(true())
      mark#(tail(X)) -> mark#(X) -> mark#(false()) -> active#(false())
      mark#(tail(X)) -> mark#(X) -> mark#(filter(X1,X2)) -> mark#(X2)
      mark#(tail(X)) -> mark#(X) -> mark#(filter(X1,X2)) -> mark#(X1)
      mark#(tail(X)) -> mark#(X) ->
      mark#(filter(X1,X2)) -> active#(filter(mark(X1),mark(X2)))
      mark#(tail(X)) -> mark#(X) -> mark#(divides(X1,X2)) -> mark#(X2)
      mark#(tail(X)) -> mark#(X) -> mark#(divides(X1,X2)) -> mark#(X1)
      mark#(tail(X)) -> mark#(X) ->
      mark#(divides(X1,X2)) -> active#(divides(mark(X1),mark(X2)))
      mark#(tail(X)) -> active#(tail(mark(X))) ->
      active#(from(X)) -> mark#(cons(X,from(s(X))))
      mark#(tail(X)) -> active#(tail(mark(X))) ->
      active#(head(cons(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#(if(true(),X,Y)) -> mark#(X)
      mark#(tail(X)) -> active#(tail(mark(X))) ->
      active#(if(false(),X,Y)) -> mark#(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#(sieve(cons(X,Y))) -> mark#(cons(X,filter(X,sieve(Y))))
      mark#(head(X)) -> mark#(X) -> mark#(primes()) -> active#(primes())
      mark#(head(X)) -> mark#(X) -> mark#(sieve(X)) -> mark#(X)
      mark#(head(X)) -> mark#(X) ->
      mark#(sieve(X)) -> active#(sieve(mark(X)))
      mark#(head(X)) -> mark#(X) -> mark#(from(X)) -> mark#(X)
      mark#(head(X)) -> mark#(X) ->
      mark#(from(X)) -> active#(from(mark(X)))
      mark#(head(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
      mark#(head(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
      mark#(head(X)) -> mark#(X) -> mark#(0()) -> active#(0())
      mark#(head(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
      mark#(head(X)) -> mark#(X) ->
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      mark#(head(X)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
      mark#(head(X)) -> mark#(X) ->
      mark#(head(X)) -> active#(head(mark(X)))
      mark#(head(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
      mark#(head(X)) -> mark#(X) ->
      mark#(tail(X)) -> active#(tail(mark(X)))
      mark#(head(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1)
      mark#(head(X)) -> mark#(X) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      mark#(head(X)) -> mark#(X) -> mark#(true()) -> active#(true())
      mark#(head(X)) -> mark#(X) -> mark#(false()) -> active#(false())
      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#(filter(X1,X2)) -> active#(filter(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#(divides(X1,X2)) -> active#(divides(mark(X1),mark(X2)))
      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#(head(X)) -> active#(head(mark(X))) ->
      active#(sieve(cons(X,Y))) -> mark#(cons(X,filter(X,sieve(Y))))
      mark#(cons(X1,X2)) -> mark#(X1) ->
      mark#(primes()) -> active#(primes())
      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#(s(X)) -> active#(s(mark(X)))
      mark#(cons(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
      mark#(cons(X1,X2)) -> mark#(X1) ->
      mark#(cons(X1,X2)) -> mark#(X1)
      mark#(cons(X1,X2)) -> mark#(X1) ->
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      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#(true()) -> active#(true())
      mark#(cons(X1,X2)) -> mark#(X1) ->
      mark#(false()) -> active#(false())
      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#(filter(X1,X2)) -> active#(filter(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#(divides(X1,X2)) -> active#(divides(mark(X1),mark(X2)))
      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#(head(cons(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#(if(true(),X,Y)) -> mark#(X)
      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#(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#(sieve(cons(X,Y))) -> mark#(cons(X,filter(X,sieve(Y))))
      mark#(sieve(X)) -> mark#(X) ->
      mark#(primes()) -> active#(primes())
      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#(s(X)) -> active#(s(mark(X)))
      mark#(sieve(X)) -> mark#(X) -> mark#(0()) -> active#(0())
      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#(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#(true()) -> active#(true())
      mark#(sieve(X)) -> mark#(X) -> mark#(false()) -> active#(false())
      mark#(sieve(X)) -> mark#(X) -> mark#(filter(X1,X2)) -> mark#(X2)
      mark#(sieve(X)) -> mark#(X) -> mark#(filter(X1,X2)) -> mark#(X1)
      mark#(sieve(X)) -> mark#(X) ->
      mark#(filter(X1,X2)) -> active#(filter(mark(X1),mark(X2)))
      mark#(sieve(X)) -> mark#(X) -> mark#(divides(X1,X2)) -> mark#(X2)
      mark#(sieve(X)) -> mark#(X) -> mark#(divides(X1,X2)) -> mark#(X1)
      mark#(sieve(X)) -> mark#(X) ->
      mark#(divides(X1,X2)) -> active#(divides(mark(X1),mark(X2)))
      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)))))
      mark#(sieve(X)) -> active#(sieve(mark(X))) ->
      active#(sieve(cons(X,Y))) -> mark#(cons(X,filter(X,sieve(Y))))
      mark#(from(X)) -> mark#(X) -> mark#(primes()) -> active#(primes())
      mark#(from(X)) -> mark#(X) -> mark#(sieve(X)) -> mark#(X)
      mark#(from(X)) -> mark#(X) ->
      mark#(sieve(X)) -> active#(sieve(mark(X)))
      mark#(from(X)) -> mark#(X) -> mark#(from(X)) -> mark#(X)
      mark#(from(X)) -> mark#(X) ->
      mark#(from(X)) -> active#(from(mark(X)))
      mark#(from(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
      mark#(from(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
      mark#(from(X)) -> mark#(X) -> mark#(0()) -> active#(0())
      mark#(from(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
      mark#(from(X)) -> mark#(X) ->
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      mark#(from(X)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
      mark#(from(X)) -> mark#(X) ->
      mark#(head(X)) -> active#(head(mark(X)))
      mark#(from(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
      mark#(from(X)) -> mark#(X) ->
      mark#(tail(X)) -> active#(tail(mark(X)))
      mark#(from(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1)
      mark#(from(X)) -> mark#(X) ->
      mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
      mark#(from(X)) -> mark#(X) -> mark#(true()) -> active#(true())
      mark#(from(X)) -> mark#(X) -> mark#(false()) -> active#(false())
      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#(filter(X1,X2)) -> active#(filter(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#(divides(X1,X2)) -> active#(divides(mark(X1),mark(X2)))
      mark#(from(X)) -> active#(from(mark(X))) ->
      active#(from(X)) -> mark#(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#(sieve(cons(X,Y))) -> mark#(cons(X,filter(X,sieve(Y))))
      mark#(s(X)) -> mark#(X) -> mark#(primes()) -> active#(primes())
      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#(s(X)) -> active#(s(mark(X)))
      mark#(s(X)) -> mark#(X) -> mark#(0()) -> active#(0())
      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#(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#(true()) -> active#(true())
      mark#(s(X)) -> mark#(X) -> mark#(false()) -> active#(false())
      mark#(s(X)) -> mark#(X) -> mark#(filter(X1,X2)) -> mark#(X2)
      mark#(s(X)) -> mark#(X) -> mark#(filter(X1,X2)) -> mark#(X1)
      mark#(s(X)) -> mark#(X) ->
      mark#(filter(X1,X2)) -> active#(filter(mark(X1),mark(X2)))
      mark#(s(X)) -> mark#(X) -> mark#(divides(X1,X2)) -> mark#(X2)
      mark#(s(X)) -> mark#(X) -> mark#(divides(X1,X2)) -> mark#(X1)
      mark#(s(X)) -> mark#(X) ->
      mark#(divides(X1,X2)) -> active#(divides(mark(X1),mark(X2)))
      mark#(s(X)) -> active#(s(mark(X))) ->
      active#(from(X)) -> mark#(cons(X,from(s(X))))
      mark#(s(X)) -> active#(s(mark(X))) ->
      active#(head(cons(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#(if(true(),X,Y)) -> mark#(X)
      mark#(s(X)) -> active#(s(mark(X))) ->
      active#(if(false(),X,Y)) -> mark#(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#(sieve(cons(X,Y))) -> mark#(cons(X,filter(X,sieve(Y))))
      mark#(primes()) -> active#(primes()) ->
      active#(primes()) -> mark#(sieve(from(s(s(0())))))
      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#(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#(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#(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#(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#(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#(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#(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#(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#(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#(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#(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#(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#(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#(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#(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#(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#(divides(X1,X2)) -> active#(divides(mark(X1),mark(X2)))
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(primes()) -> active#(primes())
      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#(s(X)) -> active#(s(mark(X)))
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(0()) -> active#(0())
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(cons(X1,X2)) -> mark#(X1)
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      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#(true()) -> active#(true())
      active#(if(false(),X,Y)) -> mark#(Y) ->
      mark#(false()) -> active#(false())
      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#(filter(X1,X2)) -> active#(filter(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#(divides(X1,X2)) -> active#(divides(mark(X1),mark(X2)))
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(primes()) -> active#(primes())
      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#(s(X)) -> active#(s(mark(X)))
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(0()) -> active#(0())
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(cons(X1,X2)) -> mark#(X1)
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      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#(true()) -> active#(true())
      active#(if(true(),X,Y)) -> mark#(X) ->
      mark#(false()) -> active#(false())
      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#(filter(X1,X2)) -> active#(filter(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#(divides(X1,X2)) -> active#(divides(mark(X1),mark(X2)))
      active#(tail(cons(X,Y))) -> mark#(Y) ->
      mark#(primes()) -> active#(primes())
      active#(tail(cons(X,Y))) -> mark#(Y) ->
      mark#(sieve(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#(from(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#(s(X)) -> 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#(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#(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#(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#(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#(true()) -> active#(true())
      active#(tail(cons(X,Y))) -> mark#(Y) ->
      mark#(false()) -> active#(false())
      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#(filter(X1,X2)) -> active#(filter(mark(X1),mark(X2)))
      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#(divides(X1,X2)) -> active#(divides(mark(X1),mark(X2)))
      active#(head(cons(X,Y))) -> mark#(X) ->
      mark#(primes()) -> active#(primes())
      active#(head(cons(X,Y))) -> mark#(X) ->
      mark#(sieve(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#(from(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#(s(X)) -> 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#(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#(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#(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#(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#(true()) -> active#(true())
      active#(head(cons(X,Y))) -> mark#(X) ->
      mark#(false()) -> active#(false())
      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#(filter(X1,X2)) -> active#(filter(mark(X1),mark(X2)))
      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#(divides(X1,X2)) -> active#(divides(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)) -> 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)) -> 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)) -> 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#(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#(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#(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#(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#(filter(X1,X2)) -> active#(filter(mark(X1),mark(X2)))
      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#(divides(X1,X2)) -> active#(divides(mark(X1),mark(X2)))
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(sieve(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#(from(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#(s(X)) -> mark#(X)
      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#(cons(X1,X2)) -> mark#(X1)
      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#(head(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#(tail(X)) -> 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#(if(X1,X2,X3)) -> 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#(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#(filter(X1,X2)) -> active#(filter(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#(divides(X1,X2)) -> active#(divides(mark(X1),mark(X2)))
      active#(primes()) -> mark#(sieve(from(s(s(0()))))) ->
      mark#(sieve(X)) -> mark#(X)
      active#(primes()) -> mark#(sieve(from(s(s(0()))))) ->
      mark#(sieve(X)) -> active#(sieve(mark(X)))
     CDG Processor:
      DPs:
       mark#(divides(X1,X2)) -> mark#(X2)
       mark#(primes()) -> active#(primes())
       active#(primes()) -> mark#(sieve(from(s(s(0())))))
       mark#(sieve(X)) -> mark#(X)
       mark#(sieve(X)) -> active#(sieve(mark(X)))
       active#(from(X)) -> mark#(cons(X,from(s(X))))
       mark#(from(X)) -> mark#(X)
       mark#(from(X)) -> active#(from(mark(X)))
       active#(head(cons(X,Y))) -> mark#(X)
       mark#(s(X)) -> mark#(X)
       mark#(s(X)) -> active#(s(mark(X)))
       active#(tail(cons(X,Y))) -> mark#(Y)
       mark#(0()) -> active#(0())
       active#(if(true(),X,Y)) -> mark#(X)
       mark#(cons(X1,X2)) -> mark#(X1)
       mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
       active#(if(false(),X,Y)) -> mark#(Y)
       mark#(head(X)) -> mark#(X)
       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#(tail(X)) -> mark#(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#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
       mark#(true()) -> active#(true())
       mark#(false()) -> active#(false())
       mark#(filter(X1,X2)) -> mark#(X2)
       mark#(filter(X1,X2)) -> mark#(X1)
       mark#(filter(X1,X2)) -> active#(filter(mark(X1),mark(X2)))
       mark#(divides(X1,X2)) -> mark#(X1)
       mark#(divides(X1,X2)) -> active#(divides(mark(X1),mark(X2)))
      TRS:
       active(primes()) -> mark(sieve(from(s(s(0())))))
       active(from(X)) -> mark(cons(X,from(s(X))))
       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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
       mark(primes()) -> active(primes())
       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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
       mark(divides(X1,X2)) -> active(divides(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)
       cons(mark(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)
       head(mark(X)) -> head(X)
       head(active(X)) -> head(X)
       tail(mark(X)) -> tail(X)
       tail(active(X)) -> tail(X)
       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(active(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,active(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,active(X3)) -> if(X1,X2,X3)
       filter(mark(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)
       divides(mark(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)
      graph:
       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)) -> mark#(X1)
       mark#(divides(X1,X2)) -> mark#(X2) ->
       mark#(divides(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)) -> mark#(X1)
       mark#(divides(X1,X2)) -> mark#(X2) ->
       mark#(filter(X1,X2)) -> mark#(X2)
       mark#(divides(X1,X2)) -> mark#(X2) ->
       mark#(false()) -> active#(false())
       mark#(divides(X1,X2)) -> mark#(X2) ->
       mark#(true()) -> active#(true())
       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)) -> mark#(X1)
       mark#(divides(X1,X2)) -> mark#(X2) ->
       mark#(tail(X)) -> active#(tail(mark(X)))
       mark#(divides(X1,X2)) -> mark#(X2) ->
       mark#(tail(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)) -> mark#(X)
       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)) -> mark#(X1)
       mark#(divides(X1,X2)) -> mark#(X2) ->
       mark#(0()) -> active#(0())
       mark#(divides(X1,X2)) -> mark#(X2) ->
       mark#(s(X)) -> active#(s(mark(X)))
       mark#(divides(X1,X2)) -> mark#(X2) ->
       mark#(s(X)) -> mark#(X)
       mark#(divides(X1,X2)) -> mark#(X2) ->
       mark#(from(X)) -> active#(from(mark(X)))
       mark#(divides(X1,X2)) -> mark#(X2) ->
       mark#(from(X)) -> mark#(X)
       mark#(divides(X1,X2)) -> mark#(X2) ->
       mark#(sieve(X)) -> active#(sieve(mark(X)))
       mark#(divides(X1,X2)) -> mark#(X2) ->
       mark#(sieve(X)) -> mark#(X)
       mark#(divides(X1,X2)) -> mark#(X2) ->
       mark#(primes()) -> active#(primes())
       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#(X1)
       mark#(divides(X1,X2)) -> mark#(X1) ->
       mark#(divides(X1,X2)) -> 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#(X1)
       mark#(divides(X1,X2)) -> mark#(X1) ->
       mark#(filter(X1,X2)) -> mark#(X2)
       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)) -> 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)) -> active#(tail(mark(X)))
       mark#(divides(X1,X2)) -> mark#(X1) ->
       mark#(tail(X)) -> 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)) -> active#(cons(mark(X1),X2))
       mark#(divides(X1,X2)) -> mark#(X1) ->
       mark#(cons(X1,X2)) -> mark#(X1)
       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)) -> mark#(X)
       mark#(divides(X1,X2)) -> mark#(X1) ->
       mark#(from(X)) -> active#(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)) -> mark#(X)
       mark#(divides(X1,X2)) -> mark#(X1) ->
       mark#(primes()) -> active#(primes())
       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#(X1)
       mark#(filter(X1,X2)) -> mark#(X2) ->
       mark#(divides(X1,X2)) -> 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#(X1)
       mark#(filter(X1,X2)) -> mark#(X2) ->
       mark#(filter(X1,X2)) -> mark#(X2)
       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)) -> 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)) -> active#(cons(mark(X1),X2))
       mark#(filter(X1,X2)) -> mark#(X2) ->
       mark#(cons(X1,X2)) -> mark#(X1)
       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)) -> 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#(filter(X1,X2)) -> mark#(X2) ->
       mark#(primes()) -> active#(primes())
       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)) -> mark#(X1)
       mark#(filter(X1,X2)) -> mark#(X1) ->
       mark#(divides(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)) -> mark#(X1)
       mark#(filter(X1,X2)) -> mark#(X1) ->
       mark#(filter(X1,X2)) -> mark#(X2)
       mark#(filter(X1,X2)) -> mark#(X1) ->
       mark#(false()) -> active#(false())
       mark#(filter(X1,X2)) -> mark#(X1) ->
       mark#(true()) -> active#(true())
       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)) -> active#(cons(mark(X1),X2))
       mark#(filter(X1,X2)) -> mark#(X1) ->
       mark#(cons(X1,X2)) -> mark#(X1)
       mark#(filter(X1,X2)) -> mark#(X1) ->
       mark#(0()) -> active#(0())
       mark#(filter(X1,X2)) -> mark#(X1) ->
       mark#(s(X)) -> active#(s(mark(X)))
       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#(filter(X1,X2)) -> mark#(X1) ->
       mark#(primes()) -> active#(primes())
       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#(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)) -> mark#(X1)
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(divides(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)) -> mark#(X1)
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(filter(X1,X2)) -> mark#(X2)
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(false()) -> active#(false())
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(true()) -> active#(true())
       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)) -> active#(cons(mark(X1),X2))
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(cons(X1,X2)) -> mark#(X1)
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(0()) -> active#(0())
       mark#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(s(X)) -> active#(s(mark(X)))
       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#(if(X1,X2,X3)) -> mark#(X1) ->
       mark#(primes()) -> active#(primes())
       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#(if(true(),X,Y)) -> mark#(X)
       mark#(tail(X)) -> mark#(X) ->
       mark#(divides(X1,X2)) -> active#(divides(mark(X1),mark(X2)))
       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)) -> active#(filter(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#(false()) -> active#(false())
       mark#(tail(X)) -> mark#(X) -> mark#(true()) -> active#(true())
       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)) -> mark#(X1)
       mark#(tail(X)) -> mark#(X) ->
       mark#(tail(X)) -> active#(tail(mark(X)))
       mark#(tail(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
       mark#(tail(X)) -> mark#(X) ->
       mark#(head(X)) -> active#(head(mark(X)))
       mark#(tail(X)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
       mark#(tail(X)) -> mark#(X) ->
       mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
       mark#(tail(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
       mark#(tail(X)) -> mark#(X) -> mark#(0()) -> active#(0())
       mark#(tail(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
       mark#(tail(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
       mark#(tail(X)) -> mark#(X) ->
       mark#(from(X)) -> active#(from(mark(X)))
       mark#(tail(X)) -> mark#(X) -> mark#(from(X)) -> mark#(X)
       mark#(tail(X)) -> mark#(X) ->
       mark#(sieve(X)) -> active#(sieve(mark(X)))
       mark#(tail(X)) -> mark#(X) -> mark#(sieve(X)) -> mark#(X)
       mark#(tail(X)) -> mark#(X) ->
       mark#(primes()) -> active#(primes())
       mark#(tail(X)) -> active#(tail(mark(X))) ->
       active#(tail(cons(X,Y))) -> mark#(Y)
       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#(X1)
       mark#(head(X)) -> mark#(X) -> mark#(divides(X1,X2)) -> 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#(X1)
       mark#(head(X)) -> mark#(X) -> mark#(filter(X1,X2)) -> mark#(X2)
       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)) -> 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)) -> active#(cons(mark(X1),X2))
       mark#(head(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
       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)) -> 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)
       mark#(head(X)) -> mark#(X) ->
       mark#(primes()) -> active#(primes())
       mark#(head(X)) -> active#(head(mark(X))) ->
       active#(head(cons(X,Y))) -> mark#(X)
       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#(X1)
       mark#(cons(X1,X2)) -> mark#(X1) ->
       mark#(divides(X1,X2)) -> 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#(X1)
       mark#(cons(X1,X2)) -> mark#(X1) ->
       mark#(filter(X1,X2)) -> mark#(X2)
       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)) -> 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)) -> active#(tail(mark(X)))
       mark#(cons(X1,X2)) -> mark#(X1) -> mark#(tail(X)) -> 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)) -> active#(cons(mark(X1),X2))
       mark#(cons(X1,X2)) -> mark#(X1) ->
       mark#(cons(X1,X2)) -> mark#(X1)
       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)) -> mark#(X)
       mark#(cons(X1,X2)) -> mark#(X1) ->
       mark#(from(X)) -> active#(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)) -> mark#(X)
       mark#(cons(X1,X2)) -> mark#(X1) ->
       mark#(primes()) -> active#(primes())
       mark#(sieve(X)) -> mark#(X) ->
       mark#(divides(X1,X2)) -> active#(divides(mark(X1),mark(X2)))
       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)) -> active#(filter(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#(false()) -> active#(false())
       mark#(sieve(X)) -> mark#(X) -> mark#(true()) -> active#(true())
       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)) -> mark#(X1)
       mark#(sieve(X)) -> mark#(X) ->
       mark#(tail(X)) -> active#(tail(mark(X)))
       mark#(sieve(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
       mark#(sieve(X)) -> mark#(X) ->
       mark#(head(X)) -> active#(head(mark(X)))
       mark#(sieve(X)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
       mark#(sieve(X)) -> mark#(X) ->
       mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
       mark#(sieve(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
       mark#(sieve(X)) -> mark#(X) -> mark#(0()) -> active#(0())
       mark#(sieve(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
       mark#(sieve(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
       mark#(sieve(X)) -> mark#(X) ->
       mark#(from(X)) -> active#(from(mark(X)))
       mark#(sieve(X)) -> mark#(X) -> mark#(from(X)) -> mark#(X)
       mark#(sieve(X)) -> mark#(X) ->
       mark#(sieve(X)) -> active#(sieve(mark(X)))
       mark#(sieve(X)) -> mark#(X) -> mark#(sieve(X)) -> mark#(X)
       mark#(sieve(X)) -> mark#(X) ->
       mark#(primes()) -> active#(primes())
       mark#(sieve(X)) -> active#(sieve(mark(X))) ->
       active#(sieve(cons(X,Y))) -> mark#(cons(X,filter(X,sieve(Y))))
       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#(X1)
       mark#(from(X)) -> mark#(X) -> mark#(divides(X1,X2)) -> 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#(X1)
       mark#(from(X)) -> mark#(X) -> mark#(filter(X1,X2)) -> mark#(X2)
       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)) -> 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)) -> active#(cons(mark(X1),X2))
       mark#(from(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
       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)) -> 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#(from(X)) -> mark#(X) ->
       mark#(primes()) -> active#(primes())
       mark#(from(X)) -> active#(from(mark(X))) ->
       active#(from(X)) -> mark#(cons(X,from(s(X))))
       mark#(s(X)) -> mark#(X) ->
       mark#(divides(X1,X2)) -> active#(divides(mark(X1),mark(X2)))
       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)) -> active#(filter(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#(false()) -> active#(false())
       mark#(s(X)) -> mark#(X) -> mark#(true()) -> active#(true())
       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)) -> mark#(X1)
       mark#(s(X)) -> mark#(X) -> mark#(tail(X)) -> active#(tail(mark(X)))
       mark#(s(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
       mark#(s(X)) -> mark#(X) -> mark#(head(X)) -> active#(head(mark(X)))
       mark#(s(X)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
       mark#(s(X)) -> mark#(X) ->
       mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
       mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
       mark#(s(X)) -> mark#(X) -> mark#(0()) -> active#(0())
       mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
       mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
       mark#(s(X)) -> mark#(X) -> mark#(from(X)) -> active#(from(mark(X)))
       mark#(s(X)) -> mark#(X) -> mark#(from(X)) -> mark#(X)
       mark#(s(X)) -> mark#(X) -> mark#(sieve(X)) -> active#(sieve(mark(X)))
       mark#(s(X)) -> mark#(X) -> mark#(sieve(X)) -> mark#(X)
       mark#(s(X)) -> mark#(X) ->
       mark#(primes()) -> active#(primes())
       mark#(primes()) -> active#(primes()) ->
       active#(primes()) -> mark#(sieve(from(s(s(0())))))
       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#(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#(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)) -> active#(filter(mark(X1),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#(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)) -> 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)) -> 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)) -> 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)) -> 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#(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)) -> 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)) -> 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)) -> mark#(X)
       active#(if(false(),X,Y)) -> mark#(Y) ->
       mark#(primes()) -> active#(primes())
       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#(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)) -> active#(filter(mark(X1),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#(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)) -> 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)) -> 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)) -> 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)) -> 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#(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)) -> 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)) -> 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)) -> mark#(X)
       active#(if(true(),X,Y)) -> mark#(X) ->
       mark#(primes()) -> active#(primes())
       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)) -> mark#(X1)
       active#(tail(cons(X,Y))) -> mark#(Y) ->
       mark#(divides(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)) -> mark#(X1)
       active#(tail(cons(X,Y))) -> mark#(Y) ->
       mark#(filter(X1,X2)) -> mark#(X2)
       active#(tail(cons(X,Y))) -> mark#(Y) ->
       mark#(false()) -> active#(false())
       active#(tail(cons(X,Y))) -> mark#(Y) ->
       mark#(true()) -> active#(true())
       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)) -> active#(cons(mark(X1),X2))
       active#(tail(cons(X,Y))) -> mark#(Y) ->
       mark#(cons(X1,X2)) -> mark#(X1)
       active#(tail(cons(X,Y))) -> mark#(Y) ->
       mark#(0()) -> active#(0())
       active#(tail(cons(X,Y))) -> mark#(Y) ->
       mark#(s(X)) -> active#(s(mark(X)))
       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#(tail(cons(X,Y))) -> mark#(Y) ->
       mark#(primes()) -> active#(primes())
       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)) -> mark#(X1)
       active#(head(cons(X,Y))) -> mark#(X) ->
       mark#(divides(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)) -> mark#(X1)
       active#(head(cons(X,Y))) -> mark#(X) ->
       mark#(filter(X1,X2)) -> mark#(X2)
       active#(head(cons(X,Y))) -> mark#(X) ->
       mark#(false()) -> active#(false())
       active#(head(cons(X,Y))) -> mark#(X) ->
       mark#(true()) -> active#(true())
       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)) -> active#(cons(mark(X1),X2))
       active#(head(cons(X,Y))) -> mark#(X) ->
       mark#(cons(X1,X2)) -> mark#(X1)
       active#(head(cons(X,Y))) -> mark#(X) ->
       mark#(0()) -> active#(0())
       active#(head(cons(X,Y))) -> mark#(X) ->
       mark#(s(X)) -> active#(s(mark(X)))
       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#(head(cons(X,Y))) -> mark#(X) ->
       mark#(primes()) -> active#(primes())
       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)) -> mark#(X1)
       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#(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)
      SCC Processor:
       #sccs: 1
       #rules: 26
       #arcs: 376/1024
       DPs:
        mark#(divides(X1,X2)) -> mark#(X2)
        mark#(primes()) -> active#(primes())
        active#(primes()) -> mark#(sieve(from(s(s(0())))))
        mark#(sieve(X)) -> mark#(X)
        mark#(sieve(X)) -> active#(sieve(mark(X)))
        active#(sieve(cons(X,Y))) -> mark#(cons(X,filter(X,sieve(Y))))
        mark#(cons(X1,X2)) -> mark#(X1)
        mark#(from(X)) -> mark#(X)
        mark#(from(X)) -> active#(from(mark(X)))
        active#(from(X)) -> mark#(cons(X,from(s(X))))
        mark#(s(X)) -> mark#(X)
        mark#(head(X)) -> mark#(X)
        mark#(head(X)) -> active#(head(mark(X)))
        active#(head(cons(X,Y))) -> mark#(X)
        mark#(tail(X)) -> mark#(X)
        mark#(tail(X)) -> active#(tail(mark(X)))
        active#(tail(cons(X,Y))) -> mark#(Y)
        mark#(if(X1,X2,X3)) -> mark#(X1)
        mark#(if(X1,X2,X3)) -> active#(if(mark(X1),X2,X3))
        active#(if(true(),X,Y)) -> mark#(X)
        mark#(filter(X1,X2)) -> mark#(X2)
        mark#(filter(X1,X2)) -> mark#(X1)
        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#(divides(X1,X2)) -> mark#(X1)
        active#(if(false(),X,Y)) -> mark#(Y)
       TRS:
        active(primes()) -> mark(sieve(from(s(s(0())))))
        active(from(X)) -> mark(cons(X,from(s(X))))
        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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
        mark(primes()) -> active(primes())
        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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
        mark(divides(X1,X2)) -> active(divides(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)
        cons(mark(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)
        head(mark(X)) -> head(X)
        head(active(X)) -> head(X)
        tail(mark(X)) -> tail(X)
        tail(active(X)) -> tail(X)
        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(active(X1),X2,X3) -> if(X1,X2,X3)
        if(X1,active(X2),X3) -> if(X1,X2,X3)
        if(X1,X2,active(X3)) -> if(X1,X2,X3)
        filter(mark(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)
        divides(mark(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)
       Open
    
    DPs:
     sieve#(mark(X)) -> sieve#(X)
     sieve#(active(X)) -> sieve#(X)
    TRS:
     active(primes()) -> mark(sieve(from(s(s(0())))))
     active(from(X)) -> mark(cons(X,from(s(X))))
     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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
     mark(primes()) -> active(primes())
     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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
     mark(divides(X1,X2)) -> active(divides(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)
     cons(mark(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)
     head(mark(X)) -> head(X)
     head(active(X)) -> head(X)
     tail(mark(X)) -> tail(X)
     tail(active(X)) -> tail(X)
     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(active(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,active(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,active(X3)) -> if(X1,X2,X3)
     filter(mark(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)
     divides(mark(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)
    Subterm Criterion Processor:
     simple projection:
      pi(sieve#) = 0
     problem:
      DPs:
       
      TRS:
       active(primes()) -> mark(sieve(from(s(s(0())))))
       active(from(X)) -> mark(cons(X,from(s(X))))
       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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
       mark(primes()) -> active(primes())
       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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
       mark(divides(X1,X2)) -> active(divides(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)
       cons(mark(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)
       head(mark(X)) -> head(X)
       head(active(X)) -> head(X)
       tail(mark(X)) -> tail(X)
       tail(active(X)) -> tail(X)
       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(active(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,active(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,active(X3)) -> if(X1,X2,X3)
       filter(mark(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)
       divides(mark(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)
     Qed
    
    DPs:
     from#(mark(X)) -> from#(X)
     from#(active(X)) -> from#(X)
    TRS:
     active(primes()) -> mark(sieve(from(s(s(0())))))
     active(from(X)) -> mark(cons(X,from(s(X))))
     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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
     mark(primes()) -> active(primes())
     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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
     mark(divides(X1,X2)) -> active(divides(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)
     cons(mark(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)
     head(mark(X)) -> head(X)
     head(active(X)) -> head(X)
     tail(mark(X)) -> tail(X)
     tail(active(X)) -> tail(X)
     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(active(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,active(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,active(X3)) -> if(X1,X2,X3)
     filter(mark(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)
     divides(mark(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)
    Subterm Criterion Processor:
     simple projection:
      pi(from#) = 0
     problem:
      DPs:
       
      TRS:
       active(primes()) -> mark(sieve(from(s(s(0())))))
       active(from(X)) -> mark(cons(X,from(s(X))))
       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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
       mark(primes()) -> active(primes())
       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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
       mark(divides(X1,X2)) -> active(divides(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)
       cons(mark(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)
       head(mark(X)) -> head(X)
       head(active(X)) -> head(X)
       tail(mark(X)) -> tail(X)
       tail(active(X)) -> tail(X)
       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(active(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,active(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,active(X3)) -> if(X1,X2,X3)
       filter(mark(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)
       divides(mark(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)
     Qed
    
    DPs:
     s#(mark(X)) -> s#(X)
     s#(active(X)) -> s#(X)
    TRS:
     active(primes()) -> mark(sieve(from(s(s(0())))))
     active(from(X)) -> mark(cons(X,from(s(X))))
     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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
     mark(primes()) -> active(primes())
     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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
     mark(divides(X1,X2)) -> active(divides(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)
     cons(mark(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)
     head(mark(X)) -> head(X)
     head(active(X)) -> head(X)
     tail(mark(X)) -> tail(X)
     tail(active(X)) -> tail(X)
     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(active(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,active(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,active(X3)) -> if(X1,X2,X3)
     filter(mark(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)
     divides(mark(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)
    Subterm Criterion Processor:
     simple projection:
      pi(s#) = 0
     problem:
      DPs:
       
      TRS:
       active(primes()) -> mark(sieve(from(s(s(0())))))
       active(from(X)) -> mark(cons(X,from(s(X))))
       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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
       mark(primes()) -> active(primes())
       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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
       mark(divides(X1,X2)) -> active(divides(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)
       cons(mark(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)
       head(mark(X)) -> head(X)
       head(active(X)) -> head(X)
       tail(mark(X)) -> tail(X)
       tail(active(X)) -> tail(X)
       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(active(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,active(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,active(X3)) -> if(X1,X2,X3)
       filter(mark(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)
       divides(mark(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)
     Qed
    
    DPs:
     cons#(mark(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)
    TRS:
     active(primes()) -> mark(sieve(from(s(s(0())))))
     active(from(X)) -> mark(cons(X,from(s(X))))
     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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
     mark(primes()) -> active(primes())
     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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
     mark(divides(X1,X2)) -> active(divides(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)
     cons(mark(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)
     head(mark(X)) -> head(X)
     head(active(X)) -> head(X)
     tail(mark(X)) -> tail(X)
     tail(active(X)) -> tail(X)
     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(active(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,active(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,active(X3)) -> if(X1,X2,X3)
     filter(mark(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)
     divides(mark(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)
    Subterm Criterion Processor:
     simple projection:
      pi(cons#) = 1
     problem:
      DPs:
       cons#(mark(X1),X2) -> cons#(X1,X2)
       cons#(active(X1),X2) -> cons#(X1,X2)
      TRS:
       active(primes()) -> mark(sieve(from(s(s(0())))))
       active(from(X)) -> mark(cons(X,from(s(X))))
       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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
       mark(primes()) -> active(primes())
       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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
       mark(divides(X1,X2)) -> active(divides(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)
       cons(mark(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)
       head(mark(X)) -> head(X)
       head(active(X)) -> head(X)
       tail(mark(X)) -> tail(X)
       tail(active(X)) -> tail(X)
       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(active(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,active(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,active(X3)) -> if(X1,X2,X3)
       filter(mark(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)
       divides(mark(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)
     Subterm Criterion Processor:
      simple projection:
       pi(cons#) = 0
      problem:
       DPs:
        
       TRS:
        active(primes()) -> mark(sieve(from(s(s(0())))))
        active(from(X)) -> mark(cons(X,from(s(X))))
        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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
        mark(primes()) -> active(primes())
        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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
        mark(divides(X1,X2)) -> active(divides(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)
        cons(mark(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)
        head(mark(X)) -> head(X)
        head(active(X)) -> head(X)
        tail(mark(X)) -> tail(X)
        tail(active(X)) -> tail(X)
        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(active(X1),X2,X3) -> if(X1,X2,X3)
        if(X1,active(X2),X3) -> if(X1,X2,X3)
        if(X1,X2,active(X3)) -> if(X1,X2,X3)
        filter(mark(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)
        divides(mark(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)
      Qed
    
    DPs:
     filter#(mark(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)
    TRS:
     active(primes()) -> mark(sieve(from(s(s(0())))))
     active(from(X)) -> mark(cons(X,from(s(X))))
     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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
     mark(primes()) -> active(primes())
     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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
     mark(divides(X1,X2)) -> active(divides(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)
     cons(mark(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)
     head(mark(X)) -> head(X)
     head(active(X)) -> head(X)
     tail(mark(X)) -> tail(X)
     tail(active(X)) -> tail(X)
     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(active(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,active(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,active(X3)) -> if(X1,X2,X3)
     filter(mark(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)
     divides(mark(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)
    Subterm Criterion Processor:
     simple projection:
      pi(filter#) = 1
     problem:
      DPs:
       filter#(mark(X1),X2) -> filter#(X1,X2)
       filter#(active(X1),X2) -> filter#(X1,X2)
      TRS:
       active(primes()) -> mark(sieve(from(s(s(0())))))
       active(from(X)) -> mark(cons(X,from(s(X))))
       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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
       mark(primes()) -> active(primes())
       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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
       mark(divides(X1,X2)) -> active(divides(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)
       cons(mark(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)
       head(mark(X)) -> head(X)
       head(active(X)) -> head(X)
       tail(mark(X)) -> tail(X)
       tail(active(X)) -> tail(X)
       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(active(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,active(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,active(X3)) -> if(X1,X2,X3)
       filter(mark(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)
       divides(mark(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)
     Subterm Criterion Processor:
      simple projection:
       pi(filter#) = 0
      problem:
       DPs:
        
       TRS:
        active(primes()) -> mark(sieve(from(s(s(0())))))
        active(from(X)) -> mark(cons(X,from(s(X))))
        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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
        mark(primes()) -> active(primes())
        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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
        mark(divides(X1,X2)) -> active(divides(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)
        cons(mark(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)
        head(mark(X)) -> head(X)
        head(active(X)) -> head(X)
        tail(mark(X)) -> tail(X)
        tail(active(X)) -> tail(X)
        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(active(X1),X2,X3) -> if(X1,X2,X3)
        if(X1,active(X2),X3) -> if(X1,X2,X3)
        if(X1,X2,active(X3)) -> if(X1,X2,X3)
        filter(mark(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)
        divides(mark(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)
      Qed
    
    DPs:
     divides#(mark(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)
    TRS:
     active(primes()) -> mark(sieve(from(s(s(0())))))
     active(from(X)) -> mark(cons(X,from(s(X))))
     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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
     mark(primes()) -> active(primes())
     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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
     mark(divides(X1,X2)) -> active(divides(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)
     cons(mark(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)
     head(mark(X)) -> head(X)
     head(active(X)) -> head(X)
     tail(mark(X)) -> tail(X)
     tail(active(X)) -> tail(X)
     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(active(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,active(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,active(X3)) -> if(X1,X2,X3)
     filter(mark(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)
     divides(mark(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)
    Subterm Criterion Processor:
     simple projection:
      pi(divides#) = 1
     problem:
      DPs:
       divides#(mark(X1),X2) -> divides#(X1,X2)
       divides#(active(X1),X2) -> divides#(X1,X2)
      TRS:
       active(primes()) -> mark(sieve(from(s(s(0())))))
       active(from(X)) -> mark(cons(X,from(s(X))))
       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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
       mark(primes()) -> active(primes())
       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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
       mark(divides(X1,X2)) -> active(divides(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)
       cons(mark(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)
       head(mark(X)) -> head(X)
       head(active(X)) -> head(X)
       tail(mark(X)) -> tail(X)
       tail(active(X)) -> tail(X)
       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(active(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,active(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,active(X3)) -> if(X1,X2,X3)
       filter(mark(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)
       divides(mark(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)
     Subterm Criterion Processor:
      simple projection:
       pi(divides#) = 0
      problem:
       DPs:
        
       TRS:
        active(primes()) -> mark(sieve(from(s(s(0())))))
        active(from(X)) -> mark(cons(X,from(s(X))))
        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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
        mark(primes()) -> active(primes())
        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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
        mark(divides(X1,X2)) -> active(divides(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)
        cons(mark(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)
        head(mark(X)) -> head(X)
        head(active(X)) -> head(X)
        tail(mark(X)) -> tail(X)
        tail(active(X)) -> tail(X)
        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(active(X1),X2,X3) -> if(X1,X2,X3)
        if(X1,active(X2),X3) -> if(X1,X2,X3)
        if(X1,X2,active(X3)) -> if(X1,X2,X3)
        filter(mark(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)
        divides(mark(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)
      Qed
    
    DPs:
     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#(active(X1),X2,X3) -> if#(X1,X2,X3)
     if#(X1,active(X2),X3) -> if#(X1,X2,X3)
     if#(X1,X2,active(X3)) -> if#(X1,X2,X3)
    TRS:
     active(primes()) -> mark(sieve(from(s(s(0())))))
     active(from(X)) -> mark(cons(X,from(s(X))))
     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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
     mark(primes()) -> active(primes())
     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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
     mark(divides(X1,X2)) -> active(divides(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)
     cons(mark(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)
     head(mark(X)) -> head(X)
     head(active(X)) -> head(X)
     tail(mark(X)) -> tail(X)
     tail(active(X)) -> tail(X)
     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(active(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,active(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,active(X3)) -> if(X1,X2,X3)
     filter(mark(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)
     divides(mark(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)
    Subterm Criterion Processor:
     simple projection:
      pi(if#) = 2
     problem:
      DPs:
       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,active(X2),X3) -> if#(X1,X2,X3)
      TRS:
       active(primes()) -> mark(sieve(from(s(s(0())))))
       active(from(X)) -> mark(cons(X,from(s(X))))
       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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
       mark(primes()) -> active(primes())
       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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
       mark(divides(X1,X2)) -> active(divides(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)
       cons(mark(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)
       head(mark(X)) -> head(X)
       head(active(X)) -> head(X)
       tail(mark(X)) -> tail(X)
       tail(active(X)) -> tail(X)
       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(active(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,active(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,active(X3)) -> if(X1,X2,X3)
       filter(mark(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)
       divides(mark(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)
     Subterm Criterion Processor:
      simple projection:
       pi(if#) = 1
      problem:
       DPs:
        if#(mark(X1),X2,X3) -> if#(X1,X2,X3)
        if#(active(X1),X2,X3) -> if#(X1,X2,X3)
       TRS:
        active(primes()) -> mark(sieve(from(s(s(0())))))
        active(from(X)) -> mark(cons(X,from(s(X))))
        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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
        mark(primes()) -> active(primes())
        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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
        mark(divides(X1,X2)) -> active(divides(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)
        cons(mark(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)
        head(mark(X)) -> head(X)
        head(active(X)) -> head(X)
        tail(mark(X)) -> tail(X)
        tail(active(X)) -> tail(X)
        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(active(X1),X2,X3) -> if(X1,X2,X3)
        if(X1,active(X2),X3) -> if(X1,X2,X3)
        if(X1,X2,active(X3)) -> if(X1,X2,X3)
        filter(mark(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)
        divides(mark(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)
      Subterm Criterion Processor:
       simple projection:
        pi(if#) = 0
       problem:
        DPs:
         
        TRS:
         active(primes()) -> mark(sieve(from(s(s(0())))))
         active(from(X)) -> mark(cons(X,from(s(X))))
         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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
         mark(primes()) -> active(primes())
         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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
         mark(divides(X1,X2)) -> active(divides(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)
         cons(mark(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)
         head(mark(X)) -> head(X)
         head(active(X)) -> head(X)
         tail(mark(X)) -> tail(X)
         tail(active(X)) -> tail(X)
         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(active(X1),X2,X3) -> if(X1,X2,X3)
         if(X1,active(X2),X3) -> if(X1,X2,X3)
         if(X1,X2,active(X3)) -> if(X1,X2,X3)
         filter(mark(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)
         divides(mark(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)
       Qed
    
    DPs:
     head#(mark(X)) -> head#(X)
     head#(active(X)) -> head#(X)
    TRS:
     active(primes()) -> mark(sieve(from(s(s(0())))))
     active(from(X)) -> mark(cons(X,from(s(X))))
     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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
     mark(primes()) -> active(primes())
     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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
     mark(divides(X1,X2)) -> active(divides(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)
     cons(mark(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)
     head(mark(X)) -> head(X)
     head(active(X)) -> head(X)
     tail(mark(X)) -> tail(X)
     tail(active(X)) -> tail(X)
     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(active(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,active(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,active(X3)) -> if(X1,X2,X3)
     filter(mark(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)
     divides(mark(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)
    Subterm Criterion Processor:
     simple projection:
      pi(head#) = 0
     problem:
      DPs:
       
      TRS:
       active(primes()) -> mark(sieve(from(s(s(0())))))
       active(from(X)) -> mark(cons(X,from(s(X))))
       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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
       mark(primes()) -> active(primes())
       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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
       mark(divides(X1,X2)) -> active(divides(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)
       cons(mark(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)
       head(mark(X)) -> head(X)
       head(active(X)) -> head(X)
       tail(mark(X)) -> tail(X)
       tail(active(X)) -> tail(X)
       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(active(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,active(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,active(X3)) -> if(X1,X2,X3)
       filter(mark(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)
       divides(mark(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)
     Qed
    
    DPs:
     tail#(mark(X)) -> tail#(X)
     tail#(active(X)) -> tail#(X)
    TRS:
     active(primes()) -> mark(sieve(from(s(s(0())))))
     active(from(X)) -> mark(cons(X,from(s(X))))
     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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
     mark(primes()) -> active(primes())
     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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
     mark(divides(X1,X2)) -> active(divides(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)
     cons(mark(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)
     head(mark(X)) -> head(X)
     head(active(X)) -> head(X)
     tail(mark(X)) -> tail(X)
     tail(active(X)) -> tail(X)
     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(active(X1),X2,X3) -> if(X1,X2,X3)
     if(X1,active(X2),X3) -> if(X1,X2,X3)
     if(X1,X2,active(X3)) -> if(X1,X2,X3)
     filter(mark(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)
     divides(mark(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)
    Subterm Criterion Processor:
     simple projection:
      pi(tail#) = 0
     problem:
      DPs:
       
      TRS:
       active(primes()) -> mark(sieve(from(s(s(0())))))
       active(from(X)) -> mark(cons(X,from(s(X))))
       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(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
       mark(primes()) -> active(primes())
       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(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(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
       mark(divides(X1,X2)) -> active(divides(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)
       cons(mark(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)
       head(mark(X)) -> head(X)
       head(active(X)) -> head(X)
       tail(mark(X)) -> tail(X)
       tail(active(X)) -> tail(X)
       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(active(X1),X2,X3) -> if(X1,X2,X3)
       if(X1,active(X2),X3) -> if(X1,X2,X3)
       if(X1,X2,active(X3)) -> if(X1,X2,X3)
       filter(mark(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)
       divides(mark(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)
     Qed