YES

Problem:
 bsort(nil()) -> nil()
 bsort(.(x,y)) -> last(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))
 bubble(nil()) -> nil()
 bubble(.(x,nil())) -> .(x,nil())
 bubble(.(x,.(y,z))) -> if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))
 last(nil()) -> 0()
 last(.(x,nil())) -> x
 last(.(x,.(y,z))) -> last(.(y,z))
 butlast(nil()) -> nil()
 butlast(.(x,nil())) -> nil()
 butlast(.(x,.(y,z))) -> .(x,butlast(.(y,z)))

Proof:
 DP Processor:
  DPs:
   bsort#(.(x,y)) -> butlast#(bubble(.(x,y)))
   bsort#(.(x,y)) -> bsort#(butlast(bubble(.(x,y))))
   bsort#(.(x,y)) -> bubble#(.(x,y))
   bsort#(.(x,y)) -> last#(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))
   bubble#(.(x,.(y,z))) -> bubble#(.(y,z))
   bubble#(.(x,.(y,z))) -> bubble#(.(x,z))
   last#(.(x,.(y,z))) -> last#(.(y,z))
   butlast#(.(x,.(y,z))) -> butlast#(.(y,z))
  TRS:
   bsort(nil()) -> nil()
   bsort(.(x,y)) -> last(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))
   bubble(nil()) -> nil()
   bubble(.(x,nil())) -> .(x,nil())
   bubble(.(x,.(y,z))) -> if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))
   last(nil()) -> 0()
   last(.(x,nil())) -> x
   last(.(x,.(y,z))) -> last(.(y,z))
   butlast(nil()) -> nil()
   butlast(.(x,nil())) -> nil()
   butlast(.(x,.(y,z))) -> .(x,butlast(.(y,z)))
  EDG Processor:
   DPs:
    bsort#(.(x,y)) -> butlast#(bubble(.(x,y)))
    bsort#(.(x,y)) -> bsort#(butlast(bubble(.(x,y))))
    bsort#(.(x,y)) -> bubble#(.(x,y))
    bsort#(.(x,y)) -> last#(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))
    bubble#(.(x,.(y,z))) -> bubble#(.(y,z))
    bubble#(.(x,.(y,z))) -> bubble#(.(x,z))
    last#(.(x,.(y,z))) -> last#(.(y,z))
    butlast#(.(x,.(y,z))) -> butlast#(.(y,z))
   TRS:
    bsort(nil()) -> nil()
    bsort(.(x,y)) -> last(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))
    bubble(nil()) -> nil()
    bubble(.(x,nil())) -> .(x,nil())
    bubble(.(x,.(y,z))) -> if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))
    last(nil()) -> 0()
    last(.(x,nil())) -> x
    last(.(x,.(y,z))) -> last(.(y,z))
    butlast(nil()) -> nil()
    butlast(.(x,nil())) -> nil()
    butlast(.(x,.(y,z))) -> .(x,butlast(.(y,z)))
   graph:
    last#(.(x,.(y,z))) -> last#(.(y,z)) ->
    last#(.(x,.(y,z))) -> last#(.(y,z))
    bubble#(.(x,.(y,z))) -> bubble#(.(y,z)) ->
    bubble#(.(x,.(y,z))) -> bubble#(.(y,z))
    bubble#(.(x,.(y,z))) -> bubble#(.(y,z)) ->
    bubble#(.(x,.(y,z))) -> bubble#(.(x,z))
    bubble#(.(x,.(y,z))) -> bubble#(.(x,z)) ->
    bubble#(.(x,.(y,z))) -> bubble#(.(y,z))
    bubble#(.(x,.(y,z))) -> bubble#(.(x,z)) ->
    bubble#(.(x,.(y,z))) -> bubble#(.(x,z))
    butlast#(.(x,.(y,z))) -> butlast#(.(y,z)) ->
    butlast#(.(x,.(y,z))) -> butlast#(.(y,z))
    bsort#(.(x,y)) -> last#(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y)))))) ->
    last#(.(x,.(y,z))) -> last#(.(y,z))
    bsort#(.(x,y)) -> bubble#(.(x,y)) ->
    bubble#(.(x,.(y,z))) -> bubble#(.(y,z))
    bsort#(.(x,y)) -> bubble#(.(x,y)) ->
    bubble#(.(x,.(y,z))) -> bubble#(.(x,z))
    bsort#(.(x,y)) -> butlast#(bubble(.(x,y))) ->
    butlast#(.(x,.(y,z))) -> butlast#(.(y,z))
    bsort#(.(x,y)) -> bsort#(butlast(bubble(.(x,y)))) ->
    bsort#(.(x,y)) -> butlast#(bubble(.(x,y)))
    bsort#(.(x,y)) -> bsort#(butlast(bubble(.(x,y)))) ->
    bsort#(.(x,y)) -> bsort#(butlast(bubble(.(x,y))))
    bsort#(.(x,y)) -> bsort#(butlast(bubble(.(x,y)))) ->
    bsort#(.(x,y)) -> bubble#(.(x,y))
    bsort#(.(x,y)) -> bsort#(butlast(bubble(.(x,y)))) ->
    bsort#(.(x,y)) -> last#(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))
   SCC Processor:
    #sccs: 4
    #rules: 5
    #arcs: 14/64
    DPs:
     bsort#(.(x,y)) -> bsort#(butlast(bubble(.(x,y))))
    TRS:
     bsort(nil()) -> nil()
     bsort(.(x,y)) -> last(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))
     bubble(nil()) -> nil()
     bubble(.(x,nil())) -> .(x,nil())
     bubble(.(x,.(y,z))) -> if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))
     last(nil()) -> 0()
     last(.(x,nil())) -> x
     last(.(x,.(y,z))) -> last(.(y,z))
     butlast(nil()) -> nil()
     butlast(.(x,nil())) -> nil()
     butlast(.(x,.(y,z))) -> .(x,butlast(.(y,z)))
    Usable Rule Processor:
     DPs:
      bsort#(.(x,y)) -> bsort#(butlast(bubble(.(x,y))))
     TRS:
      f13(x,y) -> x
      f13(x,y) -> y
      bubble(.(x,nil())) -> .(x,nil())
      bubble(.(x,.(y,z))) -> if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))
      butlast(nil()) -> nil()
      butlast(.(x,nil())) -> nil()
      butlast(.(x,.(y,z))) -> .(x,butlast(.(y,z)))
     Bounds Processor:
      bound: 0
      enrichment: top-dp
      automaton:
       final states: {9}
       transitions:
        butlast0(20) -> 14*
        butlast0(15) -> 14*
        butlast0(22) -> 14*
        butlast0(17) -> 14*
        butlast0(19) -> 14*
        butlast0(14) -> 14*
        butlast0(21) -> 22*
        butlast0(16) -> 14*
        butlast0(18) -> 14*
        bubble0(20) -> 21*
        bubble0(15) -> 15*
        bubble0(22) -> 15*
        bubble0(17) -> 15*
        bubble0(19) -> 15*
        bubble0(14) -> 15*
        bubble0(21) -> 15*
        bubble0(16) -> 15*
        bubble0(18) -> 15*
        f130(22,14) -> 16*
        f130(17,14) -> 16*
        f130(22,16) -> 16*
        f130(17,16) -> 16*
        f130(22,18) -> 16*
        f130(17,18) -> 16*
        f130(22,20) -> 16*
        f130(17,20) -> 16*
        f130(22,22) -> 16*
        f130(17,22) -> 16*
        f130(18,15) -> 16*
        f130(18,17) -> 16*
        f130(18,19) -> 16*
        f130(18,21) -> 16*
        f130(19,14) -> 16*
        f130(14,14) -> 16*
        f130(19,16) -> 16*
        f130(14,16) -> 16*
        f130(19,18) -> 16*
        f130(14,18) -> 16*
        f130(19,20) -> 16*
        f130(14,20) -> 16*
        f130(19,22) -> 16*
        f130(14,22) -> 16*
        f130(20,15) -> 16*
        f130(15,15) -> 16*
        f130(20,17) -> 16*
        f130(15,17) -> 16*
        f130(20,19) -> 16*
        f130(15,19) -> 16*
        f130(20,21) -> 16*
        f130(15,21) -> 16*
        f130(21,14) -> 16*
        f130(16,14) -> 16*
        f130(21,16) -> 16*
        f130(16,16) -> 16*
        f130(21,18) -> 16*
        f130(16,18) -> 16*
        f130(21,20) -> 16*
        f130(16,20) -> 16*
        f130(21,22) -> 16*
        f130(16,22) -> 16*
        f130(22,15) -> 16*
        f130(17,15) -> 16*
        f130(22,17) -> 16*
        f130(17,17) -> 16*
        f130(22,19) -> 16*
        f130(17,19) -> 16*
        f130(22,21) -> 16*
        f130(17,21) -> 16*
        f130(18,14) -> 16*
        f130(18,16) -> 16*
        f130(18,18) -> 16*
        f130(18,20) -> 16*
        f130(18,22) -> 16*
        f130(19,15) -> 16*
        f130(14,15) -> 16*
        f130(19,17) -> 16*
        f130(14,17) -> 16*
        f130(19,19) -> 16*
        f130(14,19) -> 16*
        f130(19,21) -> 16*
        f130(14,21) -> 16*
        f130(20,14) -> 16*
        f130(15,14) -> 16*
        f130(20,16) -> 16*
        f130(15,16) -> 16*
        f130(20,18) -> 16*
        f130(15,18) -> 16*
        f130(20,20) -> 16*
        f130(15,20) -> 16*
        f130(20,22) -> 16*
        f130(15,22) -> 16*
        f130(21,15) -> 16*
        f130(16,15) -> 16*
        f130(21,17) -> 16*
        f130(16,17) -> 16*
        f130(21,19) -> 16*
        f130(16,19) -> 16*
        f130(21,21) -> 16*
        f130(16,21) -> 16*
        nil0() -> 22,14,17
        if0(17,14,16) -> 18*
        if0(16,16,15) -> 18*
        if0(15,18,14) -> 18*
        if0(17,15,22) -> 18*
        if0(16,17,21) -> 18*
        if0(20,17,20) -> 18*
        if0(19,19,19) -> 18*
        if0(18,21,18) -> 18*
        if0(21,14,14) -> 18*
        if0(14,14,22) -> 18*
        if0(17,16,20) -> 18*
        if0(16,18,19) -> 18*
        if0(15,20,18) -> 18*
        if0(14,22,17) -> 18*
        if0(18,22,16) -> 18*
        if0(14,15,20) -> 18*
        if0(15,21,16) -> 18*
        if0(22,14,19) -> 18*
        if0(21,16,18) -> 18*
        if0(20,18,17) -> 18*
        if0(22,22,14) -> 18*
        if0(15,22,22) -> 18*
        if0(18,15,18) -> 18*
        if0(17,17,17) -> 18*
        if0(21,17,16) -> 18*
        if0(20,19,15) -> 18*
        if0(19,21,14) -> 18*
        if0(21,18,22) -> 18*
        if0(20,20,21) -> 18*
        if0(15,14,18) -> 18*
        if0(14,16,17) -> 18*
        if0(18,16,16) -> 18*
        if0(17,18,15) -> 18*
        if0(16,20,14) -> 18*
        if0(18,17,22) -> 18*
        if0(17,19,21) -> 18*
        if0(21,19,20) -> 18*
        if0(20,21,19) -> 18*
        if0(15,15,16) -> 18*
        if0(14,17,15) -> 18*
        if0(22,16,14) -> 18*
        if0(15,16,22) -> 18*
        if0(14,18,21) -> 18*
        if0(18,18,20) -> 18*
        if0(17,20,19) -> 18*
        if0(16,22,18) -> 18*
        if0(19,15,14) -> 18*
        if0(15,17,20) -> 18*
        if0(14,19,19) -> 18*
        if0(20,14,21) -> 18*
        if0(22,18,18) -> 18*
        if0(21,20,17) -> 18*
        if0(16,14,14) -> 18*
        if0(20,15,19) -> 18*
        if0(19,17,18) -> 18*
        if0(18,19,17) -> 18*
        if0(22,19,16) -> 18*
        if0(21,21,15) -> 18*
        if0(22,20,22) -> 18*
        if0(21,22,21) -> 18*
        if0(17,14,19) -> 18*
        if0(16,16,18) -> 18*
        if0(15,18,17) -> 18*
        if0(19,18,16) -> 18*
        if0(18,20,15) -> 18*
        if0(17,22,14) -> 18*
        if0(19,19,22) -> 18*
        if0(18,21,21) -> 18*
        if0(22,21,20) -> 18*
        if0(16,17,16) -> 18*
        if0(15,19,15) -> 18*
        if0(14,21,14) -> 18*
        if0(21,14,17) -> 18*
        if0(16,18,22) -> 18*
        if0(15,20,21) -> 18*
        if0(19,20,20) -> 15,21,18
        if0(18,22,19) -> 18*
        if0(21,15,15) -> 18*
        if0(20,17,14) -> 18*
        if0(16,19,20) -> 18*
        if0(15,21,19) -> 18*
        if0(22,14,22) -> 18*
        if0(21,16,21) -> 18*
        if0(22,22,17) -> 18*
        if0(18,14,15) -> 18*
        if0(17,16,14) -> 18*
        if0(18,15,21) -> 18*
        if0(22,15,20) -> 18*
        if0(21,17,19) -> 18*
        if0(20,19,18) -> 18*
        if0(19,21,17) -> 18*
        if0(14,15,14) -> 18*
        if0(15,14,21) -> 18*
        if0(19,14,20) -> 18*
        if0(18,16,19) -> 18*
        if0(17,18,18) -> 18*
        if0(16,20,17) -> 18*
        if0(20,20,16) -> 18*
        if0(19,22,15) -> 18*
        if0(20,21,22) -> 18*
        if0(15,15,19) -> 18*
        if0(14,17,18) -> 18*
        if0(17,19,16) -> 18*
        if0(16,21,15) -> 18*
        if0(22,16,17) -> 18*
        if0(17,20,22) -> 18*
        if0(16,22,21) -> 18*
        if0(20,22,20) -> 18*
        if0(14,18,16) -> 18*
        if0(19,15,17) -> 18*
        if0(22,17,15) -> 18*
        if0(21,19,14) -> 18*
        if0(14,19,22) -> 18*
        if0(17,21,20) -> 18*
        if0(22,18,21) -> 18*
        if0(16,14,17) -> 18*
        if0(20,14,16) -> 18*
        if0(19,16,15) -> 18*
        if0(18,18,14) -> 18*
        if0(14,20,20) -> 18*
        if0(20,15,22) -> 18*
        if0(19,17,21) -> 18*
        if0(22,19,19) -> 18*
        if0(21,21,18) -> 18*
        if0(16,15,15) -> 18*
        if0(15,17,14) -> 18*
        if0(17,14,22) -> 18*
        if0(16,16,21) -> 18*
        if0(20,16,20) -> 18*
        if0(19,18,19) -> 18*
        if0(18,20,18) -> 18*
        if0(17,22,17) -> 18*
        if0(21,22,16) -> 18*
        if0(17,15,20) -> 18*
        if0(16,17,19) -> 18*
        if0(15,19,18) -> 18*
        if0(14,21,17) -> 18*
        if0(18,21,16) -> 18*
        if0(18,22,22) -> 18*
        if0(14,14,20) -> 18*
        if0(15,20,16) -> 18*
        if0(14,22,15) -> 18*
        if0(21,15,18) -> 18*
        if0(20,17,17) -> 18*
        if0(22,21,14) -> 18*
        if0(15,21,22) -> 18*
        if0(18,14,18) -> 18*
        if0(17,16,17) -> 18*
        if0(21,16,16) -> 18*
        if0(20,18,15) -> 18*
        if0(19,20,14) -> 18*
        if0(15,22,20) -> 18*
        if0(21,17,22) -> 18*
        if0(20,19,21) -> 18*
        if0(14,15,17) -> 18*
        if0(18,15,16) -> 18*
        if0(17,17,15) -> 18*
        if0(16,19,14) -> 18*
        if0(18,16,22) -> 18*
        if0(17,18,21) -> 18*
        if0(21,18,20) -> 18*
        if0(20,20,19) -> 18*
        if0(19,22,18) -> 18*
        if0(15,14,16) -> 18*
        if0(14,16,15) -> 18*
        if0(22,15,14) -> 18*
        if0(15,15,22) -> 18*
        if0(14,17,21) -> 18*
        if0(18,17,20) -> 18*
        if0(17,19,19) -> 18*
        if0(16,21,18) -> 18*
        if0(19,14,14) -> 18*
        if0(15,16,20) -> 18*
        if0(14,18,19) -> 18*
        if0(16,22,16) -> 18*
        if0(22,17,18) -> 18*
        if0(21,19,17) -> 18*
        if0(20,14,19) -> 18*
        if0(19,16,18) -> 18*
        if0(18,18,17) -> 18*
        if0(22,18,16) -> 18*
        if0(21,20,15) -> 18*
        if0(20,22,14) -> 18*
        if0(22,19,22) -> 18*
        if0(21,21,21) -> 18*
        if0(16,15,18) -> 18*
        if0(15,17,17) -> 18*
        if0(19,17,16) -> 18*
        if0(18,19,15) -> 18*
        if0(17,21,14) -> 18*
        if0(19,18,22) -> 18*
        if0(18,20,21) -> 18*
        if0(22,20,20) -> 18*
        if0(21,22,19) -> 18*
        if0(16,16,16) -> 18*
        if0(15,18,15) -> 18*
        if0(14,20,14) -> 18*
        if0(16,17,22) -> 18*
        if0(15,19,21) -> 18*
        if0(19,19,20) -> 18*
        if0(18,21,19) -> 18*
        if0(21,14,15) -> 18*
        if0(20,16,14) -> 18*
        if0(16,18,20) -> 18*
        if0(15,20,19) -> 18*
        if0(14,22,18) -> 18*
        if0(21,15,21) -> 18*
        if0(22,21,17) -> 18*
        if0(17,15,14) -> 18*
        if0(18,14,21) -> 18*
        if0(22,14,20) -> 18*
        if0(21,16,19) -> 18*
        if0(20,18,18) -> 18*
        if0(19,20,17) -> 18*
        if0(22,22,15) -> 18*
        if0(14,14,14) -> 18*
        if0(18,15,19) -> 18*
        if0(17,17,18) -> 18*
        if0(16,19,17) -> 18*
        if0(20,19,16) -> 18*
        if0(19,21,15) -> 18*
        if0(20,20,22) -> 18*
        if0(19,22,21) -> 18*
        if0(15,14,19) -> 18*
        if0(14,16,18) -> 18*
        if0(17,18,16) -> 18*
        if0(16,20,15) -> 18*
        if0(15,22,14) -> 18*
        if0(22,15,17) -> 18*
        if0(17,19,22) -> 18*
        if0(16,21,21) -> 18*
        if0(20,21,20) -> 18*
        if0(14,17,16) -> 18*
        if0(19,14,17) -> 18*
        if0(22,16,15) -> 18*
        if0(21,18,14) -> 18*
        if0(14,18,22) -> 18*
        if0(17,20,20) -> 18*
        if0(16,22,19) -> 18*
        if0(22,17,21) -> 18*
        if0(19,15,15) -> 18*
        if0(18,17,14) -> 18*
        if0(14,19,20) -> 18*
        if0(20,14,22) -> 18*
        if0(19,16,21) -> 18*
        if0(22,18,19) -> 18*
        if0(21,20,18) -> 18*
        if0(20,22,17) -> 18*
        if0(16,14,15) -> 18*
        if0(15,16,14) -> 18*
        if0(16,15,21) -> 18*
        if0(20,15,20) -> 18*
        if0(19,17,19) -> 18*
        if0(18,19,18) -> 18*
        if0(17,21,17) -> 18*
        if0(21,21,16) -> 18*
        if0(21,22,22) -> 18*
        if0(17,14,20) -> 18*
        if0(16,16,19) -> 18*
        if0(15,18,18) -> 18*
        if0(14,20,17) -> 18*
        if0(18,20,16) -> 18*
        if0(17,22,15) -> 18*
        if0(18,21,22) -> 18*
        if0(15,19,16) -> 18*
        if0(14,21,15) -> 18*
        if0(21,14,18) -> 18*
        if0(20,16,17) -> 18*
        if0(22,20,14) -> 18*
        if0(15,20,22) -> 18*
        if0(14,22,21) -> 18*
        if0(18,22,20) -> 18*
        if0(17,15,17) -> 18*
        if0(21,15,16) -> 18*
        if0(20,17,15) -> 18*
        if0(19,19,14) -> 18*
        if0(15,21,20) -> 18*
        if0(21,16,22) -> 18*
        if0(20,18,21) -> 18*
        if0(22,22,18) -> 18*
        if0(14,14,17) -> 18*
        if0(18,14,16) -> 18*
        if0(17,16,15) -> 18*
        if0(16,18,14) -> 18*
        if0(18,15,22) -> 18*
        if0(17,17,21) -> 18*
        if0(21,17,20) -> 18*
        if0(20,19,19) -> 18*
        if0(19,21,18) -> 18*
        if0(14,15,15) -> 18*
        if0(22,14,14) -> 18*
        if0(15,14,22) -> 18*
        if0(14,16,21) -> 18*
        if0(18,16,20) -> 18*
        if0(17,18,19) -> 18*
        if0(16,20,18) -> 18*
        if0(15,22,17) -> 18*
        if0(19,22,16) -> 18*
        if0(15,15,20) -> 18*
        if0(14,17,19) -> 18*
        if0(16,21,16) -> 18*
        if0(22,16,18) -> 18*
        if0(21,18,17) -> 18*
        if0(16,22,22) -> 18*
        if0(19,15,18) -> 18*
        if0(18,17,17) -> 18*
        if0(22,17,16) -> 18*
        if0(21,19,15) -> 18*
        if0(20,21,14) -> 18*
        if0(22,18,22) -> 18*
        if0(21,20,21) -> 18*
        if0(16,14,18) -> 18*
        if0(15,16,17) -> 18*
        if0(19,16,16) -> 18*
        if0(18,18,15) -> 18*
        if0(17,20,14) -> 18*
        if0(19,17,22) -> 18*
        if0(18,19,21) -> 18*
        if0(22,19,20) -> 18*
        if0(21,21,19) -> 18*
        if0(16,15,16) -> 18*
        if0(15,17,15) -> 18*
        if0(14,19,14) -> 18*
        if0(16,16,22) -> 18*
        if0(15,18,21) -> 18*
        if0(19,18,20) -> 18*
        if0(18,20,19) -> 18*
        if0(17,22,18) -> 18*
        if0(20,15,14) -> 18*
        if0(16,17,20) -> 18*
        if0(15,19,19) -> 18*
        if0(14,21,18) -> 18*
        if0(21,14,21) -> 18*
        if0(22,20,17) -> 18*
        if0(17,14,14) -> 18*
        if0(14,22,16) -> 18*
        if0(21,15,19) -> 18*
        if0(20,17,18) -> 18*
        if0(19,19,17) -> 18*
        if0(22,21,15) -> 18*
        if0(22,22,21) -> 18*
        if0(18,14,19) -> 18*
        if0(17,16,18) -> 18*
        if0(16,18,17) -> 18*
        if0(20,18,16) -> 18*
        if0(19,20,15) -> 18*
        if0(18,22,14) -> 18*
        if0(20,19,22) -> 18*
        if0(19,21,21) -> 18*
        if0(14,15,18) -> 18*
        if0(17,17,16) -> 18*
        if0(16,19,15) -> 18*
        if0(15,21,14) -> 18*
        if0(22,14,17) -> 18*
        if0(17,18,22) -> 18*
        if0(16,20,21) -> 18*
        if0(20,20,20) -> 18*
        if0(19,22,19) -> 18*
        if0(14,16,16) -> 18*
        if0(22,15,15) -> 18*
        if0(21,17,14) -> 18*
        if0(14,17,22) -> 18*
        if0(17,19,20) -> 18*
        if0(16,21,19) -> 18*
        if0(22,16,21) -> 18*
        if0(19,14,15) -> 18*
        if0(18,16,14) -> 18*
        if0(14,18,20) -> 18*
        if0(19,15,21) -> 18*
        if0(22,17,19) -> 18*
        if0(21,19,18) -> 18*
        if0(20,21,17) -> 18*
        if0(15,15,14) -> 18*
        if0(16,14,21) -> 18*
        if0(20,14,20) -> 18*
        if0(19,16,19) -> 18*
        if0(18,18,18) -> 18*
        if0(17,20,17) -> 18*
        if0(21,20,16) -> 18*
        if0(20,22,15) -> 18*
        if0(21,21,22) -> 18*
        if0(16,15,19) -> 18*
        if0(15,17,18) -> 18*
        if0(14,19,17) -> 18*
        if0(18,19,16) -> 18*
        if0(17,21,15) -> 18*
        if0(18,20,22) -> 18*
        if0(17,22,21) -> 18*
        if0(21,22,20) -> 18*
        if0(15,18,16) -> 18*
        if0(14,20,15) -> 18*
        if0(20,15,17) -> 18*
        if0(22,19,14) -> 18*
        if0(15,19,22) -> 18*
        if0(14,21,21) -> 18*
        if0(18,21,20) -> 18*
        if0(17,14,17) -> 18*
        if0(21,14,16) -> 18*
        if0(20,16,15) -> 18*
        if0(19,18,14) -> 18*
        if0(15,20,20) -> 18*
        if0(14,22,19) -> 18*
        if0(21,15,22) -> 18*
        if0(20,17,21) -> 18*
        if0(22,21,18) -> 18*
        if0(17,15,15) -> 18*
        if0(16,17,14) -> 18*
        if0(18,14,22) -> 18*
        if0(17,16,21) -> 18*
        if0(21,16,20) -> 18*
        if0(20,18,19) -> 18*
        if0(19,20,18) -> 18*
        if0(18,22,17) -> 18*
        if0(22,22,16) -> 18*
        if0(14,14,15) -> 18*
        if0(14,15,21) -> 18*
        if0(18,15,20) -> 18*
        if0(17,17,19) -> 18*
        if0(16,19,18) -> 18*
        if0(15,21,17) -> 18*
        if0(19,21,16) -> 18*
        if0(19,22,22) -> 18*
        if0(15,14,20) -> 18*
        if0(14,16,19) -> 18*
        if0(16,20,16) -> 18*
        if0(15,22,15) -> 18*
        if0(22,15,18) -> 18*
        if0(21,17,17) -> 18*
        if0(16,21,22) -> 18*
        if0(19,14,18) -> 18*
        if0(18,16,17) -> 18*
        if0(22,16,16) -> 18*
        if0(21,18,15) -> 18*
        if0(20,20,14) -> 18*
        if0(16,22,20) -> 18*
        if0(22,17,22) -> 18*
        if0(21,19,21) -> 18*
        if0(15,15,17) -> 18*
        if0(19,15,16) -> 18*
        if0(18,17,15) -> 18*
        if0(17,19,14) -> 18*
        if0(19,16,22) -> 18*
        if0(18,18,21) -> 18*
        if0(22,18,20) -> 18*
        if0(21,20,19) -> 18*
        if0(20,22,18) -> 18*
        if0(16,14,16) -> 18*
        if0(15,16,15) -> 18*
        if0(14,18,14) -> 18*
        if0(16,15,22) -> 18*
        if0(15,17,21) -> 18*
        if0(19,17,20) -> 18*
        if0(18,19,19) -> 18*
        if0(17,21,18) -> 18*
        if0(20,14,14) -> 18*
        if0(16,16,20) -> 18*
        if0(15,18,19) -> 18*
        if0(14,20,18) -> 18*
        if0(17,22,16) -> 18*
        if0(22,19,17) -> 18*
        if0(14,21,16) -> 18*
        if0(21,14,19) -> 18*
        if0(20,16,18) -> 18*
        if0(19,18,17) -> 18*
        if0(22,20,15) -> 18*
        if0(21,22,14) -> 18*
        if0(14,22,22) -> 18*
        if0(22,21,21) -> 18*
        if0(17,15,18) -> 18*
        if0(16,17,17) -> 18*
        if0(20,17,16) -> 18*
        if0(19,19,15) -> 18*
        if0(18,21,14) -> 18*
        if0(20,18,22) -> 18*
        if0(19,20,21) -> 18*
        if0(22,22,19) -> 18*
        if0(14,14,18) -> 18*
        if0(17,16,16) -> 18*
        if0(16,18,15) -> 18*
        if0(15,20,14) -> 18*
        if0(17,17,22) -> 18*
        if0(16,19,21) -> 18*
        if0(20,19,20) -> 18*
        if0(19,21,19) -> 18*
        if0(14,15,16) -> 18*
        if0(22,14,15) -> 18*
        if0(21,16,14) -> 18*
        if0(14,16,22) -> 18*
        if0(17,18,20) -> 18*
        if0(16,20,19) -> 18*
        if0(15,22,18) -> 18*
        if0(22,15,21) -> 18*
        if0(18,15,14) -> 18*
        if0(14,17,20) -> 18*
        if0(19,14,21) -> 18*
        if0(22,16,19) -> 18*
        if0(21,18,18) -> 18*
        if0(20,20,17) -> 18*
        if0(15,14,14) -> 18*
        if0(19,15,19) -> 18*
        if0(18,17,18) -> 18*
        if0(17,19,17) -> 18*
        if0(21,19,16) -> 18*
        if0(20,21,15) -> 18*
        if0(21,20,22) -> 18*
        if0(20,22,21) -> 18*
        if0(16,14,19) -> 18*
        if0(15,16,18) -> 18*
        if0(14,18,17) -> 18*
        if0(18,18,16) -> 18*
        if0(17,20,15) -> 18*
        if0(16,22,14) -> 18*
        if0(18,19,22) -> 18*
        if0(17,21,21) -> 18*
        if0(21,21,20) -> 18*
        if0(15,17,16) -> 18*
        if0(14,19,15) -> 18*
        if0(20,14,17) -> 18*
        if0(22,18,14) -> 18*
        if0(15,18,22) -> 18*
        if0(14,20,21) -> 18*
        if0(18,20,20) -> 18*
        if0(17,22,19) -> 18*
        if0(20,15,15) -> 18*
        if0(19,17,14) -> 18*
        if0(15,19,20) -> 18*
        if0(14,21,19) -> 18*
        if0(21,14,22) -> 18*
        if0(20,16,21) -> 18*
        if0(22,20,18) -> 18*
        if0(21,22,17) -> 18*
        if0(17,14,15) -> 18*
        if0(16,16,14) -> 18*
        if0(17,15,21) -> 18*
        if0(21,15,20) -> 18*
        if0(20,17,19) -> 18*
        if0(19,19,18) -> 18*
        if0(18,21,17) -> 18*
        if0(22,21,16) -> 18*
        if0(22,22,22) -> 18*
        if0(14,14,21) -> 18*
        if0(18,14,20) -> 18*
        if0(17,16,19) -> 18*
        if0(16,18,18) -> 18*
        if0(15,20,17) -> 18*
        if0(19,20,16) -> 18*
        if0(18,22,15) -> 18*
        if0(19,21,22) -> 18*
        if0(14,15,19) -> 18*
        if0(16,19,16) -> 18*
        if0(15,21,15) -> 18*
        if0(22,14,18) -> 18*
        if0(21,16,17) -> 18*
        if0(16,20,22) -> 18*
        if0(15,22,21) -> 18*
        if0(19,22,20) -> 18*
        if0(18,15,17) -> 18*
        if0(22,15,16) -> 18*
        if0(21,17,15) -> 18*
        if0(20,19,14) -> 18*
        if0(16,21,20) -> 18*
        if0(22,16,22) -> 18*
        if0(21,18,21) -> 18*
        if0(15,14,17) -> 18*
        if0(19,14,16) -> 18*
        if0(18,16,15) -> 18*
        if0(17,18,14) -> 18*
        if0(19,15,22) -> 18*
        if0(18,17,21) -> 18*
        if0(22,17,20) -> 18*
        if0(21,19,19) -> 18*
        if0(20,21,18) -> 18*
        if0(15,15,15) -> 18*
        if0(14,17,14) -> 18*
        if0(16,14,22) -> 18*
        if0(15,16,21) -> 18*
        if0(19,16,20) -> 18*
        if0(18,18,19) -> 18*
        if0(17,20,18) -> 18*
        if0(16,22,17) -> 18*
        if0(20,22,16) -> 18*
        if0(16,15,20) -> 18*
        if0(15,17,19) -> 18*
        if0(14,19,18) -> 18*
        if0(17,21,16) -> 18*
        if0(22,18,17) -> 18*
        if0(17,22,22) -> 18*
        if0(14,20,16) -> 18*
        if0(20,15,18) -> 18*
        if0(19,17,17) -> 18*
        if0(22,19,15) -> 18*
        if0(21,21,14) -> 18*
        if0(14,21,22) -> 18*
        if0(22,20,21) -> 18*
        if0(17,14,18) -> 18*
        if0(16,16,17) -> 18*
        if0(20,16,16) -> 18*
        if0(19,18,15) -> 18*
        if0(18,20,14) -> 18*
        if0(14,22,20) -> 18*
        if0(20,17,22) -> 18*
        if0(19,19,21) -> 18*
        if0(22,21,19) -> 18*
        if0(17,15,16) -> 18*
        if0(16,17,15) -> 18*
        if0(15,19,14) -> 18*
        if0(17,16,22) -> 18*
        if0(16,18,21) -> 18*
        if0(20,18,20) -> 18*
        if0(19,20,19) -> 18*
        if0(18,22,18) -> 18*
        if0(14,14,16) -> 18*
        if0(21,15,14) -> 18*
        if0(14,15,22) -> 18*
        if0(17,17,20) -> 18*
        if0(16,19,19) -> 18*
        if0(15,21,18) -> 18*
        if0(22,14,21) -> 18*
        if0(18,14,14) -> 18*
        if0(14,16,20) -> 18*
        if0(15,22,16) -> 18*
        if0(22,15,19) -> 18*
        if0(21,17,18) -> 18*
        if0(20,19,17) -> 18*
        if0(19,14,19) -> 18*
        if0(18,16,18) -> 18*
        if0(17,18,17) -> 18*
        if0(21,18,16) -> 18*
        if0(20,20,15) -> 18*
        if0(19,22,14) -> 18*
        if0(21,19,22) -> 18*
        if0(20,21,21) -> 18*
        if0(15,15,18) -> 18*
        if0(14,17,17) -> 18*
        if0(18,17,16) -> 18*
        if0(17,19,15) -> 18*
        if0(16,21,14) -> 18*
        if0(18,18,22) -> 18*
        if0(17,20,21) -> 18*
        if0(21,20,20) -> 18*
        if0(20,22,19) -> 18*
        if0(15,16,16) -> 18*
        if0(14,18,15) -> 18*
        if0(22,17,14) -> 18*
        if0(15,17,22) -> 18*
        if0(14,19,21) -> 18*
        if0(18,19,20) -> 18*
        if0(17,21,19) -> 18*
        if0(20,14,15) -> 18*
        if0(19,16,14) -> 18*
        if0(15,18,20) -> 18*
        if0(14,20,19) -> 18*
        if0(20,15,21) -> 18*
        if0(22,19,18) -> 18*
        if0(21,21,17) -> 18*
        if0(16,15,14) -> 18*
        if0(17,14,21) -> 18*
        if0(21,14,20) -> 18*
        if0(20,16,19) -> 18*
        if0(19,18,18) -> 18*
        if0(18,20,17) -> 18*
        if0(22,20,16) -> 18*
        if0(21,22,15) -> 18*
        if0(22,21,22) -> 18*
        if0(17,15,19) -> 18*
        if0(16,17,18) -> 18*
        if0(15,19,17) -> 18*
        if0(19,19,16) -> 18*
        if0(18,21,15) -> 18*
        if0(19,20,22) -> 18*
        if0(18,22,21) -> 18*
        if0(22,22,20) -> 18*
        if0(14,14,19) -> 18*
        if0(16,18,16) -> 18*
        if0(15,20,15) -> 18*
        if0(14,22,14) -> 18*
        if0(21,15,17) -> 18*
        if0(16,19,22) -> 18*
        if0(15,21,21) -> 18*
        if0(19,21,20) -> 18*
        if0(18,14,17) -> 18*
        if0(22,14,16) -> 18*
        if0(21,16,15) -> 18*
        if0(20,18,14) -> 18*
        if0(16,20,20) -> 18*
        if0(15,22,19) -> 18*
        if0(22,15,22) -> 18*
        if0(21,17,21) -> 18*
        if0(18,15,15) -> 18*
        if0(17,17,14) -> 18*
        if0(19,14,22) -> 18*
        if0(18,16,21) -> 18*
        if0(22,16,20) -> 18*
        if0(21,18,19) -> 18*
        if0(20,20,18) -> 18*
        if0(19,22,17) -> 18*
        if0(15,14,15) -> 18*
        if0(14,16,14) -> 18*
        if0(15,15,21) -> 18*
        if0(19,15,20) -> 18*
        if0(18,17,19) -> 18*
        if0(17,19,18) -> 18*
        if0(16,21,17) -> 18*
        if0(20,21,16) -> 18*
        if0(20,22,22) -> 18*
        if0(16,14,20) -> 18*
        if0(15,16,19) -> 18*
        if0(14,18,18) -> 18*
        if0(17,20,16) -> 18*
        if0(16,22,15) -> 18*
        if0(22,17,17) -> 18*
        if0(17,21,22) -> 18*
        if0(14,19,16) -> 18*
        if0(20,14,18) -> 18*
        if0(19,16,17) -> 18*
        if0(22,18,15) -> 18*
        if0(21,20,14) -> 18*
        if0(14,20,22) -> 18*
        if0(17,22,20) -> 18*
        if0(22,19,21) -> 18*
        if0(16,15,17) -> 18*
        if0(20,15,16) -> 18*
        if0(19,17,15) -> 18*
        if0(18,19,14) -> 18*
        if0(14,21,20) -> 18*
        if0(20,16,22) -> 18*
        if0(19,18,21) -> 18*
        if0(22,20,19) -> 18*
        if0(21,22,18) -> 18*
        <=0(22,14) -> 19*
        <=0(17,14) -> 19*
        <=0(22,16) -> 19*
        <=0(17,16) -> 19*
        <=0(22,18) -> 19*
        <=0(17,18) -> 19*
        <=0(22,20) -> 19*
        <=0(17,20) -> 19*
        <=0(22,22) -> 19*
        <=0(17,22) -> 19*
        <=0(18,15) -> 19*
        <=0(18,17) -> 19*
        <=0(18,19) -> 19*
        <=0(18,21) -> 19*
        <=0(19,14) -> 19*
        <=0(14,14) -> 19*
        <=0(19,16) -> 19*
        <=0(14,16) -> 19*
        <=0(19,18) -> 19*
        <=0(14,18) -> 19*
        <=0(19,20) -> 19*
        <=0(14,20) -> 19*
        <=0(19,22) -> 19*
        <=0(14,22) -> 19*
        <=0(20,15) -> 19*
        <=0(15,15) -> 19*
        <=0(20,17) -> 19*
        <=0(15,17) -> 19*
        <=0(20,19) -> 19*
        <=0(15,19) -> 19*
        <=0(20,21) -> 19*
        <=0(15,21) -> 19*
        <=0(21,14) -> 19*
        <=0(16,14) -> 19*
        <=0(21,16) -> 19*
        <=0(16,16) -> 19*
        <=0(21,18) -> 19*
        <=0(16,18) -> 19*
        <=0(21,20) -> 19*
        <=0(16,20) -> 19*
        <=0(21,22) -> 19*
        <=0(16,22) -> 19*
        <=0(22,15) -> 19*
        <=0(17,15) -> 19*
        <=0(22,17) -> 19*
        <=0(17,17) -> 19*
        <=0(22,19) -> 19*
        <=0(17,19) -> 19*
        <=0(22,21) -> 19*
        <=0(17,21) -> 19*
        <=0(18,14) -> 19*
        <=0(18,16) -> 19*
        <=0(18,18) -> 19*
        <=0(18,20) -> 19*
        <=0(18,22) -> 19*
        <=0(19,15) -> 19*
        <=0(14,15) -> 19*
        <=0(19,17) -> 19*
        <=0(14,17) -> 19*
        <=0(19,19) -> 19*
        <=0(14,19) -> 19*
        <=0(19,21) -> 19*
        <=0(14,21) -> 19*
        <=0(20,14) -> 19*
        <=0(15,14) -> 19*
        <=0(20,16) -> 19*
        <=0(15,16) -> 19*
        <=0(20,18) -> 19*
        <=0(15,18) -> 19*
        <=0(20,20) -> 19*
        <=0(15,20) -> 19*
        <=0(20,22) -> 19*
        <=0(15,22) -> 19*
        <=0(21,15) -> 19*
        <=0(16,15) -> 19*
        <=0(21,17) -> 19*
        <=0(16,17) -> 19*
        <=0(21,19) -> 19*
        <=0(16,19) -> 19*
        <=0(21,21) -> 19*
        <=0(16,21) -> 19*
        bsort{#,0}(22) -> 9*
        .0(22,14) -> 14,20
        .0(17,14) -> 14,20
        .0(22,16) -> 20*
        .0(17,16) -> 20*
        .0(22,18) -> 20*
        .0(17,18) -> 20*
        .0(22,20) -> 20*
        .0(17,20) -> 20*
        .0(22,22) -> 20*
        .0(17,22) -> 20*
        .0(18,15) -> 20*
        .0(18,17) -> 21,20
        .0(18,19) -> 20*
        .0(18,21) -> 20*
        .0(19,14) -> 14,20
        .0(14,14) -> 14,20
        .0(19,16) -> 20*
        .0(14,16) -> 20*
        .0(19,18) -> 20*
        .0(14,18) -> 20*
        .0(19,20) -> 20*
        .0(14,20) -> 20*
        .0(19,22) -> 20*
        .0(14,22) -> 20*
        .0(20,15) -> 20*
        .0(15,15) -> 20*
        .0(20,17) -> 21,20
        .0(15,17) -> 21,20
        .0(20,19) -> 20*
        .0(15,19) -> 20*
        .0(20,21) -> 20*
        .0(15,21) -> 20*
        .0(21,14) -> 14,20
        .0(16,14) -> 15,14,20
        .0(21,16) -> 20*
        .0(16,16) -> 20*
        .0(21,18) -> 20*
        .0(16,18) -> 20*
        .0(21,20) -> 20*
        .0(16,20) -> 20*
        .0(21,22) -> 20*
        .0(16,22) -> 20*
        .0(22,15) -> 20*
        .0(17,15) -> 20*
        .0(22,17) -> 21,20
        .0(17,17) -> 21,20
        .0(22,19) -> 20*
        .0(17,19) -> 20*
        .0(22,21) -> 20*
        .0(17,21) -> 20*
        .0(18,14) -> 15,20
        .0(18,16) -> 20*
        .0(18,18) -> 20*
        .0(18,20) -> 20*
        .0(18,22) -> 20*
        .0(19,15) -> 20*
        .0(14,15) -> 20*
        .0(19,17) -> 21,20
        .0(14,17) -> 21,20
        .0(19,19) -> 20*
        .0(14,19) -> 20*
        .0(19,21) -> 20*
        .0(14,21) -> 20*
        .0(20,14) -> 15,20
        .0(15,14) -> 15,20
        .0(20,16) -> 20*
        .0(15,16) -> 20*
        .0(20,18) -> 20*
        .0(15,18) -> 20*
        .0(20,20) -> 20*
        .0(15,20) -> 20*
        .0(20,22) -> 20*
        .0(15,22) -> 20*
        .0(21,15) -> 20*
        .0(16,15) -> 20*
        .0(21,17) -> 21,20
        .0(16,17) -> 21,20
        .0(21,19) -> 20*
        .0(16,19) -> 20*
        .0(21,21) -> 20*
        .0(16,21) -> 20*
        14 -> 16*
        15 -> 16*
        17 -> 16*
        18 -> 16*
        19 -> 16*
        20 -> 16*
        21 -> 16*
        22 -> 16*
      problem:
       DPs:
        
       TRS:
        f13(x,y) -> x
        f13(x,y) -> y
        bubble(.(x,nil())) -> .(x,nil())
        bubble(.(x,.(y,z))) -> if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))
        butlast(nil()) -> nil()
        butlast(.(x,nil())) -> nil()
        butlast(.(x,.(y,z))) -> .(x,butlast(.(y,z)))
      Qed
    
    DPs:
     butlast#(.(x,.(y,z))) -> butlast#(.(y,z))
    TRS:
     bsort(nil()) -> nil()
     bsort(.(x,y)) -> last(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))
     bubble(nil()) -> nil()
     bubble(.(x,nil())) -> .(x,nil())
     bubble(.(x,.(y,z))) -> if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))
     last(nil()) -> 0()
     last(.(x,nil())) -> x
     last(.(x,.(y,z))) -> last(.(y,z))
     butlast(nil()) -> nil()
     butlast(.(x,nil())) -> nil()
     butlast(.(x,.(y,z))) -> .(x,butlast(.(y,z)))
    Subterm Criterion Processor:
     simple projection:
      pi(butlast#) = 0
     problem:
      DPs:
       
      TRS:
       bsort(nil()) -> nil()
       bsort(.(x,y)) -> last(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))
       bubble(nil()) -> nil()
       bubble(.(x,nil())) -> .(x,nil())
       bubble(.(x,.(y,z))) -> if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))
       last(nil()) -> 0()
       last(.(x,nil())) -> x
       last(.(x,.(y,z))) -> last(.(y,z))
       butlast(nil()) -> nil()
       butlast(.(x,nil())) -> nil()
       butlast(.(x,.(y,z))) -> .(x,butlast(.(y,z)))
     Qed
    
    DPs:
     bubble#(.(x,.(y,z))) -> bubble#(.(y,z))
     bubble#(.(x,.(y,z))) -> bubble#(.(x,z))
    TRS:
     bsort(nil()) -> nil()
     bsort(.(x,y)) -> last(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))
     bubble(nil()) -> nil()
     bubble(.(x,nil())) -> .(x,nil())
     bubble(.(x,.(y,z))) -> if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))
     last(nil()) -> 0()
     last(.(x,nil())) -> x
     last(.(x,.(y,z))) -> last(.(y,z))
     butlast(nil()) -> nil()
     butlast(.(x,nil())) -> nil()
     butlast(.(x,.(y,z))) -> .(x,butlast(.(y,z)))
    Usable Rule Processor:
     DPs:
      bubble#(.(x,.(y,z))) -> bubble#(.(y,z))
      bubble#(.(x,.(y,z))) -> bubble#(.(x,z))
     TRS:
      
     Bounds Processor:
      bound: 0
      enrichment: match-dp
      automaton:
       final states: {4}
       transitions:
        bubble{#,0}(6) -> 4*
        .0(5,5) -> 6*
        f220() -> 5*
      problem:
       DPs:
        bubble#(.(x,.(y,z))) -> bubble#(.(y,z))
       TRS:
        
      Restore Modifier:
       DPs:
        bubble#(.(x,.(y,z))) -> bubble#(.(y,z))
       TRS:
        bsort(nil()) -> nil()
        bsort(.(x,y)) -> last(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))
        bubble(nil()) -> nil()
        bubble(.(x,nil())) -> .(x,nil())
        bubble(.(x,.(y,z))) -> if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))
        last(nil()) -> 0()
        last(.(x,nil())) -> x
        last(.(x,.(y,z))) -> last(.(y,z))
        butlast(nil()) -> nil()
        butlast(.(x,nil())) -> nil()
        butlast(.(x,.(y,z))) -> .(x,butlast(.(y,z)))
       Subterm Criterion Processor:
        simple projection:
         pi(bubble#) = 0
        problem:
         DPs:
          
         TRS:
          bsort(nil()) -> nil()
          bsort(.(x,y)) -> last(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))
          bubble(nil()) -> nil()
          bubble(.(x,nil())) -> .(x,nil())
          bubble(.(x,.(y,z))) -> if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))
          last(nil()) -> 0()
          last(.(x,nil())) -> x
          last(.(x,.(y,z))) -> last(.(y,z))
          butlast(nil()) -> nil()
          butlast(.(x,nil())) -> nil()
          butlast(.(x,.(y,z))) -> .(x,butlast(.(y,z)))
        Qed
    
    DPs:
     last#(.(x,.(y,z))) -> last#(.(y,z))
    TRS:
     bsort(nil()) -> nil()
     bsort(.(x,y)) -> last(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))
     bubble(nil()) -> nil()
     bubble(.(x,nil())) -> .(x,nil())
     bubble(.(x,.(y,z))) -> if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))
     last(nil()) -> 0()
     last(.(x,nil())) -> x
     last(.(x,.(y,z))) -> last(.(y,z))
     butlast(nil()) -> nil()
     butlast(.(x,nil())) -> nil()
     butlast(.(x,.(y,z))) -> .(x,butlast(.(y,z)))
    Subterm Criterion Processor:
     simple projection:
      pi(last#) = 0
     problem:
      DPs:
       
      TRS:
       bsort(nil()) -> nil()
       bsort(.(x,y)) -> last(.(bubble(.(x,y)),bsort(butlast(bubble(.(x,y))))))
       bubble(nil()) -> nil()
       bubble(.(x,nil())) -> .(x,nil())
       bubble(.(x,.(y,z))) -> if(<=(x,y),.(y,bubble(.(x,z))),.(x,bubble(.(y,z))))
       last(nil()) -> 0()
       last(.(x,nil())) -> x
       last(.(x,.(y,z))) -> last(.(y,z))
       butlast(nil()) -> nil()
       butlast(.(x,nil())) -> nil()
       butlast(.(x,.(y,z))) -> .(x,butlast(.(y,z)))
     Qed