Prover9 Examples: Boolean Algebra Single Axioms

See

McCune, Veroff, Fitelson, Harris, Feist, Wos, "Short Single Axioms for Boolean Algebra", J. Automated Reasoning 29(1), pp. 1--16 (2002).

and

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

BA single axiom in join/complement

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

BA single axiom in Sheffer stroke

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

BA single axiom in Sheffer stroke (with definition of complement).

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

BA 2-basis in Sheffer stroke.

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

BA 2-basis in Sheffer stroke (with definition of complement).

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