The method not very interesting. The result is the 71 division candidates of sizes (15,3) and (15,4) satisfying the basic constraints.
mace4 < div.in > div.outIt turns out that the countermodel kills all 71 candidates. First, extract the countermodel from the Mace4 output.
get_interps < div.out > interps.div-15Then, check all 71 candidates against that countermodel.
modfilter interps.div-15 false_in_all < cand-div-15 > cand.final