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)
     Usable Rule Processor:
      DPs:
       d{2,#}(s1(x),s1(y)) -> d{2,#}(s1(x),sub2(y,x))
      TRS:
       sub2(x,0()) -> x
       sub2(s1(x),s1(y)) -> sub2(x,y)
      Arctic Interpretation Processor:
       dimension: 1
       usable rules:
        sub2(x,0()) -> x
        sub2(s1(x),s1(y)) -> sub2(x,y)
       interpretation:
        [d{2,#}](x0, x1) = x1,
        
        [s1](x0) = 1x0 + -1,
        
        [sub2](x0, x1) = x0 + -2,
        
        [0] = 2
       orientation:
        d{2,#}(s1(x),s1(y)) = 1y + -1 >= y + -2 = d{2,#}(s1(x),sub2(y,x))
        
        sub2(x,0()) = x + -2 >= x = x
        
        sub2(s1(x),s1(y)) = 1x + -1 >= x + -2 = sub2(x,y)
       problem:
        DPs:
         
        TRS:
         sub2(x,0()) -> x
         sub2(s1(x),s1(y)) -> sub2(x,y)
       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