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)))
  EDG 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)))
   graph:
    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)
    f_3#(pair(Y,Z),N,X) -> append#(qsort(Y),add(X,qsort(Z))) ->
    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) -> 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)))
    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)
    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)
    append#(add(N,X),Y) -> append#(X,Y) ->
    append#(add(N,X),Y) -> append#(X,Y)
    lt#(s(X),s(Y)) -> lt#(X,Y) -> lt#(s(X),s(Y)) -> lt#(X,Y)
   SCC Processor:
    #sccs: 4
    #rules: 6
    #arcs: 17/121
    DPs:
     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)
    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:
     dimension: 1
     interpretation:
      [f_3#](x0, x1, x2) = x0,
      
      [qsort#](x0) = x0,
      
      [f_3](x0, x1, x2) = x0 + 1,
      
      [qsort](x0) = x0,
      
      [f_2](x0, x1, x2, x3, x4, x5) = x0 + x4 + x5,
      
      [f_1](x0, x1, x2, x3) = x0 + 1,
      
      [pair](x0, x1) = x0 + x1,
      
      [split](x0, x1) = x1,
      
      [add](x0, x1) = x1 + 1,
      
      [append](x0, x1) = x0 + x1,
      
      [nil] = 0,
      
      [false] = 1,
      
      [true] = 1,
      
      [lt](x0, x1) = 1,
      
      [s](x0) = 0,
      
      [0] = 0
     orientation:
      f_3#(pair(Y,Z),N,X) = Y + Z >= Z = qsort#(Z)
      
      qsort#(add(N,X)) = X + 1 >= X = f_3#(split(N,X),N,X)
      
      f_3#(pair(Y,Z),N,X) = Y + Z >= Y = qsort#(Y)
      
      lt(0(),s(X)) = 1 >= 1 = true()
      
      lt(s(X),0()) = 1 >= 1 = false()
      
      lt(s(X),s(Y)) = 1 >= 1 = lt(X,Y)
      
      append(nil(),Y) = Y >= Y = Y
      
      append(add(N,X),Y) = X + Y + 1 >= X + Y + 1 = add(N,append(X,Y))
      
      split(N,nil()) = 0 >= 0 = pair(nil(),nil())
      
      split(N,add(M,Y)) = Y + 1 >= Y + 1 = f_1(split(N,Y),N,M,Y)
      
      f_1(pair(X,Z),N,M,Y) = X + Z + 1 >= X + Z + 1 = f_2(lt(N,M),N,M,Y,X,Z)
      
      f_2(true(),N,M,Y,X,Z) = X + Z + 1 >= X + Z + 1 = pair(X,add(M,Z))
      
      f_2(false(),N,M,Y,X,Z) = X + Z + 1 >= X + Z + 1 = pair(add(M,X),Z)
      
      qsort(nil()) = 0 >= 0 = nil()
      
      qsort(add(N,X)) = X + 1 >= X + 1 = f_3(split(N,X),N,X)
      
      f_3(pair(Y,Z),N,X) = Y + Z + 1 >= Y + Z + 1 = append(qsort(Y),add(X,qsort(Z)))
     problem:
      DPs:
       f_3#(pair(Y,Z),N,X) -> qsort#(Z)
       f_3#(pair(Y,Z),N,X) -> qsort#(Y)
      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)))
     Subterm Criterion Processor:
      simple projection:
       pi(qsort#) = 0
       pi(f_3#) = 0
      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
    
    DPs:
     split#(N,add(M,Y)) -> split#(N,Y)
    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)))
    Subterm Criterion Processor:
     simple projection:
      pi(split#) = 1
     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
    
    DPs:
     lt#(s(X),s(Y)) -> lt#(X,Y)
    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)))
    Subterm Criterion Processor:
     simple projection:
      pi(lt#) = 1
     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
    
    DPs:
     append#(add(N,X),Y) -> append#(X,Y)
    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)))
    Subterm Criterion Processor:
     simple projection:
      pi(append#) = 0
     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