YES

TRS:

  lt(0(),s(X)) -> true()
  lt(s(X),0()) -> false()
  lt(s(X),s(Y)) -> lt(X,Y)
  append(nil(),Y) -> Y
  append(add(N,X),Y) -> add(N,append(X,Y))
  split(N,nil()) -> pair(nil(),nil())
  split(N,add(M,Y)) -> f_1(split(N,Y),N,M,Y)
  f_1(pair(X,Z),N,M,Y) -> f_2(lt(N,M),N,M,Y,X,Z)
  f_2(true(),N,M,Y,X,Z) -> pair(X,add(M,Z))
  f_2(false(),N,M,Y,X,Z) -> pair(add(M,X),Z)
  qsort(nil()) -> nil()
  qsort(add(N,X)) -> f_3(split(N,X),N,X)
  f_3(pair(Y,Z),N,X) -> append(qsort(Y),add(X,qsort(Z)))

linear polynomial interpretations on N:

  lt_A(x1,x2) = x1 + 1
  lt#_A(x1,x2) = 3
  0_A = 1
  0#_A = 1
  s_A(x1) = x1 + 1
  s#_A(x1) = 3
  true_A = 1
  true#_A = 0
  false_A = 1
  false#_A = 2
  append_A(x1,x2) = x1 + x2
  append#_A(x1,x2) = 5
  nil_A = 0
  nil#_A = 0
  add_A(x1,x2) = x2 + 6
  add#_A(x1,x2) = 4
  split_A(x1,x2) = x2 + 1
  split#_A(x1,x2) = x2 + 3
  pair_A(x1,x2) = x1 + x2 + 1
  pair#_A(x1,x2) = 2
  f_1_A(x1,x2,x3,x4) = x1 + 6
  f_1#_A(x1,x2,x3,x4) = x1 + 5
  f_2_A(x1,x2,x3,x4,x5,x6) = x5 + x6 + 7
  f_2#_A(x1,x2,x3,x4,x5,x6) = x6 + 5
  qsort_A(x1) = x1
  qsort#_A(x1) = x1 + 1
  f_3_A(x1,x2,x3) = x1 + 5
  f_3#_A(x1,x2,x3) = x1 + 5

precedence:

  f_1 > f_2 > pair = f_3 > lt = s = add = qsort > false = append = split > 0 = nil > true