YES

Problem:
 app(app(:(),app(app(:(),app(app(:(),app(app(:(),C()),x)),y)),z)),u) ->
 app(app(:(),app(app(:(),x),z)),app(app(:(),app(app(:(),app(app(:(),x),y)),z)),u))
 app(app(map(),f),nil()) -> nil()
 app(app(map(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(f,x)),app(app(map(),f),xs))
 app(app(filter(),f),nil()) -> nil()
 app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(f,x)),f),x),xs)
 app(app(app(app(filter2(),true()),f),x),xs) -> app(app(cons(),x),app(app(filter(),f),xs))
 app(app(app(app(filter2(),false()),f),x),xs) -> app(app(filter(),f),xs)

Proof:
 Uncurry Processor:
  :2(:2(:2(:2(C(),x),y),z),u) -> :2(:2(x,z),:2(:2(:2(x,y),z),u))
  map2(f,nil()) -> nil()
  map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
  filter2(f,nil()) -> nil()
  filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
  filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
  filter24(false(),f,x,xs) -> filter2(f,xs)
  app(:1(x8),x9) -> :2(x8,x9)
  app(:(),x9) -> :1(x9)
  app(map1(x8),x9) -> map2(x8,x9)
  app(map(),x9) -> map1(x9)
  app(cons1(x8),x9) -> cons2(x8,x9)
  app(cons(),x9) -> cons1(x9)
  app(filter1(x8),x9) -> filter2(x8,x9)
  app(filter(),x9) -> filter1(x9)
  app(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9)
  app(filter22(x8,x7),x9) -> filter23(x8,x7,x9)
  app(filter21(x8),x9) -> filter22(x8,x9)
  app(filter2(),x9) -> filter21(x9)
  DP Processor:
   DPs:
    :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(x,y)
    :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(x,y),z)
    :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(:2(x,y),z),u)
    :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(x,z)
    :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(x,z),:2(:2(:2(x,y),z),u))
    map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs)
    map{2,#}(f,cons2(x,xs)) -> app#(f,x)
    filter{2,#}(f,cons2(x,xs)) -> app#(f,x)
    filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs)
    filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs)
    filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs)
    app#(:1(x8),x9) -> :{2,#}(x8,x9)
    app#(map1(x8),x9) -> map{2,#}(x8,x9)
    app#(filter1(x8),x9) -> filter{2,#}(x8,x9)
    app#(filter23(x8,x7,x6),x9) -> filter2{4,#}(x8,x7,x6,x9)
   TRS:
    :2(:2(:2(:2(C(),x),y),z),u) -> :2(:2(x,z),:2(:2(:2(x,y),z),u))
    map2(f,nil()) -> nil()
    map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
    filter2(f,nil()) -> nil()
    filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
    filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
    filter24(false(),f,x,xs) -> filter2(f,xs)
    app(:1(x8),x9) -> :2(x8,x9)
    app(:(),x9) -> :1(x9)
    app(map1(x8),x9) -> map2(x8,x9)
    app(map(),x9) -> map1(x9)
    app(cons1(x8),x9) -> cons2(x8,x9)
    app(cons(),x9) -> cons1(x9)
    app(filter1(x8),x9) -> filter2(x8,x9)
    app(filter(),x9) -> filter1(x9)
    app(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9)
    app(filter22(x8,x7),x9) -> filter23(x8,x7,x9)
    app(filter21(x8),x9) -> filter22(x8,x9)
    app(filter2(),x9) -> filter21(x9)
   TDG Processor:
    DPs:
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(x,y)
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(x,y),z)
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(:2(x,y),z),u)
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(x,z)
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(x,z),:2(:2(:2(x,y),z),u))
     map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs)
     map{2,#}(f,cons2(x,xs)) -> app#(f,x)
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x)
     filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs)
     filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs)
     filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs)
     app#(:1(x8),x9) -> :{2,#}(x8,x9)
     app#(map1(x8),x9) -> map{2,#}(x8,x9)
     app#(filter1(x8),x9) -> filter{2,#}(x8,x9)
     app#(filter23(x8,x7,x6),x9) -> filter2{4,#}(x8,x7,x6,x9)
    TRS:
     :2(:2(:2(:2(C(),x),y),z),u) -> :2(:2(x,z),:2(:2(:2(x,y),z),u))
     map2(f,nil()) -> nil()
     map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
     filter2(f,nil()) -> nil()
     filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
     filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
     filter24(false(),f,x,xs) -> filter2(f,xs)
     app(:1(x8),x9) -> :2(x8,x9)
     app(:(),x9) -> :1(x9)
     app(map1(x8),x9) -> map2(x8,x9)
     app(map(),x9) -> map1(x9)
     app(cons1(x8),x9) -> cons2(x8,x9)
     app(cons(),x9) -> cons1(x9)
     app(filter1(x8),x9) -> filter2(x8,x9)
     app(filter(),x9) -> filter1(x9)
     app(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9)
     app(filter22(x8,x7),x9) -> filter23(x8,x7,x9)
     app(filter21(x8),x9) -> filter22(x8,x9)
     app(filter2(),x9) -> filter21(x9)
    graph:
     filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs) ->
     filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs)
     filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs) ->
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x)
     filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs) ->
     filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs)
     filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs) ->
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x)
     filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs) ->
     filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs)
     filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs) ->
     filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs)
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(filter23(x8,x7,x6),x9) -> filter2{4,#}(x8,x7,x6,x9)
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(filter1(x8),x9) -> filter{2,#}(x8,x9)
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(map1(x8),x9) -> map{2,#}(x8,x9)
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(:1(x8),x9) -> :{2,#}(x8,x9)
     app#(filter23(x8,x7,x6),x9) -> filter2{4,#}(x8,x7,x6,x9) ->
     filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs)
     app#(filter23(x8,x7,x6),x9) -> filter2{4,#}(x8,x7,x6,x9) ->
     filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs)
     app#(filter1(x8),x9) -> filter{2,#}(x8,x9) ->
     filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs)
     app#(filter1(x8),x9) -> filter{2,#}(x8,x9) ->
     filter{2,#}(f,cons2(x,xs)) -> app#(f,x)
     app#(map1(x8),x9) -> map{2,#}(x8,x9) ->
     map{2,#}(f,cons2(x,xs)) -> app#(f,x)
     app#(map1(x8),x9) -> map{2,#}(x8,x9) ->
     map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs)
     app#(:1(x8),x9) -> :{2,#}(x8,x9) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(x,z),:2(:2(:2(x,y),z),u))
     app#(:1(x8),x9) -> :{2,#}(x8,x9) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(x,z)
     app#(:1(x8),x9) -> :{2,#}(x8,x9) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(:2(x,y),z),u)
     app#(:1(x8),x9) -> :{2,#}(x8,x9) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(x,y),z)
     app#(:1(x8),x9) -> :{2,#}(x8,x9) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(x,y)
     map{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(filter23(x8,x7,x6),x9) -> filter2{4,#}(x8,x7,x6,x9)
     map{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(filter1(x8),x9) -> filter{2,#}(x8,x9)
     map{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(map1(x8),x9) -> map{2,#}(x8,x9)
     map{2,#}(f,cons2(x,xs)) -> app#(f,x) ->
     app#(:1(x8),x9) -> :{2,#}(x8,x9)
     map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs) ->
     map{2,#}(f,cons2(x,xs)) -> app#(f,x)
     map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs) ->
     map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs)
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(:2(x,y),z),u) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(x,z),:2(:2(:2(x,y),z),u))
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(:2(x,y),z),u) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(x,z)
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(:2(x,y),z),u) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(:2(x,y),z),u)
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(:2(x,y),z),u) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(x,y),z)
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(:2(x,y),z),u) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(x,y)
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(x,z),:2(:2(:2(x,y),z),u)) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(x,z),:2(:2(:2(x,y),z),u))
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(x,z),:2(:2(:2(x,y),z),u)) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(x,z)
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(x,z),:2(:2(:2(x,y),z),u)) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(:2(x,y),z),u)
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(x,z),:2(:2(:2(x,y),z),u)) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(x,y),z)
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(x,z),:2(:2(:2(x,y),z),u)) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(x,y)
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(x,y),z) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(x,z),:2(:2(:2(x,y),z),u))
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(x,y),z) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(x,z)
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(x,y),z) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(:2(x,y),z),u)
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(x,y),z) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(x,y),z)
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(x,y),z) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(x,y)
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(x,z) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(x,z),:2(:2(:2(x,y),z),u))
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(x,z) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(x,z)
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(x,z) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(:2(x,y),z),u)
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(x,z) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(x,y),z)
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(x,z) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(x,y)
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(x,y) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(x,z),:2(:2(:2(x,y),z),u))
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(x,y) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(x,z)
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(x,y) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(:2(x,y),z),u)
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(x,y) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(x,y),z)
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(x,y) ->
     :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(x,y)
    SCC Processor:
     #sccs: 2
     #rules: 14
     #arcs: 52/225
     DPs:
      filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs)
      filter{2,#}(f,cons2(x,xs)) -> app#(f,x)
      app#(map1(x8),x9) -> map{2,#}(x8,x9)
      map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs)
      map{2,#}(f,cons2(x,xs)) -> app#(f,x)
      app#(filter1(x8),x9) -> filter{2,#}(x8,x9)
      filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs)
      filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs)
      app#(filter23(x8,x7,x6),x9) -> filter2{4,#}(x8,x7,x6,x9)
     TRS:
      :2(:2(:2(:2(C(),x),y),z),u) -> :2(:2(x,z),:2(:2(:2(x,y),z),u))
      map2(f,nil()) -> nil()
      map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
      filter2(f,nil()) -> nil()
      filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
      filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
      filter24(false(),f,x,xs) -> filter2(f,xs)
      app(:1(x8),x9) -> :2(x8,x9)
      app(:(),x9) -> :1(x9)
      app(map1(x8),x9) -> map2(x8,x9)
      app(map(),x9) -> map1(x9)
      app(cons1(x8),x9) -> cons2(x8,x9)
      app(cons(),x9) -> cons1(x9)
      app(filter1(x8),x9) -> filter2(x8,x9)
      app(filter(),x9) -> filter1(x9)
      app(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9)
      app(filter22(x8,x7),x9) -> filter23(x8,x7,x9)
      app(filter21(x8),x9) -> filter22(x8,x9)
      app(filter2(),x9) -> filter21(x9)
     Subterm Criterion Processor:
      simple projection:
       pi(map{2,#}) = 1
       pi(app#) = 1
       pi(filter{2,#}) = 1
       pi(filter2{4,#}) = 3
      problem:
       DPs:
        filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs)
        app#(map1(x8),x9) -> map{2,#}(x8,x9)
        app#(filter1(x8),x9) -> filter{2,#}(x8,x9)
        filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs)
        app#(filter23(x8,x7,x6),x9) -> filter2{4,#}(x8,x7,x6,x9)
       TRS:
        :2(:2(:2(:2(C(),x),y),z),u) -> :2(:2(x,z),:2(:2(:2(x,y),z),u))
        map2(f,nil()) -> nil()
        map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
        filter2(f,nil()) -> nil()
        filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
        filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
        filter24(false(),f,x,xs) -> filter2(f,xs)
        app(:1(x8),x9) -> :2(x8,x9)
        app(:(),x9) -> :1(x9)
        app(map1(x8),x9) -> map2(x8,x9)
        app(map(),x9) -> map1(x9)
        app(cons1(x8),x9) -> cons2(x8,x9)
        app(cons(),x9) -> cons1(x9)
        app(filter1(x8),x9) -> filter2(x8,x9)
        app(filter(),x9) -> filter1(x9)
        app(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9)
        app(filter22(x8,x7),x9) -> filter23(x8,x7,x9)
        app(filter21(x8),x9) -> filter22(x8,x9)
        app(filter2(),x9) -> filter21(x9)
      SCC Processor:
       #sccs: 0
       #rules: 0
       #arcs: 20/25
       
     
     DPs:
      :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(x,y)
      :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(x,y),z)
      :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(:2(x,y),z),u)
      :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(x,z)
      :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(x,z),:2(:2(:2(x,y),z),u))
     TRS:
      :2(:2(:2(:2(C(),x),y),z),u) -> :2(:2(x,z),:2(:2(:2(x,y),z),u))
      map2(f,nil()) -> nil()
      map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
      filter2(f,nil()) -> nil()
      filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
      filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
      filter24(false(),f,x,xs) -> filter2(f,xs)
      app(:1(x8),x9) -> :2(x8,x9)
      app(:(),x9) -> :1(x9)
      app(map1(x8),x9) -> map2(x8,x9)
      app(map(),x9) -> map1(x9)
      app(cons1(x8),x9) -> cons2(x8,x9)
      app(cons(),x9) -> cons1(x9)
      app(filter1(x8),x9) -> filter2(x8,x9)
      app(filter(),x9) -> filter1(x9)
      app(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9)
      app(filter22(x8,x7),x9) -> filter23(x8,x7,x9)
      app(filter21(x8),x9) -> filter22(x8,x9)
      app(filter2(),x9) -> filter21(x9)
     Arctic Interpretation Processor:
      dimension: 1
      interpretation:
       [:{2,#}](x0, x1) = 1x0 + x1 + 0,
       
       [filter21](x0) = x0 + 3,
       
       [filter22](x0, x1) = x0 + 3,
       
       [filter24](x0, x1, x2, x3) = x3,
       
       [filter23](x0, x1, x2) = x0 + 0,
       
       [filter2](x0, x1) = x1,
       
       [filter1](x0) = 0,
       
       [cons2](x0, x1) = x1,
       
       [cons1](x0) = 1x0,
       
       [map2](x0, x1) = x1 + 0,
       
       [map1](x0) = 0,
       
       [:2](x0, x1) = 1x0 + x1 + 4,
       
       [:1](x0) = 1x0 + 5,
       
       [false] = 2,
       
       [true] = 4,
       
       [filter2] = 4,
       
       [filter] = 2,
       
       [cons] = 4,
       
       [nil] = 0,
       
       [map] = 6,
       
       [app](x0, x1) = x0 + 1x1 + 2,
       
       [C] = 0,
       
       [:] = 5
      orientation:
       :{2,#}(:2(:2(:2(C(),x),y),z),u) = u + 3x + 2y + 1z + 7 >= 1x + y + 0 = :{2,#}(x,y)
       
       :{2,#}(:2(:2(:2(C(),x),y),z),u) = u + 3x + 2y + 1z + 7 >= 2x + 1y + z + 5 = :{2,#}(:2(x,y),z)
       
       :{2,#}(:2(:2(:2(C(),x),y),z),u) = u + 3x + 2y + 1z + 7 >= u + 3x + 2y + 1z + 6 = :{2,#}(:2(:2(x,y),z),u)
       
       :{2,#}(:2(:2(:2(C(),x),y),z),u) = u + 3x + 2y + 1z + 7 >= 1x + z + 0 = :{2,#}(x,z)
       
       :{2,#}(:2(:2(:2(C(),x),y),z),u) = u + 3x + 2y + 1z + 7 >= u + 3x + 2y + 1z + 6 = :{2,#}(:2(x,z),:2(:2(:2(x,y),z),u))
       
       :2(:2(:2(:2(C(),x),y),z),u) = u + 3x + 2y + 1z + 7 >= u + 3x + 2y + 1z + 6 = :2(:2(x,z),:2(:2(:2(x,y),z),u))
       
       map2(f,nil()) = 0 >= 0 = nil()
       
       map2(f,cons2(x,xs)) = xs + 0 >= xs + 0 = cons2(app(f,x),map2(f,xs))
       
       filter2(f,nil()) = 0 >= 0 = nil()
       
       filter2(f,cons2(x,xs)) = xs >= xs = filter24(app(f,x),f,x,xs)
       
       filter24(true(),f,x,xs) = xs >= xs = cons2(x,filter2(f,xs))
       
       filter24(false(),f,x,xs) = xs >= xs = filter2(f,xs)
       
       app(:1(x8),x9) = 1x8 + 1x9 + 5 >= 1x8 + x9 + 4 = :2(x8,x9)
       
       app(:(),x9) = 1x9 + 5 >= 1x9 + 5 = :1(x9)
       
       app(map1(x8),x9) = 1x9 + 2 >= x9 + 0 = map2(x8,x9)
       
       app(map(),x9) = 1x9 + 6 >= 0 = map1(x9)
       
       app(cons1(x8),x9) = 1x8 + 1x9 + 2 >= x9 = cons2(x8,x9)
       
       app(cons(),x9) = 1x9 + 4 >= 1x9 = cons1(x9)
       
       app(filter1(x8),x9) = 1x9 + 2 >= x9 = filter2(x8,x9)
       
       app(filter(),x9) = 1x9 + 2 >= 0 = filter1(x9)
       
       app(filter23(x8,x7,x6),x9) = x8 + 1x9 + 2 >= x9 = filter24(x8,x7,x6,x9)
       
       app(filter22(x8,x7),x9) = x8 + 1x9 + 3 >= x8 + 0 = filter23(x8,x7,x9)
       
       app(filter21(x8),x9) = x8 + 1x9 + 3 >= x8 + 3 = filter22(x8,x9)
       
       app(filter2(),x9) = 1x9 + 4 >= x9 + 3 = filter21(x9)
      problem:
       DPs:
        :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(:2(x,y),z),u)
        :{2,#}(:2(:2(:2(C(),x),y),z),u) -> :{2,#}(:2(x,z),:2(:2(:2(x,y),z),u))
       TRS:
        :2(:2(:2(:2(C(),x),y),z),u) -> :2(:2(x,z),:2(:2(:2(x,y),z),u))
        map2(f,nil()) -> nil()
        map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
        filter2(f,nil()) -> nil()
        filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
        filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
        filter24(false(),f,x,xs) -> filter2(f,xs)
        app(:1(x8),x9) -> :2(x8,x9)
        app(:(),x9) -> :1(x9)
        app(map1(x8),x9) -> map2(x8,x9)
        app(map(),x9) -> map1(x9)
        app(cons1(x8),x9) -> cons2(x8,x9)
        app(cons(),x9) -> cons1(x9)
        app(filter1(x8),x9) -> filter2(x8,x9)
        app(filter(),x9) -> filter1(x9)
        app(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9)
        app(filter22(x8,x7),x9) -> filter23(x8,x7,x9)
        app(filter21(x8),x9) -> filter22(x8,x9)
        app(filter2(),x9) -> filter21(x9)
      LPO Processor:
       argument filtering:
        pi(:) = []
        pi(C) = []
        pi(app) = [0,1]
        pi(map) = []
        pi(nil) = []
        pi(cons) = []
        pi(filter) = []
        pi(filter2) = []
        pi(true) = []
        pi(false) = []
        pi(:1) = [0]
        pi(:2) = [0,1]
        pi(map1) = 0
        pi(map2) = 1
        pi(cons1) = 0
        pi(cons2) = 1
        pi(filter1) = []
        pi(filter2) = 1
        pi(filter23) = []
        pi(filter24) = 3
        pi(filter22) = []
        pi(filter21) = 0
        pi(:{2,#}) = 0
       precedence:
        filter > app > filter22 > :{2,#} ~ filter21 ~ filter24 ~ filter23 ~ 
        filter2 ~ filter1 ~ cons2 ~ cons1 ~ map2 ~ map1 ~ :2 ~ :1 ~ false ~ 
        true ~ filter2 ~ cons ~ nil ~ map ~ C ~ :
       problem:
        DPs:
         
        TRS:
         :2(:2(:2(:2(C(),x),y),z),u) -> :2(:2(x,z),:2(:2(:2(x,y),z),u))
         map2(f,nil()) -> nil()
         map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs))
         filter2(f,nil()) -> nil()
         filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs)
         filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs))
         filter24(false(),f,x,xs) -> filter2(f,xs)
         app(:1(x8),x9) -> :2(x8,x9)
         app(:(),x9) -> :1(x9)
         app(map1(x8),x9) -> map2(x8,x9)
         app(map(),x9) -> map1(x9)
         app(cons1(x8),x9) -> cons2(x8,x9)
         app(cons(),x9) -> cons1(x9)
         app(filter1(x8),x9) -> filter2(x8,x9)
         app(filter(),x9) -> filter1(x9)
         app(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9)
         app(filter22(x8,x7),x9) -> filter23(x8,x7,x9)
         app(filter21(x8),x9) -> filter22(x8,x9)
         app(filter2(),x9) -> filter21(x9)
       Qed