YES

Problem:
 a(a(append(),nil()),ys) -> ys
 a(a(append(),a(a(cons(),x),xs)),ys) -> a(a(cons(),x),a(a(append(),xs),ys))
 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(le(),0()),y) -> true()
 a(a(le(),a(s(),x)),0()) -> false()
 a(a(le(),a(s(),x)),a(s(),y)) -> a(a(le(),x),y)
 a(a(a(if(),true()),x),xs) -> a(a(cons(),x),xs)
 a(a(a(if(),false()),x),xs) -> xs
 a(a(not(),f),b) -> a(not2(),a(f,b))
 a(not2(),true()) -> false()
 a(not2(),false()) -> true()
 a(qs(),nil()) -> nil()
 a(qs(),a(a(cons(),x),xs)) ->
 a(a(append(),a(qs(),a(a(filter(),a(le(),x)),xs))),a(a(cons(),x),a(qs(),
                                                                   a(
                                                                    a(filter(),a(not(),a(le(),x))),
                                                                    xs))))

Proof:
 Uncurry Processor:
  append2(nil(),ys) -> ys
  append2(cons2(x,xs),ys) -> cons2(x,append2(xs,ys))
  filter2(f,nil()) -> nil()
  filter2(f,cons2(x,xs)) -> if3(a(f,x),x,filter2(f,xs))
  le2(0(),y) -> true()
  le2(s1(x),0()) -> false()
  le2(s1(x),s1(y)) -> le2(x,y)
  if3(true(),x,xs) -> cons2(x,xs)
  if3(false(),x,xs) -> xs
  not2(f,b) -> not21(a(f,b))
  not21(true()) -> false()
  not21(false()) -> true()
  qs1(nil()) -> nil()
  qs1(cons2(x,xs)) -> append2(qs1(filter2(le1(x),xs)),cons2(x,qs1(filter2(not1(le1(x)),xs))))
  a(append1(x7),x8) -> append2(x7,x8)
  a(append(),x8) -> append1(x8)
  a(cons1(x7),x8) -> cons2(x7,x8)
  a(cons(),x8) -> cons1(x8)
  a(filter1(x7),x8) -> filter2(x7,x8)
  a(filter(),x8) -> filter1(x8)
  a(if2(x7,x6),x8) -> if3(x7,x6,x8)
  a(if1(x7),x8) -> if2(x7,x8)
  a(if(),x8) -> if1(x8)
  a(le1(x7),x8) -> le2(x7,x8)
  a(le(),x8) -> le1(x8)
  a(s(),x8) -> s1(x8)
  a(not1(x7),x8) -> not2(x7,x8)
  a(not(),x8) -> not1(x8)
  a(not2(),x8) -> not21(x8)
  a(qs(),x8) -> qs1(x8)
  DP Processor:
   DPs:
    append{2,#}(cons2(x,xs),ys) -> append{2,#}(xs,ys)
    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))
    le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y)
    not{2,#}(f,b) -> a#(f,b)
    not{2,#}(f,b) -> not2{1,#}(a(f,b))
    qs{1,#}(cons2(x,xs)) -> filter{2,#}(not1(le1(x)),xs)
    qs{1,#}(cons2(x,xs)) -> qs{1,#}(filter2(not1(le1(x)),xs))
    qs{1,#}(cons2(x,xs)) -> filter{2,#}(le1(x),xs)
    qs{1,#}(cons2(x,xs)) -> qs{1,#}(filter2(le1(x),xs))
    qs{1,#}(cons2(x,xs)) ->
    append{2,#}(qs1(filter2(le1(x),xs)),cons2(x,qs1(filter2(not1(le1(x)),xs))))
    a#(append1(x7),x8) -> append{2,#}(x7,x8)
    a#(filter1(x7),x8) -> filter{2,#}(x7,x8)
    a#(if2(x7,x6),x8) -> if{3,#}(x7,x6,x8)
    a#(le1(x7),x8) -> le{2,#}(x7,x8)
    a#(not1(x7),x8) -> not{2,#}(x7,x8)
    a#(not2(),x8) -> not2{1,#}(x8)
    a#(qs(),x8) -> qs{1,#}(x8)
   TRS:
    append2(nil(),ys) -> ys
    append2(cons2(x,xs),ys) -> cons2(x,append2(xs,ys))
    filter2(f,nil()) -> nil()
    filter2(f,cons2(x,xs)) -> if3(a(f,x),x,filter2(f,xs))
    le2(0(),y) -> true()
    le2(s1(x),0()) -> false()
    le2(s1(x),s1(y)) -> le2(x,y)
    if3(true(),x,xs) -> cons2(x,xs)
    if3(false(),x,xs) -> xs
    not2(f,b) -> not21(a(f,b))
    not21(true()) -> false()
    not21(false()) -> true()
    qs1(nil()) -> nil()
    qs1(cons2(x,xs)) -> append2(qs1(filter2(le1(x),xs)),cons2(x,qs1(filter2(not1(le1(x)),xs))))
    a(append1(x7),x8) -> append2(x7,x8)
    a(append(),x8) -> append1(x8)
    a(cons1(x7),x8) -> cons2(x7,x8)
    a(cons(),x8) -> cons1(x8)
    a(filter1(x7),x8) -> filter2(x7,x8)
    a(filter(),x8) -> filter1(x8)
    a(if2(x7,x6),x8) -> if3(x7,x6,x8)
    a(if1(x7),x8) -> if2(x7,x8)
    a(if(),x8) -> if1(x8)
    a(le1(x7),x8) -> le2(x7,x8)
    a(le(),x8) -> le1(x8)
    a(s(),x8) -> s1(x8)
    a(not1(x7),x8) -> not2(x7,x8)
    a(not(),x8) -> not1(x8)
    a(not2(),x8) -> not21(x8)
    a(qs(),x8) -> qs1(x8)
   TDG Processor:
    DPs:
     append{2,#}(cons2(x,xs),ys) -> append{2,#}(xs,ys)
     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))
     le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y)
     not{2,#}(f,b) -> a#(f,b)
     not{2,#}(f,b) -> not2{1,#}(a(f,b))
     qs{1,#}(cons2(x,xs)) -> filter{2,#}(not1(le1(x)),xs)
     qs{1,#}(cons2(x,xs)) -> qs{1,#}(filter2(not1(le1(x)),xs))
     qs{1,#}(cons2(x,xs)) -> filter{2,#}(le1(x),xs)
     qs{1,#}(cons2(x,xs)) -> qs{1,#}(filter2(le1(x),xs))
     qs{1,#}(cons2(x,xs)) ->
     append{2,#}(qs1(filter2(le1(x),xs)),cons2(x,qs1(filter2(not1(le1(x)),xs))))
     a#(append1(x7),x8) -> append{2,#}(x7,x8)
     a#(filter1(x7),x8) -> filter{2,#}(x7,x8)
     a#(if2(x7,x6),x8) -> if{3,#}(x7,x6,x8)
     a#(le1(x7),x8) -> le{2,#}(x7,x8)
     a#(not1(x7),x8) -> not{2,#}(x7,x8)
     a#(not2(),x8) -> not2{1,#}(x8)
     a#(qs(),x8) -> qs{1,#}(x8)
    TRS:
     append2(nil(),ys) -> ys
     append2(cons2(x,xs),ys) -> cons2(x,append2(xs,ys))
     filter2(f,nil()) -> nil()
     filter2(f,cons2(x,xs)) -> if3(a(f,x),x,filter2(f,xs))
     le2(0(),y) -> true()
     le2(s1(x),0()) -> false()
     le2(s1(x),s1(y)) -> le2(x,y)
     if3(true(),x,xs) -> cons2(x,xs)
     if3(false(),x,xs) -> xs
     not2(f,b) -> not21(a(f,b))
     not21(true()) -> false()
     not21(false()) -> true()
     qs1(nil()) -> nil()
     qs1(cons2(x,xs)) -> append2(qs1(filter2(le1(x),xs)),cons2(x,qs1(filter2(not1(le1(x)),xs))))
     a(append1(x7),x8) -> append2(x7,x8)
     a(append(),x8) -> append1(x8)
     a(cons1(x7),x8) -> cons2(x7,x8)
     a(cons(),x8) -> cons1(x8)
     a(filter1(x7),x8) -> filter2(x7,x8)
     a(filter(),x8) -> filter1(x8)
     a(if2(x7,x6),x8) -> if3(x7,x6,x8)
     a(if1(x7),x8) -> if2(x7,x8)
     a(if(),x8) -> if1(x8)
     a(le1(x7),x8) -> le2(x7,x8)
     a(le(),x8) -> le1(x8)
     a(s(),x8) -> s1(x8)
     a(not1(x7),x8) -> not2(x7,x8)
     a(not(),x8) -> not1(x8)
     a(not2(),x8) -> not21(x8)
     a(qs(),x8) -> qs1(x8)
    graph:
     qs{1,#}(cons2(x,xs)) -> qs{1,#}(filter2(not1(le1(x)),xs)) ->
     qs{1,#}(cons2(x,xs)) ->
     append{2,#}(qs1(filter2(le1(x),xs)),cons2(x,qs1(filter2(not1(le1(x)),xs))))
     qs{1,#}(cons2(x,xs)) -> qs{1,#}(filter2(not1(le1(x)),xs)) ->
     qs{1,#}(cons2(x,xs)) -> qs{1,#}(filter2(le1(x),xs))
     qs{1,#}(cons2(x,xs)) -> qs{1,#}(filter2(not1(le1(x)),xs)) ->
     qs{1,#}(cons2(x,xs)) -> filter{2,#}(le1(x),xs)
     qs{1,#}(cons2(x,xs)) -> qs{1,#}(filter2(not1(le1(x)),xs)) ->
     qs{1,#}(cons2(x,xs)) -> qs{1,#}(filter2(not1(le1(x)),xs))
     qs{1,#}(cons2(x,xs)) -> qs{1,#}(filter2(not1(le1(x)),xs)) ->
     qs{1,#}(cons2(x,xs)) -> filter{2,#}(not1(le1(x)),xs)
     qs{1,#}(cons2(x,xs)) -> qs{1,#}(filter2(le1(x),xs)) ->
     qs{1,#}(cons2(x,xs)) ->
     append{2,#}(qs1(filter2(le1(x),xs)),cons2(x,qs1(filter2(not1(le1(x)),xs))))
     qs{1,#}(cons2(x,xs)) -> qs{1,#}(filter2(le1(x),xs)) ->
     qs{1,#}(cons2(x,xs)) -> qs{1,#}(filter2(le1(x),xs))
     qs{1,#}(cons2(x,xs)) -> qs{1,#}(filter2(le1(x),xs)) ->
     qs{1,#}(cons2(x,xs)) -> filter{2,#}(le1(x),xs)
     qs{1,#}(cons2(x,xs)) -> qs{1,#}(filter2(le1(x),xs)) ->
     qs{1,#}(cons2(x,xs)) -> qs{1,#}(filter2(not1(le1(x)),xs))
     qs{1,#}(cons2(x,xs)) -> qs{1,#}(filter2(le1(x),xs)) ->
     qs{1,#}(cons2(x,xs)) -> filter{2,#}(not1(le1(x)),xs)
     qs{1,#}(cons2(x,xs)) -> filter{2,#}(not1(le1(x)),xs) ->
     filter{2,#}(f,cons2(x,xs)) -> if{3,#}(a(f,x),x,filter2(f,xs))
     qs{1,#}(cons2(x,xs)) -> filter{2,#}(not1(le1(x)),xs) ->
     filter{2,#}(f,cons2(x,xs)) -> a#(f,x)
     qs{1,#}(cons2(x,xs)) -> filter{2,#}(not1(le1(x)),xs) ->
     filter{2,#}(f,cons2(x,xs)) -> filter{2,#}(f,xs)
     qs{1,#}(cons2(x,xs)) -> filter{2,#}(le1(x),xs) ->
     filter{2,#}(f,cons2(x,xs)) -> if{3,#}(a(f,x),x,filter2(f,xs))
     qs{1,#}(cons2(x,xs)) -> filter{2,#}(le1(x),xs) ->
     filter{2,#}(f,cons2(x,xs)) -> a#(f,x)
     qs{1,#}(cons2(x,xs)) -> filter{2,#}(le1(x),xs) ->
     filter{2,#}(f,cons2(x,xs)) -> filter{2,#}(f,xs)
     qs{1,#}(cons2(x,xs)) ->
     append{2,#}(qs1(filter2(le1(x),xs)),cons2(x,qs1(filter2(not1(le1(x)),xs)))) ->
     append{2,#}(cons2(x,xs),ys) -> append{2,#}(xs,ys)
     not{2,#}(f,b) -> a#(f,b) -> a#(qs(),x8) -> qs{1,#}(x8)
     not{2,#}(f,b) -> a#(f,b) -> a#(not2(),x8) -> not2{1,#}(x8)
     not{2,#}(f,b) -> a#(f,b) -> a#(not1(x7),x8) -> not{2,#}(x7,x8)
     not{2,#}(f,b) -> a#(f,b) -> a#(le1(x7),x8) -> le{2,#}(x7,x8)
     not{2,#}(f,b) -> a#(f,b) -> a#(if2(x7,x6),x8) -> if{3,#}(x7,x6,x8)
     not{2,#}(f,b) -> a#(f,b) -> a#(filter1(x7),x8) -> filter{2,#}(x7,x8)
     not{2,#}(f,b) -> a#(f,b) ->
     a#(append1(x7),x8) -> append{2,#}(x7,x8)
     le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y) ->
     le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y)
     a#(not1(x7),x8) -> not{2,#}(x7,x8) ->
     not{2,#}(f,b) -> not2{1,#}(a(f,b))
     a#(not1(x7),x8) -> not{2,#}(x7,x8) -> not{2,#}(f,b) -> a#(f,b)
     a#(le1(x7),x8) -> le{2,#}(x7,x8) ->
     le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y)
     a#(filter1(x7),x8) -> filter{2,#}(x7,x8) ->
     filter{2,#}(f,cons2(x,xs)) -> if{3,#}(a(f,x),x,filter2(f,xs))
     a#(filter1(x7),x8) -> filter{2,#}(x7,x8) ->
     filter{2,#}(f,cons2(x,xs)) -> a#(f,x)
     a#(filter1(x7),x8) -> filter{2,#}(x7,x8) ->
     filter{2,#}(f,cons2(x,xs)) -> filter{2,#}(f,xs)
     a#(append1(x7),x8) -> append{2,#}(x7,x8) ->
     append{2,#}(cons2(x,xs),ys) -> append{2,#}(xs,ys)
     a#(qs(),x8) -> qs{1,#}(x8) ->
     qs{1,#}(cons2(x,xs)) ->
     append{2,#}(qs1(filter2(le1(x),xs)),cons2(x,qs1(filter2(not1(le1(x)),xs))))
     a#(qs(),x8) -> qs{1,#}(x8) ->
     qs{1,#}(cons2(x,xs)) -> qs{1,#}(filter2(le1(x),xs))
     a#(qs(),x8) -> qs{1,#}(x8) ->
     qs{1,#}(cons2(x,xs)) -> filter{2,#}(le1(x),xs)
     a#(qs(),x8) -> qs{1,#}(x8) ->
     qs{1,#}(cons2(x,xs)) -> qs{1,#}(filter2(not1(le1(x)),xs))
     a#(qs(),x8) -> qs{1,#}(x8) ->
     qs{1,#}(cons2(x,xs)) -> filter{2,#}(not1(le1(x)),xs)
     filter{2,#}(f,cons2(x,xs)) -> a#(f,x) ->
     a#(qs(),x8) -> qs{1,#}(x8)
     filter{2,#}(f,cons2(x,xs)) -> a#(f,x) ->
     a#(not2(),x8) -> not2{1,#}(x8)
     filter{2,#}(f,cons2(x,xs)) -> a#(f,x) ->
     a#(not1(x7),x8) -> not{2,#}(x7,x8)
     filter{2,#}(f,cons2(x,xs)) -> a#(f,x) ->
     a#(le1(x7),x8) -> le{2,#}(x7,x8)
     filter{2,#}(f,cons2(x,xs)) -> a#(f,x) ->
     a#(if2(x7,x6),x8) -> if{3,#}(x7,x6,x8)
     filter{2,#}(f,cons2(x,xs)) -> a#(f,x) ->
     a#(filter1(x7),x8) -> filter{2,#}(x7,x8)
     filter{2,#}(f,cons2(x,xs)) -> a#(f,x) ->
     a#(append1(x7),x8) -> append{2,#}(x7,x8)
     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)
     append{2,#}(cons2(x,xs),ys) -> append{2,#}(xs,ys) ->
     append{2,#}(cons2(x,xs),ys) -> append{2,#}(xs,ys)
    SCC Processor:
     #sccs: 3
     #rules: 12
     #arcs: 48/361
     DPs:
      qs{1,#}(cons2(x,xs)) -> qs{1,#}(filter2(not1(le1(x)),xs))
      qs{1,#}(cons2(x,xs)) -> filter{2,#}(not1(le1(x)),xs)
      filter{2,#}(f,cons2(x,xs)) -> filter{2,#}(f,xs)
      filter{2,#}(f,cons2(x,xs)) -> a#(f,x)
      a#(filter1(x7),x8) -> filter{2,#}(x7,x8)
      a#(not1(x7),x8) -> not{2,#}(x7,x8)
      not{2,#}(f,b) -> a#(f,b)
      a#(qs(),x8) -> qs{1,#}(x8)
      qs{1,#}(cons2(x,xs)) -> filter{2,#}(le1(x),xs)
      qs{1,#}(cons2(x,xs)) -> qs{1,#}(filter2(le1(x),xs))
     TRS:
      append2(nil(),ys) -> ys
      append2(cons2(x,xs),ys) -> cons2(x,append2(xs,ys))
      filter2(f,nil()) -> nil()
      filter2(f,cons2(x,xs)) -> if3(a(f,x),x,filter2(f,xs))
      le2(0(),y) -> true()
      le2(s1(x),0()) -> false()
      le2(s1(x),s1(y)) -> le2(x,y)
      if3(true(),x,xs) -> cons2(x,xs)
      if3(false(),x,xs) -> xs
      not2(f,b) -> not21(a(f,b))
      not21(true()) -> false()
      not21(false()) -> true()
      qs1(nil()) -> nil()
      qs1(cons2(x,xs)) -> append2(qs1(filter2(le1(x),xs)),cons2(x,qs1(filter2(not1(le1(x)),xs))))
      a(append1(x7),x8) -> append2(x7,x8)
      a(append(),x8) -> append1(x8)
      a(cons1(x7),x8) -> cons2(x7,x8)
      a(cons(),x8) -> cons1(x8)
      a(filter1(x7),x8) -> filter2(x7,x8)
      a(filter(),x8) -> filter1(x8)
      a(if2(x7,x6),x8) -> if3(x7,x6,x8)
      a(if1(x7),x8) -> if2(x7,x8)
      a(if(),x8) -> if1(x8)
      a(le1(x7),x8) -> le2(x7,x8)
      a(le(),x8) -> le1(x8)
      a(s(),x8) -> s1(x8)
      a(not1(x7),x8) -> not2(x7,x8)
      a(not(),x8) -> not1(x8)
      a(not2(),x8) -> not21(x8)
      a(qs(),x8) -> qs1(x8)
     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:
       [qs{1,#}](x0) = 3/2x0 + 1/2,
       
       [not{2,#}](x0, x1) = x0 + 2x1 + 2,
       
       [a#](x0, x1) = 1/2x0 + 2x1 + 2,
       
       [filter{2,#}](x0, x1) = 1/2x0 + 3/2x1 + 2,
       
       [qs1](x0) = 3,
       
       [not21](x0) = 3x0 + 5/2,
       
       [not2](x0, x1) = 0,
       
       [not1](x0) = 3x0,
       
       [s1](x0) = 3x0 + 3,
       
       [le2](x0, x1) = 2x0 + 2x1,
       
       [le1](x0) = x0,
       
       [if1](x0) = 3x0 + 2,
       
       [if3](x0, x1, x2) = 3x1 + x2 + 1,
       
       [if2](x0, x1) = x1 + 2,
       
       [filter2](x0, x1) = x0 + x1 + 1,
       
       [filter1](x0) = 3x0,
       
       [cons2](x0, x1) = 3x0 + x1 + 1,
       
       [cons1](x0) = 1/2,
       
       [append2](x0, x1) = 3x0 + x1 + 1/2,
       
       [append1](x0) = 1/2x0 + 1,
       
       [qs] = 1,
       
       [not2] = 5/2,
       
       [not] = 1/2,
       
       [false] = 3/2,
       
       [s] = 2,
       
       [true] = 1,
       
       [0] = 7/2,
       
       [le] = 1/2,
       
       [if] = 3,
       
       [filter] = 1,
       
       [cons] = 1,
       
       [a](x0, x1) = 2x0 + 3/2x1 + 1/2,
       
       [nil] = 2,
       
       [append] = 1
      orientation:
       qs{1,#}(cons2(x,xs)) = 9/2x + 3/2xs + 2 >= 9/2x + 3/2xs + 2 = qs{1,#}(filter2(not1(le1(x)),xs))
       
       qs{1,#}(cons2(x,xs)) = 9/2x + 3/2xs + 2 >= 3/2x + 3/2xs + 2 = filter{2,#}(not1(le1(x)),xs)
       
       filter{2,#}(f,cons2(x,xs)) = 1/2f + 9/2x + 3/2xs + 7/2 >= 1/2f + 3/2xs + 2 = filter{2,#}(f,xs)
       
       filter{2,#}(f,cons2(x,xs)) = 1/2f + 9/2x + 3/2xs + 7/2 >= 1/2f + 2x + 2 = a#(f,x)
       
       a#(filter1(x7),x8) = 3/2x7 + 2x8 + 2 >= 1/2x7 + 3/2x8 + 2 = filter{2,#}(x7,x8)
       
       a#(not1(x7),x8) = 3/2x7 + 2x8 + 2 >= x7 + 2x8 + 2 = not{2,#}(x7,x8)
       
       not{2,#}(f,b) = 2b + f + 2 >= 2b + 1/2f + 2 = a#(f,b)
       
       a#(qs(),x8) = 2x8 + 5/2 >= 3/2x8 + 1/2 = qs{1,#}(x8)
       
       qs{1,#}(cons2(x,xs)) = 9/2x + 3/2xs + 2 >= 1/2x + 3/2xs + 2 = filter{2,#}(le1(x),xs)
       
       qs{1,#}(cons2(x,xs)) = 9/2x + 3/2xs + 2 >= 3/2x + 3/2xs + 2 = qs{1,#}(filter2(le1(x),xs))
       
       append2(nil(),ys) = ys + 13/2 >= ys = ys
       
       append2(cons2(x,xs),ys) = 9x + 3xs + ys + 7/2 >= 3x + 3xs + ys + 3/2 = cons2(x,append2(xs,ys))
       
       filter2(f,nil()) = f + 3 >= 2 = nil()
       
       filter2(f,cons2(x,xs)) = f + 3x + xs + 2 >= f + 3x + xs + 2 = if3(a(f,x),x,filter2(f,xs))
       
       le2(0(),y) = 2y + 7 >= 1 = true()
       
       le2(s1(x),0()) = 6x + 13 >= 3/2 = false()
       
       le2(s1(x),s1(y)) = 6x + 6y + 12 >= 2x + 2y = le2(x,y)
       
       if3(true(),x,xs) = 3x + xs + 1 >= 3x + xs + 1 = cons2(x,xs)
       
       if3(false(),x,xs) = 3x + xs + 1 >= xs = xs
       
       not2(f,b) = 0 >= 9/2b + 6f + 4 = not21(a(f,b))
       
       not21(true()) = 11/2 >= 3/2 = false()
       
       not21(false()) = 7 >= 1 = true()
       
       qs1(nil()) = 3 >= 2 = nil()
       
       qs1(cons2(x,xs)) = 3 >= 3x + 27/2 = append2(qs1(filter2(le1(x),xs)),cons2(x,qs1(filter2(not1(le1(x)),xs))))
       
       a(append1(x7),x8) = x7 + 3/2x8 + 5/2 >= 3x7 + x8 + 1/2 = append2(x7,x8)
       
       a(append(),x8) = 3/2x8 + 5/2 >= 1/2x8 + 1 = append1(x8)
       
       a(cons1(x7),x8) = 3/2x8 + 3/2 >= 3x7 + x8 + 1 = cons2(x7,x8)
       
       a(cons(),x8) = 3/2x8 + 5/2 >= 1/2 = cons1(x8)
       
       a(filter1(x7),x8) = 6x7 + 3/2x8 + 1/2 >= x7 + x8 + 1 = filter2(x7,x8)
       
       a(filter(),x8) = 3/2x8 + 5/2 >= 3x8 = filter1(x8)
       
       a(if2(x7,x6),x8) = 2x6 + 3/2x8 + 9/2 >= 3x6 + x8 + 1 = if3(x7,x6,x8)
       
       a(if1(x7),x8) = 6x7 + 3/2x8 + 9/2 >= x8 + 2 = if2(x7,x8)
       
       a(if(),x8) = 3/2x8 + 13/2 >= 3x8 + 2 = if1(x8)
       
       a(le1(x7),x8) = 2x7 + 3/2x8 + 1/2 >= 2x7 + 2x8 = le2(x7,x8)
       
       a(le(),x8) = 3/2x8 + 3/2 >= x8 = le1(x8)
       
       a(s(),x8) = 3/2x8 + 9/2 >= 3x8 + 3 = s1(x8)
       
       a(not1(x7),x8) = 6x7 + 3/2x8 + 1/2 >= 0 = not2(x7,x8)
       
       a(not(),x8) = 3/2x8 + 3/2 >= 3x8 = not1(x8)
       
       a(not2(),x8) = 3/2x8 + 11/2 >= 3x8 + 5/2 = not21(x8)
       
       a(qs(),x8) = 3/2x8 + 5/2 >= 3 = qs1(x8)
      problem:
       DPs:
        qs{1,#}(cons2(x,xs)) -> qs{1,#}(filter2(not1(le1(x)),xs))
        qs{1,#}(cons2(x,xs)) -> filter{2,#}(not1(le1(x)),xs)
        a#(filter1(x7),x8) -> filter{2,#}(x7,x8)
        a#(not1(x7),x8) -> not{2,#}(x7,x8)
        not{2,#}(f,b) -> a#(f,b)
        qs{1,#}(cons2(x,xs)) -> filter{2,#}(le1(x),xs)
        qs{1,#}(cons2(x,xs)) -> qs{1,#}(filter2(le1(x),xs))
       TRS:
        append2(nil(),ys) -> ys
        append2(cons2(x,xs),ys) -> cons2(x,append2(xs,ys))
        filter2(f,nil()) -> nil()
        filter2(f,cons2(x,xs)) -> if3(a(f,x),x,filter2(f,xs))
        le2(0(),y) -> true()
        le2(s1(x),0()) -> false()
        le2(s1(x),s1(y)) -> le2(x,y)
        if3(true(),x,xs) -> cons2(x,xs)
        if3(false(),x,xs) -> xs
        not2(f,b) -> not21(a(f,b))
        not21(true()) -> false()
        not21(false()) -> true()
        qs1(nil()) -> nil()
        qs1(cons2(x,xs)) -> append2(qs1(filter2(le1(x),xs)),cons2(x,qs1(filter2(not1(le1(x)),xs))))
        a(append1(x7),x8) -> append2(x7,x8)
        a(append(),x8) -> append1(x8)
        a(cons1(x7),x8) -> cons2(x7,x8)
        a(cons(),x8) -> cons1(x8)
        a(filter1(x7),x8) -> filter2(x7,x8)
        a(filter(),x8) -> filter1(x8)
        a(if2(x7,x6),x8) -> if3(x7,x6,x8)
        a(if1(x7),x8) -> if2(x7,x8)
        a(if(),x8) -> if1(x8)
        a(le1(x7),x8) -> le2(x7,x8)
        a(le(),x8) -> le1(x8)
        a(s(),x8) -> s1(x8)
        a(not1(x7),x8) -> not2(x7,x8)
        a(not(),x8) -> not1(x8)
        a(not2(),x8) -> not21(x8)
        a(qs(),x8) -> qs1(x8)
      Restore Modifier:
       DPs:
        qs{1,#}(cons2(x,xs)) -> qs{1,#}(filter2(not1(le1(x)),xs))
        qs{1,#}(cons2(x,xs)) -> filter{2,#}(not1(le1(x)),xs)
        a#(filter1(x7),x8) -> filter{2,#}(x7,x8)
        a#(not1(x7),x8) -> not{2,#}(x7,x8)
        not{2,#}(f,b) -> a#(f,b)
        qs{1,#}(cons2(x,xs)) -> filter{2,#}(le1(x),xs)
        qs{1,#}(cons2(x,xs)) -> qs{1,#}(filter2(le1(x),xs))
       TRS:
        append2(nil(),ys) -> ys
        append2(cons2(x,xs),ys) -> cons2(x,append2(xs,ys))
        filter2(f,nil()) -> nil()
        filter2(f,cons2(x,xs)) -> if3(a(f,x),x,filter2(f,xs))
        le2(0(),y) -> true()
        le2(s1(x),0()) -> false()
        le2(s1(x),s1(y)) -> le2(x,y)
        if3(true(),x,xs) -> cons2(x,xs)
        if3(false(),x,xs) -> xs
        not2(f,b) -> not21(a(f,b))
        not21(true()) -> false()
        not21(false()) -> true()
        qs1(nil()) -> nil()
        qs1(cons2(x,xs)) -> append2(qs1(filter2(le1(x),xs)),cons2(x,qs1(filter2(not1(le1(x)),xs))))
        a(append1(x7),x8) -> append2(x7,x8)
        a(append(),x8) -> append1(x8)
        a(cons1(x7),x8) -> cons2(x7,x8)
        a(cons(),x8) -> cons1(x8)
        a(filter1(x7),x8) -> filter2(x7,x8)
        a(filter(),x8) -> filter1(x8)
        a(if2(x7,x6),x8) -> if3(x7,x6,x8)
        a(if1(x7),x8) -> if2(x7,x8)
        a(if(),x8) -> if1(x8)
        a(le1(x7),x8) -> le2(x7,x8)
        a(le(),x8) -> le1(x8)
        a(s(),x8) -> s1(x8)
        a(not1(x7),x8) -> not2(x7,x8)
        a(not(),x8) -> not1(x8)
        a(not2(),x8) -> not21(x8)
        a(qs(),x8) -> qs1(x8)
       SCC Processor:
        #sccs: 2
        #rules: 4
        #arcs: 27/49
        DPs:
         not{2,#}(f,b) -> a#(f,b)
         a#(not1(x7),x8) -> not{2,#}(x7,x8)
        TRS:
         append2(nil(),ys) -> ys
         append2(cons2(x,xs),ys) -> cons2(x,append2(xs,ys))
         filter2(f,nil()) -> nil()
         filter2(f,cons2(x,xs)) -> if3(a(f,x),x,filter2(f,xs))
         le2(0(),y) -> true()
         le2(s1(x),0()) -> false()
         le2(s1(x),s1(y)) -> le2(x,y)
         if3(true(),x,xs) -> cons2(x,xs)
         if3(false(),x,xs) -> xs
         not2(f,b) -> not21(a(f,b))
         not21(true()) -> false()
         not21(false()) -> true()
         qs1(nil()) -> nil()
         qs1(cons2(x,xs)) ->
         append2(qs1(filter2(le1(x),xs)),cons2(x,qs1(filter2(not1(le1(x)),xs))))
         a(append1(x7),x8) -> append2(x7,x8)
         a(append(),x8) -> append1(x8)
         a(cons1(x7),x8) -> cons2(x7,x8)
         a(cons(),x8) -> cons1(x8)
         a(filter1(x7),x8) -> filter2(x7,x8)
         a(filter(),x8) -> filter1(x8)
         a(if2(x7,x6),x8) -> if3(x7,x6,x8)
         a(if1(x7),x8) -> if2(x7,x8)
         a(if(),x8) -> if1(x8)
         a(le1(x7),x8) -> le2(x7,x8)
         a(le(),x8) -> le1(x8)
         a(s(),x8) -> s1(x8)
         a(not1(x7),x8) -> not2(x7,x8)
         a(not(),x8) -> not1(x8)
         a(not2(),x8) -> not21(x8)
         a(qs(),x8) -> qs1(x8)
        Subterm Criterion Processor:
         simple projection:
          pi(a#) = 0
          pi(not{2,#}) = 0
         problem:
          DPs:
           not{2,#}(f,b) -> a#(f,b)
          TRS:
           append2(nil(),ys) -> ys
           append2(cons2(x,xs),ys) -> cons2(x,append2(xs,ys))
           filter2(f,nil()) -> nil()
           filter2(f,cons2(x,xs)) -> if3(a(f,x),x,filter2(f,xs))
           le2(0(),y) -> true()
           le2(s1(x),0()) -> false()
           le2(s1(x),s1(y)) -> le2(x,y)
           if3(true(),x,xs) -> cons2(x,xs)
           if3(false(),x,xs) -> xs
           not2(f,b) -> not21(a(f,b))
           not21(true()) -> false()
           not21(false()) -> true()
           qs1(nil()) -> nil()
           qs1(cons2(x,xs)) ->
           append2(qs1(filter2(le1(x),xs)),cons2(x,qs1(filter2(not1(le1(x)),xs))))
           a(append1(x7),x8) -> append2(x7,x8)
           a(append(),x8) -> append1(x8)
           a(cons1(x7),x8) -> cons2(x7,x8)
           a(cons(),x8) -> cons1(x8)
           a(filter1(x7),x8) -> filter2(x7,x8)
           a(filter(),x8) -> filter1(x8)
           a(if2(x7,x6),x8) -> if3(x7,x6,x8)
           a(if1(x7),x8) -> if2(x7,x8)
           a(if(),x8) -> if1(x8)
           a(le1(x7),x8) -> le2(x7,x8)
           a(le(),x8) -> le1(x8)
           a(s(),x8) -> s1(x8)
           a(not1(x7),x8) -> not2(x7,x8)
           a(not(),x8) -> not1(x8)
           a(not2(),x8) -> not21(x8)
           a(qs(),x8) -> qs1(x8)
         SCC Processor:
          #sccs: 0
          #rules: 0
          #arcs: 2/1
          
        
        DPs:
         qs{1,#}(cons2(x,xs)) -> qs{1,#}(filter2(not1(le1(x)),xs))
         qs{1,#}(cons2(x,xs)) -> qs{1,#}(filter2(le1(x),xs))
        TRS:
         append2(nil(),ys) -> ys
         append2(cons2(x,xs),ys) -> cons2(x,append2(xs,ys))
         filter2(f,nil()) -> nil()
         filter2(f,cons2(x,xs)) -> if3(a(f,x),x,filter2(f,xs))
         le2(0(),y) -> true()
         le2(s1(x),0()) -> false()
         le2(s1(x),s1(y)) -> le2(x,y)
         if3(true(),x,xs) -> cons2(x,xs)
         if3(false(),x,xs) -> xs
         not2(f,b) -> not21(a(f,b))
         not21(true()) -> false()
         not21(false()) -> true()
         qs1(nil()) -> nil()
         qs1(cons2(x,xs)) ->
         append2(qs1(filter2(le1(x),xs)),cons2(x,qs1(filter2(not1(le1(x)),xs))))
         a(append1(x7),x8) -> append2(x7,x8)
         a(append(),x8) -> append1(x8)
         a(cons1(x7),x8) -> cons2(x7,x8)
         a(cons(),x8) -> cons1(x8)
         a(filter1(x7),x8) -> filter2(x7,x8)
         a(filter(),x8) -> filter1(x8)
         a(if2(x7,x6),x8) -> if3(x7,x6,x8)
         a(if1(x7),x8) -> if2(x7,x8)
         a(if(),x8) -> if1(x8)
         a(le1(x7),x8) -> le2(x7,x8)
         a(le(),x8) -> le1(x8)
         a(s(),x8) -> s1(x8)
         a(not1(x7),x8) -> not2(x7,x8)
         a(not(),x8) -> not1(x8)
         a(not2(),x8) -> not21(x8)
         a(qs(),x8) -> qs1(x8)
        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:
          [qs{1,#}](x0) = x0 + 0,
          
          [qs1](x0) = 4,
          
          [not21](x0) = 3x0 + 0,
          
          [not2](x0, x1) = x0 + x1 + 0,
          
          [not1](x0) = 4,
          
          [s1](x0) = x0 + 1,
          
          [le2](x0, x1) = 4x0 + x1 + 6,
          
          [le1](x0) = x0 + 3,
          
          [if1](x0) = 4x0 + 2,
          
          [if3](x0, x1, x2) = 2x2 + 4,
          
          [if2](x0, x1) = 3x0 + 2x1 + 4,
          
          [filter2](x0, x1) = x1,
          
          [filter1](x0) = x0 + 1,
          
          [cons2](x0, x1) = 2x1 + 4,
          
          [cons1](x0) = 3x0 + 0,
          
          [append2](x0, x1) = x0 + 1x1 + 0,
          
          [append1](x0) = x0 + 2,
          
          [qs] = 2,
          
          [not2] = 4,
          
          [not] = 1,
          
          [false] = 3,
          
          [s] = 5,
          
          [true] = 2,
          
          [0] = 2,
          
          [le] = 5,
          
          [if] = 3,
          
          [filter] = 1,
          
          [cons] = 6,
          
          [a](x0, x1) = x1 + 0,
          
          [nil] = 0,
          
          [append] = 2
         orientation:
          qs{1,#}(cons2(x,xs)) = 2xs + 4 >= xs + 0 = qs{1,#}(filter2(not1(le1(x)),xs))
          
          qs{1,#}(cons2(x,xs)) = 2xs + 4 >= xs + 0 = qs{1,#}(filter2(le1(x),xs))
          
          append2(nil(),ys) = 1ys + 0 >= ys = ys
          
          append2(cons2(x,xs),ys) = 2xs + 1ys + 4 >= 2xs + 3ys + 4 = cons2(x,append2(xs,ys))
          
          filter2(f,nil()) = 0 >= 0 = nil()
          
          filter2(f,cons2(x,xs)) = 2xs + 4 >= 2xs + 4 = if3(a(f,x),x,filter2(f,xs))
          
          le2(0(),y) = y + 6 >= 2 = true()
          
          le2(s1(x),0()) = 4x + 6 >= 3 = false()
          
          le2(s1(x),s1(y)) = 4x + y + 6 >= 4x + y + 6 = le2(x,y)
          
          if3(true(),x,xs) = 2xs + 4 >= 2xs + 4 = cons2(x,xs)
          
          if3(false(),x,xs) = 2xs + 4 >= xs = xs
          
          not2(f,b) = b + f + 0 >= 3b + 3 = not21(a(f,b))
          
          not21(true()) = 5 >= 3 = false()
          
          not21(false()) = 6 >= 2 = true()
          
          qs1(nil()) = 4 >= 0 = nil()
          
          qs1(cons2(x,xs)) = 4 >= 7 = append2(qs1(filter2(le1(x),xs)),cons2(x,qs1(filter2(not1(le1(x)),xs))))
          
          a(append1(x7),x8) = x8 + 0 >= x7 + 1x8 + 0 = append2(x7,x8)
          
          a(append(),x8) = x8 + 0 >= x8 + 2 = append1(x8)
          
          a(cons1(x7),x8) = x8 + 0 >= 2x8 + 4 = cons2(x7,x8)
          
          a(cons(),x8) = x8 + 0 >= 3x8 + 0 = cons1(x8)
          
          a(filter1(x7),x8) = x8 + 0 >= x8 = filter2(x7,x8)
          
          a(filter(),x8) = x8 + 0 >= x8 + 1 = filter1(x8)
          
          a(if2(x7,x6),x8) = x8 + 0 >= 2x8 + 4 = if3(x7,x6,x8)
          
          a(if1(x7),x8) = x8 + 0 >= 3x7 + 2x8 + 4 = if2(x7,x8)
          
          a(if(),x8) = x8 + 0 >= 4x8 + 2 = if1(x8)
          
          a(le1(x7),x8) = x8 + 0 >= 4x7 + x8 + 6 = le2(x7,x8)
          
          a(le(),x8) = x8 + 0 >= x8 + 3 = le1(x8)
          
          a(s(),x8) = x8 + 0 >= x8 + 1 = s1(x8)
          
          a(not1(x7),x8) = x8 + 0 >= x7 + x8 + 0 = not2(x7,x8)
          
          a(not(),x8) = x8 + 0 >= 4 = not1(x8)
          
          a(not2(),x8) = x8 + 0 >= 3x8 + 0 = not21(x8)
          
          a(qs(),x8) = x8 + 0 >= 4 = qs1(x8)
         problem:
          DPs:
           
          TRS:
           append2(nil(),ys) -> ys
           append2(cons2(x,xs),ys) -> cons2(x,append2(xs,ys))
           filter2(f,nil()) -> nil()
           filter2(f,cons2(x,xs)) -> if3(a(f,x),x,filter2(f,xs))
           le2(0(),y) -> true()
           le2(s1(x),0()) -> false()
           le2(s1(x),s1(y)) -> le2(x,y)
           if3(true(),x,xs) -> cons2(x,xs)
           if3(false(),x,xs) -> xs
           not2(f,b) -> not21(a(f,b))
           not21(true()) -> false()
           not21(false()) -> true()
           qs1(nil()) -> nil()
           qs1(cons2(x,xs)) ->
           append2(qs1(filter2(le1(x),xs)),cons2(x,qs1(filter2(not1(le1(x)),xs))))
           a(append1(x7),x8) -> append2(x7,x8)
           a(append(),x8) -> append1(x8)
           a(cons1(x7),x8) -> cons2(x7,x8)
           a(cons(),x8) -> cons1(x8)
           a(filter1(x7),x8) -> filter2(x7,x8)
           a(filter(),x8) -> filter1(x8)
           a(if2(x7,x6),x8) -> if3(x7,x6,x8)
           a(if1(x7),x8) -> if2(x7,x8)
           a(if(),x8) -> if1(x8)
           a(le1(x7),x8) -> le2(x7,x8)
           a(le(),x8) -> le1(x8)
           a(s(),x8) -> s1(x8)
           a(not1(x7),x8) -> not2(x7,x8)
           a(not(),x8) -> not1(x8)
           a(not2(),x8) -> not21(x8)
           a(qs(),x8) -> qs1(x8)
         Qed
     
     DPs:
      le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y)
     TRS:
      append2(nil(),ys) -> ys
      append2(cons2(x,xs),ys) -> cons2(x,append2(xs,ys))
      filter2(f,nil()) -> nil()
      filter2(f,cons2(x,xs)) -> if3(a(f,x),x,filter2(f,xs))
      le2(0(),y) -> true()
      le2(s1(x),0()) -> false()
      le2(s1(x),s1(y)) -> le2(x,y)
      if3(true(),x,xs) -> cons2(x,xs)
      if3(false(),x,xs) -> xs
      not2(f,b) -> not21(a(f,b))
      not21(true()) -> false()
      not21(false()) -> true()
      qs1(nil()) -> nil()
      qs1(cons2(x,xs)) -> append2(qs1(filter2(le1(x),xs)),cons2(x,qs1(filter2(not1(le1(x)),xs))))
      a(append1(x7),x8) -> append2(x7,x8)
      a(append(),x8) -> append1(x8)
      a(cons1(x7),x8) -> cons2(x7,x8)
      a(cons(),x8) -> cons1(x8)
      a(filter1(x7),x8) -> filter2(x7,x8)
      a(filter(),x8) -> filter1(x8)
      a(if2(x7,x6),x8) -> if3(x7,x6,x8)
      a(if1(x7),x8) -> if2(x7,x8)
      a(if(),x8) -> if1(x8)
      a(le1(x7),x8) -> le2(x7,x8)
      a(le(),x8) -> le1(x8)
      a(s(),x8) -> s1(x8)
      a(not1(x7),x8) -> not2(x7,x8)
      a(not(),x8) -> not1(x8)
      a(not2(),x8) -> not21(x8)
      a(qs(),x8) -> qs1(x8)
     Subterm Criterion Processor:
      simple projection:
       pi(le{2,#}) = 1
      problem:
       DPs:
        
       TRS:
        append2(nil(),ys) -> ys
        append2(cons2(x,xs),ys) -> cons2(x,append2(xs,ys))
        filter2(f,nil()) -> nil()
        filter2(f,cons2(x,xs)) -> if3(a(f,x),x,filter2(f,xs))
        le2(0(),y) -> true()
        le2(s1(x),0()) -> false()
        le2(s1(x),s1(y)) -> le2(x,y)
        if3(true(),x,xs) -> cons2(x,xs)
        if3(false(),x,xs) -> xs
        not2(f,b) -> not21(a(f,b))
        not21(true()) -> false()
        not21(false()) -> true()
        qs1(nil()) -> nil()
        qs1(cons2(x,xs)) -> append2(qs1(filter2(le1(x),xs)),cons2(x,qs1(filter2(not1(le1(x)),xs))))
        a(append1(x7),x8) -> append2(x7,x8)
        a(append(),x8) -> append1(x8)
        a(cons1(x7),x8) -> cons2(x7,x8)
        a(cons(),x8) -> cons1(x8)
        a(filter1(x7),x8) -> filter2(x7,x8)
        a(filter(),x8) -> filter1(x8)
        a(if2(x7,x6),x8) -> if3(x7,x6,x8)
        a(if1(x7),x8) -> if2(x7,x8)
        a(if(),x8) -> if1(x8)
        a(le1(x7),x8) -> le2(x7,x8)
        a(le(),x8) -> le1(x8)
        a(s(),x8) -> s1(x8)
        a(not1(x7),x8) -> not2(x7,x8)
        a(not(),x8) -> not1(x8)
        a(not2(),x8) -> not21(x8)
        a(qs(),x8) -> qs1(x8)
      Qed
     
     DPs:
      append{2,#}(cons2(x,xs),ys) -> append{2,#}(xs,ys)
     TRS:
      append2(nil(),ys) -> ys
      append2(cons2(x,xs),ys) -> cons2(x,append2(xs,ys))
      filter2(f,nil()) -> nil()
      filter2(f,cons2(x,xs)) -> if3(a(f,x),x,filter2(f,xs))
      le2(0(),y) -> true()
      le2(s1(x),0()) -> false()
      le2(s1(x),s1(y)) -> le2(x,y)
      if3(true(),x,xs) -> cons2(x,xs)
      if3(false(),x,xs) -> xs
      not2(f,b) -> not21(a(f,b))
      not21(true()) -> false()
      not21(false()) -> true()
      qs1(nil()) -> nil()
      qs1(cons2(x,xs)) -> append2(qs1(filter2(le1(x),xs)),cons2(x,qs1(filter2(not1(le1(x)),xs))))
      a(append1(x7),x8) -> append2(x7,x8)
      a(append(),x8) -> append1(x8)
      a(cons1(x7),x8) -> cons2(x7,x8)
      a(cons(),x8) -> cons1(x8)
      a(filter1(x7),x8) -> filter2(x7,x8)
      a(filter(),x8) -> filter1(x8)
      a(if2(x7,x6),x8) -> if3(x7,x6,x8)
      a(if1(x7),x8) -> if2(x7,x8)
      a(if(),x8) -> if1(x8)
      a(le1(x7),x8) -> le2(x7,x8)
      a(le(),x8) -> le1(x8)
      a(s(),x8) -> s1(x8)
      a(not1(x7),x8) -> not2(x7,x8)
      a(not(),x8) -> not1(x8)
      a(not2(),x8) -> not21(x8)
      a(qs(),x8) -> qs1(x8)
     Subterm Criterion Processor:
      simple projection:
       pi(append{2,#}) = 0
      problem:
       DPs:
        
       TRS:
        append2(nil(),ys) -> ys
        append2(cons2(x,xs),ys) -> cons2(x,append2(xs,ys))
        filter2(f,nil()) -> nil()
        filter2(f,cons2(x,xs)) -> if3(a(f,x),x,filter2(f,xs))
        le2(0(),y) -> true()
        le2(s1(x),0()) -> false()
        le2(s1(x),s1(y)) -> le2(x,y)
        if3(true(),x,xs) -> cons2(x,xs)
        if3(false(),x,xs) -> xs
        not2(f,b) -> not21(a(f,b))
        not21(true()) -> false()
        not21(false()) -> true()
        qs1(nil()) -> nil()
        qs1(cons2(x,xs)) -> append2(qs1(filter2(le1(x),xs)),cons2(x,qs1(filter2(not1(le1(x)),xs))))
        a(append1(x7),x8) -> append2(x7,x8)
        a(append(),x8) -> append1(x8)
        a(cons1(x7),x8) -> cons2(x7,x8)
        a(cons(),x8) -> cons1(x8)
        a(filter1(x7),x8) -> filter2(x7,x8)
        a(filter(),x8) -> filter1(x8)
        a(if2(x7,x6),x8) -> if3(x7,x6,x8)
        a(if1(x7),x8) -> if2(x7,x8)
        a(if(),x8) -> if1(x8)
        a(le1(x7),x8) -> le2(x7,x8)
        a(le(),x8) -> le1(x8)
        a(s(),x8) -> s1(x8)
        a(not1(x7),x8) -> not2(x7,x8)
        a(not(),x8) -> not1(x8)
        a(not2(),x8) -> not21(x8)
        a(qs(),x8) -> qs1(x8)
      Qed