MAYBE Proof: ConCon could not decide if this system is quasi-decreasing. \cite{A14}, Theorem 11.5.9 does not apply. System R transformed to V(R) + Emb. Call external tool: ttt2 - trs 30 Input: le(0, x) -> true le(s(x), 0) -> false le(s(x), s(y)) -> le(x, y) app(nil, x) -> x app(cons(x, xs), ys) -> cons(x, app(xs, ys)) split(x, nil) -> pair(nil, nil) qsort(nil) -> nil split(x, cons(y, ys)) -> pair(split(x, ys), cons(y, split(x, ys))) split(x, cons(y, ys)) -> le(x, y) split(x, cons(y, ys)) -> split(x, ys) split(x, cons(y, ys)) -> pair(cons(y, split(x, ys)), split(x, ys)) qsort(cons(x, xs)) -> app(qsort(split(x, xs)), cons(x, qsort(split(x, xs)))) qsort(cons(x, xs)) -> split(x, xs) pair(x, y) -> x pair(x, y) -> y app(x, y) -> x app(x, y) -> y s(x) -> x split(x, y) -> x split(x, y) -> y le(x, y) -> x le(x, y) -> y qsort(x) -> x cons(x, y) -> x cons(x, y) -> y The external tool could not decide termination.