Prover9 Examples: Lattice Theory Single Axioms

See

W. McCune and R. Padmanabhan and R. Veroff, "Yet another single law for lattices", Algebra Universalis 50(2), pp. 165--169 (2003).

and

http://www.mcs.anl.gov/~mccune/papers/ltsax/.

Starting with a single axiom (a1) for lattice theory, prove McKenzie's 4-basis.

prover9 -f a1.in > a1.out ; ### ( a1.out.xml )

Same for single axiom (a2).

prover9 -f a2.in > a2.out ; ### ( a2.out.xml )

Starting with McKenzie's 4-basis for LT, prove a standard 6-basis.

prover9 -f mckenzie.in > mckenzie.out ; ### ( mckenzie.out.xml )