Once assertion checking is working properly we should figure out if sorting the terms by size improves the speed. The hypotheses are:
1) that a greedy approach (grab the log running assertions first) helps
2) that term size is (often enough) related to run time
Both hypotheses are not true in general but hopefully in practice.
Nope, term size is not a good heuristic as we pointed out in a paper two years ago. Curse you Alzheimer's ...