Mace4 Miscellaneous Examples


Schubert's steamroller with a bug
mace4 -f steam.in > steam.out ; ### ( steam.out.xml )
Mutilated checkerboard
mace4 -f toughnut.in > toughnut.out ; ### ( toughnut.out.xml )
Logic puzzle about an ordering relation
mace4 -f kauer.in > kauer.out ; ### ( kauer.out.xml )
Noncommutative group, quantified formulas
mace4 -f group2.in > group2.out ; ### ( group2.out.xml )
Big noncommutative groups
mace4 -f ncg-48.in > ncg-48.out ; ### ( ncg-48.out.xml )
Noncommutative rings
mace4 -f noncommutative-ring.in > noncommutative-ring.out ; ### ( noncommutative-ring.out.xml )
Quasigroups
mace4 -f qg.in > qg.out ; ### ( qg.out.xml )
Ring structure for group candidates
mace4 -f ring19.in > ring19.out ; ### ( ring19.out.xml )
Nonmodular orthomodular lattice
mace4 -f nonmodular-oml.in > nonmodular-oml.out ; ### ( nonmodular-oml.out.xml )
Weak orthomodular lattice
mace4 -f rw1.in > rw1.out ; ### ( rw1.out.xml )
Candidate single axiom for BA
mace4 -f sheffer8.in > sheffer8.out ; ### ( sheffer8.out.xml )
Equivalential calculus
mace4 -f ec.in > ec.out ; ### ( ec.out.xml )
Fixed point combinator
mace4 -f cl_ql.in > cl_ql.out ; ### ( cl_ql.out.xml )
Ternary Boolean Algebra
mace4 -f tba.in > tba.out ; ### ( tba.out.xml )