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)))}
 DP:
  Strict:
   {          lt#(s(X), s(Y)) -> lt#(X, Y),
        append#(add(N, X), Y) -> append#(X, Y),
         split#(N, add(M, Y)) -> split#(N, Y),
         split#(N, add(M, Y)) -> f_1#(split(N, Y), N, M, Y),
    f_1#(pair(X, Z), N, M, Y) -> lt#(N, M),
    f_1#(pair(X, Z), N, M, Y) -> f_2#(lt(N, M), N, M, Y, X, Z),
            qsort#(add(N, X)) -> split#(N, X),
            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))),
       f_3#(pair(Y, Z), N, X) -> qsort#(Y),
       f_3#(pair(Y, Z), N, X) -> qsort#(Z)}
  Weak:
  {              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)))}
  EDG:
   {(qsort#(add(N, X)) -> f_3#(split(N, X), N, X), f_3#(pair(Y, Z), N, X) -> qsort#(Z))
    (qsort#(add(N, X)) -> f_3#(split(N, X), N, X), f_3#(pair(Y, Z), N, X) -> qsort#(Y))
    (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))))
    (f_3#(pair(Y, Z), N, X) -> qsort#(Z), qsort#(add(N, X)) -> f_3#(split(N, X), N, X))
    (f_3#(pair(Y, Z), N, X) -> qsort#(Z), qsort#(add(N, X)) -> split#(N, X))
    (append#(add(N, X), Y) -> append#(X, Y), append#(add(N, X), Y) -> append#(X, Y))
    (f_1#(pair(X, Z), N, M, Y) -> lt#(N, M), lt#(s(X), s(Y)) -> lt#(X, Y))
    (split#(N, add(M, Y)) -> f_1#(split(N, Y), N, M, Y), f_1#(pair(X, Z), N, M, Y) -> lt#(N, M))
    (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))
    (split#(N, add(M, Y)) -> split#(N, Y), split#(N, add(M, Y)) -> split#(N, Y))
    (split#(N, add(M, Y)) -> split#(N, Y), split#(N, add(M, Y)) -> f_1#(split(N, Y), N, M, Y))
    (lt#(s(X), s(Y)) -> lt#(X, Y), lt#(s(X), s(Y)) -> lt#(X, Y))
    (f_3#(pair(Y, Z), N, X) -> append#(qsort(Y), add(X, qsort(Z))), append#(add(N, X), Y) -> append#(X, Y))
    (f_3#(pair(Y, Z), N, X) -> qsort#(Y), qsort#(add(N, X)) -> split#(N, X))
    (f_3#(pair(Y, Z), N, X) -> qsort#(Y), qsort#(add(N, X)) -> f_3#(split(N, X), N, X))
    (qsort#(add(N, X)) -> split#(N, X), split#(N, add(M, Y)) -> split#(N, Y))
    (qsort#(add(N, X)) -> split#(N, X), split#(N, add(M, Y)) -> f_1#(split(N, Y), N, M, Y))}
   SCCS:
    Scc:
     {     qsort#(add(N, X)) -> f_3#(split(N, X), N, X),
      f_3#(pair(Y, Z), N, X) -> qsort#(Y),
      f_3#(pair(Y, Z), N, X) -> qsort#(Z)}
    Scc:
     {split#(N, add(M, Y)) -> split#(N, Y)}
    Scc:
     {append#(add(N, X), Y) -> append#(X, Y)}
    Scc:
     {lt#(s(X), s(Y)) -> lt#(X, Y)}
    SCC:
     Strict:
      {     qsort#(add(N, X)) -> f_3#(split(N, X), N, X),
       f_3#(pair(Y, Z), N, X) -> qsort#(Y),
       f_3#(pair(Y, Z), N, X) -> qsort#(Z)}
     Weak:
     {              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)))}
     POLY:
      Argument Filtering:
       pi(f_3#) = 0, pi(f_3) = [], pi(qsort#) = 0, pi(qsort) = [], pi(f_2) = [0,4,5], pi(f_1) = [0], pi(split) = 1, pi(pair) = [0,1], pi(add) = [1], pi(nil) = [], pi(append) = [], pi(false) = [], pi(s) = [], pi(0) = [], pi(lt) = [], pi(true) = []
      Usable Rules:
       {}
      Interpretation:
       [pair](x0, x1) = x0 + x1,
       [add](x0) = x0 + 1
      Strict:
       {f_3#(pair(Y, Z), N, X) -> qsort#(Y),
        f_3#(pair(Y, Z), N, X) -> qsort#(Z)}
      Weak:
       {              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)))}
      EDG:
       {}
       SCCS:
        
        Qed
    SCC:
     Strict:
      {split#(N, add(M, Y)) -> split#(N, Y)}
     Weak:
     {              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)))}
     SPSC:
      Simple Projection:
       pi(split#) = 1
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {append#(add(N, X), Y) -> append#(X, Y)}
     Weak:
     {              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)))}
     SPSC:
      Simple Projection:
       pi(append#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {lt#(s(X), s(Y)) -> lt#(X, Y)}
     Weak:
     {              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)))}
     SPSC:
      Simple Projection:
       pi(lt#) = 0
      Strict:
       {}
      Qed