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.