---
name: "clausetester"
section: "1"
platform: "linux"
package: "ladr4-apps"
version: "0.0.200911a-2.1+b2"
release: "Debian 10 (Buster)"
platforms: ["linux"]
url: "https://new.carta.tech/clausetester"
---

# clausetester(1)

check formulas in models

## NAME

clausetester - check formulas in models

## SYNOPSIS

**clausetester** \<*interpretations-file*\> \< \<*formulas-file*\> \> \<*annotated-formulas-file*\>

## DESCRIPTION

This manual page documents briefly the **clausetester** command.

This program takes a set of *interpretations* and stream of *formulas*. 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.

## SEE ALSO

[**prover9**(1)](/prover9/1.md), [**mace4**(1)](/mace4/1.md).\
 Full documentation for **clausetester** is found in the **prover9** manual, available on Debian systems in the *prover9-doc* package at */usr/share/doc/prover9-doc/manual/index.html*.

## AUTHOR

**clausetester** was written by William McCune \<mccune@cs.unm.edu\>

This manual page was written by Peter Collingbourne \<peter@pcc.me.uk\>, for the Debian project (but may be used by others).