MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { msort(nil()) -> nil() , msort(.(x, y)) -> .(min(x, y), msort(del(min(x, y), .(x, y)))) , min(x, nil()) -> x , min(x, .(y, z)) -> if(<=(x, y), min(x, z), min(y, z)) , del(x, nil()) -> nil() , del(x, .(y, z)) -> if(=(x, y), z, .(y, del(x, z))) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..