W. McCune, R. Padmanabhan, M. A. Rose, R. Veroff, "Short Equational Bases for Ortholattices: Proofs and Countermodels," Technical Memorandum ANL/MCS-TM-265, September 2003.
This document contains proofs and countermodels in support of the paper "Short Equational Bases for Ortholattices'', by the same set of authors. In that paper, short single axioms for ortholattices, orthomodular lattices, and modular ortholattices are
presented, all in terms of the Sheffer stroke. The ortholattice axiom is the shortest possible. Other equational bases in terms of the Sheffer stroke and in terms of join, meet, and complement are presented. Computers were used extensively to find candidates, reject candidates, and search for proofs that candidates are single axioms.