MAYBE

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:
 DP Processor:
  DPs:
   a#(a(append(),a(a(cons(),x),xs)),ys) -> a#(append(),xs)
   a#(a(append(),a(a(cons(),x),xs)),ys) -> a#(a(append(),xs),ys)
   a#(a(append(),a(a(cons(),x),xs)),ys) -> a#(a(cons(),x),a(a(append(),xs),ys))
   a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(a(filter(),f),xs)
   a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x)
   a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(if(),a(f,x))
   a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(a(if(),a(f,x)),x)
   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(),a(s(),x)),a(s(),y)) -> a#(le(),x)
   a#(a(le(),a(s(),x)),a(s(),y)) -> a#(a(le(),x),y)
   a#(a(a(if(),true()),x),xs) -> a#(cons(),x)
   a#(a(a(if(),true()),x),xs) -> a#(a(cons(),x),xs)
   a#(a(not(),f),b) -> a#(f,b)
   a#(a(not(),f),b) -> a#(not2(),a(f,b))
   a#(qs(),a(a(cons(),x),xs)) -> a#(not(),a(le(),x))
   a#(qs(),a(a(cons(),x),xs)) -> a#(filter(),a(not(),a(le(),x)))
   a#(qs(),a(a(cons(),x),xs)) -> a#(a(filter(),a(not(),a(le(),x))),xs)
   a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(not(),a(le(),x))),xs))
   a#(qs(),a(a(cons(),x),xs)) -> a#(a(cons(),x),a(qs(),a(a(filter(),a(not(),a(le(),x))),xs)))
   a#(qs(),a(a(cons(),x),xs)) -> a#(le(),x)
   a#(qs(),a(a(cons(),x),xs)) -> a#(filter(),a(le(),x))
   a#(qs(),a(a(cons(),x),xs)) -> a#(a(filter(),a(le(),x)),xs)
   a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(le(),x)),xs))
   a#(qs(),a(a(cons(),x),xs)) -> a#(append(),a(qs(),a(a(filter(),a(le(),x)),xs)))
   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))))
  TRS:
   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))))
  EDG Processor:
   DPs:
    a#(a(append(),a(a(cons(),x),xs)),ys) -> a#(append(),xs)
    a#(a(append(),a(a(cons(),x),xs)),ys) -> a#(a(append(),xs),ys)
    a#(a(append(),a(a(cons(),x),xs)),ys) -> a#(a(cons(),x),a(a(append(),xs),ys))
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(a(filter(),f),xs)
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x)
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(if(),a(f,x))
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(a(if(),a(f,x)),x)
    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(),a(s(),x)),a(s(),y)) -> a#(le(),x)
    a#(a(le(),a(s(),x)),a(s(),y)) -> a#(a(le(),x),y)
    a#(a(a(if(),true()),x),xs) -> a#(cons(),x)
    a#(a(a(if(),true()),x),xs) -> a#(a(cons(),x),xs)
    a#(a(not(),f),b) -> a#(f,b)
    a#(a(not(),f),b) -> a#(not2(),a(f,b))
    a#(qs(),a(a(cons(),x),xs)) -> a#(not(),a(le(),x))
    a#(qs(),a(a(cons(),x),xs)) -> a#(filter(),a(not(),a(le(),x)))
    a#(qs(),a(a(cons(),x),xs)) -> a#(a(filter(),a(not(),a(le(),x))),xs)
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(not(),a(le(),x))),xs))
    a#(qs(),a(a(cons(),x),xs)) -> a#(a(cons(),x),a(qs(),a(a(filter(),a(not(),a(le(),x))),xs)))
    a#(qs(),a(a(cons(),x),xs)) -> a#(le(),x)
    a#(qs(),a(a(cons(),x),xs)) -> a#(filter(),a(le(),x))
    a#(qs(),a(a(cons(),x),xs)) -> a#(a(filter(),a(le(),x)),xs)
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(le(),x)),xs))
    a#(qs(),a(a(cons(),x),xs)) -> a#(append(),a(qs(),a(a(filter(),a(le(),x)),xs)))
    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))))
   TRS:
    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))))
   graph:
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(not(),a(le(),x))),xs)) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(not(),a(le(),x))
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(not(),a(le(),x))),xs)) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(filter(),a(not(),a(le(),x)))
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(not(),a(le(),x))),xs)) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(a(filter(),a(not(),a(le(),x))),xs)
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(not(),a(le(),x))),xs)) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(not(),a(le(),x))),xs))
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(not(),a(le(),x))),xs)) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(a(cons(),x),a(qs(),a(a(filter(),a(not(),a(le(),x))),xs)))
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(not(),a(le(),x))),xs)) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(le(),x)
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(not(),a(le(),x))),xs)) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(filter(),a(le(),x))
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(not(),a(le(),x))),xs)) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(a(filter(),a(le(),x)),xs)
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(not(),a(le(),x))),xs)) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(le(),x)),xs))
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(not(),a(le(),x))),xs)) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(append(),a(qs(),a(a(filter(),a(le(),x)),xs)))
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(not(),a(le(),x))),xs)) ->
    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))))
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(le(),x)),xs)) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(not(),a(le(),x))
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(le(),x)),xs)) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(filter(),a(not(),a(le(),x)))
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(le(),x)),xs)) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(a(filter(),a(not(),a(le(),x))),xs)
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(le(),x)),xs)) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(not(),a(le(),x))),xs))
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(le(),x)),xs)) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(a(cons(),x),a(qs(),a(a(filter(),a(not(),a(le(),x))),xs)))
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(le(),x)),xs)) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(le(),x)
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(le(),x)),xs)) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(filter(),a(le(),x))
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(le(),x)),xs)) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(a(filter(),a(le(),x)),xs)
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(le(),x)),xs)) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(le(),x)),xs))
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(le(),x)),xs)) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(append(),a(qs(),a(a(filter(),a(le(),x)),xs)))
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(le(),x)),xs)) ->
    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))))
    a#(qs(),a(a(cons(),x),xs)) -> a#(a(filter(),a(not(),a(le(),x))),xs) ->
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(a(filter(),f),xs)
    a#(qs(),a(a(cons(),x),xs)) -> a#(a(filter(),a(not(),a(le(),x))),xs) ->
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x)
    a#(qs(),a(a(cons(),x),xs)) -> a#(a(filter(),a(not(),a(le(),x))),xs) ->
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(if(),a(f,x))
    a#(qs(),a(a(cons(),x),xs)) -> a#(a(filter(),a(not(),a(le(),x))),xs) ->
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(a(if(),a(f,x)),x)
    a#(qs(),a(a(cons(),x),xs)) -> a#(a(filter(),a(not(),a(le(),x))),xs) ->
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(a(a(if(),a(f,x)),x),a(a(filter(),f),xs))
    a#(qs(),a(a(cons(),x),xs)) -> a#(a(filter(),a(le(),x)),xs) ->
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(a(filter(),f),xs)
    a#(qs(),a(a(cons(),x),xs)) -> a#(a(filter(),a(le(),x)),xs) ->
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x)
    a#(qs(),a(a(cons(),x),xs)) -> a#(a(filter(),a(le(),x)),xs) ->
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(if(),a(f,x))
    a#(qs(),a(a(cons(),x),xs)) -> a#(a(filter(),a(le(),x)),xs) ->
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(a(if(),a(f,x)),x)
    a#(qs(),a(a(cons(),x),xs)) -> a#(a(filter(),a(le(),x)),xs) ->
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(a(a(if(),a(f,x)),x),a(a(filter(),f),xs))
    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))))
    ->
    a#(a(append(),a(a(cons(),x),xs)),ys) -> a#(append(),xs)
    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))))
    ->
    a#(a(append(),a(a(cons(),x),xs)),ys) -> a#(a(append(),xs),ys)
    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))))
    ->
    a#(a(append(),a(a(cons(),x),xs)),ys) -> a#(a(cons(),x),a(a(append(),xs),ys))
    a#(a(not(),f),b) -> a#(f,b) ->
    a#(a(append(),a(a(cons(),x),xs)),ys) -> a#(append(),xs)
    a#(a(not(),f),b) -> a#(f,b) ->
    a#(a(append(),a(a(cons(),x),xs)),ys) -> a#(a(append(),xs),ys)
    a#(a(not(),f),b) -> a#(f,b) ->
    a#(a(append(),a(a(cons(),x),xs)),ys) -> a#(a(cons(),x),a(a(append(),xs),ys))
    a#(a(not(),f),b) -> a#(f,b) ->
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(a(filter(),f),xs)
    a#(a(not(),f),b) -> a#(f,b) ->
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x)
    a#(a(not(),f),b) -> a#(f,b) ->
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(if(),a(f,x))
    a#(a(not(),f),b) -> a#(f,b) ->
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(a(if(),a(f,x)),x)
    a#(a(not(),f),b) -> a#(f,b) ->
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(a(a(if(),a(f,x)),x),a(a(filter(),f),xs))
    a#(a(not(),f),b) -> a#(f,b) ->
    a#(a(le(),a(s(),x)),a(s(),y)) -> a#(le(),x)
    a#(a(not(),f),b) -> a#(f,b) ->
    a#(a(le(),a(s(),x)),a(s(),y)) -> a#(a(le(),x),y)
    a#(a(not(),f),b) -> a#(f,b) ->
    a#(a(a(if(),true()),x),xs) -> a#(cons(),x)
    a#(a(not(),f),b) -> a#(f,b) ->
    a#(a(a(if(),true()),x),xs) -> a#(a(cons(),x),xs)
    a#(a(not(),f),b) -> a#(f,b) -> a#(a(not(),f),b) -> a#(f,b)
    a#(a(not(),f),b) -> a#(f,b) -> a#(a(not(),f),b) -> a#(not2(),a(f,b))
    a#(a(not(),f),b) -> a#(f,b) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(not(),a(le(),x))
    a#(a(not(),f),b) -> a#(f,b) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(filter(),a(not(),a(le(),x)))
    a#(a(not(),f),b) -> a#(f,b) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(a(filter(),a(not(),a(le(),x))),xs)
    a#(a(not(),f),b) -> a#(f,b) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(not(),a(le(),x))),xs))
    a#(a(not(),f),b) -> a#(f,b) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(a(cons(),x),a(qs(),a(a(filter(),a(not(),a(le(),x))),xs)))
    a#(a(not(),f),b) -> a#(f,b) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(le(),x)
    a#(a(not(),f),b) -> a#(f,b) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(filter(),a(le(),x))
    a#(a(not(),f),b) -> a#(f,b) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(a(filter(),a(le(),x)),xs)
    a#(a(not(),f),b) -> a#(f,b) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(le(),x)),xs))
    a#(a(not(),f),b) -> a#(f,b) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(append(),a(qs(),a(a(filter(),a(le(),x)),xs)))
    a#(a(not(),f),b) -> a#(f,b) ->
    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))))
    a#(a(le(),a(s(),x)),a(s(),y)) -> a#(a(le(),x),y) ->
    a#(a(le(),a(s(),x)),a(s(),y)) -> a#(le(),x)
    a#(a(le(),a(s(),x)),a(s(),y)) -> a#(a(le(),x),y) ->
    a#(a(le(),a(s(),x)),a(s(),y)) -> a#(a(le(),x),y)
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(a(filter(),f),xs) ->
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(a(filter(),f),xs)
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(a(filter(),f),xs) ->
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x)
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(a(filter(),f),xs) ->
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(if(),a(f,x))
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(a(filter(),f),xs) ->
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(a(if(),a(f,x)),x)
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(a(filter(),f),xs) ->
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(a(a(if(),a(f,x)),x),a(a(filter(),f),xs))
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(a(a(if(),a(f,x)),x),a(a(filter(),f),xs)) ->
    a#(a(a(if(),true()),x),xs) -> a#(cons(),x)
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(a(a(if(),a(f,x)),x),a(a(filter(),f),xs)) ->
    a#(a(a(if(),true()),x),xs) -> a#(a(cons(),x),xs)
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x) ->
    a#(a(append(),a(a(cons(),x),xs)),ys) -> a#(append(),xs)
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x) ->
    a#(a(append(),a(a(cons(),x),xs)),ys) -> a#(a(append(),xs),ys)
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x) ->
    a#(a(append(),a(a(cons(),x),xs)),ys) -> a#(a(cons(),x),a(a(append(),xs),ys))
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x) ->
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(a(filter(),f),xs)
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x) ->
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x)
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x) ->
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(if(),a(f,x))
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x) ->
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(a(if(),a(f,x)),x)
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x) ->
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(a(a(if(),a(f,x)),x),a(a(filter(),f),xs))
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x) ->
    a#(a(le(),a(s(),x)),a(s(),y)) -> a#(le(),x)
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x) ->
    a#(a(le(),a(s(),x)),a(s(),y)) -> a#(a(le(),x),y)
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x) ->
    a#(a(a(if(),true()),x),xs) -> a#(cons(),x)
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x) ->
    a#(a(a(if(),true()),x),xs) -> a#(a(cons(),x),xs)
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x) ->
    a#(a(not(),f),b) -> a#(f,b)
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x) ->
    a#(a(not(),f),b) -> a#(not2(),a(f,b))
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(not(),a(le(),x))
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(filter(),a(not(),a(le(),x)))
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(a(filter(),a(not(),a(le(),x))),xs)
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(not(),a(le(),x))),xs))
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(a(cons(),x),a(qs(),a(a(filter(),a(not(),a(le(),x))),xs)))
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(le(),x)
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(filter(),a(le(),x))
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(a(filter(),a(le(),x)),xs)
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(le(),x)),xs))
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x) ->
    a#(qs(),a(a(cons(),x),xs)) -> a#(append(),a(qs(),a(a(filter(),a(le(),x)),xs)))
    a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x) ->
    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))))
    a#(a(append(),a(a(cons(),x),xs)),ys) -> a#(a(append(),xs),ys) ->
    a#(a(append(),a(a(cons(),x),xs)),ys) -> a#(append(),xs)
    a#(a(append(),a(a(cons(),x),xs)),ys) -> a#(a(append(),xs),ys) ->
    a#(a(append(),a(a(cons(),x),xs)),ys) -> a#(a(append(),xs),ys)
    a#(a(append(),a(a(cons(),x),xs)),ys) -> a#(a(append(),xs),ys) ->
    a#(a(append(),a(a(cons(),x),xs)),ys) -> a#(a(cons(),x),a(a(append(),xs),ys))
   SCC Processor:
    #sccs: 3
    #rules: 9
    #arcs: 97/625
    DPs:
     a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(not(),a(le(),x))),xs))
     a#(qs(),a(a(cons(),x),xs)) -> a#(qs(),a(a(filter(),a(le(),x)),xs))
     a#(qs(),a(a(cons(),x),xs)) -> a#(a(filter(),a(le(),x)),xs)
     a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(f,x)
     a#(qs(),a(a(cons(),x),xs)) -> a#(a(filter(),a(not(),a(le(),x))),xs)
     a#(a(filter(),f),a(a(cons(),x),xs)) -> a#(a(filter(),f),xs)
     a#(a(not(),f),b) -> a#(f,b)
    TRS:
     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))))
    Open
    
    DPs:
     a#(a(le(),a(s(),x)),a(s(),y)) -> a#(a(le(),x),y)
    TRS:
     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))))
    Open
    
    DPs:
     a#(a(append(),a(a(cons(),x),xs)),ys) -> a#(a(append(),xs),ys)
    TRS:
     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))))
    Open