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 )