Create stackable recorders
Enforce total ordering between write events

This encoding is slightly different from the literature in that it uses
disjunction instead of implication. In addition, the encoding guards
both possible orderings by a single antecedent.