YES
Time: 0.052336
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))}
  UR:
   {               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)),
                        a(x, y) -> x,
                        a(x, y) -> y}
   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)}
    STATUS:
     arrows: 0.859504
     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:
       {lt#(s X, s Y) -> lt#(X, Y)}
      Scc:
       {append#(add(N, X), Y) -> append#(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:
         f_3(pair(Y, Z), N, X) -> append(qsort Y, add(X, qsort Z))
         0 + 0X + 0Y + 0N + 0Z >= 3 + 0X + 0Y + 0Z
         qsort add(N, X) -> f_3(split(N, X), N, X)
         1 + 0X + 0N >= 0 + 0X + 0N
         qsort nil() -> nil()
         1 >= 0
         f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z)
         1 + 1X + 0Y + 0N + 0M + 1Z >= 1 + 1X + 0M + 1Z
         f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z))
         1 + 1X + 0Y + 0N + 0M + 1Z >= 1 + 1X + 0M + 1Z
         f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z)
         1 + 1X + 0Y + 0N + 0M + 1Z >= 1 + 1X + 0Y + 0N + 0M + 1Z
         split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y)
         1 + 1Y + 0N + 0M >= 1 + 1Y + 0N + 0M
         split(N, nil()) -> pair(nil(), nil())
         0 + 0N >= 0
         append(add(N, X), Y) -> add(N, append(X, Y))
         1 + 1X + 1Y + 0N >= 1 + 1X + 1Y + 0N
         append(nil(), Y) -> Y
         0 + 1Y >= 1Y
         lt(s X, s Y) -> lt(X, Y)
         0 + 0X + 0Y >= 0 + 0X + 0Y
         lt(s X, 0()) -> false()
         0 + 0X >= 0
         lt(0(), s X) -> true()
         0 + 0X >= 0
       SCCS (0):
        
        
        
     
     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))}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [f_2](x0, x1, x2, x3, x4, x5) = x0 + x1 + x2 + 1,
        
        [f_1](x0, x1, x2, x3) = x0 + x1 + x2 + 1,
        
        [f_3](x0, x1, x2) = 0,
        
        [lt](x0, x1) = x0 + x1 + 1,
        
        [append](x0, x1) = x0 + 1,
        
        [add](x0, x1) = x0 + 1,
        
        [pair](x0, x1) = 0,
        
        [split](x0, x1) = x0 + x1 + 1,
        
        [s](x0) = 1,
        
        [qsort](x0) = x0 + 1,
        
        [true] = 1,
        
        [0] = 0,
        
        [false] = 1,
        
        [nil] = 1,
        
        [split#](x0, x1) = x0
       Strict:
        split#(N, add(M, Y)) -> split#(N, Y)
        1 + 1Y + 0N + 0M >= 0 + 1Y + 0N
       Weak:
        f_3(pair(Y, Z), N, X) -> append(qsort Y, add(X, qsort Z))
        0 + 0X + 0Y + 0N + 0Z >= 2 + 0X + 1Y + 0Z
        qsort add(N, X) -> f_3(split(N, X), N, X)
        2 + 1X + 0N >= 0 + 0X + 0N
        qsort nil() -> nil()
        2 >= 1
        f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z)
        2 + 0X + 0Y + 1N + 1M + 0Z >= 0 + 0X + 0M + 0Z
        f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z))
        2 + 0X + 0Y + 1N + 1M + 0Z >= 0 + 0X + 0M + 0Z
        f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z)
        1 + 0X + 1Y + 1N + 0M + 0Z >= 2 + 0X + 0Y + 2N + 2M + 0Z
        split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y)
        2 + 1Y + 1N + 0M >= 2 + 2Y + 2N + 0M
        split(N, nil()) -> pair(nil(), nil())
        2 + 1N >= 0
        append(add(N, X), Y) -> add(N, append(X, Y))
        2 + 1X + 0Y + 0N >= 2 + 1X + 0Y + 0N
        append(nil(), Y) -> Y
        2 + 0Y >= 1Y
        lt(s X, s Y) -> lt(X, Y)
        3 + 0X + 0Y >= 1 + 1X + 1Y
        lt(s X, 0()) -> false()
        2 + 0X >= 1
        lt(0(), s X) -> true()
        2 + 0X >= 1
      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))}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [f_2](x0, x1, x2, x3, x4, x5) = x0 + x1 + x2 + 1,
        
        [f_1](x0, x1, x2, x3) = x0 + x1 + x2 + 1,
        
        [f_3](x0, x1, x2) = x0 + x1 + x2 + 1,
        
        [lt](x0, x1) = x0 + x1 + 1,
        
        [append](x0, x1) = x0 + 1,
        
        [add](x0, x1) = 0,
        
        [pair](x0, x1) = 0,
        
        [split](x0, x1) = x0 + x1 + 1,
        
        [s](x0) = x0 + 1,
        
        [qsort](x0) = 0,
        
        [true] = 1,
        
        [0] = 0,
        
        [false] = 1,
        
        [nil] = 1,
        
        [lt#](x0, x1) = x0
       Strict:
        lt#(s X, s Y) -> lt#(X, Y)
        1 + 0X + 1Y >= 0 + 0X + 1Y
       Weak:
        f_3(pair(Y, Z), N, X) -> append(qsort Y, add(X, qsort Z))
        1 + 1X + 0Y + 1N + 0Z >= 1 + 0X + 0Y + 0Z
        qsort add(N, X) -> f_3(split(N, X), N, X)
        0 + 0X + 0N >= 2 + 2X + 2N
        qsort nil() -> nil()
        0 >= 1
        f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z)
        2 + 0X + 0Y + 1N + 1M + 0Z >= 0 + 0X + 0M + 0Z
        f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z))
        2 + 0X + 0Y + 1N + 1M + 0Z >= 0 + 0X + 0M + 0Z
        f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z)
        1 + 0X + 1Y + 1N + 0M + 0Z >= 2 + 0X + 0Y + 2N + 2M + 0Z
        split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y)
        1 + 0Y + 1N + 0M >= 2 + 2Y + 2N + 0M
        split(N, nil()) -> pair(nil(), nil())
        2 + 1N >= 0
        append(add(N, X), Y) -> add(N, append(X, Y))
        1 + 0X + 0Y + 0N >= 0 + 0X + 0Y + 0N
        append(nil(), Y) -> Y
        2 + 0Y >= 1Y
        lt(s X, s Y) -> lt(X, Y)
        3 + 1X + 1Y >= 1 + 1X + 1Y
        lt(s X, 0()) -> false()
        2 + 1X >= 1
        lt(0(), s X) -> true()
        2 + 1X >= 1
      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))}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [f_2](x0, x1, x2, x3, x4, x5) = x0 + x1 + x2 + 1,
       
       [f_1](x0, x1, x2, x3) = x0 + x1 + x2 + 1,
       
       [f_3](x0, x1, x2) = 0,
       
       [lt](x0, x1) = x0 + x1 + 1,
       
       [append](x0, x1) = x0 + 1,
       
       [add](x0, x1) = x0 + 1,
       
       [pair](x0, x1) = 0,
       
       [split](x0, x1) = x0 + x1 + 1,
       
       [s](x0) = 1,
       
       [qsort](x0) = x0 + 1,
       
       [true] = 1,
       
       [0] = 0,
       
       [false] = 1,
       
       [nil] = 1,
       
       [append#](x0, x1) = x0
      Strict:
       append#(add(N, X), Y) -> append#(X, Y)
       1 + 1X + 0Y + 0N >= 0 + 1X + 0Y
      Weak:
       f_3(pair(Y, Z), N, X) -> append(qsort Y, add(X, qsort Z))
       0 + 0X + 0Y + 0N + 0Z >= 2 + 0X + 1Y + 0Z
       qsort add(N, X) -> f_3(split(N, X), N, X)
       2 + 1X + 0N >= 0 + 0X + 0N
       qsort nil() -> nil()
       2 >= 1
       f_2(false(), N, M, Y, X, Z) -> pair(add(M, X), Z)
       2 + 0X + 0Y + 1N + 1M + 0Z >= 0 + 0X + 0M + 0Z
       f_2(true(), N, M, Y, X, Z) -> pair(X, add(M, Z))
       2 + 0X + 0Y + 1N + 1M + 0Z >= 0 + 0X + 0M + 0Z
       f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z)
       1 + 0X + 1Y + 1N + 0M + 0Z >= 2 + 0X + 0Y + 2N + 2M + 0Z
       split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y)
       2 + 1Y + 1N + 0M >= 2 + 2Y + 2N + 0M
       split(N, nil()) -> pair(nil(), nil())
       2 + 1N >= 0
       append(add(N, X), Y) -> add(N, append(X, Y))
       2 + 1X + 0Y + 0N >= 2 + 1X + 0Y + 0N
       append(nil(), Y) -> Y
       2 + 0Y >= 1Y
       lt(s X, s Y) -> lt(X, Y)
       3 + 0X + 0Y >= 1 + 1X + 1Y
       lt(s X, 0()) -> false()
       2 + 0X >= 1
       lt(0(), s X) -> true()
       2 + 0X >= 1
     Qed