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