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)))
  TDG 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)) -> f_3#(split(N,X),N,X)
    f_3#(pair(Y,Z),N,X) -> qsort#(Z) ->
    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) -> qsort#(Y) ->
    qsort#(add(N,X)) -> split#(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) -> 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)
    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)
    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) -> f_2#(lt(N,M),N,M,Y,X,Z)
    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)) -> 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)
    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)))
    Usable Rule Processor:
     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:
      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)
      lt(0(),s(X)) -> true()
      lt(s(X),0()) -> false()
      lt(s(X),s(Y)) -> lt(X,Y)
     Arctic Interpretation Processor:
      dimension: 1
      usable rules:
       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)
      interpretation:
       [f_3#](x0, x1, x2) = 1x0 + 3x2 + 4,
       
       [qsort#](x0) = 1x0 + 4,
       
       [f_2](x0, x1, x2, x3, x4, x5) = 2x3 + 4x4 + 4x5 + 7,
       
       [f_1](x0, x1, x2, x3) = 4x0 + 7x3 + 7,
       
       [pair](x0, x1) = x0 + x1 + 3,
       
       [split](x0, x1) = 3x1 + 0,
       
       [add](x0, x1) = 4x1 + 4,
       
       [nil] = 3,
       
       [false] = 1,
       
       [true] = 0,
       
       [lt](x0, x1) = x0 + 0,
       
       [s](x0) = 2x0 + 0,
       
       [0] = 6
      orientation:
       f_3#(pair(Y,Z),N,X) = 3X + 1Y + 1Z + 4 >= 1Z + 4 = qsort#(Z)
       
       qsort#(add(N,X)) = 5X + 5 >= 4X + 4 = f_3#(split(N,X),N,X)
       
       f_3#(pair(Y,Z),N,X) = 3X + 1Y + 1Z + 4 >= 1Y + 4 = qsort#(Y)
       
       split(N,nil()) = 6 >= 3 = pair(nil(),nil())
       
       split(N,add(M,Y)) = 7Y + 7 >= 7Y + 7 = f_1(split(N,Y),N,M,Y)
       
       f_1(pair(X,Z),N,M,Y) = 4X + 7Y + 4Z + 7 >= 4X + 2Y + 4Z + 7 = f_2(lt(N,M),N,M,Y,X,Z)
       
       f_2(true(),N,M,Y,X,Z) = 4X + 2Y + 4Z + 7 >= X + 4Z + 4 = pair(X,add(M,Z))
       
       f_2(false(),N,M,Y,X,Z) = 4X + 2Y + 4Z + 7 >= 4X + Z + 4 = pair(add(M,X),Z)
       
       lt(0(),s(X)) = 6 >= 0 = true()
       
       lt(s(X),0()) = 2X + 0 >= 1 = false()
       
       lt(s(X),s(Y)) = 2X + 0 >= X + 0 = lt(X,Y)
      problem:
       DPs:
        f_3#(pair(Y,Z),N,X) -> qsort#(Z)
        f_3#(pair(Y,Z),N,X) -> qsort#(Y)
       TRS:
        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)
        lt(0(),s(X)) -> true()
        lt(s(X),0()) -> false()
        lt(s(X),s(Y)) -> lt(X,Y)
      Restore Modifier:
       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)))
       SCC Processor:
        #sccs: 0
        #rules: 0
        #arcs: 4/4
        
    
    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
    
    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