---
name: "dfg2otter"
section: "1"
platform: "linux"
package: "spass"
version: "3.7-4"
release: "Debian 9 (Stretch)"
platforms: ["linux"]
url: "https://new.carta.tech/dfg2otter"
---

# dfg2otter(1)

transforms DFG clause files into Otter format

## NAME

dfg2otter - transforms DFG clause files into Otter format

## SYNOPSIS

**dfg2otter** \[options\] \<infile\> \<outfile\>

## DESCRIPTION

**dfg2otter** is a C-program to transform problem input files in **DFG** syntax into **Otter** syntax. It accepts all options from **SPASS**, although only a subset has an effect on translation.

**dfg2otter** negates conjecture formulae of the **SPASS** input file before printing the Otter usable list. The **SPASS** conjecture formula list is translated into a disjunction of the negated single conjectures. If the **SPASS** input file consits of clauses, these are not modified.

## SEE ALSO

*checkstat*(1), *filestat*(1), [*pcs*(1)](/pcs/1.md), [*pgen*(1)](/pgen/1.md), *rescmp*(1), *tpform*(1), *tpget*(1), *deprose*(1), [*dfg2otter.pl*(1)](/dfg2otter.pl/1.md), [*SPASS*(1)](/SPASS/1.md)

## AUTHORS

Thomas Hillenbrand, Dalibor Topic and Christoph Weidenbach

Contact : spass@mpi-inf.mpg.de