YES
Time: 0.016287
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:
  DP:
   {            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}
  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))}
  EDG:
   {(lt#(s X, s Y) -> lt#(X, Y), lt#(s X, s Y) -> lt#(X, Y))
    (split#(N, add(M, Y)) -> split#(N, Y), split#(N, add(M, Y)) -> f_1#(split(N, Y), N, M, Y))
    (split#(N, add(M, Y)) -> split#(N, Y), split#(N, add(M, Y)) -> split#(N, Y))
    (f_1#(pair(X, Z), N, M, Y) -> lt#(N, M), lt#(s X, s Y) -> lt#(X, Y))
    (qsort# add(N, X) -> split#(N, X), split#(N, add(M, Y)) -> f_1#(split(N, Y), N, M, Y))
    (qsort# add(N, X) -> split#(N, X), 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))
    (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_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# Z, qsort# add(N, X) -> split#(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) -> split#(N, X))
    (f_3#(pair(Y, Z), N, X) -> qsort# Y, qsort# add(N, X) -> f_3#(split(N, X), N, X))
    (append#(add(N, X), Y) -> append#(X, Y), append#(add(N, X), Y) -> append#(X, 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)))
    (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) -> qsort# Z)}
   SCCS (4):
    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 (3):
     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:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [f_2](x0, x1, x2, x3, x4, x5) = x0 + x1 + 1,
       
       [f_1](x0, x1, x2, x3) = x0 + 1,
       
       [f_3](x0, x1, x2) = 0,
       
       [lt](x0, x1) = 0,
       
       [append](x0, x1) = x0 + x1,
       
       [add](x0, x1) = x0 + 1,
       
       [pair](x0, x1) = x0 + x1,
       
       [split](x0, x1) = x0,
       
       [s](x0) = 0,
       
       [qsort](x0) = 1,
       
       [true] = 0,
       
       [0] = 0,
       
       [false] = 0,
       
       [nil] = 0,
       
       [f_3#](x0, x1, x2) = x0 + 1,
       
       [qsort#](x0) = x0 + 1
      Strict:
       f_3#(pair(Y, Z), N, X) -> qsort# Z
       1 + 0X + 1Y + 0N + 1Z >= 1 + 1Z
       f_3#(pair(Y, Z), N, X) -> qsort# Y
       1 + 0X + 1Y + 0N + 1Z >= 1 + 1Y
       qsort# add(N, X) -> f_3#(split(N, X), N, X)
       2 + 1X + 0N >= 1 + 1X + 0N
      Weak:
       
     EDG:
      {}
      SCCS (0):
       
       Qed
   SCC (1):
    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 (1):
    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 (1):
    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#) = 1
     Strict:
      {}
     Qed