MAYBE

Problem:
 primes() -> sieve(from(s(s(0()))))
 from(X) -> cons(X,n__from(s(X)))
 head(cons(X,Y)) -> X
 tail(cons(X,Y)) -> activate(Y)
 if(true(),X,Y) -> activate(X)
 if(false(),X,Y) -> activate(Y)
 filter(s(s(X)),cons(Y,Z)) ->
 if(divides(s(s(X)),Y),n__filter(s(s(X)),activate(Z)),n__cons(Y,n__filter(X,sieve(Y))))
 sieve(cons(X,Y)) -> cons(X,n__filter(X,sieve(activate(Y))))
 from(X) -> n__from(X)
 filter(X1,X2) -> n__filter(X1,X2)
 cons(X1,X2) -> n__cons(X1,X2)
 activate(n__from(X)) -> from(X)
 activate(n__filter(X1,X2)) -> filter(X1,X2)
 activate(n__cons(X1,X2)) -> cons(X1,X2)
 activate(X) -> X

Proof:
 DP Processor:
  DPs:
   primes#() -> from#(s(s(0())))
   primes#() -> sieve#(from(s(s(0()))))
   from#(X) -> cons#(X,n__from(s(X)))
   tail#(cons(X,Y)) -> activate#(Y)
   if#(true(),X,Y) -> activate#(X)
   if#(false(),X,Y) -> activate#(Y)
   filter#(s(s(X)),cons(Y,Z)) -> sieve#(Y)
   filter#(s(s(X)),cons(Y,Z)) -> activate#(Z)
   filter#(s(s(X)),cons(Y,Z)) ->
   if#(divides(s(s(X)),Y),n__filter(s(s(X)),activate(Z)),n__cons(Y,n__filter(X,sieve(Y))))
   sieve#(cons(X,Y)) -> activate#(Y)
   sieve#(cons(X,Y)) -> sieve#(activate(Y))
   sieve#(cons(X,Y)) -> cons#(X,n__filter(X,sieve(activate(Y))))
   activate#(n__from(X)) -> from#(X)
   activate#(n__filter(X1,X2)) -> filter#(X1,X2)
   activate#(n__cons(X1,X2)) -> cons#(X1,X2)
  TRS:
   primes() -> sieve(from(s(s(0()))))
   from(X) -> cons(X,n__from(s(X)))
   head(cons(X,Y)) -> X
   tail(cons(X,Y)) -> activate(Y)
   if(true(),X,Y) -> activate(X)
   if(false(),X,Y) -> activate(Y)
   filter(s(s(X)),cons(Y,Z)) ->
   if(divides(s(s(X)),Y),n__filter(s(s(X)),activate(Z)),n__cons(Y,n__filter(X,sieve(Y))))
   sieve(cons(X,Y)) -> cons(X,n__filter(X,sieve(activate(Y))))
   from(X) -> n__from(X)
   filter(X1,X2) -> n__filter(X1,X2)
   cons(X1,X2) -> n__cons(X1,X2)
   activate(n__from(X)) -> from(X)
   activate(n__filter(X1,X2)) -> filter(X1,X2)
   activate(n__cons(X1,X2)) -> cons(X1,X2)
   activate(X) -> X
  EDG Processor:
   DPs:
    primes#() -> from#(s(s(0())))
    primes#() -> sieve#(from(s(s(0()))))
    from#(X) -> cons#(X,n__from(s(X)))
    tail#(cons(X,Y)) -> activate#(Y)
    if#(true(),X,Y) -> activate#(X)
    if#(false(),X,Y) -> activate#(Y)
    filter#(s(s(X)),cons(Y,Z)) -> sieve#(Y)
    filter#(s(s(X)),cons(Y,Z)) -> activate#(Z)
    filter#(s(s(X)),cons(Y,Z)) ->
    if#(divides(s(s(X)),Y),n__filter(s(s(X)),activate(Z)),n__cons(Y,n__filter(X,sieve(Y))))
    sieve#(cons(X,Y)) -> activate#(Y)
    sieve#(cons(X,Y)) -> sieve#(activate(Y))
    sieve#(cons(X,Y)) -> cons#(X,n__filter(X,sieve(activate(Y))))
    activate#(n__from(X)) -> from#(X)
    activate#(n__filter(X1,X2)) -> filter#(X1,X2)
    activate#(n__cons(X1,X2)) -> cons#(X1,X2)
   TRS:
    primes() -> sieve(from(s(s(0()))))
    from(X) -> cons(X,n__from(s(X)))
    head(cons(X,Y)) -> X
    tail(cons(X,Y)) -> activate(Y)
    if(true(),X,Y) -> activate(X)
    if(false(),X,Y) -> activate(Y)
    filter(s(s(X)),cons(Y,Z)) ->
    if(divides(s(s(X)),Y),n__filter(s(s(X)),activate(Z)),n__cons(Y,n__filter(X,sieve(Y))))
    sieve(cons(X,Y)) -> cons(X,n__filter(X,sieve(activate(Y))))
    from(X) -> n__from(X)
    filter(X1,X2) -> n__filter(X1,X2)
    cons(X1,X2) -> n__cons(X1,X2)
    activate(n__from(X)) -> from(X)
    activate(n__filter(X1,X2)) -> filter(X1,X2)
    activate(n__cons(X1,X2)) -> cons(X1,X2)
    activate(X) -> X
   graph:
    filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) ->
    activate#(n__from(X)) -> from#(X)
    filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) ->
    activate#(n__filter(X1,X2)) -> filter#(X1,X2)
    filter#(s(s(X)),cons(Y,Z)) -> activate#(Z) ->
    activate#(n__cons(X1,X2)) -> cons#(X1,X2)
    filter#(s(s(X)),cons(Y,Z)) -> sieve#(Y) ->
    sieve#(cons(X,Y)) -> activate#(Y)
    filter#(s(s(X)),cons(Y,Z)) -> sieve#(Y) ->
    sieve#(cons(X,Y)) -> sieve#(activate(Y))
    filter#(s(s(X)),cons(Y,Z)) -> sieve#(Y) ->
    sieve#(cons(X,Y)) -> cons#(X,n__filter(X,sieve(activate(Y))))
    if#(false(),X,Y) -> activate#(Y) ->
    activate#(n__from(X)) -> from#(X)
    if#(false(),X,Y) -> activate#(Y) ->
    activate#(n__filter(X1,X2)) -> filter#(X1,X2)
    if#(false(),X,Y) -> activate#(Y) ->
    activate#(n__cons(X1,X2)) -> cons#(X1,X2)
    if#(true(),X,Y) -> activate#(X) ->
    activate#(n__from(X)) -> from#(X)
    if#(true(),X,Y) -> activate#(X) ->
    activate#(n__filter(X1,X2)) -> filter#(X1,X2)
    if#(true(),X,Y) -> activate#(X) ->
    activate#(n__cons(X1,X2)) -> cons#(X1,X2)
    activate#(n__filter(X1,X2)) -> filter#(X1,X2) ->
    filter#(s(s(X)),cons(Y,Z)) -> sieve#(Y)
    activate#(n__filter(X1,X2)) -> filter#(X1,X2) ->
    filter#(s(s(X)),cons(Y,Z)) -> activate#(Z)
    activate#(n__filter(X1,X2)) -> filter#(X1,X2) ->
    filter#(s(s(X)),cons(Y,Z)) ->
    if#(divides(s(s(X)),Y),n__filter(s(s(X)),activate(Z)),n__cons(Y,n__filter(X,sieve(Y))))
    activate#(n__from(X)) -> from#(X) ->
    from#(X) -> cons#(X,n__from(s(X)))
    tail#(cons(X,Y)) -> activate#(Y) ->
    activate#(n__from(X)) -> from#(X)
    tail#(cons(X,Y)) -> activate#(Y) ->
    activate#(n__filter(X1,X2)) -> filter#(X1,X2)
    tail#(cons(X,Y)) -> activate#(Y) ->
    activate#(n__cons(X1,X2)) -> cons#(X1,X2)
    sieve#(cons(X,Y)) -> activate#(Y) ->
    activate#(n__from(X)) -> from#(X)
    sieve#(cons(X,Y)) -> activate#(Y) ->
    activate#(n__filter(X1,X2)) -> filter#(X1,X2)
    sieve#(cons(X,Y)) -> activate#(Y) ->
    activate#(n__cons(X1,X2)) -> cons#(X1,X2)
    sieve#(cons(X,Y)) -> sieve#(activate(Y)) ->
    sieve#(cons(X,Y)) -> activate#(Y)
    sieve#(cons(X,Y)) -> sieve#(activate(Y)) ->
    sieve#(cons(X,Y)) -> sieve#(activate(Y))
    sieve#(cons(X,Y)) -> sieve#(activate(Y)) ->
    sieve#(cons(X,Y)) -> cons#(X,n__filter(X,sieve(activate(Y))))
    primes#() -> sieve#(from(s(s(0())))) ->
    sieve#(cons(X,Y)) -> activate#(Y)
    primes#() -> sieve#(from(s(s(0())))) ->
    sieve#(cons(X,Y)) -> sieve#(activate(Y))
    primes#() -> sieve#(from(s(s(0())))) ->
    sieve#(cons(X,Y)) -> cons#(X,n__filter(X,sieve(activate(Y))))
    primes#() -> from#(s(s(0()))) -> from#(X) -> cons#(X,n__from(s(X)))
   SCC Processor:
    #sccs: 1
    #rules: 5
    #arcs: 29/225
    DPs:
     filter#(s(s(X)),cons(Y,Z)) -> activate#(Z)
     activate#(n__filter(X1,X2)) -> filter#(X1,X2)
     filter#(s(s(X)),cons(Y,Z)) -> sieve#(Y)
     sieve#(cons(X,Y)) -> sieve#(activate(Y))
     sieve#(cons(X,Y)) -> activate#(Y)
    TRS:
     primes() -> sieve(from(s(s(0()))))
     from(X) -> cons(X,n__from(s(X)))
     head(cons(X,Y)) -> X
     tail(cons(X,Y)) -> activate(Y)
     if(true(),X,Y) -> activate(X)
     if(false(),X,Y) -> activate(Y)
     filter(s(s(X)),cons(Y,Z)) ->
     if(divides(s(s(X)),Y),n__filter(s(s(X)),activate(Z)),n__cons(Y,n__filter(X,sieve(Y))))
     sieve(cons(X,Y)) -> cons(X,n__filter(X,sieve(activate(Y))))
     from(X) -> n__from(X)
     filter(X1,X2) -> n__filter(X1,X2)
     cons(X1,X2) -> n__cons(X1,X2)
     activate(n__from(X)) -> from(X)
     activate(n__filter(X1,X2)) -> filter(X1,X2)
     activate(n__cons(X1,X2)) -> cons(X1,X2)
     activate(X) -> X
    Open