Input TRS:
    1: qsort(nil()) -> nil()
    2: qsort(cons(x,xs)) -> append(qsort(filterlow(x,cons(x,xs))),cons(x,qsort(filterhigh(x,cons(x,xs)))))
    3: filterlow(n,nil()) -> nil()
    4: filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
    5: if1(true(),n,x,xs) -> filterlow(n,xs)
    6: if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
    7: filterhigh(n,nil()) -> nil()
    8: filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
    9: if2(true(),n,x,xs) -> filterhigh(n,xs)
    10: if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
    11: ge(x,0()) -> true()
    12: ge(0(),s(x)) -> false()
    13: ge(s(x),s(y)) -> ge(x,y)
    14: append(nil(),ys()) -> ys()
    15: append(cons(x,xs),ys()) -> cons(x,append(xs,ys()))
Number of strict rules: 15
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #qsort(cons(x,xs)) -> #append(qsort(filterlow(x,cons(x,xs))),cons(x,qsort(filterhigh(x,cons(x,xs)))))
   #2: #qsort(cons(x,xs)) -> #qsort(filterlow(x,cons(x,xs)))
   #3: #qsort(cons(x,xs)) -> #filterlow(x,cons(x,xs))
   #4: #qsort(cons(x,xs)) -> #qsort(filterhigh(x,cons(x,xs)))
   #5: #qsort(cons(x,xs)) -> #filterhigh(x,cons(x,xs))
   #6: #if1(false(),n,x,xs) -> #filterlow(n,xs)
   #7: #ge(s(x),s(y)) -> #ge(x,y)
   #8: #if2(true(),n,x,xs) -> #filterhigh(n,xs)
   #9: #if2(false(),n,x,xs) -> #filterhigh(n,xs)
   #10: #if1(true(),n,x,xs) -> #filterlow(n,xs)
   #11: #filterhigh(n,cons(x,xs)) -> #if2(ge(x,n),n,x,xs)
   #12: #filterhigh(n,cons(x,xs)) -> #ge(x,n)
   #13: #append(cons(x,xs),ys()) -> #append(xs,ys())
   #14: #filterlow(n,cons(x,xs)) -> #if1(ge(n,x),n,x,xs)
   #15: #filterlow(n,cons(x,xs)) -> #ge(n,x)
Number of SCCs: 5, DPs: 10, edges: 14
	SCC { #7 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     s(x1)	weight: (/ 1 2) + x1
#append(x1,x2)	weight: 0
   if1(x1,x2,x3,x4)	weight: 0
 false()	weight: 0
  #ge(x1,x2)	weight: x2
filterlow(x1,x2)	weight: 0
 qsort(x1)	weight: 0
  true()	weight: 0
 #if1(x1,x2,x3,x4)	weight: 0
   if2(x1,x2,x3,x4)	weight: 0
#qsort(x1)	weight: 0
append(x1,x2)	weight: 0
     0()	weight: 0
    ge(x1,x2)	weight: 0
   nil()	weight: 0
#filterlow(x1,x2)	weight: 0
  cons(x1,x2)	weight: 0
filterhigh(x1,x2)	weight: 0
    ys()	weight: 0
#filterhigh(x1,x2)	weight: 0
 #if2(x1,x2,x3,x4)	weight: 0
    Usable rules: { }
    Removed DPs: #7
Number of SCCs: 4, DPs: 9, edges: 13
	SCC { #13 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     s(x1)	weight: (/ 1 2)
#append(x1,x2)	weight: x1
   if1(x1,x2,x3,x4)	weight: 0
 false()	weight: 0
  #ge(x1,x2)	weight: 0
filterlow(x1,x2)	weight: 0
 qsort(x1)	weight: 0
  true()	weight: 0
 #if1(x1,x2,x3,x4)	weight: 0
   if2(x1,x2,x3,x4)	weight: 0
#qsort(x1)	weight: 0
append(x1,x2)	weight: 0
     0()	weight: 0
    ge(x1,x2)	weight: 0
   nil()	weight: 0
#filterlow(x1,x2)	weight: 0
  cons(x1,x2)	weight: (/ 1 2) + x2
filterhigh(x1,x2)	weight: 0
    ys()	weight: 0
#filterhigh(x1,x2)	weight: 0
 #if2(x1,x2,x3,x4)	weight: 0
    Usable rules: { }
    Removed DPs: #13
Number of SCCs: 3, DPs: 8, edges: 12
	SCC { #2 #4 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)... Order(PosReal,>,Sum-Sum; NegReal,≥,Sum)... Order(PosReal,>,MaxSum-Sum; NegReal,≥,Sum)... failed.
Removing edges: failed.
Finding a loop...  failed.
MAYBE