It does two things concurrently: (1) search for an algorithm along with proofs for its correctness and time upper bound (2) run the fastest algorithm found so far, possibly aborting an slower algorithm when a faster one is found.

Everything is scheduled so it's asymptotically optimal. However, there's an added cost to search for algorithms. This cost is exponential in the proof length, but constant for each problem since it is independent from the inputs. Of course, this constant is ridiculously huge.

First you vote once, and then you vote again.

@theemathas thanks, @pwdisswordfish - nice one :D