Input TRS:
    1: bsort(nil()) -> nil()
    2: bsort(.(x,y)) -> last(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))
    3: bubble(nil()) -> nil()
    4: bubble(.(x,nil())) -> .(x,nil())
    5: bubble(.(x,.(y,z))) -> if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))
    6: last(nil()) -> 0()
    7: last(.(x,nil())) -> x
    8: last(.(x,.(y,z))) -> last(.(y,z))
    9: butlast(nil()) -> nil()
    10: butlast(.(x,nil())) -> nil()
    11: butlast(.(x,.(y,z))) -> .(x,butlast(.(y,z)))
Number of strict rules: 11
Direct Order(PosReal,>,Poly) ... failed.
Freezing butlast last bubble
1: bsort(nil()) -> nil()
2: bsort(.(x,y)) -> last❆1_.(bubble❆1_.(x,y),bsort(butlast(bubble❆1_.(x,y))))
3: bubble❆1_nil() -> nil()
4: bubble❆1_.(x,nil()) -> .(x,nil())
5: bubble❆1_.(x,.(y,z)) -> if(<=(x,y),.(y,bubble❆1_.(x,z)),.(x,bubble❆1_.(y,z)))
6: last❆1_nil() -> 0()
7: last❆1_.(x,nil()) -> x
8: last❆1_.(x,.(y,z)) -> last❆1_.(y,z)
9: butlast❆1_nil() -> nil()
10: butlast❆1_.(x,nil()) -> nil()
11: butlast❆1_.(x,.(y,z)) -> .(x,butlast❆1_.(y,z))
12: bubble(nil()) ->= bubble❆1_nil()
13: bubble(.(_1,_2)) ->= bubble❆1_.(_1,_2)
14: last(nil()) ->= last❆1_nil()
15: last(.(_1,_2)) ->= last❆1_.(_1,_2)
16: butlast(nil()) ->= butlast❆1_nil()
17: butlast(.(_1,_2)) ->= butlast❆1_.(_1,_2)
Number of strict rules: 11
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #bsort(.(x,y)) -> #last❆1_.(bubble❆1_.(x,y),bsort(butlast(bubble❆1_.(x,y))))
   #2: #bsort(.(x,y)) -> #bubble❆1_.(x,y)
   #3: #bsort(.(x,y)) -> #bsort(butlast(bubble❆1_.(x,y)))
   #4: #bsort(.(x,y)) -> #butlast(bubble❆1_.(x,y))
   #5: #bsort(.(x,y)) -> #bubble❆1_.(x,y)
   #6: #bubble(.(_1,_2)) ->? #bubble❆1_.(_1,_2)
   #7: #butlast❆1_.(x,.(y,z)) -> #butlast❆1_.(y,z)
   #8: #bubble(nil()) ->? #bubble❆1_nil()
   #9: #last(nil()) ->? #last❆1_nil()
   #10: #bubble❆1_.(x,.(y,z)) -> #bubble❆1_.(x,z)
   #11: #bubble❆1_.(x,.(y,z)) -> #bubble❆1_.(y,z)
   #12: #butlast(.(_1,_2)) ->? #butlast❆1_.(_1,_2)
   #13: #butlast(nil()) ->? #butlast❆1_nil()
   #14: #last❆1_.(x,.(y,z)) -> #last❆1_.(y,z)
   #15: #last(.(_1,_2)) ->? #last❆1_.(_1,_2)
