The state of a proof, contains a set of active clauses (processed),
a set of passive clauses (to be processed), and an ordering
that is used for redundancy elimination.
module type S =
Create a Proof State
with module C = C and module Ctx = C.Ctx