Input TRS: 1: qsort(nil()) -> nil() 2: qsort(.(x,y)) -> ++(qsort(lowers(x,y)),.(x,qsort(greaters(x,y)))) 3: lowers(x,nil()) -> nil() 4: lowers(x,.(y,z)) -> if(<=(y,x),.(y,lowers(x,z)),lowers(x,z)) 5: greaters(x,nil()) -> nil() 6: greaters(x,.(y,z)) -> if(<=(y,x),greaters(x,z),.(y,greaters(x,z))) Number of strict rules: 6 Direct Order(PosReal,>,Poly) ... failed. Freezing ... failed. Dependency Pairs: #1: #qsort(.(x,y)) -> #qsort(lowers(x,y)) #2: #qsort(.(x,y)) -> #lowers(x,y) #3: #qsort(.(x,y)) -> #qsort(greaters(x,y)) #4: #qsort(.(x,y)) -> #greaters(x,y) #5: #greaters(x,.(y,z)) -> #greaters(x,z) #6: #greaters(x,.(y,z)) -> #greaters(x,z) #7: #lowers(x,.(y,z)) -> #lowers(x,z) #8: #lowers(x,.(y,z)) -> #lowers(x,z) Number of SCCs: 2, DPs: 4, edges: 8 SCC { #7 #8 } Removing DPs: Order(PosReal,>,Sum)... succeeded. lowers(x1,x2) weight: 0 greaters(x1,x2) weight: 0 <=(x1,x2) weight: 0 ++(x1,x2) weight: 0 qsort(x1) weight: 0 #qsort(x1) weight: 0 if(x1,x2,x3) weight: 0 #lowers(x1,x2) weight: x2 nil() weight: 0 #greaters(x1,x2) weight: 0 .(x1,x2) weight: (/ 1 2) + x2 Usable rules: { } Removed DPs: #7 #8 Number of SCCs: 1, DPs: 2, edges: 4 SCC { #5 #6 } Removing DPs: Order(PosReal,>,Sum)... succeeded. lowers(x1,x2) weight: 0 greaters(x1,x2) weight: 0 <=(x1,x2) weight: 0 ++(x1,x2) weight: 0 qsort(x1) weight: 0 #qsort(x1) weight: 0 if(x1,x2,x3) weight: 0 #lowers(x1,x2) weight: 0 nil() weight: 0 #greaters(x1,x2) weight: x2 .(x1,x2) weight: (/ 1 2) + x2 Usable rules: { } Removed DPs: #5 #6 Number of SCCs: 0, DPs: 0, edges: 0 YES