MAYBE
Time: 0.030747
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))}
   SCCS (4):
    Scc:
     {butlast# .(x, .(y, z)) -> butlast# .(y, z)}
    Scc:
     {bubble# .(x, .(y, z)) -> bubble# .(x, z),
      bubble# .(x, .(y, z)) -> bubble# .(y, z)}
    Scc:
     {last# .(x, .(y, z)) -> last# .(y, z)}
    Scc:
     {bsort# .(x, y) -> bsort# butlast bubble .(x, y)}
    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))}
     SPSC:
      Simple Projection:
       pi(butlast#) = 0
      Strict:
       {}
      Qed
    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))}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [if](x0, x1, x2) = x0 + 1,
       
       [.](x0, x1) = x0 + 1,
       
       [<=](x0, x1) = 0,
       
       [bsort](x0) = x0 + 1,
       
       [last](x0) = x0,
       
       [bubble](x0) = x0 + 1,
       
       [butlast](x0) = 0,
       
       [nil] = 1,
       
       [0] = 0,
       
       [bubble#](x0) = x0
      Strict:
       bubble# .(x, .(y, z)) -> bubble# .(y, z)
       2 + 0x + 0y + 1z >= 1 + 0y + 1z
       bubble# .(x, .(y, z)) -> bubble# .(x, z)
       2 + 0x + 0y + 1z >= 1 + 0x + 1z
      Weak:
       
     Qed
   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))}
    SPSC:
     Simple Projection:
      pi(last#) = 0
     Strict:
      {}
     Qed
   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))}
    Fail