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 "help".
• 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.