# Product and Inverse

## Generating Candidates

(Not written yet.)
The method not very interesting. The result is the
20,568 product/inverse candidates of size (18,3)
satisfying the basic constraints.

## Finding the Counterexamples

This section contains a (cleaned-up) account of how the countermodels were found.
In particular, it doesn't show the jobs that failed to find countermodels.
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.filtered

The 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 > cand5

Next 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 > cand7

Then 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 > cand8

Thirty-six candidates remain.
(Some of those can be derived from others, and
others can be completed, showing they are not single axioms.)

## Update, May 2007

In the Spring of 2007,
Michael Kinyon
joined the project and made several important contributions.
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.

*By "complete", we mean that if we apply
Knuth-Bendix completion
to the candidate, the procedure terminates without deriving
enough to be a basis for group theory. This shows that the candidate
is not a single axiom, but it does not produce an explicit counterexample.