CPU Times

Depth of convergence

Size of Invariant (Number of clauses)

Time spent on Extending trace

Time spent searching for extension level