Number of SCCs: 4, DPs: 5, edges: 7
	SCC { #7 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#butlast❆1_nil()	weight: 0
last❆1_nil()	weight: 0
#bubble(x1)	weight: 0
#butlast(x1)	weight: 0
    <=(x1,x2)	weight: 0
#bubble❆1_nil()	weight: 0
#bsort(x1)	weight: 0
last❆1_.(x1,x2)	weight: 0
#last❆1_nil()	weight: 0
butlast(x1)	weight: 0
butlast❆1_.(x1,x2)	weight: 0
#butlast❆1_.(x1,x2)	weight: x2
#last(x1)	weight: 0
#bubble❆1_.(x1,x2)	weight: 0
    if(x1,x2,x3)	weight: 0
     0()	weight: 0
  last(x1)	weight: 0
   nil()	weight: 0
bubble❆1_.(x1,x2)	weight: 0
butlast❆1_nil()	weight: 0
     .(x1,x2)	weight: (/ 1 2) + x2
bubble❆1_nil()	weight: 0
bubble(x1)	weight: 0
#last❆1_.(x1,x2)	weight: 0
 bsort(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #7
Number of SCCs: 3, DPs: 4, edges: 6
	SCC { #14 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#butlast❆1_nil()	weight: 0
last❆1_nil()	weight: 0
#bubble(x1)	weight: 0
#butlast(x1)	weight: 0
    <=(x1,x2)	weight: 0
#bubble❆1_nil()	weight: 0
#bsort(x1)	weight: 0
last❆1_.(x1,x2)	weight: 0
#last❆1_nil()	weight: 0
butlast(x1)	weight: 0
butlast❆1_.(x1,x2)	weight: 0
#butlast❆1_.(x1,x2)	weight: 0
#last(x1)	weight: 0
#bubble❆1_.(x1,x2)	weight: 0
    if(x1,x2,x3)	weight: 0
     0()	weight: 0
  last(x1)	weight: 0
   nil()	weight: 0
bubble❆1_.(x1,x2)	weight: 0
butlast❆1_nil()	weight: 0
     .(x1,x2)	weight: (/ 1 2) + x2
bubble❆1_nil()	weight: 0
bubble(x1)	weight: 0
#last❆1_.(x1,x2)	weight: x2
 bsort(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #14
Number of SCCs: 2, DPs: 3, edges: 5
	SCC { #3 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... succeeded.
#butlast❆1_nil()	weight: 0
last❆1_nil()	weight: 0
#bubble(x1)	weight: 0
#butlast(x1)	weight: 0
    <=(x1,x2)	weight: 0
#bubble❆1_nil()	weight: 0
#bsort(x1)	weight: max{0, (/ 1 16) + x1}
last❆1_.(x1,x2)	weight: 0
#last❆1_nil()	weight: 0
butlast(x1)	weight: max{0, (- (/ 1 8)) + x1}
butlast❆1_.(x1,x2)	weight: max{0, (/ 1 16) + x2}
#butlast❆1_.(x1,x2)	weight: 0
#last(x1)	weight: 0
#bubble❆1_.(x1,x2)	weight: 0
    if(x1,x2,x3)	weight: max{0, (- (/ 1 4)) + x2}
     0()	weight: 0
  last(x1)	weight: 0
   nil()	weight: (/ 1 16)
bubble❆1_.(x1,x2)	weight: (max (/ 1 4) 0)
butlast❆1_nil()	weight: 0
     .(x1,x2)	weight: max{0, (/ 3 16) + x2}
bubble❆1_nil()	weight: 0
bubble(x1)	weight: 0
#last❆1_.(x1,x2)	weight: 0
 bsort(x1)	weight: 0
    Usable rules: { 4 5 10 11 17 }
    Removed DPs: #3
Number of SCCs: 1, DPs: 2, edges: 4
	SCC { #10 #11 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#butlast❆1_nil()	weight: 0
last❆1_nil()	weight: 0
#bubble(x1)	weight: 0
#butlast(x1)	weight: 0
    <=(x1,x2)	weight: (/ 1 4)
#bubble❆1_nil()	weight: 0
#bsort(x1)	weight: 0
last❆1_.(x1,x2)	weight: 0
#last❆1_nil()	weight: 0
butlast(x1)	weight: 0
butlast❆1_.(x1,x2)	weight: (/ 1 4) + x2
#butlast❆1_.(x1,x2)	weight: 0
#last(x1)	weight: 0
#bubble❆1_.(x1,x2)	weight: x2
    if(x1,x2,x3)	weight: x2
     0()	weight: 0
  last(x1)	weight: 0
   nil()	weight: 0
bubble❆1_.(x1,x2)	weight: (/ 1 4) + x1 + x2
butlast❆1_nil()	weight: 0
     .(x1,x2)	weight: (/ 1 4) + x2
bubble❆1_nil()	weight: 0
bubble(x1)	weight: 0
#last❆1_.(x1,x2)	weight: 0
 bsort(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #10 #11
Number of SCCs: 0, DPs: 0, edges: 0
YES