(GOAL COMPLEXITY)
(STARTTERM CONSTRUCTORBASED)
(VAR n x xs y )
(STRATEGY INNERMOST)
(RULES 
        qsort(xs) -> qs(half(length(xs)), xs)
        qs(n, nil) -> nil
        qs(n, cons(x, xs)) -> append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
        filterlow(n, nil) -> nil
        filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
        if1(true, n, x, xs) -> filterlow(n, xs)
        if1(false, n, x, xs) -> cons(x, filterlow(n, xs))
        filterhigh(n, nil) -> nil
        filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
        if2(true, n, x, xs) -> filterhigh(n, xs)
        if2(false, n, x, xs) -> cons(x, filterhigh(n, xs))
        ge(x, 0) -> true
        ge(0, s(x)) -> false
        ge(s(x), s(y)) -> ge(x, y)
        append(nil, ys) -> ys
        append(cons(x, xs), ys) -> cons(x, append(xs, ys))
        length(nil) -> 0
        length(cons(x, xs)) -> s(length(xs))
        half(0) -> 0
        half(s(0)) -> 0
        half(s(s(x))) -> s(half(x))
        get(n, nil) -> 0
        get(n, cons(x, nil)) -> x
        get(0, cons(x, cons(y, xs))) -> x
        get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
        
)