Given a candidate that passed all of the current filters, we asked Mace to find countermodels to serve as filters for the given candidate and subsequent candidates.
Other countermodels were found with Mace4 by giving a candidate, stating that some of the properties of OLs hold, and other OL properties fail. For example,
mace4 -N10 < OL-cand-c1.in > OL-cand-c1.out
These methods produced many models, up through size 8. Many of filters became redundant, however, because later models would do the jobs of earlier models. Because we were filtering large numbers of candidates, we wished to keep the number of filters small, so we eliminated many of the redundant filters. We arrived at the filter sets non-OL.A-4 and non-OL.B-9 in this way.
all x all y exists z (x * z = y). all x all y exists z (z * x = y).The Sheffer stroke operation of a nontrivial ortholattice cannot be a quasigroup. Therefore any OL, OML, or MOL candidate with a nontrivial quasigoup model cannot be a single axiom.
Here is an example. Consider the OML candidate
f(f(f(y,x),x),f(f(f(z,x),f(y,x)),f(f(y,y),z))) = x.This candidate passed the filters non-OL.A-4 and non-OL.B-9. Mace4 searches for noncommutative models failed (allowing several hours), but a Mace4 search for a quasigroup model quickly found a quasigroup of size 7, which happens to be noncommutative:
mace4 -N10 < OML-cand-qg.in > OML-cand-qg.outThat structure became a member of non-OL.C-23.
interpfilter modularity nonmodels < OML.16 > nonmod-OML.16
Theory | Size | Step-8 | Step-9 |
OL | all | OL decision procedure | non-OL.A-4 |
OML | <= 19 | OML.6 | non-OL.B-9 |
21,23 | OML.6 OML.10 |
non-OL.C-23 | |
MOL | <= 19 | MOL.6 (= OML.6) | non-OL.B-9 |
21,23,25,27 | MOL.6 (= OML.6) | non-OL.C-23 non-OL.D-14 non-MOL-OML |