.TH CLAUSETESTER 1 "January 20, 2007"
.SH NAME
clausetester - check formulas in models
.SH SYNOPSIS
.B clausetester
.RI < interpretations-file >
<
.RI < formulas-file >
>
.RI < annotated-formulas-file >
.SH DESCRIPTION
This manual page documents briefly the
.B clausetester
command.
.PP
This program takes a set of \fIinterpretations\fP and stream of
\fIformulas\fP. For each formula, the interpretations in which the
formula is true are shown, and at the end the number of formulas true
in each interpretation is shown.
.SH SEE ALSO
.BR prover9 (1),
.BR mace4 (1).
.br
Full documentation for \fBclausetester\fP is found in the \fBprover9\fP manual, available on Debian systems in the \fIprover9-doc\fP package at \fI/usr/share/doc/prover9-doc/manual/index.html\fP.
.SH AUTHOR
\fBclausetester\fP was written by William McCune <mccune@cs.unm.edu>
.PP
This manual page was written by Peter Collingbourne <peter@pcc.me.uk>,
for the Debian project (but may be used by others).