---
name: "clausefilter"
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/clausefilter"
---

# clausefilter(1)

filter formulas with models

## NAME

clausefilter - filter formulas with models

## SYNOPSIS

**clausefilter** \<*interpretations-file*\> \<*test*\> \< \<*formulas-file*\> \> \<*passing-formulas-file*\>

## DESCRIPTION

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.

## TESTS

The following tests are available.

- **true\_in\_all**

  Formula true in all interpretations.

- **true\_in\_some**

  Formula true in some interpretation.

- **false\_in\_all**

  Formula false in all interpretations.

- **false\_in\_some**

  Formula false in some interpretation.

## SEE ALSO

[**prover9**(1)](/prover9/1.md), [**mace4**(1)](/mace4/1.md).\
 Full documentation for **clausefilter** 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

**clausefilter** 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).