clausefilter - filter formulas with models
clausefilter <interpretations-file> <test> < <formulas-file> >
This manual page documents briefly the clausefilter command.
Given a set of interpretations, a test to perform, and a stream of
formulas, clausefilter outputs the formulas that pass the test.
The following tests are available.
Formula true in all interpretations.
Formula true in some interpretation.
Formula false in all interpretations.
Formula false in some interpretation.
Full documentation for clausefilter is found in the prover9 manual,
available on Debian systems in the prover9-doc package at
clausefilter was written by William McCune <email@example.com>
This manual page was written by Peter Collingbourne <firstname.lastname@example.org>,
for the Debian project (but may be used by others).
January 20, 2007