IC3 is one of the most influential unbounded model checking algorithms. It has inspired many top hardware model checking algorithms like PDR, QUIP, AVY and TRUSS. A unique feature of IC3 is its incremental reasoning: a proof is constructed by putting together many lemmas that support the proof. QUIP takes this a step further by prioritizing proving support lemmas over proving the property itself. Since these lemmas are interdependent, the order in which they are proven has a huge impact on the performance of the algorithm. The dynamic nature of such dependencies make it challenging to figure out an ordering of the lemmas. We frame this as an optimization problem and come up with a data driven approach to solving it.