.\" format with nroff|troff|groff -man
.TH EPROOF_RAM 1 
.fp 5 CW
.nr mH 5
.de H0
.nr mH 0
.in 5n
\fB\\$1\fP
.in 7n
..
.de H1
.nr mH 1
.in 7n
\fB\\$1\fP
.in 9n
..
.de H2
.nr mH 2
.in 11n
\fB\\$1\fP
.in 13n
..
.de H3
.nr mH 3
.in 15n
\fB\\$1\fP
.in 17n
..
.de H4
.nr mH 4
.in 19n
\fB\\$1\fP
.in 21n
..
.de OP
.nr mH 0
.ie !'\\$1'-' \{
.ds mO \\fB\\-\\$1\\fP
.ds mS ,\\0
.\}
.el \{
.ds mO \\&
.ds mS \\&
.\}
.ie '\\$2'-' \{
.if !'\\$4'-' .as mO \\0\\fI\\$4\\fP
.\}
.el \{
.as mO \\*(mS\\fB\\-\\-\\$2\\fP
.if !'\\$4'-' .as mO =\\fI\\$4\\fP
.\}
.in 5n
\\*(mO
.in 9n
..
.de SP
.if \\n(mH==2 .in 9n
.if \\n(mH==3 .in 13n
.if \\n(mH==4 .in 17n
..
.de FN
.nr mH 0
.in 5n
\\$1 \\$2
.in 9n
..
.de DS
.in +3n
.ft 5
.nf
..
.de DE
.fi
.ft R
.in -3n
..
.SH NAME
eproof_ram \- a wrapper around eprover and epclextract
.SH SYNOPSIS
\fBeproof_ram\fP\ [\ \fIoptions\fP\ ]\ \fIfile\fP\ \&.\&.\&.
.SH DESCRIPTION
eproof_ram is a wrapper around eprover and epclextract\&. It will run eprover
with output level 4 (full output of all potentially proof\-relevant inferences)
and, in the case of success, automatically run epclextract to provide a proof
derivation or a derivation of all clauses in the saturated proof state\&.
.PP
Please note that eproof_ram, unlike most E tools, does not support reading
problems from stdin\&. It will silently assume an empty input from stdin\&.
.PP
Remember that all options and arguments which should be passed on to eprover or
epclextract need to be given as operands to this script, i\&.e\&. use the
"\-\-" string to avoid, that this script chomps these (possibly unknown)
options\&. E\&.g\&. "eproof_ram \-o \fIoutfile\fP \fB\-\-\fP \-W none \-\-prune
\fIfile\fP" would result into "eprover \-W none \-\-prune \fIfile\fP"\&.
.PP
In particular, eproof will automatically do a close approximation of "the right
thing" (tm) with the options describing input\- and output formats\&.
.SH OPTIONS
.OP h help flag -
Print this help and exit\&.
.OP F functions flag -
Print a list of all functions available\&.
.OP T trace string fnList
A comma separated list of functions of this script to trace (convinience for
troubleshooting)\&.
.PP
.OP o output\-file string file
Redirect output into the given \fIfile\fP\&.
.OP V version flag -
Print the version numbers of \fBeprover\fP(1) and \fBepclextract\fP(1) used by
this script\&. Please include this with all bug reports (if any)\&.
.OP u proof\-time\-unlimited flag -
If eprover succeeds within the overall timelimit, do not stop
\fBepclextract\fP(1) due to timeout\&.
.OP - tstp\-in flag -
Parse TPTP\-3 format instead of E\-LOP\&.
.OP - tstp\-out flag -
Print output clauses in TPTP\-3 syntax\&.
.OP - tstp\-format flag -
Same as \fB\-\-tstp\-in \-\-tstp\-out\fP\&.
.OP - tptp3\-out flag -
Same as \fB\-\-tstp\-out\fP\&.
.OP - tptp3\-format flag -
Same as \fB\-\-tstp\-format\fP\&.
.SH SEE\ ALSO
\fBeprover\fP(1), \fBepclextract\fP(1)\&.
.SH IMPLEMENTATION
.H0 version
1\&.9
.H0 copyright
(C) 1998\-2009 Stephan Schulz (schulz@eprover\&.org)
.H0 portions\ copyright
(C) 2015 Jens Elkner (ksh93 port/cleanup)
.H0 license
GPL 2+
.H0 source
http://www\&.eprover\&.org