TIMEOUT We are left with following problem, upon which TcT provides the certificate TIMEOUT. Strict 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))) } Obligation: innermost runtime complexity Answer: TIMEOUT Computation stopped due to timeout after 60.0 seconds. Arrrr..