The method not very interesting. The result is the 20,568 product/inverse candidates of size (18,3) satisfying the basic constraints.
We used a Perl script called attack, which collects a set of countermodels and filters candidates w.r.t. those countermodels. Attack takes two filename as arguments, reads a stream of candidates from the standard input, and writes filtered candidates to the standard ouput. For example,
attack head interps < candidates > candidates.filteredThe file "head" is a Mace4 input file, and "interps" (which must not exist when attack is called) is the set of structures that is constructed during execution of the command.
We have 20,568 candidates in cand0, and we start attacking.
attack head.2-3 interps.2-3 < cand0 > cand1 attack head.r9 interps.r9 < cand1 > cand2 attack head.r29 interps.r29 < cand2 > cand3 attack head.da10 interps.da10 < cand3 > cand5Next we ran a simple Mace4 job, without a candidate, to get all nonassociative diassociative inverse loops (is that what they're called??) of size 12. We get 16 of them; we could run isofilter to get rid of the isomorphic ones (leaving 2), but that takes a half an hour and is not necessary here.
mace4 -n12 -m -1 < da.in | get_interps > interps.da12 modfilter interps.da12 false_in_all < cand5 > cand6 attack head.r41 interps.r41 < cand6 > cand7Then we ran some Otter jobs on the candidates. One of them seemed close to being a single axiom, deriving all but associativity, so we ran some Mace4 jobs, including a lot of group-like properties that were derived. A size-16 countermodel was found, which eliminated that candidate and 5 others.
mace4 < da16.in | get_interps > interps.da16 modfilter interps.da16 false_in_all < cand7 > cand8Thirty-six candidates remain. (Some of those can be derived from others, and others can be completed, showing they are not single axioms.)
Six more candidates were eliminated, four of the remaining candidates were shown to be equivalent, and several insights arose.
Kinyon's email summary.
From the 36 candidates, if we remove the four that complete*, the six with finite counterexamples, and three that are redundant because they are equivalent to another, we are left with 23 candidates.