MAYBE
Time: 0.038002
TRS:
 {           a(a(a(if(), true()), x), xs) -> a(a(cons(), x), xs),
            a(a(a(if(), false()), x), xs) -> xs,
  a(a(append(), a(a(cons(), x), xs)), ys) -> a(a(cons(), x), a(a(append(), xs), ys)),
                a(a(append(), nil()), ys) -> ys,
   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), nil()) -> nil(),
         a(a(le(), a(s(), x)), a(s(), y)) -> a(a(le(), x), y),
               a(a(le(), a(s(), x)), 0()) -> false(),
                       a(a(le(), 0()), y) -> true(),
                        a(a(not(), f), b) -> a(not2(), a(f, b)),
                        a(not2(), true()) -> false(),
                       a(not2(), false()) -> true(),
             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(), nil()) -> nil()}
 DP:
  DP:
   {           a#(a(a(if(), true()), x), xs) -> a#(a(cons(), x), xs),
               a#(a(a(if(), true()), x), xs) -> a#(cons(), x),
    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(append(), a(a(cons(), x), xs)), ys) -> a#(append(), xs),
     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#(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#(if(), a(f, 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#(le(), x),
                          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#(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(cons(), x), 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#(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#(filter(), 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#(le(), x),
               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#(qs(), a(a(filter(), a(not(), a(le(), x))), xs))}
  TRS:
  {           a(a(a(if(), true()), x), xs) -> a(a(cons(), x), xs),
             a(a(a(if(), false()), x), xs) -> xs,
   a(a(append(), a(a(cons(), x), xs)), ys) -> a(a(cons(), x), a(a(append(), xs), ys)),
                 a(a(append(), nil()), ys) -> ys,
    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), nil()) -> nil(),
          a(a(le(), a(s(), x)), a(s(), y)) -> a(a(le(), x), y),
                a(a(le(), a(s(), x)), 0()) -> false(),
                        a(a(le(), 0()), y) -> true(),
                         a(a(not(), f), b) -> a(not2(), a(f, b)),
                         a(not2(), true()) -> false(),
                        a(not2(), false()) -> true(),
              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(), nil()) -> nil()}
  EDG:
   {
    (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(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(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#(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#(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(cons(), x), 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(append(), xs), ys))
    (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#(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#(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#(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#(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#(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#(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(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(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(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#(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#(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#(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#(not(), a(le(), x)))
    (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(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(le(), x)))
    (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(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(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#(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(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#(a(not(), f), b) -> a#(f, b))
    (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(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(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(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(filter(), f), a(a(cons(), x), xs)) -> a#(f, x))
    (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(cons(), x), 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(append(), xs), ys))
    (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(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(a(if(), true()), x), xs) -> a#(cons(), x))
    (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(append(), a(a(cons(), x), xs)), ys) -> a#(append(), 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#(a(a(if(), a(f, x)), x), a(a(filter(), f), xs)))
    (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#(a(if(), a(f, x)), 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(le(), a(s(), x)), a(s(), y)) -> a#(a(le(), x), y))
    (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(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#(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(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#(a(filter(), a(le(), x)), xs))
    (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#(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#(filter(), 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#(le(), x))
    (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#(qs(), 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(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#(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)))
    (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#(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#(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#(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(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#(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#(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#(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#(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#(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#(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(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#(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(a(if(), a(f, x)), x), 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#(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#(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#(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#(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(a(if(), a(f, x)), x), 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#(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#(if(), a(f, x)))
   }
   STATUS:
    arrows: 0.844800
    SCCS (3):
     Scc:
      {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(not(), f), b) -> a#(f, b),
                 a#(qs(), a(a(cons(), x), xs)) -> 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))}
     Scc:
      {a#(a(le(), a(s(), x)), a(s(), y)) -> a#(a(le(), x), y)}
     Scc:
      {a#(a(append(), a(a(cons(), x), xs)), ys) -> a#(a(append(), xs), ys)}
     
     SCC (7):
      Strict:
       {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(not(), f), b) -> a#(f, b),
                  a#(qs(), a(a(cons(), x), xs)) -> 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))}
      Weak:
      {           a(a(a(if(), true()), x), xs) -> a(a(cons(), x), xs),
                 a(a(a(if(), false()), x), xs) -> xs,
       a(a(append(), a(a(cons(), x), xs)), ys) -> a(a(cons(), x), a(a(append(), xs), ys)),
                     a(a(append(), nil()), ys) -> ys,
        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), nil()) -> nil(),
              a(a(le(), a(s(), x)), a(s(), y)) -> a(a(le(), x), y),
                    a(a(le(), a(s(), x)), 0()) -> false(),
                            a(a(le(), 0()), y) -> true(),
                             a(a(not(), f), b) -> a(not2(), a(f, b)),
                             a(not2(), true()) -> false(),
                            a(not2(), false()) -> true(),
                  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(), nil()) -> nil()}
      Open
     
     
     
     
     
     
     
     
     SCC (1):
      Strict:
       {a#(a(le(), a(s(), x)), a(s(), y)) -> a#(a(le(), x), y)}
      Weak:
      {           a(a(a(if(), true()), x), xs) -> a(a(cons(), x), xs),
                 a(a(a(if(), false()), x), xs) -> xs,
       a(a(append(), a(a(cons(), x), xs)), ys) -> a(a(cons(), x), a(a(append(), xs), ys)),
                     a(a(append(), nil()), ys) -> ys,
        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), nil()) -> nil(),
              a(a(le(), a(s(), x)), a(s(), y)) -> a(a(le(), x), y),
                    a(a(le(), a(s(), x)), 0()) -> false(),
                            a(a(le(), 0()), y) -> true(),
                             a(a(not(), f), b) -> a(not2(), a(f, b)),
                             a(not2(), true()) -> false(),
                            a(not2(), false()) -> true(),
                  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(), nil()) -> nil()}
      Open
     
     
     
     
     SCC (1):
      Strict:
       {a#(a(append(), a(a(cons(), x), xs)), ys) -> a#(a(append(), xs), ys)}
      Weak:
      {           a(a(a(if(), true()), x), xs) -> a(a(cons(), x), xs),
                 a(a(a(if(), false()), x), xs) -> xs,
       a(a(append(), a(a(cons(), x), xs)), ys) -> a(a(cons(), x), a(a(append(), xs), ys)),
                     a(a(append(), nil()), ys) -> ys,
        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), nil()) -> nil(),
              a(a(le(), a(s(), x)), a(s(), y)) -> a(a(le(), x), y),
                    a(a(le(), a(s(), x)), 0()) -> false(),
                            a(a(le(), 0()), y) -> true(),
                             a(a(not(), f), b) -> a(not2(), a(f, b)),
                             a(not2(), true()) -> false(),
                            a(not2(), false()) -> true(),
                  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(), nil()) -> nil()}
      Open