Footnote

The current implementation does this by ordering to minimise backward dependencies, then adjusting the start of the sequence so that most dependents of assumable clauses are at the end. The partition takes at most one extra iteration to complete. This algorithm seems to work well.