Invariant Printing

This treatment minimizes the invariants used in the proof of the valid properties, and shows them in the output without logging them on disk.