YES

Problem:
 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)))

Proof:
 DP Processor:
  DPs:
   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) -> qsort#(Z)
   f_3#(pair(Y,Z),N,X) -> qsort#(Y)
   f_3#(pair(Y,Z),N,X) -> append#(qsort(Y),add(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)))
  Matrix Interpretation Processor: dim=2
   
   usable rules:
    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)))
   interpretation:
    [f_3#](x0, x1, x2) = [1 0]x0 + [0 1]x1 + [2],
    
    [qsort#](x0) = [1 0]x0 + [1],
    
    [f_2#](x0, x1, x2, x3, x4, x5) = [0 1]x1 + [1 0]x3,
    
    [f_1#](x0, x1, x2, x3) = [0 3]x0 + [0 1]x1 + [1 0]x3 + [2],
    
    [split#](x0, x1) = [0 1]x0 + [1 0]x1 + [1],
    
    [append#](x0, x1) = [1 0]x0,
    
    [lt#](x0, x1) = [0 1]x0 + [1],
    
                        [1 1]     [0 1]     [0 2]     [2]
    [f_3](x0, x1, x2) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0],
    
                  [1 2]  
    [qsort](x0) = [0 0]x0,
    
                                    [0 2]     [1 2]     [1 1]     [2]
    [f_2](x0, x1, x2, x3, x4, x5) = [0 0]x2 + [0 0]x4 + [0 1]x5 + [0],
    
                            [1 0]     [0 2]     [2]
    [f_1](x0, x1, x2, x3) = [0 2]x0 + [0 0]x2 + [0],
    
                     [1 2]     [1 1]  
    [pair](x0, x1) = [0 0]x0 + [0 1]x1,
    
                      [0 1]     [1 0]  
    [split](x0, x1) = [0 0]x0 + [0 0]x1,
    
                    [0 2]          [2]
    [add](x0, x1) = [0 0]x0 + x1 + [0],
    
                       [1 0]     [1 0]  
    [append](x0, x1) = [0 0]x0 + [0 2]x1,
    
            [0]
    [nil] = [0],
    
              [0]
    [false] = [0],
    
             [0]
    [true] = [0],
    
                   [0 2]     [0 1]     [0]
    [lt](x0, x1) = [3 0]x0 + [2 0]x1 + [1],
    
              [2 1]     [1]
    [s](x0) = [1 1]x0 + [2],
    
          [1]
    [0] = [2]
   orientation:
    lt#(s(X),s(Y)) = [1 1]X + [3] >= [0 1]X + [1] = lt#(X,Y)
    
    append#(add(N,X),Y) = [0 2]N + [1 0]X + [2] >= [1 0]X = append#(X,Y)
    
    split#(N,add(M,Y)) = [0 2]M + [0 1]N + [1 0]Y + [3] >= [0 1]N + [1 0]Y + [1] = split#(N,Y)
    
    split#(N,add(M,Y)) = [0 2]M + [0 1]N + [1 0]Y + [3] >= [0 1]N + [1 0]Y + [2] = f_1#(split(N,Y),N,M,Y)
    
    f_1#(pair(X,Z),N,M,Y) = [0 1]N + [1 0]Y + [0 3]Z + [2] >= [0 1]N + [1] = lt#(N,M)
    
    f_1#(pair(X,Z),N,M,Y) = [0 1]N + [1 0]Y + [0 3]Z + [2] >= [0 1]N + [1 0]Y = f_2#(lt(N,M),N,M,Y,X,Z)
    
    qsort#(add(N,X)) = [0 2]N + [1 0]X + [3] >= [0 1]N + [1 0]X + [1] = split#(N,X)
    
    qsort#(add(N,X)) = [0 2]N + [1 0]X + [3] >= [0 2]N + [1 0]X + [2] = f_3#(split(N,X),N,X)
    
    f_3#(pair(Y,Z),N,X) = [0 1]N + [1 2]Y + [1 1]Z + [2] >= [1 0]Z + [1] = qsort#(Z)
    
    f_3#(pair(Y,Z),N,X) = [0 1]N + [1 2]Y + [1 1]Z + [2] >= [1 0]Y + [1] = qsort#(Y)
    
    f_3#(pair(Y,Z),N,X) = [0 1]N + [1 2]Y + [1 1]Z + [2] >= [1 2]Y = append#(qsort(Y),add(X,qsort(Z)))
    
                   [1 1]    [6]    [0]         
    lt(0(),s(X)) = [4 2]X + [6] >= [0] = true()
    
                   [2 2]    [6]    [0]          
    lt(s(X),0()) = [6 3]X + [6] >= [0] = false()
    
                    [2 2]    [1 1]    [6]    [0 2]    [0 1]    [0]          
    lt(s(X),s(Y)) = [6 3]X + [4 2]Y + [6] >= [3 0]X + [2 0]Y + [1] = lt(X,Y)
    
                      [1 0]          
    append(nil(),Y) = [0 2]Y >= Y = Y
    
                         [0 2]    [1 0]    [1 0]    [2]    [0 2]    [1 0]    [1 0]    [2]                     
    append(add(N,X),Y) = [0 0]N + [0 0]X + [0 2]Y + [0] >= [0 0]N + [0 0]X + [0 2]Y + [0] = add(N,append(X,Y))
    
                     [0 1]     [0]                    
    split(N,nil()) = [0 0]N >= [0] = pair(nil(),nil())
    
                        [0 2]    [0 1]    [1 0]    [2]    [0 2]    [0 1]    [1 0]    [2]                        
    split(N,add(M,Y)) = [0 0]M + [0 0]N + [0 0]Y + [0] >= [0 0]M + [0 0]N + [0 0]Y + [0] = f_1(split(N,Y),N,M,Y)
    
                           [0 2]    [1 2]    [1 1]    [2]    [0 2]    [1 2]    [1 1]    [2]                         
    f_1(pair(X,Z),N,M,Y) = [0 0]M + [0 0]X + [0 2]Z + [0] >= [0 0]M + [0 0]X + [0 1]Z + [0] = f_2(lt(N,M),N,M,Y,X,Z)
    
                            [0 2]    [1 2]    [1 1]    [2]    [0 2]    [1 2]    [1 1]    [2]                   
    f_2(true(),N,M,Y,X,Z) = [0 0]M + [0 0]X + [0 1]Z + [0] >= [0 0]M + [0 0]X + [0 1]Z + [0] = pair(X,add(M,Z))
    
                             [0 2]    [1 2]    [1 1]    [2]    [0 2]    [1 2]    [1 1]    [2]                   
    f_2(false(),N,M,Y,X,Z) = [0 0]M + [0 0]X + [0 1]Z + [0] >= [0 0]M + [0 0]X + [0 1]Z + [0] = pair(add(M,X),Z)
    
                   [0]    [0]        
    qsort(nil()) = [0] >= [0] = nil()
    
                      [0 2]    [1 2]    [2]    [0 2]    [1 2]    [2]                      
    qsort(add(N,X)) = [0 0]N + [0 0]X + [0] >= [0 0]N + [0 0]X + [0] = f_3(split(N,X),N,X)
    
                         [0 1]    [0 2]    [1 2]    [1 2]    [2]    [0 2]    [1 2]    [1 2]    [2]                                   
    f_3(pair(Y,Z),N,X) = [0 0]N + [0 0]X + [0 0]Y + [0 0]Z + [0] >= [0 0]X + [0 0]Y + [0 0]Z + [0] = append(qsort(Y),add(X,qsort(Z)))
   problem:
    DPs:
     
    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)))
   Qed