The file Sheffer-mgi-without-mirrors contains 352 Boolean algebra identities in terms of the Sheffer stroke. Every such identity of length up through 15, or its mirror image, is subsumed by a member of that file.
The Perl program commute4_filter goes through a file of equations (one equation per line) and calls MACE4 for each, looking for a noncommutative model of size up through 4. If none exists, the equation is printed.
The command
commute4_filter < Sheffer-mgi-without-mirrors > candidatesshould produce 25 candidates in a few seconds.
This process eliminates candidates that are too weak to be single axioms for Boolean Algebra in terms of the Sheffer Stroke, because they have noncommutative models.
NOTE: You might have to edit commute4_filter to point it at the MACE4 binary.
These activities are projects of the Mathematics and Computer Science Division of Argonne National Laboratory.