Operational Semantic
Upon invocation, the CS should always return immediately
- with failure, if the new constraint is inconsistent with the others
- with a partially-instantiated proof object, if the constraint is consistent
Backtracking should usually fail on a constraint, even if there are other proofs