MAYBE 'Pop* (timeout of 60.0 seconds)' -------------------------------- Answer: MAYBE Input Problem: innermost runtime-complexity with respect to 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))} Proof Output: The input cannot be shown compatible