Let K be an equational class of lattices such that no lattice in K contains an
+M3 (= the unique 5-element lattice with three atoms, 0 and 1, like a pumpkin).
+For example, the variety of all lattices generated by the non-modular pentagon
+lattice N5 is one such variety.

Conjecture:
Every uniquely complemented lattice in K is distributive.

One method of proving this result using Prover9.
Find an implication (say, **, a Horn sentence) that is equivalent to the
+non-occurrence of M3 as a sublattice.
Assume lattice axioms, unique complementation as well as the above implication
+**. Ask Prover9 to prove distributivity (equivalently, non-occurrence of N5).

One useful reference in this context:
Padmanabhan, R; McCune, W; Veroff, R.
Lattice laws forcing distributivity under unique complementation.
Houston J. Math. 33 (2007), no. 2, 391?401