MAYBE

Problem:
 primes() -> sieve(from(s(s(0()))))
 from(X) -> cons(X,from(s(X)))
 head(cons(X,Y)) -> X
 tail(cons(X,Y)) -> Y
 if(true(),X,Y) -> X
 if(false(),X,Y) -> Y
 filter(s(s(X)),cons(Y,Z)) -> if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))
 sieve(cons(X,Y)) -> cons(X,filter(X,sieve(Y)))

Proof:
 DP Processor:
  DPs:
   primes#() -> from#(s(s(0())))
   primes#() -> sieve#(from(s(s(0()))))
   from#(X) -> from#(s(X))
   filter#(s(s(X)),cons(Y,Z)) -> sieve#(Y)
   filter#(s(s(X)),cons(Y,Z)) -> filter#(X,sieve(Y))
   filter#(s(s(X)),cons(Y,Z)) -> filter#(s(s(X)),Z)
   filter#(s(s(X)),cons(Y,Z)) ->
   if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))
   sieve#(cons(X,Y)) -> sieve#(Y)
   sieve#(cons(X,Y)) -> filter#(X,sieve(Y))
  TRS:
   primes() -> sieve(from(s(s(0()))))
   from(X) -> cons(X,from(s(X)))
   head(cons(X,Y)) -> X
   tail(cons(X,Y)) -> Y
   if(true(),X,Y) -> X
   if(false(),X,Y) -> Y
   filter(s(s(X)),cons(Y,Z)) -> if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))
   sieve(cons(X,Y)) -> cons(X,filter(X,sieve(Y)))
  EDG Processor:
   DPs:
    primes#() -> from#(s(s(0())))
    primes#() -> sieve#(from(s(s(0()))))
    from#(X) -> from#(s(X))
    filter#(s(s(X)),cons(Y,Z)) -> sieve#(Y)
    filter#(s(s(X)),cons(Y,Z)) -> filter#(X,sieve(Y))
    filter#(s(s(X)),cons(Y,Z)) -> filter#(s(s(X)),Z)
    filter#(s(s(X)),cons(Y,Z)) ->
    if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))
    sieve#(cons(X,Y)) -> sieve#(Y)
    sieve#(cons(X,Y)) -> filter#(X,sieve(Y))
   TRS:
    primes() -> sieve(from(s(s(0()))))
    from(X) -> cons(X,from(s(X)))
    head(cons(X,Y)) -> X
    tail(cons(X,Y)) -> Y
    if(true(),X,Y) -> X
    if(false(),X,Y) -> Y
    filter(s(s(X)),cons(Y,Z)) ->
    if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))
    sieve(cons(X,Y)) -> cons(X,filter(X,sieve(Y)))
   graph:
    filter#(s(s(X)),cons(Y,Z)) -> filter#(s(s(X)),Z) ->
    filter#(s(s(X)),cons(Y,Z)) -> sieve#(Y)
    filter#(s(s(X)),cons(Y,Z)) -> filter#(s(s(X)),Z) ->
    filter#(s(s(X)),cons(Y,Z)) -> filter#(X,sieve(Y))
    filter#(s(s(X)),cons(Y,Z)) -> filter#(s(s(X)),Z) ->
    filter#(s(s(X)),cons(Y,Z)) -> filter#(s(s(X)),Z)
    filter#(s(s(X)),cons(Y,Z)) -> filter#(s(s(X)),Z) ->
    filter#(s(s(X)),cons(Y,Z)) ->
    if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))
    filter#(s(s(X)),cons(Y,Z)) -> filter#(X,sieve(Y)) ->
    filter#(s(s(X)),cons(Y,Z)) -> sieve#(Y)
    filter#(s(s(X)),cons(Y,Z)) -> filter#(X,sieve(Y)) ->
    filter#(s(s(X)),cons(Y,Z)) -> filter#(X,sieve(Y))
    filter#(s(s(X)),cons(Y,Z)) -> filter#(X,sieve(Y)) ->
    filter#(s(s(X)),cons(Y,Z)) -> filter#(s(s(X)),Z)
    filter#(s(s(X)),cons(Y,Z)) -> filter#(X,sieve(Y)) ->
    filter#(s(s(X)),cons(Y,Z)) ->
    if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))
    filter#(s(s(X)),cons(Y,Z)) -> sieve#(Y) ->
    sieve#(cons(X,Y)) -> sieve#(Y)
    filter#(s(s(X)),cons(Y,Z)) -> sieve#(Y) ->
    sieve#(cons(X,Y)) -> filter#(X,sieve(Y))
    sieve#(cons(X,Y)) -> filter#(X,sieve(Y)) ->
    filter#(s(s(X)),cons(Y,Z)) -> sieve#(Y)
    sieve#(cons(X,Y)) -> filter#(X,sieve(Y)) ->
    filter#(s(s(X)),cons(Y,Z)) -> filter#(X,sieve(Y))
    sieve#(cons(X,Y)) -> filter#(X,sieve(Y)) ->
    filter#(s(s(X)),cons(Y,Z)) -> filter#(s(s(X)),Z)
    sieve#(cons(X,Y)) -> filter#(X,sieve(Y)) ->
    filter#(s(s(X)),cons(Y,Z)) ->
    if#(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))
    sieve#(cons(X,Y)) -> sieve#(Y) -> sieve#(cons(X,Y)) -> sieve#(Y)
    sieve#(cons(X,Y)) -> sieve#(Y) ->
    sieve#(cons(X,Y)) -> filter#(X,sieve(Y))
    from#(X) -> from#(s(X)) -> from#(X) -> from#(s(X))
    primes#() -> sieve#(from(s(s(0())))) ->
    sieve#(cons(X,Y)) -> sieve#(Y)
    primes#() -> sieve#(from(s(s(0())))) ->
    sieve#(cons(X,Y)) -> filter#(X,sieve(Y))
    primes#() -> from#(s(s(0()))) -> from#(X) -> from#(s(X))
   SCC Processor:
    #sccs: 2
    #rules: 6
    #arcs: 20/81
    DPs:
     from#(X) -> from#(s(X))
    TRS:
     primes() -> sieve(from(s(s(0()))))
     from(X) -> cons(X,from(s(X)))
     head(cons(X,Y)) -> X
     tail(cons(X,Y)) -> Y
     if(true(),X,Y) -> X
     if(false(),X,Y) -> Y
     filter(s(s(X)),cons(Y,Z)) ->
     if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))
     sieve(cons(X,Y)) -> cons(X,filter(X,sieve(Y)))
    Open
    
    DPs:
     filter#(s(s(X)),cons(Y,Z)) -> filter#(s(s(X)),Z)
     filter#(s(s(X)),cons(Y,Z)) -> filter#(X,sieve(Y))
     filter#(s(s(X)),cons(Y,Z)) -> sieve#(Y)
     sieve#(cons(X,Y)) -> filter#(X,sieve(Y))
     sieve#(cons(X,Y)) -> sieve#(Y)
    TRS:
     primes() -> sieve(from(s(s(0()))))
     from(X) -> cons(X,from(s(X)))
     head(cons(X,Y)) -> X
     tail(cons(X,Y)) -> Y
     if(true(),X,Y) -> X
     if(false(),X,Y) -> Y
     filter(s(s(X)),cons(Y,Z)) ->
     if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))
     sieve(cons(X,Y)) -> cons(X,filter(X,sieve(Y)))
    Open