Version 2009-11A
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