Here are examples of running the auxiliary programs described in the MACE4 manual. You can get a synopsis of each program by giving it an argument "

- Remove isomorphic interpretations.
This example produces the quasigroups of order 3.
mace4 -n3 < qg.in | get_interps > qg.out3 isofilter < qg.out3 > qg.iso3

- Use a set of interpretations to filter a stream of clauses.
This example removes clauses that are true in any of a set
of non-modular orthomodular lattices.
modfilter non-MOL-OML false_in_all < MOL-cand.296 > MOL-cand.238

- Use a set of clauses to filter a stream of interpretations.
This example removes distributive models from a set of ortholattices.
mace4 -n8 < OL.in | get_interps | isofilter > OL.8 interpfilter distributivity nonmodels < OL.8 > OL.8.out

- Given a set of interpretations and a stream of clauses, show the interpretations that model each clause.
mace4 -n6 < OL.in | get_interps | isofilter > OL.6 modtester OL.6 < BA-sheffer > BA-sheffer.out

- Decision procedure for lattice identities in meet/join.
latfilter < meet-join-equations > meet-join-equations.out

- Decision procedure for ortholattice identities in meet/join/complement/0/1/shefferstroke.
olfilter < mjc01s-equations > mjc01s-equations.out

- Given a set of rewrite rules (demodulators), rewrite a stream of terms or clauses.
rewriter lattice.rules < lattice-sax > lattice-sax.rewritten

- Print the upper covers of the 5 ortholattices of order 8. The output is suitable for
input to Ralph Freese's lattice drawing program.
upper-covers < OL.8 > OL.8.upper-covers

*
These activities are projects of the
Mathematics and Computer Science Division
of
Argonne National Laboratory.
*