YES

Problem:
 app(app(app(consif(),true()),x),ys) -> app(app(cons(),x),ys)
 app(app(app(consif(),false()),x),ys) -> ys
 app(app(filter(),f),nil()) -> nil()
 app(app(filter(),f),app(app(cons(),x),xs)) ->
 app(app(app(consif(),app(f,x)),x),app(app(filter(),f),xs))

Proof:
 Uncurry Processor:
  consif3(true(),x,ys) -> cons2(x,ys)
  consif3(false(),x,ys) -> ys
  filter2(f,nil()) -> nil()
  filter2(f,cons2(x,xs)) -> consif3(app(f,x),x,filter2(f,xs))
  app(consif2(x5,x4),x6) -> consif3(x5,x4,x6)
  app(consif1(x5),x6) -> consif2(x5,x6)
  app(consif(),x6) -> consif1(x6)
  app(cons1(x5),x6) -> cons2(x5,x6)
  app(cons(),x6) -> cons1(x6)
  app(filter1(x5),x6) -> filter2(x5,x6)
  app(filter(),x6) -> filter1(x6)
  DP Processor:
   DPs:
    filter{2,#}(f,cons2(x,xs)) -> filter{2,#}(f,xs)
    filter{2,#}(f,cons2(x,xs)) -> app#(f,x)
    filter{2,#}(f,cons2(x,xs)) -> consif{3,#}(app(f,x),x,filter2(f,xs))
    app#(consif2(x5,x4),x6) -> consif{3,#}(x5,x4,x6)
    app#(filter1(x5),x6) -> filter{2,#}(x5,x6)
   TRS:
    consif3(true(),x,ys) -> cons2(x,ys)
    consif3(false(),x,ys) -> ys
    filter2(f,nil()) -> nil()
    filter2(f,cons2(x,xs)) -> consif3(app(f,x),x,filter2(f,xs))
    app(consif2(x5,x4),x6) -> consif3(x5,x4,x6)
    app(consif1(x5),x6) -> consif2(x5,x6)
    app(consif(),x6) -> consif1(x6)
    app(cons1(x5),x6) -> cons2(x5,x6)
    app(cons(),x6) -> cons1(x6)
    app(filter1(x5),x6) -> filter2(x5,x6)
    app(filter(),x6) -> filter1(x6)
   TDG Processor:
    DPs:
     filter{2,#}(f,cons2(x,xs)) -> filter{2,#}(f,xs)
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x)
     filter{2,#}(f,cons2(x,xs)) -> consif{3,#}(app(f,x),x,filter2(f,xs))
     app#(consif2(x5,x4),x6) -> consif{3,#}(x5,x4,x6)
     app#(filter1(x5),x6) -> filter{2,#}(x5,x6)
    TRS:
     consif3(true(),x,ys) -> cons2(x,ys)
     consif3(false(),x,ys) -> ys
     filter2(f,nil()) -> nil()
     filter2(f,cons2(x,xs)) -> consif3(app(f,x),x,filter2(f,xs))
     app(consif2(x5,x4),x6) -> consif3(x5,x4,x6)
     app(consif1(x5),x6) -> consif2(x5,x6)
     app(consif(),x6) -> consif1(x6)
     app(cons1(x5),x6) -> cons2(x5,x6)
     app(cons(),x6) -> cons1(x6)
     app(filter1(x5),x6) -> filter2(x5,x6)
     app(filter(),x6) -> filter1(x6)
    graph:
     app#(filter1(x5),x6) -> filter{2,#}(x5,x6) ->
     filter{2,#}(f,cons2(x,xs)) -> consif{3,#}(app(f,x),x,filter2(f,xs))
     app#(filter1(x5),x6) -> filter{2,#}(x5,x6) ->
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x)
     app#(filter1(x5),x6) -> filter{2,#}(x5,x6) ->
     filter{2,#}(f,cons2(x,xs)) -> filter{2,#}(f,xs)
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(filter1(x5),x6) -> filter{2,#}(x5,x6)
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(consif2(x5,x4),x6) -> consif{3,#}(x5,x4,x6)
     filter{2,#}(f,cons2(x,xs)) -> filter{2,#}(f,xs) ->
     filter{2,#}(f,cons2(x,xs)) -> consif{3,#}(app(f,x),x,filter2(f,xs))
     filter{2,#}(f,cons2(x,xs)) -> filter{2,#}(f,xs) ->
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x)
     filter{2,#}(f,cons2(x,xs)) -> filter{2,#}(f,xs) ->
     filter{2,#}(f,cons2(x,xs)) -> filter{2,#}(f,xs)
    SCC Processor:
     #sccs: 1
     #rules: 3
     #arcs: 8/25
     DPs:
      app#(filter1(x5),x6) -> filter{2,#}(x5,x6)
      filter{2,#}(f,cons2(x,xs)) -> filter{2,#}(f,xs)
      filter{2,#}(f,cons2(x,xs)) -> app#(f,x)
     TRS:
      consif3(true(),x,ys) -> cons2(x,ys)
      consif3(false(),x,ys) -> ys
      filter2(f,nil()) -> nil()
      filter2(f,cons2(x,xs)) -> consif3(app(f,x),x,filter2(f,xs))
      app(consif2(x5,x4),x6) -> consif3(x5,x4,x6)
      app(consif1(x5),x6) -> consif2(x5,x6)
      app(consif(),x6) -> consif1(x6)
      app(cons1(x5),x6) -> cons2(x5,x6)
      app(cons(),x6) -> cons1(x6)
      app(filter1(x5),x6) -> filter2(x5,x6)
      app(filter(),x6) -> filter1(x6)
     Subterm Criterion Processor:
      simple projection:
       pi(filter{2,#}) = 1
       pi(app#) = 1
      problem:
       DPs:
        app#(filter1(x5),x6) -> filter{2,#}(x5,x6)
       TRS:
        consif3(true(),x,ys) -> cons2(x,ys)
        consif3(false(),x,ys) -> ys
        filter2(f,nil()) -> nil()
        filter2(f,cons2(x,xs)) -> consif3(app(f,x),x,filter2(f,xs))
        app(consif2(x5,x4),x6) -> consif3(x5,x4,x6)
        app(consif1(x5),x6) -> consif2(x5,x6)
        app(consif(),x6) -> consif1(x6)
        app(cons1(x5),x6) -> cons2(x5,x6)
        app(cons(),x6) -> cons1(x6)
        app(filter1(x5),x6) -> filter2(x5,x6)
        app(filter(),x6) -> filter1(x6)
      SCC Processor:
       #sccs: 0
       #rules: 0
       #arcs: 5/1