YES

Problem:
 a(a(divides(),0()),a(s(),y)) -> true()
 a(a(divides(),a(s(),x)),a(s(),y)) -> a(a(a(div2(),x),a(s(),y)),y)
 a(a(a(div2(),x),y),0()) -> a(a(divides(),x),y)
 a(a(a(div2(),0()),y),a(s(),z)) -> false()
 a(a(a(div2(),a(s(),x)),y),a(s(),z)) -> a(a(a(div2(),x),y),z)
 a(a(filter(),f),nil()) -> nil()
 a(a(filter(),f),a(a(cons(),x),xs)) -> a(a(a(if(),a(f,x)),x),a(a(filter(),f),xs))
 a(a(a(if(),true()),x),xs) -> a(a(cons(),x),xs)
 a(a(a(if(),false()),x),xs) -> xs
 a(a(not(),f),x) -> a(not2(),a(f,x))
 a(not2(),true()) -> false()
 a(not2(),false()) -> true()
 a(sieve(),nil()) -> nil()
 a(sieve(),a(a(cons(),x),xs)) ->
 a(a(cons(),x),a(sieve(),a(a(filter(),a(not(),a(divides(),x))),xs)))

Proof:
 Uncurry Processor:
  divides2(0(),s1(y)) -> true()
  divides2(s1(x),s1(y)) -> div23(x,s1(y),y)
  div23(x,y,0()) -> divides2(x,y)
  div23(0(),y,s1(z)) -> false()
  div23(s1(x),y,s1(z)) -> div23(x,y,z)
  filter2(f,nil()) -> nil()
  filter2(f,cons2(x,xs)) -> if3(a(f,x),x,filter2(f,xs))
  if3(true(),x,xs) -> cons2(x,xs)
  if3(false(),x,xs) -> xs
  not2(f,x) -> not21(a(f,x))
  not21(true()) -> false()
  not21(false()) -> true()
  sieve1(nil()) -> nil()
  sieve1(cons2(x,xs)) -> cons2(x,sieve1(filter2(not1(divides1(x)),xs)))
  a(divides1(x6),x7) -> divides2(x6,x7)
  a(divides(),x7) -> divides1(x7)
  a(s(),x7) -> s1(x7)
  a(div22(x6,x5),x7) -> div23(x6,x5,x7)
  a(div21(x6),x7) -> div22(x6,x7)
  a(div2(),x7) -> div21(x7)
  a(filter1(x6),x7) -> filter2(x6,x7)
  a(filter(),x7) -> filter1(x7)
  a(cons1(x6),x7) -> cons2(x6,x7)
  a(cons(),x7) -> cons1(x7)
  a(if2(x6,x5),x7) -> if3(x6,x5,x7)
  a(if1(x6),x7) -> if2(x6,x7)
  a(if(),x7) -> if1(x7)
  a(not1(x6),x7) -> not2(x6,x7)
  a(not(),x7) -> not1(x7)
  a(not2(),x7) -> not21(x7)
  a(sieve(),x7) -> sieve1(x7)
  DP Processor:
   DPs:
    divides{2,#}(s1(x),s1(y)) -> div2{3,#}(x,s1(y),y)
    div2{3,#}(x,y,0()) -> divides{2,#}(x,y)
    div2{3,#}(s1(x),y,s1(z)) -> div2{3,#}(x,y,z)
    filter{2,#}(f,cons2(x,xs)) -> filter{2,#}(f,xs)
    filter{2,#}(f,cons2(x,xs)) -> a#(f,x)
    filter{2,#}(f,cons2(x,xs)) -> if{3,#}(a(f,x),x,filter2(f,xs))
    not{2,#}(f,x) -> a#(f,x)
    not{2,#}(f,x) -> not2{1,#}(a(f,x))
    sieve{1,#}(cons2(x,xs)) -> filter{2,#}(not1(divides1(x)),xs)
    sieve{1,#}(cons2(x,xs)) -> sieve{1,#}(filter2(not1(divides1(x)),xs))
    a#(divides1(x6),x7) -> divides{2,#}(x6,x7)
    a#(div22(x6,x5),x7) -> div2{3,#}(x6,x5,x7)
    a#(filter1(x6),x7) -> filter{2,#}(x6,x7)
    a#(if2(x6,x5),x7) -> if{3,#}(x6,x5,x7)
    a#(not1(x6),x7) -> not{2,#}(x6,x7)
    a#(not2(),x7) -> not2{1,#}(x7)
    a#(sieve(),x7) -> sieve{1,#}(x7)
   TRS:
    divides2(0(),s1(y)) -> true()
    divides2(s1(x),s1(y)) -> div23(x,s1(y),y)
    div23(x,y,0()) -> divides2(x,y)
    div23(0(),y,s1(z)) -> false()
    div23(s1(x),y,s1(z)) -> div23(x,y,z)
    filter2(f,nil()) -> nil()
    filter2(f,cons2(x,xs)) -> if3(a(f,x),x,filter2(f,xs))
    if3(true(),x,xs) -> cons2(x,xs)
    if3(false(),x,xs) -> xs
    not2(f,x) -> not21(a(f,x))
    not21(true()) -> false()
    not21(false()) -> true()
    sieve1(nil()) -> nil()
    sieve1(cons2(x,xs)) -> cons2(x,sieve1(filter2(not1(divides1(x)),xs)))
    a(divides1(x6),x7) -> divides2(x6,x7)
    a(divides(),x7) -> divides1(x7)
    a(s(),x7) -> s1(x7)
    a(div22(x6,x5),x7) -> div23(x6,x5,x7)
    a(div21(x6),x7) -> div22(x6,x7)
    a(div2(),x7) -> div21(x7)
    a(filter1(x6),x7) -> filter2(x6,x7)
    a(filter(),x7) -> filter1(x7)
    a(cons1(x6),x7) -> cons2(x6,x7)
    a(cons(),x7) -> cons1(x7)
    a(if2(x6,x5),x7) -> if3(x6,x5,x7)
    a(if1(x6),x7) -> if2(x6,x7)
    a(if(),x7) -> if1(x7)
    a(not1(x6),x7) -> not2(x6,x7)
    a(not(),x7) -> not1(x7)
    a(not2(),x7) -> not21(x7)
    a(sieve(),x7) -> sieve1(x7)
   TDG Processor:
    DPs:
     divides{2,#}(s1(x),s1(y)) -> div2{3,#}(x,s1(y),y)
     div2{3,#}(x,y,0()) -> divides{2,#}(x,y)
     div2{3,#}(s1(x),y,s1(z)) -> div2{3,#}(x,y,z)
     filter{2,#}(f,cons2(x,xs)) -> filter{2,#}(f,xs)
     filter{2,#}(f,cons2(x,xs)) -> a#(f,x)
     filter{2,#}(f,cons2(x,xs)) -> if{3,#}(a(f,x),x,filter2(f,xs))
     not{2,#}(f,x) -> a#(f,x)
     not{2,#}(f,x) -> not2{1,#}(a(f,x))
     sieve{1,#}(cons2(x,xs)) -> filter{2,#}(not1(divides1(x)),xs)
     sieve{1,#}(cons2(x,xs)) -> sieve{1,#}(filter2(not1(divides1(x)),xs))
     a#(divides1(x6),x7) -> divides{2,#}(x6,x7)
     a#(div22(x6,x5),x7) -> div2{3,#}(x6,x5,x7)
     a#(filter1(x6),x7) -> filter{2,#}(x6,x7)
     a#(if2(x6,x5),x7) -> if{3,#}(x6,x5,x7)
     a#(not1(x6),x7) -> not{2,#}(x6,x7)
     a#(not2(),x7) -> not2{1,#}(x7)
     a#(sieve(),x7) -> sieve{1,#}(x7)
    TRS:
     divides2(0(),s1(y)) -> true()
     divides2(s1(x),s1(y)) -> div23(x,s1(y),y)
     div23(x,y,0()) -> divides2(x,y)
     div23(0(),y,s1(z)) -> false()
     div23(s1(x),y,s1(z)) -> div23(x,y,z)
     filter2(f,nil()) -> nil()
     filter2(f,cons2(x,xs)) -> if3(a(f,x),x,filter2(f,xs))
     if3(true(),x,xs) -> cons2(x,xs)
     if3(false(),x,xs) -> xs
     not2(f,x) -> not21(a(f,x))
     not21(true()) -> false()
     not21(false()) -> true()
     sieve1(nil()) -> nil()
     sieve1(cons2(x,xs)) -> cons2(x,sieve1(filter2(not1(divides1(x)),xs)))
     a(divides1(x6),x7) -> divides2(x6,x7)
     a(divides(),x7) -> divides1(x7)
     a(s(),x7) -> s1(x7)
     a(div22(x6,x5),x7) -> div23(x6,x5,x7)
     a(div21(x6),x7) -> div22(x6,x7)
     a(div2(),x7) -> div21(x7)
     a(filter1(x6),x7) -> filter2(x6,x7)
     a(filter(),x7) -> filter1(x7)
     a(cons1(x6),x7) -> cons2(x6,x7)
     a(cons(),x7) -> cons1(x7)
     a(if2(x6,x5),x7) -> if3(x6,x5,x7)
     a(if1(x6),x7) -> if2(x6,x7)
     a(if(),x7) -> if1(x7)
     a(not1(x6),x7) -> not2(x6,x7)
     a(not(),x7) -> not1(x7)
     a(not2(),x7) -> not21(x7)
     a(sieve(),x7) -> sieve1(x7)
    graph:
     sieve{1,#}(cons2(x,xs)) -> sieve{1,#}(filter2(not1(divides1(x)),xs)) ->
     sieve{1,#}(cons2(x,xs)) -> sieve{1,#}(filter2(not1(divides1(x)),xs))
     sieve{1,#}(cons2(x,xs)) -> sieve{1,#}(filter2(not1(divides1(x)),xs)) ->
     sieve{1,#}(cons2(x,xs)) -> filter{2,#}(not1(divides1(x)),xs)
     sieve{1,#}(cons2(x,xs)) -> filter{2,#}(not1(divides1(x)),xs) ->
     filter{2,#}(f,cons2(x,xs)) -> if{3,#}(a(f,x),x,filter2(f,xs))
     sieve{1,#}(cons2(x,xs)) -> filter{2,#}(not1(divides1(x)),xs) ->
     filter{2,#}(f,cons2(x,xs)) -> a#(f,x)
     sieve{1,#}(cons2(x,xs)) -> filter{2,#}(not1(divides1(x)),xs) ->
     filter{2,#}(f,cons2(x,xs)) -> filter{2,#}(f,xs)
     not{2,#}(f,x) -> a#(f,x) -> a#(sieve(),x7) -> sieve{1,#}(x7)
     not{2,#}(f,x) -> a#(f,x) -> a#(not2(),x7) -> not2{1,#}(x7)
     not{2,#}(f,x) -> a#(f,x) -> a#(not1(x6),x7) -> not{2,#}(x6,x7)
     not{2,#}(f,x) -> a#(f,x) -> a#(if2(x6,x5),x7) -> if{3,#}(x6,x5,x7)
     not{2,#}(f,x) -> a#(f,x) -> a#(filter1(x6),x7) -> filter{2,#}(x6,x7)
     not{2,#}(f,x) -> a#(f,x) -> a#(div22(x6,x5),x7) -> div2{3,#}(x6,x5,x7)
     not{2,#}(f,x) -> a#(f,x) ->
     a#(divides1(x6),x7) -> divides{2,#}(x6,x7)
     a#(not1(x6),x7) -> not{2,#}(x6,x7) ->
     not{2,#}(f,x) -> not2{1,#}(a(f,x))
     a#(not1(x6),x7) -> not{2,#}(x6,x7) ->
     not{2,#}(f,x) -> a#(f,x)
     a#(filter1(x6),x7) -> filter{2,#}(x6,x7) ->
     filter{2,#}(f,cons2(x,xs)) -> if{3,#}(a(f,x),x,filter2(f,xs))
     a#(filter1(x6),x7) -> filter{2,#}(x6,x7) ->
     filter{2,#}(f,cons2(x,xs)) -> a#(f,x)
     a#(filter1(x6),x7) -> filter{2,#}(x6,x7) ->
     filter{2,#}(f,cons2(x,xs)) -> filter{2,#}(f,xs)
     a#(div22(x6,x5),x7) -> div2{3,#}(x6,x5,x7) ->
     div2{3,#}(s1(x),y,s1(z)) -> div2{3,#}(x,y,z)
     a#(div22(x6,x5),x7) -> div2{3,#}(x6,x5,x7) ->
     div2{3,#}(x,y,0()) -> divides{2,#}(x,y)
     a#(divides1(x6),x7) -> divides{2,#}(x6,x7) ->
     divides{2,#}(s1(x),s1(y)) -> div2{3,#}(x,s1(y),y)
     a#(sieve(),x7) -> sieve{1,#}(x7) ->
     sieve{1,#}(cons2(x,xs)) -> sieve{1,#}(filter2(not1(divides1(x)),xs))
     a#(sieve(),x7) -> sieve{1,#}(x7) ->
     sieve{1,#}(cons2(x,xs)) -> filter{2,#}(not1(divides1(x)),xs)
     filter{2,#}(f,cons2(x,xs)) -> a#(f,x) ->
     a#(sieve(),x7) -> sieve{1,#}(x7)
     filter{2,#}(f,cons2(x,xs)) -> a#(f,x) ->
     a#(not2(),x7) -> not2{1,#}(x7)
     filter{2,#}(f,cons2(x,xs)) -> a#(f,x) ->
     a#(not1(x6),x7) -> not{2,#}(x6,x7)
     filter{2,#}(f,cons2(x,xs)) -> a#(f,x) ->
     a#(if2(x6,x5),x7) -> if{3,#}(x6,x5,x7)
     filter{2,#}(f,cons2(x,xs)) -> a#(f,x) ->
     a#(filter1(x6),x7) -> filter{2,#}(x6,x7)
     filter{2,#}(f,cons2(x,xs)) -> a#(f,x) ->
     a#(div22(x6,x5),x7) -> div2{3,#}(x6,x5,x7)
     filter{2,#}(f,cons2(x,xs)) -> a#(f,x) ->
     a#(divides1(x6),x7) -> divides{2,#}(x6,x7)
     filter{2,#}(f,cons2(x,xs)) -> filter{2,#}(f,xs) ->
     filter{2,#}(f,cons2(x,xs)) -> if{3,#}(a(f,x),x,filter2(f,xs))
     filter{2,#}(f,cons2(x,xs)) -> filter{2,#}(f,xs) ->
     filter{2,#}(f,cons2(x,xs)) -> a#(f,x)
     filter{2,#}(f,cons2(x,xs)) -> filter{2,#}(f,xs) ->
     filter{2,#}(f,cons2(x,xs)) -> filter{2,#}(f,xs)
     div2{3,#}(s1(x),y,s1(z)) -> div2{3,#}(x,y,z) ->
     div2{3,#}(s1(x),y,s1(z)) -> div2{3,#}(x,y,z)
     div2{3,#}(s1(x),y,s1(z)) -> div2{3,#}(x,y,z) ->
     div2{3,#}(x,y,0()) -> divides{2,#}(x,y)
     div2{3,#}(x,y,0()) -> divides{2,#}(x,y) ->
     divides{2,#}(s1(x),s1(y)) -> div2{3,#}(x,s1(y),y)
     divides{2,#}(s1(x),s1(y)) -> div2{3,#}(x,s1(y),y) ->
     div2{3,#}(s1(x),y,s1(z)) -> div2{3,#}(x,y,z)
     divides{2,#}(s1(x),s1(y)) -> div2{3,#}(x,s1(y),y) -> div2{3,#}(x,y,0()) -> divides{2,#}(x,y)
    SCC Processor:
     #sccs: 2
     #rules: 11
     #arcs: 37/289
     DPs:
      sieve{1,#}(cons2(x,xs)) -> sieve{1,#}(filter2(not1(divides1(x)),xs))
      sieve{1,#}(cons2(x,xs)) -> filter{2,#}(not1(divides1(x)),xs)
      filter{2,#}(f,cons2(x,xs)) -> filter{2,#}(f,xs)
      filter{2,#}(f,cons2(x,xs)) -> a#(f,x)
      a#(filter1(x6),x7) -> filter{2,#}(x6,x7)
      a#(not1(x6),x7) -> not{2,#}(x6,x7)
      not{2,#}(f,x) -> a#(f,x)
      a#(sieve(),x7) -> sieve{1,#}(x7)
     TRS:
      divides2(0(),s1(y)) -> true()
      divides2(s1(x),s1(y)) -> div23(x,s1(y),y)
      div23(x,y,0()) -> divides2(x,y)
      div23(0(),y,s1(z)) -> false()
      div23(s1(x),y,s1(z)) -> div23(x,y,z)
      filter2(f,nil()) -> nil()
      filter2(f,cons2(x,xs)) -> if3(a(f,x),x,filter2(f,xs))
      if3(true(),x,xs) -> cons2(x,xs)
      if3(false(),x,xs) -> xs
      not2(f,x) -> not21(a(f,x))
      not21(true()) -> false()
      not21(false()) -> true()
      sieve1(nil()) -> nil()
      sieve1(cons2(x,xs)) -> cons2(x,sieve1(filter2(not1(divides1(x)),xs)))
      a(divides1(x6),x7) -> divides2(x6,x7)
      a(divides(),x7) -> divides1(x7)
      a(s(),x7) -> s1(x7)
      a(div22(x6,x5),x7) -> div23(x6,x5,x7)
      a(div21(x6),x7) -> div22(x6,x7)
      a(div2(),x7) -> div21(x7)
      a(filter1(x6),x7) -> filter2(x6,x7)
      a(filter(),x7) -> filter1(x7)
      a(cons1(x6),x7) -> cons2(x6,x7)
      a(cons(),x7) -> cons1(x7)
      a(if2(x6,x5),x7) -> if3(x6,x5,x7)
      a(if1(x6),x7) -> if2(x6,x7)
      a(if(),x7) -> if1(x7)
      a(not1(x6),x7) -> not2(x6,x7)
      a(not(),x7) -> not1(x7)
      a(not2(),x7) -> not21(x7)
      a(sieve(),x7) -> sieve1(x7)
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [sieve{1,#}](x0) = 0,
       
       [not{2,#}](x0, x1) = 2x0,
       
       [a#](x0, x1) = 2x0,
       
       [filter{2,#}](x0, x1) = 2x0,
       
       [sieve1](x0) = 0,
       
       [not21](x0) = 0,
       
       [not2](x0, x1) = 2x1,
       
       [not1](x0) = 2x0,
       
       [if1](x0) = 2x0 + 3/2,
       
       [if3](x0, x1, x2) = 2x2,
       
       [if2](x0, x1) = 0,
       
       [cons2](x0, x1) = 0,
       
       [cons1](x0) = 0,
       
       [filter2](x0, x1) = 0,
       
       [filter1](x0) = x0,
       
       [div21](x0) = 2x0,
       
       [div23](x0, x1, x2) = 1,
       
       [div22](x0, x1) = 0,
       
       [s1](x0) = 0,
       
       [divides2](x0, x1) = 1,
       
       [divides1](x0) = 0,
       
       [sieve] = 2,
       
       [not2] = 0,
       
       [not] = 0,
       
       [if] = 0,
       
       [cons] = 0,
       
       [nil] = 0,
       
       [filter] = 0,
       
       [false] = 0,
       
       [div2] = 0,
       
       [true] = 0,
       
       [s] = 0,
       
       [a](x0, x1) = 2x1 + 3/2,
       
       [0] = 0,
       
       [divides] = 0
      orientation:
       sieve{1,#}(cons2(x,xs)) = 0 >= 0 = sieve{1,#}(filter2(not1(divides1(x)),xs))
       
       sieve{1,#}(cons2(x,xs)) = 0 >= 0 = filter{2,#}(not1(divides1(x)),xs)
       
       filter{2,#}(f,cons2(x,xs)) = 2f >= 2f = filter{2,#}(f,xs)
       
       filter{2,#}(f,cons2(x,xs)) = 2f >= 2f = a#(f,x)
       
       a#(filter1(x6),x7) = 2x6 >= 2x6 = filter{2,#}(x6,x7)
       
       a#(not1(x6),x7) = 4x6 >= 2x6 = not{2,#}(x6,x7)
       
       not{2,#}(f,x) = 2f >= 2f = a#(f,x)
       
       a#(sieve(),x7) = 4 >= 0 = sieve{1,#}(x7)
       
       divides2(0(),s1(y)) = 1 >= 0 = true()
       
       divides2(s1(x),s1(y)) = 1 >= 1 = div23(x,s1(y),y)
       
       div23(x,y,0()) = 1 >= 1 = divides2(x,y)
       
       div23(0(),y,s1(z)) = 1 >= 0 = false()
       
       div23(s1(x),y,s1(z)) = 1 >= 1 = div23(x,y,z)
       
       filter2(f,nil()) = 0 >= 0 = nil()
       
       filter2(f,cons2(x,xs)) = 0 >= 0 = if3(a(f,x),x,filter2(f,xs))
       
       if3(true(),x,xs) = 2xs >= 0 = cons2(x,xs)
       
       if3(false(),x,xs) = 2xs >= xs = xs
       
       not2(f,x) = 2x >= 0 = not21(a(f,x))
       
       not21(true()) = 0 >= 0 = false()
       
       not21(false()) = 0 >= 0 = true()
       
       sieve1(nil()) = 0 >= 0 = nil()
       
       sieve1(cons2(x,xs)) = 0 >= 0 = cons2(x,sieve1(filter2(not1(divides1(x)),xs)))
       
       a(divides1(x6),x7) = 2x7 + 3/2 >= 1 = divides2(x6,x7)
       
       a(divides(),x7) = 2x7 + 3/2 >= 0 = divides1(x7)
       
       a(s(),x7) = 2x7 + 3/2 >= 0 = s1(x7)
       
       a(div22(x6,x5),x7) = 2x7 + 3/2 >= 1 = div23(x6,x5,x7)
       
       a(div21(x6),x7) = 2x7 + 3/2 >= 0 = div22(x6,x7)
       
       a(div2(),x7) = 2x7 + 3/2 >= 2x7 = div21(x7)
       
       a(filter1(x6),x7) = 2x7 + 3/2 >= 0 = filter2(x6,x7)
       
       a(filter(),x7) = 2x7 + 3/2 >= x7 = filter1(x7)
       
       a(cons1(x6),x7) = 2x7 + 3/2 >= 0 = cons2(x6,x7)
       
       a(cons(),x7) = 2x7 + 3/2 >= 0 = cons1(x7)
       
       a(if2(x6,x5),x7) = 2x7 + 3/2 >= 2x7 = if3(x6,x5,x7)
       
       a(if1(x6),x7) = 2x7 + 3/2 >= 0 = if2(x6,x7)
       
       a(if(),x7) = 2x7 + 3/2 >= 2x7 + 3/2 = if1(x7)
       
       a(not1(x6),x7) = 2x7 + 3/2 >= 2x7 = not2(x6,x7)
       
       a(not(),x7) = 2x7 + 3/2 >= 2x7 = not1(x7)
       
       a(not2(),x7) = 2x7 + 3/2 >= 0 = not21(x7)
       
       a(sieve(),x7) = 2x7 + 3/2 >= 0 = sieve1(x7)
      problem:
       DPs:
        sieve{1,#}(cons2(x,xs)) -> sieve{1,#}(filter2(not1(divides1(x)),xs))
        sieve{1,#}(cons2(x,xs)) -> filter{2,#}(not1(divides1(x)),xs)
        filter{2,#}(f,cons2(x,xs)) -> filter{2,#}(f,xs)
        filter{2,#}(f,cons2(x,xs)) -> a#(f,x)
        a#(filter1(x6),x7) -> filter{2,#}(x6,x7)
        a#(not1(x6),x7) -> not{2,#}(x6,x7)
        not{2,#}(f,x) -> a#(f,x)
       TRS:
        divides2(0(),s1(y)) -> true()
        divides2(s1(x),s1(y)) -> div23(x,s1(y),y)
        div23(x,y,0()) -> divides2(x,y)
        div23(0(),y,s1(z)) -> false()
        div23(s1(x),y,s1(z)) -> div23(x,y,z)
        filter2(f,nil()) -> nil()
        filter2(f,cons2(x,xs)) -> if3(a(f,x),x,filter2(f,xs))
        if3(true(),x,xs) -> cons2(x,xs)
        if3(false(),x,xs) -> xs
        not2(f,x) -> not21(a(f,x))
        not21(true()) -> false()
        not21(false()) -> true()
        sieve1(nil()) -> nil()
        sieve1(cons2(x,xs)) -> cons2(x,sieve1(filter2(not1(divides1(x)),xs)))
        a(divides1(x6),x7) -> divides2(x6,x7)
        a(divides(),x7) -> divides1(x7)
        a(s(),x7) -> s1(x7)
        a(div22(x6,x5),x7) -> div23(x6,x5,x7)
        a(div21(x6),x7) -> div22(x6,x7)
        a(div2(),x7) -> div21(x7)
        a(filter1(x6),x7) -> filter2(x6,x7)
        a(filter(),x7) -> filter1(x7)
        a(cons1(x6),x7) -> cons2(x6,x7)
        a(cons(),x7) -> cons1(x7)
        a(if2(x6,x5),x7) -> if3(x6,x5,x7)
        a(if1(x6),x7) -> if2(x6,x7)
        a(if(),x7) -> if1(x7)
        a(not1(x6),x7) -> not2(x6,x7)
        a(not(),x7) -> not1(x7)
        a(not2(),x7) -> not21(x7)
        a(sieve(),x7) -> sieve1(x7)
      SCC Processor:
       #sccs: 2
       #rules: 6
       #arcs: 17/49
       DPs:
        sieve{1,#}(cons2(x,xs)) -> sieve{1,#}(filter2(not1(divides1(x)),xs))
       TRS:
        divides2(0(),s1(y)) -> true()
        divides2(s1(x),s1(y)) -> div23(x,s1(y),y)
        div23(x,y,0()) -> divides2(x,y)
        div23(0(),y,s1(z)) -> false()
        div23(s1(x),y,s1(z)) -> div23(x,y,z)
        filter2(f,nil()) -> nil()
        filter2(f,cons2(x,xs)) -> if3(a(f,x),x,filter2(f,xs))
        if3(true(),x,xs) -> cons2(x,xs)
        if3(false(),x,xs) -> xs
        not2(f,x) -> not21(a(f,x))
        not21(true()) -> false()
        not21(false()) -> true()
        sieve1(nil()) -> nil()
        sieve1(cons2(x,xs)) -> cons2(x,sieve1(filter2(not1(divides1(x)),xs)))
        a(divides1(x6),x7) -> divides2(x6,x7)
        a(divides(),x7) -> divides1(x7)
        a(s(),x7) -> s1(x7)
        a(div22(x6,x5),x7) -> div23(x6,x5,x7)
        a(div21(x6),x7) -> div22(x6,x7)
        a(div2(),x7) -> div21(x7)
        a(filter1(x6),x7) -> filter2(x6,x7)
        a(filter(),x7) -> filter1(x7)
        a(cons1(x6),x7) -> cons2(x6,x7)
        a(cons(),x7) -> cons1(x7)
        a(if2(x6,x5),x7) -> if3(x6,x5,x7)
        a(if1(x6),x7) -> if2(x6,x7)
        a(if(),x7) -> if1(x7)
        a(not1(x6),x7) -> not2(x6,x7)
        a(not(),x7) -> not1(x7)
        a(not2(),x7) -> not21(x7)
        a(sieve(),x7) -> sieve1(x7)
       Arctic Interpretation Processor:
        dimension: 1
        interpretation:
         [sieve{1,#}](x0) = 4x0,
         
         [sieve1](x0) = 1x0 + 0,
         
         [not21](x0) = 0,
         
         [not2](x0, x1) = 3,
         
         [not1](x0) = x0 + 3,
         
         [if1](x0) = 2x0,
         
         [if3](x0, x1, x2) = x1 + 1x2 + 0,
         
         [if2](x0, x1) = 1x0 + 2x1,
         
         [cons2](x0, x1) = x0 + 1x1 + 0,
         
         [cons1](x0) = x0 + 0,
         
         [filter2](x0, x1) = x1,
         
         [filter1](x0) = x0,
         
         [div21](x0) = 2x0,
         
         [div23](x0, x1, x2) = x1 + x2 + 0,
         
         [div22](x0, x1) = 1x1,
         
         [s1](x0) = x0 + 0,
         
         [divides2](x0, x1) = x1,
         
         [divides1](x0) = 4,
         
         [sieve] = 1,
         
         [not2] = 4,
         
         [not] = 3,
         
         [if] = 0,
         
         [cons] = 2,
         
         [nil] = 3,
         
         [filter] = 0,
         
         [false] = 0,
         
         [div2] = 0,
         
         [true] = 0,
         
         [s] = 4,
         
         [a](x0, x1) = x0 + 2x1 + 0,
         
         [0] = 0,
         
         [divides] = 5
        orientation:
         sieve{1,#}(cons2(x,xs)) = 4x + 5xs + 4 >= 4xs = sieve{1,#}(filter2(not1(divides1(x)),xs))
         
         divides2(0(),s1(y)) = y + 0 >= 0 = true()
         
         divides2(s1(x),s1(y)) = y + 0 >= y + 0 = div23(x,s1(y),y)
         
         div23(x,y,0()) = y + 0 >= y = divides2(x,y)
         
         div23(0(),y,s1(z)) = y + z + 0 >= 0 = false()
         
         div23(s1(x),y,s1(z)) = y + z + 0 >= y + z + 0 = div23(x,y,z)
         
         filter2(f,nil()) = 3 >= 3 = nil()
         
         filter2(f,cons2(x,xs)) = x + 1xs + 0 >= x + 1xs + 0 = if3(a(f,x),x,filter2(f,xs))
         
         if3(true(),x,xs) = x + 1xs + 0 >= x + 1xs + 0 = cons2(x,xs)
         
         if3(false(),x,xs) = x + 1xs + 0 >= xs = xs
         
         not2(f,x) = 3 >= 0 = not21(a(f,x))
         
         not21(true()) = 0 >= 0 = false()
         
         not21(false()) = 0 >= 0 = true()
         
         sieve1(nil()) = 4 >= 3 = nil()
         
         sieve1(cons2(x,xs)) = 1x + 2xs + 1 >= x + 2xs + 1 = cons2(x,sieve1(filter2(not1(divides1(x)),xs)))
         
         a(divides1(x6),x7) = 2x7 + 4 >= x7 = divides2(x6,x7)
         
         a(divides(),x7) = 2x7 + 5 >= 4 = divides1(x7)
         
         a(s(),x7) = 2x7 + 4 >= x7 + 0 = s1(x7)
         
         a(div22(x6,x5),x7) = 1x5 + 2x7 + 0 >= x5 + x7 + 0 = div23(x6,x5,x7)
         
         a(div21(x6),x7) = 2x6 + 2x7 + 0 >= 1x7 = div22(x6,x7)
         
         a(div2(),x7) = 2x7 + 0 >= 2x7 = div21(x7)
         
         a(filter1(x6),x7) = x6 + 2x7 + 0 >= x7 = filter2(x6,x7)
         
         a(filter(),x7) = 2x7 + 0 >= x7 = filter1(x7)
         
         a(cons1(x6),x7) = x6 + 2x7 + 0 >= x6 + 1x7 + 0 = cons2(x6,x7)
         
         a(cons(),x7) = 2x7 + 2 >= x7 + 0 = cons1(x7)
         
         a(if2(x6,x5),x7) = 2x5 + 1x6 + 2x7 + 0 >= x5 + 1x7 + 0 = if3(x6,x5,x7)
         
         a(if1(x6),x7) = 2x6 + 2x7 + 0 >= 1x6 + 2x7 = if2(x6,x7)
         
         a(if(),x7) = 2x7 + 0 >= 2x7 = if1(x7)
         
         a(not1(x6),x7) = x6 + 2x7 + 3 >= 3 = not2(x6,x7)
         
         a(not(),x7) = 2x7 + 3 >= x7 + 3 = not1(x7)
         
         a(not2(),x7) = 2x7 + 4 >= 0 = not21(x7)
         
         a(sieve(),x7) = 2x7 + 1 >= 1x7 + 0 = sieve1(x7)
        problem:
         DPs:
          
         TRS:
          divides2(0(),s1(y)) -> true()
          divides2(s1(x),s1(y)) -> div23(x,s1(y),y)
          div23(x,y,0()) -> divides2(x,y)
          div23(0(),y,s1(z)) -> false()
          div23(s1(x),y,s1(z)) -> div23(x,y,z)
          filter2(f,nil()) -> nil()
          filter2(f,cons2(x,xs)) -> if3(a(f,x),x,filter2(f,xs))
          if3(true(),x,xs) -> cons2(x,xs)
          if3(false(),x,xs) -> xs
          not2(f,x) -> not21(a(f,x))
          not21(true()) -> false()
          not21(false()) -> true()
          sieve1(nil()) -> nil()
          sieve1(cons2(x,xs)) -> cons2(x,sieve1(filter2(not1(divides1(x)),xs)))
          a(divides1(x6),x7) -> divides2(x6,x7)
          a(divides(),x7) -> divides1(x7)
          a(s(),x7) -> s1(x7)
          a(div22(x6,x5),x7) -> div23(x6,x5,x7)
          a(div21(x6),x7) -> div22(x6,x7)
          a(div2(),x7) -> div21(x7)
          a(filter1(x6),x7) -> filter2(x6,x7)
          a(filter(),x7) -> filter1(x7)
          a(cons1(x6),x7) -> cons2(x6,x7)
          a(cons(),x7) -> cons1(x7)
          a(if2(x6,x5),x7) -> if3(x6,x5,x7)
          a(if1(x6),x7) -> if2(x6,x7)
          a(if(),x7) -> if1(x7)
          a(not1(x6),x7) -> not2(x6,x7)
          a(not(),x7) -> not1(x7)
          a(not2(),x7) -> not21(x7)
          a(sieve(),x7) -> sieve1(x7)
        Qed
       
       DPs:
        filter{2,#}(f,cons2(x,xs)) -> filter{2,#}(f,xs)
        filter{2,#}(f,cons2(x,xs)) -> a#(f,x)
        a#(filter1(x6),x7) -> filter{2,#}(x6,x7)
        a#(not1(x6),x7) -> not{2,#}(x6,x7)
        not{2,#}(f,x) -> a#(f,x)
       TRS:
        divides2(0(),s1(y)) -> true()
        divides2(s1(x),s1(y)) -> div23(x,s1(y),y)
        div23(x,y,0()) -> divides2(x,y)
        div23(0(),y,s1(z)) -> false()
        div23(s1(x),y,s1(z)) -> div23(x,y,z)
        filter2(f,nil()) -> nil()
        filter2(f,cons2(x,xs)) -> if3(a(f,x),x,filter2(f,xs))
        if3(true(),x,xs) -> cons2(x,xs)
        if3(false(),x,xs) -> xs
        not2(f,x) -> not21(a(f,x))
        not21(true()) -> false()
        not21(false()) -> true()
        sieve1(nil()) -> nil()
        sieve1(cons2(x,xs)) -> cons2(x,sieve1(filter2(not1(divides1(x)),xs)))
        a(divides1(x6),x7) -> divides2(x6,x7)
        a(divides(),x7) -> divides1(x7)
        a(s(),x7) -> s1(x7)
        a(div22(x6,x5),x7) -> div23(x6,x5,x7)
        a(div21(x6),x7) -> div22(x6,x7)
        a(div2(),x7) -> div21(x7)
        a(filter1(x6),x7) -> filter2(x6,x7)
        a(filter(),x7) -> filter1(x7)
        a(cons1(x6),x7) -> cons2(x6,x7)
        a(cons(),x7) -> cons1(x7)
        a(if2(x6,x5),x7) -> if3(x6,x5,x7)
        a(if1(x6),x7) -> if2(x6,x7)
        a(if(),x7) -> if1(x7)
        a(not1(x6),x7) -> not2(x6,x7)
        a(not(),x7) -> not1(x7)
        a(not2(),x7) -> not21(x7)
        a(sieve(),x7) -> sieve1(x7)
       Subterm Criterion Processor:
        simple projection:
         pi(filter{2,#}) = 1
         pi(a#) = 1
         pi(not{2,#}) = 1
        problem:
         DPs:
          a#(filter1(x6),x7) -> filter{2,#}(x6,x7)
          a#(not1(x6),x7) -> not{2,#}(x6,x7)
          not{2,#}(f,x) -> a#(f,x)
         TRS:
          divides2(0(),s1(y)) -> true()
          divides2(s1(x),s1(y)) -> div23(x,s1(y),y)
          div23(x,y,0()) -> divides2(x,y)
          div23(0(),y,s1(z)) -> false()
          div23(s1(x),y,s1(z)) -> div23(x,y,z)
          filter2(f,nil()) -> nil()
          filter2(f,cons2(x,xs)) -> if3(a(f,x),x,filter2(f,xs))
          if3(true(),x,xs) -> cons2(x,xs)
          if3(false(),x,xs) -> xs
          not2(f,x) -> not21(a(f,x))
          not21(true()) -> false()
          not21(false()) -> true()
          sieve1(nil()) -> nil()
          sieve1(cons2(x,xs)) -> cons2(x,sieve1(filter2(not1(divides1(x)),xs)))
          a(divides1(x6),x7) -> divides2(x6,x7)
          a(divides(),x7) -> divides1(x7)
          a(s(),x7) -> s1(x7)
          a(div22(x6,x5),x7) -> div23(x6,x5,x7)
          a(div21(x6),x7) -> div22(x6,x7)
          a(div2(),x7) -> div21(x7)
          a(filter1(x6),x7) -> filter2(x6,x7)
          a(filter(),x7) -> filter1(x7)
          a(cons1(x6),x7) -> cons2(x6,x7)
          a(cons(),x7) -> cons1(x7)
          a(if2(x6,x5),x7) -> if3(x6,x5,x7)
          a(if1(x6),x7) -> if2(x6,x7)
          a(if(),x7) -> if1(x7)
          a(not1(x6),x7) -> not2(x6,x7)
          a(not(),x7) -> not1(x7)
          a(not2(),x7) -> not21(x7)
          a(sieve(),x7) -> sieve1(x7)
        SCC Processor:
         #sccs: 1
         #rules: 2
         #arcs: 9/9
         DPs:
          not{2,#}(f,x) -> a#(f,x)
          a#(not1(x6),x7) -> not{2,#}(x6,x7)
         TRS:
          divides2(0(),s1(y)) -> true()
          divides2(s1(x),s1(y)) -> div23(x,s1(y),y)
          div23(x,y,0()) -> divides2(x,y)
          div23(0(),y,s1(z)) -> false()
          div23(s1(x),y,s1(z)) -> div23(x,y,z)
          filter2(f,nil()) -> nil()
          filter2(f,cons2(x,xs)) -> if3(a(f,x),x,filter2(f,xs))
          if3(true(),x,xs) -> cons2(x,xs)
          if3(false(),x,xs) -> xs
          not2(f,x) -> not21(a(f,x))
          not21(true()) -> false()
          not21(false()) -> true()
          sieve1(nil()) -> nil()
          sieve1(cons2(x,xs)) -> cons2(x,sieve1(filter2(not1(divides1(x)),xs)))
          a(divides1(x6),x7) -> divides2(x6,x7)
          a(divides(),x7) -> divides1(x7)
          a(s(),x7) -> s1(x7)
          a(div22(x6,x5),x7) -> div23(x6,x5,x7)
          a(div21(x6),x7) -> div22(x6,x7)
          a(div2(),x7) -> div21(x7)
          a(filter1(x6),x7) -> filter2(x6,x7)
          a(filter(),x7) -> filter1(x7)
          a(cons1(x6),x7) -> cons2(x6,x7)
          a(cons(),x7) -> cons1(x7)
          a(if2(x6,x5),x7) -> if3(x6,x5,x7)
          a(if1(x6),x7) -> if2(x6,x7)
          a(if(),x7) -> if1(x7)
          a(not1(x6),x7) -> not2(x6,x7)
          a(not(),x7) -> not1(x7)
          a(not2(),x7) -> not21(x7)
          a(sieve(),x7) -> sieve1(x7)
         Subterm Criterion Processor:
          simple projection:
           pi(a#) = 0
           pi(not{2,#}) = 0
          problem:
           DPs:
            not{2,#}(f,x) -> a#(f,x)
           TRS:
            divides2(0(),s1(y)) -> true()
            divides2(s1(x),s1(y)) -> div23(x,s1(y),y)
            div23(x,y,0()) -> divides2(x,y)
            div23(0(),y,s1(z)) -> false()
            div23(s1(x),y,s1(z)) -> div23(x,y,z)
            filter2(f,nil()) -> nil()
            filter2(f,cons2(x,xs)) -> if3(a(f,x),x,filter2(f,xs))
            if3(true(),x,xs) -> cons2(x,xs)
            if3(false(),x,xs) -> xs
            not2(f,x) -> not21(a(f,x))
            not21(true()) -> false()
            not21(false()) -> true()
            sieve1(nil()) -> nil()
            sieve1(cons2(x,xs)) -> cons2(x,sieve1(filter2(not1(divides1(x)),xs)))
            a(divides1(x6),x7) -> divides2(x6,x7)
            a(divides(),x7) -> divides1(x7)
            a(s(),x7) -> s1(x7)
            a(div22(x6,x5),x7) -> div23(x6,x5,x7)
            a(div21(x6),x7) -> div22(x6,x7)
            a(div2(),x7) -> div21(x7)
            a(filter1(x6),x7) -> filter2(x6,x7)
            a(filter(),x7) -> filter1(x7)
            a(cons1(x6),x7) -> cons2(x6,x7)
            a(cons(),x7) -> cons1(x7)
            a(if2(x6,x5),x7) -> if3(x6,x5,x7)
            a(if1(x6),x7) -> if2(x6,x7)
            a(if(),x7) -> if1(x7)
            a(not1(x6),x7) -> not2(x6,x7)
            a(not(),x7) -> not1(x7)
            a(not2(),x7) -> not21(x7)
            a(sieve(),x7) -> sieve1(x7)
          SCC Processor:
           #sccs: 0
           #rules: 0
           #arcs: 2/1
           
     
     DPs:
      divides{2,#}(s1(x),s1(y)) -> div2{3,#}(x,s1(y),y)
      div2{3,#}(x,y,0()) -> divides{2,#}(x,y)
      div2{3,#}(s1(x),y,s1(z)) -> div2{3,#}(x,y,z)
     TRS:
      divides2(0(),s1(y)) -> true()
      divides2(s1(x),s1(y)) -> div23(x,s1(y),y)
      div23(x,y,0()) -> divides2(x,y)
      div23(0(),y,s1(z)) -> false()
      div23(s1(x),y,s1(z)) -> div23(x,y,z)
      filter2(f,nil()) -> nil()
      filter2(f,cons2(x,xs)) -> if3(a(f,x),x,filter2(f,xs))
      if3(true(),x,xs) -> cons2(x,xs)
      if3(false(),x,xs) -> xs
      not2(f,x) -> not21(a(f,x))
      not21(true()) -> false()
      not21(false()) -> true()
      sieve1(nil()) -> nil()
      sieve1(cons2(x,xs)) -> cons2(x,sieve1(filter2(not1(divides1(x)),xs)))
      a(divides1(x6),x7) -> divides2(x6,x7)
      a(divides(),x7) -> divides1(x7)
      a(s(),x7) -> s1(x7)
      a(div22(x6,x5),x7) -> div23(x6,x5,x7)
      a(div21(x6),x7) -> div22(x6,x7)
      a(div2(),x7) -> div21(x7)
      a(filter1(x6),x7) -> filter2(x6,x7)
      a(filter(),x7) -> filter1(x7)
      a(cons1(x6),x7) -> cons2(x6,x7)
      a(cons(),x7) -> cons1(x7)
      a(if2(x6,x5),x7) -> if3(x6,x5,x7)
      a(if1(x6),x7) -> if2(x6,x7)
      a(if(),x7) -> if1(x7)
      a(not1(x6),x7) -> not2(x6,x7)
      a(not(),x7) -> not1(x7)
      a(not2(),x7) -> not21(x7)
      a(sieve(),x7) -> sieve1(x7)
     Subterm Criterion Processor:
      simple projection:
       pi(divides{2,#}) = 0
       pi(div2{3,#}) = 0
      problem:
       DPs:
        div2{3,#}(x,y,0()) -> divides{2,#}(x,y)
       TRS:
        divides2(0(),s1(y)) -> true()
        divides2(s1(x),s1(y)) -> div23(x,s1(y),y)
        div23(x,y,0()) -> divides2(x,y)
        div23(0(),y,s1(z)) -> false()
        div23(s1(x),y,s1(z)) -> div23(x,y,z)
        filter2(f,nil()) -> nil()
        filter2(f,cons2(x,xs)) -> if3(a(f,x),x,filter2(f,xs))
        if3(true(),x,xs) -> cons2(x,xs)
        if3(false(),x,xs) -> xs
        not2(f,x) -> not21(a(f,x))
        not21(true()) -> false()
        not21(false()) -> true()
        sieve1(nil()) -> nil()
        sieve1(cons2(x,xs)) -> cons2(x,sieve1(filter2(not1(divides1(x)),xs)))
        a(divides1(x6),x7) -> divides2(x6,x7)
        a(divides(),x7) -> divides1(x7)
        a(s(),x7) -> s1(x7)
        a(div22(x6,x5),x7) -> div23(x6,x5,x7)
        a(div21(x6),x7) -> div22(x6,x7)
        a(div2(),x7) -> div21(x7)
        a(filter1(x6),x7) -> filter2(x6,x7)
        a(filter(),x7) -> filter1(x7)
        a(cons1(x6),x7) -> cons2(x6,x7)
        a(cons(),x7) -> cons1(x7)
        a(if2(x6,x5),x7) -> if3(x6,x5,x7)
        a(if1(x6),x7) -> if2(x6,x7)
        a(if(),x7) -> if1(x7)
        a(not1(x6),x7) -> not2(x6,x7)
        a(not(),x7) -> not1(x7)
        a(not2(),x7) -> not21(x7)
        a(sieve(),x7) -> sieve1(x7)
      SCC Processor:
       #sccs: 0
       #rules: 0
       #arcs: 5/1