Milehigh Examples
Prover9 (and Mace4) examples from
a talk on Prover9 at
The Milehigh Conference on Quasigroups, Loops, and Nonassociative Systems,
July 2005.
These examples have been updated for version March-2006 of Prover9/Mace4.
Nonassociative Ring
Left, flexible -> right
prover9 -f na-ring-1.in > na-ring-1.out ; ### ( na-ring-1.out.xml )
Counterexample to left -> right
mace4 -c -N20 -f na-ring-2.in > na-ring-2.out ; ### ( na-ring-2.out.xml )
Left, flexible -> right (with associator)
prover9 -f na-ring-3.in > na-ring-3.out ; ### ( na-ring-3.out.xml )
xxx=x Rings are Commutative
prover9 -f x3-ring.in > x3-ring.out ; ### ( x3-ring.out.xml )
Padmanabhan Example
A Ring model of K
prover9 -f rp-ident.in > rp-ident.out ; ### ( rp-ident.out.xml )
First-order proof of the identity in question
mace4 -f rp-ring.in > rp-ring.out ; ### ( rp-ring.out.xml )
GT Single Axiom Counterexamples
An easy candidate; no additional constraints
mace4 -f cand3.in > cand3.out ; ### ( cand3.out.xml )
A candidate with inverse loop constraints
mace4 -f cand10.in > cand10.out ; ### ( cand10.out.xml )
A candidate with ring constraints
mace4 -f cand23.in > cand23.out ; ### ( cand23.out.xml )
A 4-variable single axiom
prover9 -f gtsax.in > gtsax.out ; ### ( gtsax.out.xml )