YES

Problem:
 app(app(app(if(),true()),xs),ys) -> xs
 app(app(app(if(),false()),xs),ys) -> ys
 app(app(sub(),x),0()) -> x
 app(app(sub(),app(s(),x)),app(s(),y)) -> app(app(sub(),x),y)
 app(app(gtr(),0()),y) -> false()
 app(app(gtr(),app(s(),x)),0()) -> true()
 app(app(gtr(),app(s(),x)),app(s(),y)) -> app(app(gtr(),x),y)
 app(app(d(),x),0()) -> true()
 app(app(d(),app(s(),x)),app(s(),y)) ->
 app(app(app(if(),app(app(gtr(),x),y)),false()),app(app(d(),app(s(),x)),app(app(sub(),y),x)))
 app(len(),nil()) -> 0()
 app(len(),app(app(cons(),x),xs)) -> app(s(),app(len(),xs))
 app(app(filter(),p),nil()) -> nil()
 app(app(filter(),p),app(app(cons(),x),xs)) ->
 app(app(app(if(),app(p,x)),app(app(cons(),x),app(app(filter(),p),xs))),app(app(filter(),p),xs))

Proof:
 Uncurry Processor:
  if3(true(),xs,ys) -> xs
  if3(false(),xs,ys) -> ys
  sub2(x,0()) -> x
  sub2(s1(x),s1(y)) -> sub2(x,y)
  gtr2(0(),y) -> false()
  gtr2(s1(x),0()) -> true()
  gtr2(s1(x),s1(y)) -> gtr2(x,y)
  d2(x,0()) -> true()
  d2(s1(x),s1(y)) -> if3(gtr2(x,y),false(),d2(s1(x),sub2(y,x)))
  len1(nil()) -> 0()
  len1(cons2(x,xs)) -> s1(len1(xs))
  filter2(p,nil()) -> nil()
  filter2(p,cons2(x,xs)) -> if3(app(p,x),cons2(x,filter2(p,xs)),filter2(p,xs))
  app(if2(x6,x5),x7) -> if3(x6,x5,x7)
  app(if1(x6),x7) -> if2(x6,x7)
  app(if(),x7) -> if1(x7)
  app(sub1(x6),x7) -> sub2(x6,x7)
  app(sub(),x7) -> sub1(x7)
  app(s(),x7) -> s1(x7)
  app(gtr1(x6),x7) -> gtr2(x6,x7)
  app(gtr(),x7) -> gtr1(x7)
  app(d1(x6),x7) -> d2(x6,x7)
  app(d(),x7) -> d1(x7)
  app(len(),x7) -> len1(x7)
  app(cons1(x6),x7) -> cons2(x6,x7)
  app(cons(),x7) -> cons1(x7)
  app(filter1(x6),x7) -> filter2(x6,x7)
  app(filter(),x7) -> filter1(x7)
  DP Processor:
   DPs:
    sub{2,#}(s1(x),s1(y)) -> sub{2,#}(x,y)
    gtr{2,#}(s1(x),s1(y)) -> gtr{2,#}(x,y)
    d{2,#}(s1(x),s1(y)) -> sub{2,#}(y,x)
    d{2,#}(s1(x),s1(y)) -> d{2,#}(s1(x),sub2(y,x))
    d{2,#}(s1(x),s1(y)) -> gtr{2,#}(x,y)
    d{2,#}(s1(x),s1(y)) -> if{3,#}(gtr2(x,y),false(),d2(s1(x),sub2(y,x)))
    len{1,#}(cons2(x,xs)) -> len{1,#}(xs)
    filter{2,#}(p,cons2(x,xs)) -> filter{2,#}(p,xs)
    filter{2,#}(p,cons2(x,xs)) -> app#(p,x)
    filter{2,#}(p,cons2(x,xs)) -> if{3,#}(app(p,x),cons2(x,filter2(p,xs)),filter2(p,xs))
    app#(if2(x6,x5),x7) -> if{3,#}(x6,x5,x7)
    app#(sub1(x6),x7) -> sub{2,#}(x6,x7)
    app#(gtr1(x6),x7) -> gtr{2,#}(x6,x7)
    app#(d1(x6),x7) -> d{2,#}(x6,x7)
    app#(len(),x7) -> len{1,#}(x7)
    app#(filter1(x6),x7) -> filter{2,#}(x6,x7)
   TRS:
    if3(true(),xs,ys) -> xs
    if3(false(),xs,ys) -> ys
    sub2(x,0()) -> x
    sub2(s1(x),s1(y)) -> sub2(x,y)
    gtr2(0(),y) -> false()
    gtr2(s1(x),0()) -> true()
    gtr2(s1(x),s1(y)) -> gtr2(x,y)
    d2(x,0()) -> true()
    d2(s1(x),s1(y)) -> if3(gtr2(x,y),false(),d2(s1(x),sub2(y,x)))
    len1(nil()) -> 0()
    len1(cons2(x,xs)) -> s1(len1(xs))
    filter2(p,nil()) -> nil()
    filter2(p,cons2(x,xs)) -> if3(app(p,x),cons2(x,filter2(p,xs)),filter2(p,xs))
    app(if2(x6,x5),x7) -> if3(x6,x5,x7)
    app(if1(x6),x7) -> if2(x6,x7)
    app(if(),x7) -> if1(x7)
    app(sub1(x6),x7) -> sub2(x6,x7)
    app(sub(),x7) -> sub1(x7)
    app(s(),x7) -> s1(x7)
    app(gtr1(x6),x7) -> gtr2(x6,x7)
    app(gtr(),x7) -> gtr1(x7)
    app(d1(x6),x7) -> d2(x6,x7)
    app(d(),x7) -> d1(x7)
    app(len(),x7) -> len1(x7)
    app(cons1(x6),x7) -> cons2(x6,x7)
    app(cons(),x7) -> cons1(x7)
    app(filter1(x6),x7) -> filter2(x6,x7)
    app(filter(),x7) -> filter1(x7)
   TDG Processor:
    DPs:
     sub{2,#}(s1(x),s1(y)) -> sub{2,#}(x,y)
     gtr{2,#}(s1(x),s1(y)) -> gtr{2,#}(x,y)
     d{2,#}(s1(x),s1(y)) -> sub{2,#}(y,x)
     d{2,#}(s1(x),s1(y)) -> d{2,#}(s1(x),sub2(y,x))
     d{2,#}(s1(x),s1(y)) -> gtr{2,#}(x,y)
     d{2,#}(s1(x),s1(y)) -> if{3,#}(gtr2(x,y),false(),d2(s1(x),sub2(y,x)))
     len{1,#}(cons2(x,xs)) -> len{1,#}(xs)
     filter{2,#}(p,cons2(x,xs)) -> filter{2,#}(p,xs)
     filter{2,#}(p,cons2(x,xs)) -> app#(p,x)
     filter{2,#}(p,cons2(x,xs)) -> if{3,#}(app(p,x),cons2(x,filter2(p,xs)),filter2(p,xs))
     app#(if2(x6,x5),x7) -> if{3,#}(x6,x5,x7)
     app#(sub1(x6),x7) -> sub{2,#}(x6,x7)
     app#(gtr1(x6),x7) -> gtr{2,#}(x6,x7)
     app#(d1(x6),x7) -> d{2,#}(x6,x7)
     app#(len(),x7) -> len{1,#}(x7)
     app#(filter1(x6),x7) -> filter{2,#}(x6,x7)
    TRS:
     if3(true(),xs,ys) -> xs
     if3(false(),xs,ys) -> ys
     sub2(x,0()) -> x
     sub2(s1(x),s1(y)) -> sub2(x,y)
     gtr2(0(),y) -> false()
     gtr2(s1(x),0()) -> true()
     gtr2(s1(x),s1(y)) -> gtr2(x,y)
     d2(x,0()) -> true()
     d2(s1(x),s1(y)) -> if3(gtr2(x,y),false(),d2(s1(x),sub2(y,x)))
     len1(nil()) -> 0()
     len1(cons2(x,xs)) -> s1(len1(xs))
     filter2(p,nil()) -> nil()
     filter2(p,cons2(x,xs)) -> if3(app(p,x),cons2(x,filter2(p,xs)),filter2(p,xs))
     app(if2(x6,x5),x7) -> if3(x6,x5,x7)
     app(if1(x6),x7) -> if2(x6,x7)
     app(if(),x7) -> if1(x7)
     app(sub1(x6),x7) -> sub2(x6,x7)
     app(sub(),x7) -> sub1(x7)
     app(s(),x7) -> s1(x7)
     app(gtr1(x6),x7) -> gtr2(x6,x7)
     app(gtr(),x7) -> gtr1(x7)
     app(d1(x6),x7) -> d2(x6,x7)
     app(d(),x7) -> d1(x7)
     app(len(),x7) -> len1(x7)
     app(cons1(x6),x7) -> cons2(x6,x7)
     app(cons(),x7) -> cons1(x7)
     app(filter1(x6),x7) -> filter2(x6,x7)
     app(filter(),x7) -> filter1(x7)
    graph:
     app#(filter1(x6),x7) -> filter{2,#}(x6,x7) ->
     filter{2,#}(p,cons2(x,xs)) -> if{3,#}(app(p,x),cons2(x,filter2(p,xs)),filter2(p,xs))
     app#(filter1(x6),x7) -> filter{2,#}(x6,x7) ->
     filter{2,#}(p,cons2(x,xs)) -> app#(p,x)
     app#(filter1(x6),x7) -> filter{2,#}(x6,x7) ->
     filter{2,#}(p,cons2(x,xs)) -> filter{2,#}(p,xs)
     app#(d1(x6),x7) -> d{2,#}(x6,x7) ->
     d{2,#}(s1(x),s1(y)) -> if{3,#}(gtr2(x,y),false(),d2(s1(x),sub2(y,x)))
     app#(d1(x6),x7) -> d{2,#}(x6,x7) ->
     d{2,#}(s1(x),s1(y)) -> gtr{2,#}(x,y)
     app#(d1(x6),x7) -> d{2,#}(x6,x7) ->
     d{2,#}(s1(x),s1(y)) -> d{2,#}(s1(x),sub2(y,x))
     app#(d1(x6),x7) -> d{2,#}(x6,x7) ->
     d{2,#}(s1(x),s1(y)) -> sub{2,#}(y,x)
     app#(gtr1(x6),x7) -> gtr{2,#}(x6,x7) ->
     gtr{2,#}(s1(x),s1(y)) -> gtr{2,#}(x,y)
     app#(sub1(x6),x7) -> sub{2,#}(x6,x7) ->
     sub{2,#}(s1(x),s1(y)) -> sub{2,#}(x,y)
     app#(len(),x7) -> len{1,#}(x7) ->
     len{1,#}(cons2(x,xs)) -> len{1,#}(xs)
     filter{2,#}(p,cons2(x,xs)) -> app#(p,x) ->
     app#(filter1(x6),x7) -> filter{2,#}(x6,x7)
     filter{2,#}(p,cons2(x,xs)) -> app#(p,x) ->
     app#(len(),x7) -> len{1,#}(x7)
     filter{2,#}(p,cons2(x,xs)) -> app#(p,x) ->
     app#(d1(x6),x7) -> d{2,#}(x6,x7)
     filter{2,#}(p,cons2(x,xs)) -> app#(p,x) ->
     app#(gtr1(x6),x7) -> gtr{2,#}(x6,x7)
     filter{2,#}(p,cons2(x,xs)) -> app#(p,x) ->
     app#(sub1(x6),x7) -> sub{2,#}(x6,x7)
     filter{2,#}(p,cons2(x,xs)) -> app#(p,x) ->
     app#(if2(x6,x5),x7) -> if{3,#}(x6,x5,x7)
     filter{2,#}(p,cons2(x,xs)) -> filter{2,#}(p,xs) ->
     filter{2,#}(p,cons2(x,xs)) -> if{3,#}(app(p,x),cons2(x,filter2(p,xs)),filter2(p,xs))
     filter{2,#}(p,cons2(x,xs)) -> filter{2,#}(p,xs) ->
     filter{2,#}(p,cons2(x,xs)) -> app#(p,x)
     filter{2,#}(p,cons2(x,xs)) -> filter{2,#}(p,xs) ->
     filter{2,#}(p,cons2(x,xs)) -> filter{2,#}(p,xs)
     len{1,#}(cons2(x,xs)) -> len{1,#}(xs) ->
     len{1,#}(cons2(x,xs)) -> len{1,#}(xs)
     d{2,#}(s1(x),s1(y)) -> d{2,#}(s1(x),sub2(y,x)) ->
     d{2,#}(s1(x),s1(y)) -> if{3,#}(gtr2(x,y),false(),d2(s1(x),sub2(y,x)))
     d{2,#}(s1(x),s1(y)) -> d{2,#}(s1(x),sub2(y,x)) ->
     d{2,#}(s1(x),s1(y)) -> gtr{2,#}(x,y)
     d{2,#}(s1(x),s1(y)) -> d{2,#}(s1(x),sub2(y,x)) ->
     d{2,#}(s1(x),s1(y)) -> d{2,#}(s1(x),sub2(y,x))
     d{2,#}(s1(x),s1(y)) -> d{2,#}(s1(x),sub2(y,x)) ->
     d{2,#}(s1(x),s1(y)) -> sub{2,#}(y,x)
     d{2,#}(s1(x),s1(y)) -> gtr{2,#}(x,y) ->
     gtr{2,#}(s1(x),s1(y)) -> gtr{2,#}(x,y)
     d{2,#}(s1(x),s1(y)) -> sub{2,#}(y,x) ->
     sub{2,#}(s1(x),s1(y)) -> sub{2,#}(x,y)
     gtr{2,#}(s1(x),s1(y)) -> gtr{2,#}(x,y) ->
     gtr{2,#}(s1(x),s1(y)) -> gtr{2,#}(x,y)
     sub{2,#}(s1(x),s1(y)) -> sub{2,#}(x,y) -> sub{2,#}(s1(x),s1(y)) -> sub{2,#}(x,y)
    SCC Processor:
     #sccs: 5
     #rules: 7
     #arcs: 28/256
     DPs:
      app#(filter1(x6),x7) -> filter{2,#}(x6,x7)
      filter{2,#}(p,cons2(x,xs)) -> filter{2,#}(p,xs)
      filter{2,#}(p,cons2(x,xs)) -> app#(p,x)
     TRS:
      if3(true(),xs,ys) -> xs
      if3(false(),xs,ys) -> ys
      sub2(x,0()) -> x
      sub2(s1(x),s1(y)) -> sub2(x,y)
      gtr2(0(),y) -> false()
      gtr2(s1(x),0()) -> true()
      gtr2(s1(x),s1(y)) -> gtr2(x,y)
      d2(x,0()) -> true()
      d2(s1(x),s1(y)) -> if3(gtr2(x,y),false(),d2(s1(x),sub2(y,x)))
      len1(nil()) -> 0()
      len1(cons2(x,xs)) -> s1(len1(xs))
      filter2(p,nil()) -> nil()
      filter2(p,cons2(x,xs)) -> if3(app(p,x),cons2(x,filter2(p,xs)),filter2(p,xs))
      app(if2(x6,x5),x7) -> if3(x6,x5,x7)
      app(if1(x6),x7) -> if2(x6,x7)
      app(if(),x7) -> if1(x7)
      app(sub1(x6),x7) -> sub2(x6,x7)
      app(sub(),x7) -> sub1(x7)
      app(s(),x7) -> s1(x7)
      app(gtr1(x6),x7) -> gtr2(x6,x7)
      app(gtr(),x7) -> gtr1(x7)
      app(d1(x6),x7) -> d2(x6,x7)
      app(d(),x7) -> d1(x7)
      app(len(),x7) -> len1(x7)
      app(cons1(x6),x7) -> cons2(x6,x7)
      app(cons(),x7) -> cons1(x7)
      app(filter1(x6),x7) -> filter2(x6,x7)
      app(filter(),x7) -> filter1(x7)
     Subterm Criterion Processor:
      simple projection:
       pi(filter{2,#}) = 1
       pi(app#) = 1
      problem:
       DPs:
        app#(filter1(x6),x7) -> filter{2,#}(x6,x7)
       TRS:
        if3(true(),xs,ys) -> xs
        if3(false(),xs,ys) -> ys
        sub2(x,0()) -> x
        sub2(s1(x),s1(y)) -> sub2(x,y)
        gtr2(0(),y) -> false()
        gtr2(s1(x),0()) -> true()
        gtr2(s1(x),s1(y)) -> gtr2(x,y)
        d2(x,0()) -> true()
        d2(s1(x),s1(y)) -> if3(gtr2(x,y),false(),d2(s1(x),sub2(y,x)))
        len1(nil()) -> 0()
        len1(cons2(x,xs)) -> s1(len1(xs))
        filter2(p,nil()) -> nil()
        filter2(p,cons2(x,xs)) -> if3(app(p,x),cons2(x,filter2(p,xs)),filter2(p,xs))
        app(if2(x6,x5),x7) -> if3(x6,x5,x7)
        app(if1(x6),x7) -> if2(x6,x7)
        app(if(),x7) -> if1(x7)
        app(sub1(x6),x7) -> sub2(x6,x7)
        app(sub(),x7) -> sub1(x7)
        app(s(),x7) -> s1(x7)
        app(gtr1(x6),x7) -> gtr2(x6,x7)
        app(gtr(),x7) -> gtr1(x7)
        app(d1(x6),x7) -> d2(x6,x7)
        app(d(),x7) -> d1(x7)
        app(len(),x7) -> len1(x7)
        app(cons1(x6),x7) -> cons2(x6,x7)
        app(cons(),x7) -> cons1(x7)
        app(filter1(x6),x7) -> filter2(x6,x7)
        app(filter(),x7) -> filter1(x7)
      SCC Processor:
       #sccs: 0
       #rules: 0
       #arcs: 5/1
       
     
     DPs:
      len{1,#}(cons2(x,xs)) -> len{1,#}(xs)
     TRS:
      if3(true(),xs,ys) -> xs
      if3(false(),xs,ys) -> ys
      sub2(x,0()) -> x
      sub2(s1(x),s1(y)) -> sub2(x,y)
      gtr2(0(),y) -> false()
      gtr2(s1(x),0()) -> true()
      gtr2(s1(x),s1(y)) -> gtr2(x,y)
      d2(x,0()) -> true()
      d2(s1(x),s1(y)) -> if3(gtr2(x,y),false(),d2(s1(x),sub2(y,x)))
      len1(nil()) -> 0()
      len1(cons2(x,xs)) -> s1(len1(xs))
      filter2(p,nil()) -> nil()
      filter2(p,cons2(x,xs)) -> if3(app(p,x),cons2(x,filter2(p,xs)),filter2(p,xs))
      app(if2(x6,x5),x7) -> if3(x6,x5,x7)
      app(if1(x6),x7) -> if2(x6,x7)
      app(if(),x7) -> if1(x7)
      app(sub1(x6),x7) -> sub2(x6,x7)
      app(sub(),x7) -> sub1(x7)
      app(s(),x7) -> s1(x7)
      app(gtr1(x6),x7) -> gtr2(x6,x7)
      app(gtr(),x7) -> gtr1(x7)
      app(d1(x6),x7) -> d2(x6,x7)
      app(d(),x7) -> d1(x7)
      app(len(),x7) -> len1(x7)
      app(cons1(x6),x7) -> cons2(x6,x7)
      app(cons(),x7) -> cons1(x7)
      app(filter1(x6),x7) -> filter2(x6,x7)
      app(filter(),x7) -> filter1(x7)
     Subterm Criterion Processor:
      simple projection:
       pi(len{1,#}) = 0
      problem:
       DPs:
        
       TRS:
        if3(true(),xs,ys) -> xs
        if3(false(),xs,ys) -> ys
        sub2(x,0()) -> x
        sub2(s1(x),s1(y)) -> sub2(x,y)
        gtr2(0(),y) -> false()
        gtr2(s1(x),0()) -> true()
        gtr2(s1(x),s1(y)) -> gtr2(x,y)
        d2(x,0()) -> true()
        d2(s1(x),s1(y)) -> if3(gtr2(x,y),false(),d2(s1(x),sub2(y,x)))
        len1(nil()) -> 0()
        len1(cons2(x,xs)) -> s1(len1(xs))
        filter2(p,nil()) -> nil()
        filter2(p,cons2(x,xs)) -> if3(app(p,x),cons2(x,filter2(p,xs)),filter2(p,xs))
        app(if2(x6,x5),x7) -> if3(x6,x5,x7)
        app(if1(x6),x7) -> if2(x6,x7)
        app(if(),x7) -> if1(x7)
        app(sub1(x6),x7) -> sub2(x6,x7)
        app(sub(),x7) -> sub1(x7)
        app(s(),x7) -> s1(x7)
        app(gtr1(x6),x7) -> gtr2(x6,x7)
        app(gtr(),x7) -> gtr1(x7)
        app(d1(x6),x7) -> d2(x6,x7)
        app(d(),x7) -> d1(x7)
        app(len(),x7) -> len1(x7)
        app(cons1(x6),x7) -> cons2(x6,x7)
        app(cons(),x7) -> cons1(x7)
        app(filter1(x6),x7) -> filter2(x6,x7)
        app(filter(),x7) -> filter1(x7)
      Qed
     
     DPs:
      d{2,#}(s1(x),s1(y)) -> d{2,#}(s1(x),sub2(y,x))
     TRS:
      if3(true(),xs,ys) -> xs
      if3(false(),xs,ys) -> ys
      sub2(x,0()) -> x
      sub2(s1(x),s1(y)) -> sub2(x,y)
      gtr2(0(),y) -> false()
      gtr2(s1(x),0()) -> true()
      gtr2(s1(x),s1(y)) -> gtr2(x,y)
      d2(x,0()) -> true()
      d2(s1(x),s1(y)) -> if3(gtr2(x,y),false(),d2(s1(x),sub2(y,x)))
      len1(nil()) -> 0()
      len1(cons2(x,xs)) -> s1(len1(xs))
      filter2(p,nil()) -> nil()
      filter2(p,cons2(x,xs)) -> if3(app(p,x),cons2(x,filter2(p,xs)),filter2(p,xs))
      app(if2(x6,x5),x7) -> if3(x6,x5,x7)
      app(if1(x6),x7) -> if2(x6,x7)
      app(if(),x7) -> if1(x7)
      app(sub1(x6),x7) -> sub2(x6,x7)
      app(sub(),x7) -> sub1(x7)
      app(s(),x7) -> s1(x7)
      app(gtr1(x6),x7) -> gtr2(x6,x7)
      app(gtr(),x7) -> gtr1(x7)
      app(d1(x6),x7) -> d2(x6,x7)
      app(d(),x7) -> d1(x7)
      app(len(),x7) -> len1(x7)
      app(cons1(x6),x7) -> cons2(x6,x7)
      app(cons(),x7) -> cons1(x7)
      app(filter1(x6),x7) -> filter2(x6,x7)
      app(filter(),x7) -> filter1(x7)
     Arctic Interpretation Processor:
      dimension: 1
      interpretation:
       [d{2,#}](x0, x1) = 2x1,
       
       [filter2](x0, x1) = 2x1,
       
       [filter1](x0) = 1x0,
       
       [cons2](x0, x1) = 1x1 + 2,
       
       [cons1](x0) = 5,
       
       [len1](x0) = x0 + 0,
       
       [d2](x0, x1) = 4x1,
       
       [d1](x0) = 1x0,
       
       [gtr2](x0, x1) = x0 + 0,
       
       [gtr1](x0) = 2x0,
       
       [s1](x0) = 1x0 + 2,
       
       [sub2](x0, x1) = x0 + 0,
       
       [sub1](x0) = 4x0 + 0,
       
       [if1](x0) = x0 + 4,
       
       [if3](x0, x1, x2) = x1 + x2 + 4,
       
       [if2](x0, x1) = x0 + x1 + 4,
       
       [filter] = 0,
       
       [cons] = 5,
       
       [nil] = 2,
       
       [len] = 6,
       
       [d] = 0,
       
       [gtr] = 2,
       
       [s] = 3,
       
       [0] = 2,
       
       [sub] = 4,
       
       [false] = 1,
       
       [app](x0, x1) = x0 + 4x1 + 0,
       
       [true] = 2,
       
       [if] = 7
      orientation:
       d{2,#}(s1(x),s1(y)) = 3y + 4 >= 2y + 2 = d{2,#}(s1(x),sub2(y,x))
       
       if3(true(),xs,ys) = xs + ys + 4 >= xs = xs
       
       if3(false(),xs,ys) = xs + ys + 4 >= ys = ys
       
       sub2(x,0()) = x + 0 >= x = x
       
       sub2(s1(x),s1(y)) = 1x + 2 >= x + 0 = sub2(x,y)
       
       gtr2(0(),y) = 2 >= 1 = false()
       
       gtr2(s1(x),0()) = 1x + 2 >= 2 = true()
       
       gtr2(s1(x),s1(y)) = 1x + 2 >= x + 0 = gtr2(x,y)
       
       d2(x,0()) = 6 >= 2 = true()
       
       d2(s1(x),s1(y)) = 5y + 6 >= 4y + 4 = if3(gtr2(x,y),false(),d2(s1(x),sub2(y,x)))
       
       len1(nil()) = 2 >= 2 = 0()
       
       len1(cons2(x,xs)) = 1xs + 2 >= 1xs + 2 = s1(len1(xs))
       
       filter2(p,nil()) = 4 >= 2 = nil()
       
       filter2(p,cons2(x,xs)) = 3xs + 4 >= 3xs + 4 = if3(app(p,x),cons2(x,filter2(p,xs)),filter2(p,xs))
       
       app(if2(x6,x5),x7) = x5 + x6 + 4x7 + 4 >= x5 + x7 + 4 = if3(x6,x5,x7)
       
       app(if1(x6),x7) = x6 + 4x7 + 4 >= x6 + x7 + 4 = if2(x6,x7)
       
       app(if(),x7) = 4x7 + 7 >= x7 + 4 = if1(x7)
       
       app(sub1(x6),x7) = 4x6 + 4x7 + 0 >= x6 + 0 = sub2(x6,x7)
       
       app(sub(),x7) = 4x7 + 4 >= 4x7 + 0 = sub1(x7)
       
       app(s(),x7) = 4x7 + 3 >= 1x7 + 2 = s1(x7)
       
       app(gtr1(x6),x7) = 2x6 + 4x7 + 0 >= x6 + 0 = gtr2(x6,x7)
       
       app(gtr(),x7) = 4x7 + 2 >= 2x7 = gtr1(x7)
       
       app(d1(x6),x7) = 1x6 + 4x7 + 0 >= 4x7 = d2(x6,x7)
       
       app(d(),x7) = 4x7 + 0 >= 1x7 = d1(x7)
       
       app(len(),x7) = 4x7 + 6 >= x7 + 0 = len1(x7)
       
       app(cons1(x6),x7) = 4x7 + 5 >= 1x7 + 2 = cons2(x6,x7)
       
       app(cons(),x7) = 4x7 + 5 >= 5 = cons1(x7)
       
       app(filter1(x6),x7) = 1x6 + 4x7 + 0 >= 2x7 = filter2(x6,x7)
       
       app(filter(),x7) = 4x7 + 0 >= 1x7 = filter1(x7)
      problem:
       DPs:
        
       TRS:
        if3(true(),xs,ys) -> xs
        if3(false(),xs,ys) -> ys
        sub2(x,0()) -> x
        sub2(s1(x),s1(y)) -> sub2(x,y)
        gtr2(0(),y) -> false()
        gtr2(s1(x),0()) -> true()
        gtr2(s1(x),s1(y)) -> gtr2(x,y)
        d2(x,0()) -> true()
        d2(s1(x),s1(y)) -> if3(gtr2(x,y),false(),d2(s1(x),sub2(y,x)))
        len1(nil()) -> 0()
        len1(cons2(x,xs)) -> s1(len1(xs))
        filter2(p,nil()) -> nil()
        filter2(p,cons2(x,xs)) -> if3(app(p,x),cons2(x,filter2(p,xs)),filter2(p,xs))
        app(if2(x6,x5),x7) -> if3(x6,x5,x7)
        app(if1(x6),x7) -> if2(x6,x7)
        app(if(),x7) -> if1(x7)
        app(sub1(x6),x7) -> sub2(x6,x7)
        app(sub(),x7) -> sub1(x7)
        app(s(),x7) -> s1(x7)
        app(gtr1(x6),x7) -> gtr2(x6,x7)
        app(gtr(),x7) -> gtr1(x7)
        app(d1(x6),x7) -> d2(x6,x7)
        app(d(),x7) -> d1(x7)
        app(len(),x7) -> len1(x7)
        app(cons1(x6),x7) -> cons2(x6,x7)
        app(cons(),x7) -> cons1(x7)
        app(filter1(x6),x7) -> filter2(x6,x7)
        app(filter(),x7) -> filter1(x7)
      Qed
     
     DPs:
      gtr{2,#}(s1(x),s1(y)) -> gtr{2,#}(x,y)
     TRS:
      if3(true(),xs,ys) -> xs
      if3(false(),xs,ys) -> ys
      sub2(x,0()) -> x
      sub2(s1(x),s1(y)) -> sub2(x,y)
      gtr2(0(),y) -> false()
      gtr2(s1(x),0()) -> true()
      gtr2(s1(x),s1(y)) -> gtr2(x,y)
      d2(x,0()) -> true()
      d2(s1(x),s1(y)) -> if3(gtr2(x,y),false(),d2(s1(x),sub2(y,x)))
      len1(nil()) -> 0()
      len1(cons2(x,xs)) -> s1(len1(xs))
      filter2(p,nil()) -> nil()
      filter2(p,cons2(x,xs)) -> if3(app(p,x),cons2(x,filter2(p,xs)),filter2(p,xs))
      app(if2(x6,x5),x7) -> if3(x6,x5,x7)
      app(if1(x6),x7) -> if2(x6,x7)
      app(if(),x7) -> if1(x7)
      app(sub1(x6),x7) -> sub2(x6,x7)
      app(sub(),x7) -> sub1(x7)
      app(s(),x7) -> s1(x7)
      app(gtr1(x6),x7) -> gtr2(x6,x7)
      app(gtr(),x7) -> gtr1(x7)
      app(d1(x6),x7) -> d2(x6,x7)
      app(d(),x7) -> d1(x7)
      app(len(),x7) -> len1(x7)
      app(cons1(x6),x7) -> cons2(x6,x7)
      app(cons(),x7) -> cons1(x7)
      app(filter1(x6),x7) -> filter2(x6,x7)
      app(filter(),x7) -> filter1(x7)
     Subterm Criterion Processor:
      simple projection:
       pi(gtr{2,#}) = 1
      problem:
       DPs:
        
       TRS:
        if3(true(),xs,ys) -> xs
        if3(false(),xs,ys) -> ys
        sub2(x,0()) -> x
        sub2(s1(x),s1(y)) -> sub2(x,y)
        gtr2(0(),y) -> false()
        gtr2(s1(x),0()) -> true()
        gtr2(s1(x),s1(y)) -> gtr2(x,y)
        d2(x,0()) -> true()
        d2(s1(x),s1(y)) -> if3(gtr2(x,y),false(),d2(s1(x),sub2(y,x)))
        len1(nil()) -> 0()
        len1(cons2(x,xs)) -> s1(len1(xs))
        filter2(p,nil()) -> nil()
        filter2(p,cons2(x,xs)) -> if3(app(p,x),cons2(x,filter2(p,xs)),filter2(p,xs))
        app(if2(x6,x5),x7) -> if3(x6,x5,x7)
        app(if1(x6),x7) -> if2(x6,x7)
        app(if(),x7) -> if1(x7)
        app(sub1(x6),x7) -> sub2(x6,x7)
        app(sub(),x7) -> sub1(x7)
        app(s(),x7) -> s1(x7)
        app(gtr1(x6),x7) -> gtr2(x6,x7)
        app(gtr(),x7) -> gtr1(x7)
        app(d1(x6),x7) -> d2(x6,x7)
        app(d(),x7) -> d1(x7)
        app(len(),x7) -> len1(x7)
        app(cons1(x6),x7) -> cons2(x6,x7)
        app(cons(),x7) -> cons1(x7)
        app(filter1(x6),x7) -> filter2(x6,x7)
        app(filter(),x7) -> filter1(x7)
      Qed
     
     DPs:
      sub{2,#}(s1(x),s1(y)) -> sub{2,#}(x,y)
     TRS:
      if3(true(),xs,ys) -> xs
      if3(false(),xs,ys) -> ys
      sub2(x,0()) -> x
      sub2(s1(x),s1(y)) -> sub2(x,y)
      gtr2(0(),y) -> false()
      gtr2(s1(x),0()) -> true()
      gtr2(s1(x),s1(y)) -> gtr2(x,y)
      d2(x,0()) -> true()
      d2(s1(x),s1(y)) -> if3(gtr2(x,y),false(),d2(s1(x),sub2(y,x)))
      len1(nil()) -> 0()
      len1(cons2(x,xs)) -> s1(len1(xs))
      filter2(p,nil()) -> nil()
      filter2(p,cons2(x,xs)) -> if3(app(p,x),cons2(x,filter2(p,xs)),filter2(p,xs))
      app(if2(x6,x5),x7) -> if3(x6,x5,x7)
      app(if1(x6),x7) -> if2(x6,x7)
      app(if(),x7) -> if1(x7)
      app(sub1(x6),x7) -> sub2(x6,x7)
      app(sub(),x7) -> sub1(x7)
      app(s(),x7) -> s1(x7)
      app(gtr1(x6),x7) -> gtr2(x6,x7)
      app(gtr(),x7) -> gtr1(x7)
      app(d1(x6),x7) -> d2(x6,x7)
      app(d(),x7) -> d1(x7)
      app(len(),x7) -> len1(x7)
      app(cons1(x6),x7) -> cons2(x6,x7)
      app(cons(),x7) -> cons1(x7)
      app(filter1(x6),x7) -> filter2(x6,x7)
      app(filter(),x7) -> filter1(x7)
     Subterm Criterion Processor:
      simple projection:
       pi(sub{2,#}) = 1
      problem:
       DPs:
        
       TRS:
        if3(true(),xs,ys) -> xs
        if3(false(),xs,ys) -> ys
        sub2(x,0()) -> x
        sub2(s1(x),s1(y)) -> sub2(x,y)
        gtr2(0(),y) -> false()
        gtr2(s1(x),0()) -> true()
        gtr2(s1(x),s1(y)) -> gtr2(x,y)
        d2(x,0()) -> true()
        d2(s1(x),s1(y)) -> if3(gtr2(x,y),false(),d2(s1(x),sub2(y,x)))
        len1(nil()) -> 0()
        len1(cons2(x,xs)) -> s1(len1(xs))
        filter2(p,nil()) -> nil()
        filter2(p,cons2(x,xs)) -> if3(app(p,x),cons2(x,filter2(p,xs)),filter2(p,xs))
        app(if2(x6,x5),x7) -> if3(x6,x5,x7)
        app(if1(x6),x7) -> if2(x6,x7)
        app(if(),x7) -> if1(x7)
        app(sub1(x6),x7) -> sub2(x6,x7)
        app(sub(),x7) -> sub1(x7)
        app(s(),x7) -> s1(x7)
        app(gtr1(x6),x7) -> gtr2(x6,x7)
        app(gtr(),x7) -> gtr1(x7)
        app(d1(x6),x7) -> d2(x6,x7)
        app(d(),x7) -> d1(x7)
        app(len(),x7) -> len1(x7)
        app(cons1(x6),x7) -> cons2(x6,x7)
        app(cons(),x7) -> cons1(x7)
        app(filter1(x6),x7) -> filter2(x6,x7)
        app(filter(),x7) -> filter1(x7)
      Qed