# Division

## Generating Candidates

(Not written yet.)
The method not very interesting. The result is the
71 division candidates of sizes (15,3) and (15,4)
satisfying the basic constraints.

## Finding the Counterexample

Here is a Mace4 job with one of the 71 candidates.
Note that it has an extra constraint *x / x = 0*.
mace4 < div.in > div.out

It turns out that the countermodel kills all 71 candidates.
First, extract the countermodel from the Mace4 output.
get_interps < div.out > interps.div-15

Then, check all 71 candidates against that countermodel.
modfilter interps.div-15 false_in_all < cand-div-15 > cand.final