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), pgen(1), rescmp(1), tpform(1), tpget(1), deprose(1),
       dfg2otter.pl(1), SPASS(1)

AUTHORS

       Thomas Hillenbrand, Dalibor Topic and Christoph Weidenbach

       Contact : spass@mpi-inf.mpg.de