Input TRS:
    1: lt(0(),s(X)) -> true()
    2: lt(s(X),0()) -> false()
    3: lt(s(X),s(Y)) -> lt(X,Y)
    4: append(nil(),Y) -> Y
    5: append(add(N,X),Y) -> add(N,append(X,Y))
    6: split(N,nil()) -> pair(nil(),nil())
    7: split(N,add(M,Y)) -> f_1(split(N,Y),N,M,Y)
    8: f_1(pair(X,Z),N,M,Y) -> f_2(lt(N,M),N,M,Y,X,Z)
    9: f_2(true(),N,M,Y,X,Z) -> pair(X,add(M,Z))
    10: f_2(false(),N,M,Y,X,Z) -> pair(add(M,X),Z)
    11: qsort(nil()) -> nil()
    12: qsort(add(N,X)) -> f_3(split(N,X),N,X)
    13: f_3(pair(Y,Z),N,X) -> append(qsort(Y),add(X,qsort(Z)))
Number of strict rules: 13
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #f_3(pair(Y,Z),N,X) -> #append(qsort(Y),add(X,qsort(Z)))
   #2: #f_3(pair(Y,Z),N,X) -> #qsort(Y)
   #3: #f_3(pair(Y,Z),N,X) -> #qsort(Z)
   #4: #qsort(add(N,X)) -> #f_3(split(N,X),N,X)
   #5: #qsort(add(N,X)) -> #split(N,X)
   #6: #split(N,add(M,Y)) -> #f_1(split(N,Y),N,M,Y)
   #7: #split(N,add(M,Y)) -> #split(N,Y)
   #8: #append(add(N,X),Y) -> #append(X,Y)
   #9: #lt(s(X),s(Y)) -> #lt(X,Y)
   #10: #f_1(pair(X,Z),N,M,Y) -> #f_2(lt(N,M),N,M,Y,X,Z)
   #11: #f_1(pair(X,Z),N,M,Y) -> #lt(N,M)
Number of SCCs: 4, DPs: 6, edges: 7
	SCC { #9 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     s(x1)	weight: (/ 1 2) + x1
#append(x1,x2)	weight: 0
  #lt(x1,x2)	weight: x1
   f_2(x1,x2,x3,x4,x5,x6)	weight: 0
  pair(x1,x2)	weight: 0
 false()	weight: 0
 #f_2(x1,x2,x3,x4,x5,x6)	weight: 0
 qsort(x1)	weight: 0
#split(x1,x2)	weight: 0
  true()	weight: 0
#qsort(x1)	weight: 0
append(x1,x2)	weight: 0
   f_1(x1,x2,x3,x4)	weight: 0
     0()	weight: 0
   nil()	weight: 0
 split(x1,x2)	weight: 0
 #f_3(x1,x2,x3)	weight: 0
 #f_1(x1,x2,x3,x4)	weight: 0
   add(x1,x2)	weight: 0
   f_3(x1,x2,x3)	weight: 0
    lt(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #9
Number of SCCs: 3, DPs: 5, edges: 6
	SCC { #7 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     s(x1)	weight: (/ 1 2)
#append(x1,x2)	weight: 0
  #lt(x1,x2)	weight: 0
   f_2(x1,x2,x3,x4,x5,x6)	weight: 0
  pair(x1,x2)	weight: 0
 false()	weight: 0
 #f_2(x1,x2,x3,x4,x5,x6)	weight: 0
 qsort(x1)	weight: 0
#split(x1,x2)	weight: x2
  true()	weight: 0
#qsort(x1)	weight: 0
append(x1,x2)	weight: 0
   f_1(x1,x2,x3,x4)	weight: 0
     0()	weight: 0
   nil()	weight: 0
 split(x1,x2)	weight: 0
 #f_3(x1,x2,x3)	weight: 0
 #f_1(x1,x2,x3,x4)	weight: 0
   add(x1,x2)	weight: (/ 1 2) + x2
   f_3(x1,x2,x3)	weight: 0
    lt(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #7
Number of SCCs: 2, DPs: 4, edges: 5
	SCC { #8 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     s(x1)	weight: (/ 1 2)
#append(x1,x2)	weight: x1
  #lt(x1,x2)	weight: 0
   f_2(x1,x2,x3,x4,x5,x6)	weight: 0
  pair(x1,x2)	weight: 0
 false()	weight: 0
 #f_2(x1,x2,x3,x4,x5,x6)	weight: 0
 qsort(x1)	weight: 0
#split(x1,x2)	weight: 0
  true()	weight: 0
#qsort(x1)	weight: 0
append(x1,x2)	weight: 0
   f_1(x1,x2,x3,x4)	weight: 0
     0()	weight: 0
   nil()	weight: 0
 split(x1,x2)	weight: 0
 #f_3(x1,x2,x3)	weight: 0
 #f_1(x1,x2,x3,x4)	weight: 0
   add(x1,x2)	weight: (/ 1 2) + x2
   f_3(x1,x2,x3)	weight: 0
    lt(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #8
Number of SCCs: 1, DPs: 3, edges: 4
	SCC { #2..4 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     s(x1)	weight: (/ 1 4)
#append(x1,x2)	weight: 0
  #lt(x1,x2)	weight: 0
   f_2(x1,x2,x3,x4,x5,x6)	weight: (/ 3 4) + x3 + x5 + x6
  pair(x1,x2)	weight: (/ 1 4) + x1 + x2
 false()	weight: 0
 #f_2(x1,x2,x3,x4,x5,x6)	weight: 0
 qsort(x1)	weight: 0
#split(x1,x2)	weight: 0
  true()	weight: 0
#qsort(x1)	weight: x1
append(x1,x2)	weight: 0
   f_1(x1,x2,x3,x4)	weight: (/ 1 2) + x1 + x3
     0()	weight: 0
   nil()	weight: 0
 split(x1,x2)	weight: (/ 1 4) + x1 + x2
 #f_3(x1,x2,x3)	weight: x1
 #f_1(x1,x2,x3,x4)	weight: 0
   add(x1,x2)	weight: (/ 1 2) + x1 + x2
   f_3(x1,x2,x3)	weight: 0
    lt(x1,x2)	weight: (/ 1 4) + x2
    Usable rules: { 6..10 }
    Removed DPs: #2..4
Number of SCCs: 0, DPs: 0, edges: 0
YES