0.00/0.82	YES
0.00/0.83	
0.00/0.83	Problem:
0.00/0.83	le(0(), x) -> true()
0.00/0.83	le(s(x), 0()) -> false()
0.00/0.83	le(s(x), s(y)) -> le(x, y)
0.00/0.83	app(nil(), x) -> x
0.00/0.83	app(cons(x, xs), ys) -> cons(x, app(xs, ys))
0.00/0.83	split(x, nil()) -> pair(nil(), nil())
0.00/0.83	qsort(nil()) -> nil()
0.00/0.83	split(x, cons(y, ys)) -> pair(xs, cons(y, zs)) <= split(x, ys) = pair(xs, zs), le(x, y) = true()
0.00/0.83	split(x, cons(y, ys)) -> pair(cons(y, xs), zs) <= split(x, ys) = pair(xs, zs), le(x, y) = false()
0.00/0.83	qsort(cons(x, xs)) -> app(qsort(ys), cons(x, qsort(zs))) <= split(x, xs) = pair(ys, zs)
0.00/0.83	
0.00/0.83	Proof:
0.00/0.83	This system is confluent.
0.00/0.83	By \cite{GNG13}, Theorem 9.
0.00/0.83	This system is of type 3 or smaller.
0.00/0.83	This system is deterministic.
0.00/0.83	This system is weakly left-linear.
0.00/0.83	System R transformed to optimized U(R).
0.00/0.83	This system is orthogonal.
0.00/0.83	
2.29/1.15	EOF