Summary. We can eliminate all OML Sheffer stroke candidates up through length 19, we can eliminate all all but 58 candidates of length 21, and we present a single axiom of length 23.
Generating equations satisfying properties 1--7 is the same as in the OL case. However, for property 8, we do not have a decision procedure for OML identities. Therefore, we check against a small set of OMLs.
Note that in this case, any unsound candidates that slipped through step 8 are killed in step 9.
We have not found proofs or countermodels for any of the 58 surviving candidates. Recall that the method we used to produce the 58 candidates does not necessarily produce OML identities, but we have used Otter to show that 40 of the 58 (enumerate/OML/21/sound/58-denials.out) are OML identities.
When we told Norm Megill about this work, he proved (by hand, using the Foulis-Holland theorem) that the remaining 18 OML candidates are, in fact, OML identities.
The script enumerate/OML/23/go does that and then sends those candidates to ploop3 which calls Otter for each candidate. Otter proved several of the 3053 candidates to be single axioms, including the following.
f(f(f(f(y,x),f(x,z)),u),f(x,f(f(z,f(f(x,x),z)),z))) = x. % OML-ShRecall that the method for OML does not necessarily produce OML identities, so we have to give a soundness proof as well as a completeness proof.
otter < OML-Sh.in > OML-Sh.out otter < OML-Sh-jc.in > OML-Sh-jc.out
otter < OML-Sh-sound.in > OML-Sh-sound.out