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)
     Arctic Interpretation Processor:
      dimension: 1
      usable rules:
       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
      interpretation:
       [sieve{1,#}](x0) = x0 + 0,
       
       [not{2,#}](x0, x1) = x0 + 1x1 + 0,
       
       [a#](x0, x1) = x0 + 1x1 + 0,
       
       [filter{2,#}](x0, x1) = x0 + x1 + 0,
       
       [sieve1](x0) = 4x0 + 0,
       
       [not21](x0) = 4x0 + 0,
       
       [not2](x0, x1) = x0 + x1 + 2,
       
       [not1](x0) = x0,
       
       [if1](x0) = 6x0 + 0,
       
       [if3](x0, x1, x2) = 1x1 + x2 + 0,
       
       [if2](x0, x1) = 5x0 + x1 + 0,
       
       [cons2](x0, x1) = 1x0 + x1,
       
       [cons1](x0) = 4x0 + 2,
       
       [filter2](x0, x1) = x1 + 0,
       
       [filter1](x0) = x0 + 0,
       
       [div21](x0) = 1x0 + 0,
       
       [div23](x0, x1, x2) = 4x1 + 0,
       
       [div22](x0, x1) = x0 + x1 + 4,
       
       [s1](x0) = 3x0 + 1,
       
       [divides2](x0, x1) = 3x1 + 0,
       
       [divides1](x0) = 0,
       
       [sieve] = 2,
       
       [not2] = 1,
       
       [not] = 1,
       
       [if] = 2,
       
       [cons] = 1,
       
       [nil] = 2,
       
       [filter] = 2,
       
       [false] = 0,
       
       [div2] = 6,
       
       [true] = 0,
       
       [s] = 2,
       
       [a](x0, x1) = x1 + 2,
       
       [0] = 6,
       
       [divides] = 3
      orientation:
       sieve{1,#}(cons2(x,xs)) = 1x + xs + 0 >= xs + 0 = sieve{1,#}(filter2(not1(divides1(x)),xs))
       
       sieve{1,#}(cons2(x,xs)) = 1x + xs + 0 >= xs + 0 = filter{2,#}(not1(divides1(x)),xs)
       
       filter{2,#}(f,cons2(x,xs)) = f + 1x + xs + 0 >= f + xs + 0 = filter{2,#}(f,xs)
       
       filter{2,#}(f,cons2(x,xs)) = f + 1x + xs + 0 >= f + 1x + 0 = a#(f,x)
       
       a#(filter1(x6),x7) = x6 + 1x7 + 0 >= x6 + x7 + 0 = filter{2,#}(x6,x7)
       
       a#(not1(x6),x7) = x6 + 1x7 + 0 >= x6 + 1x7 + 0 = not{2,#}(x6,x7)
       
       not{2,#}(f,x) = f + 1x + 0 >= f + 1x + 0 = a#(f,x)
       
       a#(sieve(),x7) = 1x7 + 2 >= x7 + 0 = sieve{1,#}(x7)
       
       divides2(0(),s1(y)) = 6y + 4 >= 0 = true()
       
       divides2(s1(x),s1(y)) = 6y + 4 >= 7y + 5 = div23(x,s1(y),y)
       
       div23(x,y,0()) = 4y + 0 >= 3y + 0 = divides2(x,y)
       
       div23(0(),y,s1(z)) = 4y + 0 >= 0 = false()
       
       div23(s1(x),y,s1(z)) = 4y + 0 >= 4y + 0 = div23(x,y,z)
       
       filter2(f,nil()) = 2 >= 2 = nil()
       
       filter2(f,cons2(x,xs)) = 1x + xs + 0 >= 1x + xs + 0 = if3(a(f,x),x,filter2(f,xs))
       
       if3(true(),x,xs) = 1x + xs + 0 >= 1x + xs = cons2(x,xs)
       
       if3(false(),x,xs) = 1x + xs + 0 >= xs = xs
       
       not2(f,x) = f + x + 2 >= 4x + 6 = not21(a(f,x))
       
       not21(true()) = 4 >= 0 = false()
       
       not21(false()) = 4 >= 0 = true()
       
       sieve1(nil()) = 6 >= 2 = nil()
       
       sieve1(cons2(x,xs)) = 5x + 4xs + 0 >= 1x + 4xs + 4 = cons2(x,sieve1(filter2(not1(divides1(x)),xs)))
       
       a(divides1(x6),x7) = x7 + 2 >= 3x7 + 0 = divides2(x6,x7)
       
       a(divides(),x7) = x7 + 2 >= 0 = divides1(x7)
       
       a(s(),x7) = x7 + 2 >= 3x7 + 1 = s1(x7)
       
       a(div22(x6,x5),x7) = x7 + 2 >= 4x5 + 0 = div23(x6,x5,x7)
       
       a(div21(x6),x7) = x7 + 2 >= x6 + x7 + 4 = div22(x6,x7)
       
       a(div2(),x7) = x7 + 2 >= 1x7 + 0 = div21(x7)
       
       a(filter1(x6),x7) = x7 + 2 >= x7 + 0 = filter2(x6,x7)
       
       a(filter(),x7) = x7 + 2 >= x7 + 0 = filter1(x7)
       
       a(cons1(x6),x7) = x7 + 2 >= 1x6 + x7 = cons2(x6,x7)
       
       a(cons(),x7) = x7 + 2 >= 4x7 + 2 = cons1(x7)
       
       a(if2(x6,x5),x7) = x7 + 2 >= 1x5 + x7 + 0 = if3(x6,x5,x7)
       
       a(if1(x6),x7) = x7 + 2 >= 5x6 + x7 + 0 = if2(x6,x7)
       
       a(if(),x7) = x7 + 2 >= 6x7 + 0 = if1(x7)
       
       a(not1(x6),x7) = x7 + 2 >= x6 + x7 + 2 = not2(x6,x7)
       
       a(not(),x7) = x7 + 2 >= x7 = not1(x7)
       
       a(not2(),x7) = x7 + 2 >= 4x7 + 0 = not21(x7)
       
       a(sieve(),x7) = x7 + 2 >= 4x7 + 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)
      Restore Modifier:
       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)
        Matrix Interpretation Processor: dim=1
         
         usable rules:
          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
         interpretation:
          [sieve{1,#}](x0) = 4x0 + 1,
          
          [sieve1](x0) = 2x0,
          
          [not21](x0) = x0 + 4,
          
          [not2](x0, x1) = 0,
          
          [not1](x0) = x0,
          
          [if1](x0) = 0,
          
          [if3](x0, x1, x2) = 2x1 + 4x2 + 2,
          
          [if2](x0, x1) = 0,
          
          [cons2](x0, x1) = x0 + 4x1 + 1,
          
          [cons1](x0) = 0,
          
          [filter2](x0, x1) = 2x1,
          
          [filter1](x0) = 0,
          
          [div21](x0) = 0,
          
          [div23](x0, x1, x2) = 4x0 + 4x1 + 4,
          
          [div22](x0, x1) = 0,
          
          [s1](x0) = x0 + 2,
          
          [divides2](x0, x1) = 0,
          
          [divides1](x0) = x0,
          
          [sieve] = 0,
          
          [not2] = 0,
          
          [not] = 0,
          
          [if] = 0,
          
          [cons] = 0,
          
          [nil] = 4,
          
          [filter] = 0,
          
          [false] = 1,
          
          [div2] = 0,
          
          [true] = 3,
          
          [s] = 0,
          
          [a](x0, x1) = 1,
          
          [0] = 1,
          
          [divides] = 0
         orientation:
          sieve{1,#}(cons2(x,xs)) = 4x + 16xs + 5 >= 8xs + 1 = sieve{1,#}(filter2(not1(divides1(x)),xs))
          
          divides2(0(),s1(y)) = 0 >= 3 = true()
          
          divides2(s1(x),s1(y)) = 0 >= 4x + 4y + 12 = div23(x,s1(y),y)
          
          div23(x,y,0()) = 4x + 4y + 4 >= 0 = divides2(x,y)
          
          div23(0(),y,s1(z)) = 4y + 8 >= 1 = false()
          
          div23(s1(x),y,s1(z)) = 4x + 4y + 12 >= 4x + 4y + 4 = div23(x,y,z)
          
          filter2(f,nil()) = 8 >= 4 = nil()
          
          filter2(f,cons2(x,xs)) = 2x + 8xs + 2 >= 2x + 8xs + 2 = if3(a(f,x),x,filter2(f,xs))
          
          if3(true(),x,xs) = 2x + 4xs + 2 >= x + 4xs + 1 = cons2(x,xs)
          
          if3(false(),x,xs) = 2x + 4xs + 2 >= xs = xs
          
          not2(f,x) = 0 >= 5 = not21(a(f,x))
          
          not21(true()) = 7 >= 1 = false()
          
          not21(false()) = 5 >= 3 = true()
          
          sieve1(nil()) = 8 >= 4 = nil()
          
          sieve1(cons2(x,xs)) = 2x + 8xs + 2 >= x + 16xs + 1 = cons2(x,sieve1(filter2(not1(divides1(x)),xs)))
          
          a(divides1(x6),x7) = 1 >= 0 = divides2(x6,x7)
          
          a(divides(),x7) = 1 >= x7 = divides1(x7)
          
          a(s(),x7) = 1 >= x7 + 2 = s1(x7)
          
          a(div22(x6,x5),x7) = 1 >= 4x5 + 4x6 + 4 = div23(x6,x5,x7)
          
          a(div21(x6),x7) = 1 >= 0 = div22(x6,x7)
          
          a(div2(),x7) = 1 >= 0 = div21(x7)
          
          a(filter1(x6),x7) = 1 >= 2x7 = filter2(x6,x7)
          
          a(filter(),x7) = 1 >= 0 = filter1(x7)
          
          a(cons1(x6),x7) = 1 >= x6 + 4x7 + 1 = cons2(x6,x7)
          
          a(cons(),x7) = 1 >= 0 = cons1(x7)
          
          a(if2(x6,x5),x7) = 1 >= 2x5 + 4x7 + 2 = if3(x6,x5,x7)
          
          a(if1(x6),x7) = 1 >= 0 = if2(x6,x7)
          
          a(if(),x7) = 1 >= 0 = if1(x7)
          
          a(not1(x6),x7) = 1 >= 0 = not2(x6,x7)
          
          a(not(),x7) = 1 >= x7 = not1(x7)
          
          a(not2(),x7) = 1 >= x7 + 4 = not21(x7)
          
          a(sieve(),x7) = 1 >= 2x7 = 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