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