MAYBE
Time: 0.004469
TRS:
 {          bsort nil() -> nil(),
          bsort .(x, y) -> last .(bubble .(x, y), bsort butlast bubble .(x, y)),
             last nil() -> 0(),
       last .(x, nil()) -> x,
     last .(x, .(y, z)) -> last .(y, z),
           bubble nil() -> nil(),
     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))}
 DP:
  DP:
   {        bsort# .(x, y) -> bsort# butlast bubble .(x, y),
            bsort# .(x, y) -> last# .(bubble .(x, y), bsort butlast bubble .(x, y)),
            bsort# .(x, y) -> bubble# .(x, y),
            bsort# .(x, y) -> butlast# bubble .(x, y),
       last# .(x, .(y, z)) -> last# .(y, z),
     bubble# .(x, .(y, z)) -> bubble# .(x, z),
     bubble# .(x, .(y, z)) -> bubble# .(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)),
              last nil() -> 0(),
        last .(x, nil()) -> x,
      last .(x, .(y, z)) -> last .(y, z),
            bubble nil() -> nil(),
      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))}
  EDG:
   {(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))
    (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) -> bsort# butlast bubble .(x, y), bsort# .(x, y) -> 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)))
    (bsort# .(x, y) -> bsort# butlast bubble .(x, y), bsort# .(x, y) -> bsort# butlast bubble .(x, y))
    (bsort# .(x, y) -> last# .(bubble .(x, y), bsort butlast bubble .(x, y)), last# .(x, .(y, z)) -> last# .(y, z))
    (bubble# .(x, .(y, z)) -> bubble# .(y, z), bubble# .(x, .(y, z)) -> bubble# .(x, z))
    (bubble# .(x, .(y, z)) -> bubble# .(y, z), bubble# .(x, .(y, z)) -> bubble# .(y, z))
    (last# .(x, .(y, z)) -> last# .(y, z), last# .(x, .(y, z)) -> last# .(y, z))
    (bsort# .(x, y) -> butlast# bubble .(x, y), butlast# .(x, .(y, z)) -> butlast# .(y, z))}
   STATUS:
    arrows: 0.781250
    SCCS (4):
     Scc:
      {bsort# .(x, y) -> bsort# butlast bubble .(x, y)}
     Scc:
      {last# .(x, .(y, z)) -> last# .(y, z)}
     Scc:
      {bubble# .(x, .(y, z)) -> bubble# .(x, z),
       bubble# .(x, .(y, z)) -> bubble# .(y, z)}
     Scc:
      {butlast# .(x, .(y, z)) -> butlast# .(y, z)}
     
     SCC (1):
      Strict:
       {bsort# .(x, y) -> bsort# butlast bubble .(x, y)}
      Weak:
      {          bsort nil() -> nil(),
               bsort .(x, y) -> last .(bubble .(x, y), bsort butlast bubble .(x, y)),
                  last nil() -> 0(),
            last .(x, nil()) -> x,
          last .(x, .(y, z)) -> last .(y, z),
                bubble nil() -> nil(),
          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))}
      Open
     
     SCC (1):
      Strict:
       {last# .(x, .(y, z)) -> last# .(y, z)}
      Weak:
      {          bsort nil() -> nil(),
               bsort .(x, y) -> last .(bubble .(x, y), bsort butlast bubble .(x, y)),
                  last nil() -> 0(),
            last .(x, nil()) -> x,
          last .(x, .(y, z)) -> last .(y, z),
                bubble nil() -> nil(),
          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))}
      Open
     
     SCC (2):
      Strict:
       {bubble# .(x, .(y, z)) -> bubble# .(x, z),
        bubble# .(x, .(y, z)) -> bubble# .(y, z)}
      Weak:
      {          bsort nil() -> nil(),
               bsort .(x, y) -> last .(bubble .(x, y), bsort butlast bubble .(x, y)),
                  last nil() -> 0(),
            last .(x, nil()) -> x,
          last .(x, .(y, z)) -> last .(y, z),
                bubble nil() -> nil(),
          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))}
      Open
     
     SCC (1):
      Strict:
       {butlast# .(x, .(y, z)) -> butlast# .(y, z)}
      Weak:
      {          bsort nil() -> nil(),
               bsort .(x, y) -> last .(bubble .(x, y), bsort butlast bubble .(x, y)),
                  last nil() -> 0(),
            last .(x, nil()) -> x,
          last .(x, .(y, z)) -> last .(y, z),
                bubble nil() -> nil(),
          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))}
      Open