Prover9 (and some Mace4) Examples

The examples show Prover9 and Mace4 jobs, with links to the input and output files. Most also show XML output.

Basic Examples

• from the Milehigh Conference on Quasigroups, Loops, and Nonassociative Systems
• from R. Padmanabhan (overlaps with Milehigh examples)
• Prover9 Miscellany
• Mace4 Miscellany
• Hao Wang Problems
• FOF Reduction

Examples From Recent Projects

• Lattice Theory Single Axioms
• Boolean Algebra Bases
• Ortholattice Single Axioms
• Commutators in Cancellative Semigroups
• Uniquely Complemented Lattices
• Ternary Relations in Lattices
• Distributivity in Median Algebras
• Semantic Guidance
• CS and Ore's Quotient Condition