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

# tptp2dfg(1)

transforms DFG files into TPTP files

## NAME

tptp2dfg - transforms DFG files into TPTP files

## SYNOPSIS

**tptp2dfg** \[-include\] \<input-file\> \<output-file\>

## DESCRIPTION

**tptp2dfg** is a program which converts a problem input file in **TPTP** format into a problem input file in **DFG** format. The **TPTP** problem format is used by the  TPTP library of test problems for automated theorem proving, available at **http://www.math.miami.edu/~tptp/**.

## OPTIONS

**tptp2dfg** supports the following command line options.

- \-include

  This option enables the expansion of include directives in tptp files. If set all TPTP include directives in hte input-file are replaced by the respective file content during translation. If not set the TPTP include directives are translated into DFG include directives. Default is off.

## SEE ALSO

[*dfg2tptp*(1)](/dfg2tptp/1.md), [*dfg2otter*(1)](/dfg2otter/1.md), [*SPASS*(1)](/SPASS/1.md)

## AUTHORS

Martin Suda and Christoph Weidenbach

Contact : spass@mpi-inf.mpg.de