This is an interesting early use of computer proof search. McCune also worked on a single axiom for boolean algebra, again in 1996 https://en.wikipedia.org/wiki

This is an interesting early use of computer proof search. McCune also worked on a single axiom for boolean algebra, again in 1996 https://en.wikipedia.org/wiki/Minimal_axioms_for_Boolean_algebra https://en.wikipedia.org/wiki/Minimal_axioms_for_Boolean_alg...