1
.\" Automatically generated by Pod::Man 2.1801 (Pod::Simple 3.05)
4
.\" ========================================================================
5
.de Sp \" Vertical space (when we can't use .PP)
9
.de Vb \" Begin verbatim text
14
.de Ve \" End verbatim text
18
.\" Set up some character translations and predefined strings. \*(-- will
19
.\" give an unbreakable dash, \*(PI will give pi, \*(L" will give a left
20
.\" double quote, and \*(R" will give a right double quote. \*(C+ will
21
.\" give a nicer C++. Capital omega is used to do unbreakable dashes and
22
.\" therefore won't be available. \*(C` and \*(C' expand to `' in nroff,
23
.\" nothing in troff, for use with C<>.
25
.ds C+ C\v'-.1v'\h'-1p'\s-2+\h'-1p'+\s0\v'.1v'\h'-1p'
29
. if (\n(.H=4u)&(1m=24u) .ds -- \(*W\h'-12u'\(*W\h'-12u'-\" diablo 10 pitch
30
. if (\n(.H=4u)&(1m=20u) .ds -- \(*W\h'-12u'\(*W\h'-8u'-\" diablo 12 pitch
43
.\" Escape single quotes in literal strings from groff's Unicode transform.
47
.\" If the F register is turned on, we'll generate index entries on stderr for
48
.\" titles (.TH), headers (.SH), subsections (.SS), items (.Ip), and index
49
.\" entries marked with X<> in POD. Of course, you'll have to process the
50
.\" output yourself in some meaningful fashion.
53
. tm Index:\\$1\t\\n%\t"\\$2"
63
.\" Accent mark definitions (@(#)ms.acc 1.5 88/02/08 SMI; from UCB 4.2).
64
.\" Fear. Run. Save yourself. No user-serviceable parts.
65
. \" fudge factors for nroff and troff
74
. ds #H ((1u-(\\\\n(.fu%2u))*.13m)
80
. \" simple accents for nroff and troff
90
. ds ' \\k:\h'-(\\n(.wu*8/10-\*(#H)'\'\h"|\\n:u"
91
. ds ` \\k:\h'-(\\n(.wu*8/10-\*(#H)'\`\h'|\\n:u'
92
. ds ^ \\k:\h'-(\\n(.wu*10/11-\*(#H)'^\h'|\\n:u'
93
. ds , \\k:\h'-(\\n(.wu*8/10)',\h'|\\n:u'
94
. ds ~ \\k:\h'-(\\n(.wu-\*(#H-.1m)'~\h'|\\n:u'
95
. ds / \\k:\h'-(\\n(.wu*8/10-\*(#H)'\z\(sl\h'|\\n:u'
97
. \" troff and (daisy-wheel) nroff accents
98
.ds : \\k:\h'-(\\n(.wu*8/10-\*(#H+.1m+\*(#F)'\v'-\*(#V'\z.\h'.2m+\*(#F'.\h'|\\n:u'\v'\*(#V'
99
.ds 8 \h'\*(#H'\(*b\h'-\*(#H'
100
.ds o \\k:\h'-(\\n(.wu+\w'\(de'u-\*(#H)/2u'\v'-.3n'\*(#[\z\(de\v'.3n'\h'|\\n:u'\*(#]
101
.ds d- \h'\*(#H'\(pd\h'-\w'~'u'\v'-.25m'\f2\(hy\fP\v'.25m'\h'-\*(#H'
102
.ds D- D\\k:\h'-\w'D'u'\v'-.11m'\z\(hy\v'.11m'\h'|\\n:u'
103
.ds th \*(#[\v'.3m'\s+1I\s-1\v'-.3m'\h'-(\w'I'u*2/3)'\s-1o\s+1\*(#]
104
.ds Th \*(#[\s+2I\s-2\h'-\w'I'u*3/5'\v'-.3m'o\v'.3m'\*(#]
105
.ds ae a\h'-(\w'a'u*4/10)'e
106
.ds Ae A\h'-(\w'A'u*4/10)'E
107
. \" corrections for vroff
108
.if v .ds ~ \\k:\h'-(\\n(.wu*9/10-\*(#H)'\s-2\u~\d\s+2\h'|\\n:u'
109
.if v .ds ^ \\k:\h'-(\\n(.wu*10/11-\*(#H)'\v'-.4m'^\v'.4m'\h'|\\n:u'
110
. \" for low resolution devices (crt and lpr)
111
.if \n(.H>23 .if \n(.V>19 \
124
.\" ========================================================================
126
.IX Title "TPTP2DFG 1"
127
.TH TPTP2DFG 1 "2010-02-23" "perl v5.10.0" "SPASS"
128
.\" For nroff, turn off justification. Always turn off hyphenation; it makes
129
.\" way too many mistakes in technical documents.
133
tptp2dfg \- transforms DFG files into TPTP files
135
.IX Header "SYNOPSIS"
136
\&\fBtptp2dfg\fR [\-include] <input\-file> <output\-file>
138
.IX Header "DESCRIPTION"
139
\&\fBtptp2dfg\fR is a program which converts a problem input file in
140
\&\fB\s-1TPTP\s0\fR format into a problem input file in \fB\s-1DFG\s0\fR format.
141
The \fB\s-1TPTP\s0\fR problem format is used by the
142
\&\s-1TPTP\s0 library of test problems for automated theorem proving, available
143
at \fBhttp://www.math.miami.edu/~tptp/\fR.
146
\&\fBtptp2dfg\fR supports the following command line options.
149
This option enables the expansion of include directives in tptp files.
150
If set all \s-1TPTP\s0 include directives in hte input-file are replaced by the respective file content
151
during translation. If not set the \s-1TPTP\s0 include directives are translated
152
into \s-1DFG\s0 include directives.
155
.IX Header "SEE ALSO"
156
\&\fIdfg2tptp\fR\|(1), \fIdfg2otter\fR\|(1), \s-1\fISPASS\s0\fR\|(1)
159
Martin Suda and Christoph Weidenbach
161
Contact : spass@mpi\-inf.mpg.de