.\" Automatically generated by Pod::Man v1.3, Pod::Parser v1.13
.\"
.\" Standard preamble:
.\" ========================================================================
.de Sh \" Subsection heading
.br
.if t .Sp
.ne 5
.PP
\fB\\$1\fR
.PP
..
.de Sp \" Vertical space (when we can't use .PP)
.if t .sp .5v
.if n .sp
..
.de Vb \" Begin verbatim text
.ft CW
.nf
.ne \\$1
..
.de Ve \" End verbatim text
.ft R

.fi
..
.\" Set up some character translations and predefined strings.  \*(-- will
.\" give an unbreakable dash, \*(PI will give pi, \*(L" will give a left
.\" double quote, and \*(R" will give a right double quote.  | will give a
.\" real vertical bar.  \*(C+ will give a nicer C++.  Capital omega is used to
.\" do unbreakable dashes and therefore won't be available.  \*(C` and \*(C'
.\" expand to `' in nroff, nothing in troff, for use with C<>.
.tr \(*W-|\(bv\*(Tr
.ds C+ C\v'-.1v'\h'-1p'\s-2+\h'-1p'+\s0\v'.1v'\h'-1p'
.ie n \{\
.    ds -- \(*W-
.    ds PI pi
.    if (\n(.H=4u)&(1m=24u) .ds -- \(*W\h'-12u'\(*W\h'-12u'-\" diablo 10 pitch
.    if (\n(.H=4u)&(1m=20u) .ds -- \(*W\h'-12u'\(*W\h'-8u'-\"  diablo 12 pitch
.    ds L" ""
.    ds R" ""
.    ds C` ""
.    ds C' ""
'br\}
.el\{\
.    ds -- \|\(em\|
.    ds PI \(*p
.    ds L" ``
.    ds R" ''
'br\}
.\"
.\" If the F register is turned on, we'll generate index entries on stderr for
.\" titles (.TH), headers (.SH), subsections (.Sh), items (.Ip), and index
.\" entries marked with X<> in POD.  Of course, you'll have to process the
.\" output yourself in some meaningful fashion.
.if \nF \{\
.    de IX
.    tm Index:\\$1\t\\n%\t"\\$2"
..
.    nr % 0
.    rr F
.\}
.\"
.\" For nroff, turn off justification.  Always turn off hyphenation; it makes
.\" way too many mistakes in technical documents.
.hy 0
.if n .na
.\"
.\" Accent mark definitions (@(#)ms.acc 1.5 88/02/08 SMI; from UCB 4.2).
.\" Fear.  Run.  Save yourself.  No user-serviceable parts.
.    \" fudge factors for nroff and troff
.if n \{\
.    ds #H 0
.    ds #V .8m
.    ds #F .3m
.    ds #[ \f1
.    ds #] \fP
.\}
.if t \{\
.    ds #H ((1u-(\\\\n(.fu%2u))*.13m)
.    ds #V .6m
.    ds #F 0
.    ds #[ \&
.    ds #] \&
.\}
.    \" simple accents for nroff and troff
.if n \{\
.    ds ' \&
.    ds ` \&
.    ds ^ \&
.    ds , \&
.    ds ~ ~
.    ds /
.\}
.if t \{\
.    ds ' \\k:\h'-(\\n(.wu*8/10-\*(#H)'\'\h"|\\n:u"
.    ds ` \\k:\h'-(\\n(.wu*8/10-\*(#H)'\`\h'|\\n:u'
.    ds ^ \\k:\h'-(\\n(.wu*10/11-\*(#H)'^\h'|\\n:u'
.    ds , \\k:\h'-(\\n(.wu*8/10)',\h'|\\n:u'
.    ds ~ \\k:\h'-(\\n(.wu-\*(#H-.1m)'~\h'|\\n:u'
.    ds / \\k:\h'-(\\n(.wu*8/10-\*(#H)'\z\(sl\h'|\\n:u'
.\}
.    \" troff and (daisy-wheel) nroff accents
.ds : \\k:\h'-(\\n(.wu*8/10-\*(#H+.1m+\*(#F)'\v'-\*(#V'\z.\h'.2m+\*(#F'.\h'|\\n:u'\v'\*(#V'
.ds 8 \h'\*(#H'\(*b\h'-\*(#H'
.ds o \\k:\h'-(\\n(.wu+\w'\(de'u-\*(#H)/2u'\v'-.3n'\*(#[\z\(de\v'.3n'\h'|\\n:u'\*(#]
.ds d- \h'\*(#H'\(pd\h'-\w'~'u'\v'-.25m'\f2\(hy\fP\v'.25m'\h'-\*(#H'
.ds D- D\\k:\h'-\w'D'u'\v'-.11m'\z\(hy\v'.11m'\h'|\\n:u'
.ds th \*(#[\v'.3m'\s+1I\s-1\v'-.3m'\h'-(\w'I'u*2/3)'\s-1o\s+1\*(#]
.ds Th \*(#[\s+2I\s-2\h'-\w'I'u*3/5'\v'-.3m'o\v'.3m'\*(#]
.ds ae a\h'-(\w'a'u*4/10)'e
.ds Ae A\h'-(\w'A'u*4/10)'E
.    \" corrections for vroff
.if v .ds ~ \\k:\h'-(\\n(.wu*9/10-\*(#H)'\s-2\u~\d\s+2\h'|\\n:u'
.if v .ds ^ \\k:\h'-(\\n(.wu*10/11-\*(#H)'\v'-.4m'^\v'.4m'\h'|\\n:u'
.    \" for low resolution devices (crt and lpr)
.if \n(.H>23 .if \n(.V>19 \
\{\
.    ds : e
.    ds 8 ss
.    ds o a
.    ds d- d\h'-1'\(ga
.    ds D- D\h'-1'\(hy
.    ds th \o'bp'
.    ds Th \o'LP'
.    ds ae ae
.    ds Ae AE
.\}
.rm #[ #] #H #V #F C
.\" ========================================================================
.\"
.IX Title "SPASS 1"
.TH SPASS 1 "2003-04-29" "perl v5.6.1" "SPASS"
.UC
.SH "NAME"
\&\s-1SPASS\s0 \- automated theorem prover for full first-order logic with equality
.SH "SYNOPSIS"
.IX Header "SYNOPSIS"
\&\s-1SPASS\s0 [\fBoptions\fR] [\fIinputfile\fR]
.SH "DESCRIPTION"
.IX Header "DESCRIPTION"
\&\s-1SPASS\s0 is an automated theorem prover for full sorted first-order logic with equality
that extends superposition by sorts and a splitting rule for case analysis.
.SH "OPTIONS"
.IX Header "OPTIONS"
Command line options in \s-1SPASS\s0 are implemented via modifications to the \s-1GNU\s0 command
line option package for C. Just giving the option sets its value to 1 and means enabling
the option. In order to disable
an option the value has to be set to 0 by declaring \-\fIOption\fR=0.
The following options are currently supported by \s-1SPASS:\s0
.ie n .IP """\-Auto""" 4
.el .IP "\f(CW\-Auto\fR" 4
.IX Item "-Auto"
Enables/disables the auto mode where \s-1SPASS\s0 configures itself automatically.
The inference/reduction rules, the sort technology, the ordering and precedence
as well as the splitting and selection strategy are set.
In auto mode \s-1SPASS\s0 is complete. Mixing the auto mode with user defined options
may destroy completeness.
Default is 1.
.ie n .IP """\-Stdin""" 4
.el .IP "\f(CW\-Stdin\fR" 4
.IX Item "-Stdin"
Enables/disables input in \s-1SPASS\s0 via stdin. The file argument is ignored. Default is 0.
.ie n .IP """\-Interactive""" 4
.el .IP "\f(CW\-Interactive\fR" 4
.IX Item "-Interactive"
Enables/disables the interactive mode. First, \s-1SPASS\s0 is given a set of axioms and then
the prover accepts subsequent proof tasks. Default is 0.
.ie n .IP """\-Flotter""" 4
.el .IP "\f(CW\-Flotter\fR" 4
.IX Item "-Flotter"
Enables/disables the \s-1CNF\s0 translation mode of \s-1SPASS\s0. If the option is set, \s-1SPASS\s0 only
performs a clause normal form translation. If no output file argument is given
\&\s-1SPASS\s0 prints the \s-1CNF\s0 to stdout. Default is 0.
.ie n .IP """\-SOS""" 4
.el .IP "\f(CW\-SOS\fR" 4
.IX Item "-SOS"
Enables/disables the set of support strategy. Default is 0.
.ie n .IP """\-Splits=\f(CIn\f(CW""" 4
.el .IP "\f(CW\-Splits=\f(CIn\f(CW\fR" 4
.IX Item "-Splits=n"
Sets the number of possible splitting applications to \fIn\fR. If \fIn\fR=\-1 then
the number of splits is not limited. Default is 0.
.ie n .IP """\-Memory=\f(CIn\f(CW""" 4
.el .IP "\f(CW\-Memory=\f(CIn\f(CW\fR" 4
.IX Item "-Memory=n"
Sets the amount of memory available to \s-1SPASS\s0 for the proof search to \fIn\fR bytes. 
The memory needed to startup \s-1SPASS\s0 cannot be restricted.
Default is \-1 meaning that memory allocations is only restricted by available memory.
.ie n .IP """\-TimeLimit=\f(CIn\f(CW""" 4
.el .IP "\f(CW\-TimeLimit=\f(CIn\f(CW\fR" 4
.IX Item "-TimeLimit=n"
Sets a time limit for the proof search to \fIn\fR seconds. Default is \-1 meaning that
\&\s-1SPASS\s0 may run forever. The time limit is polled when \s-1SPASS\s0 selects a new clause for
inferences. If a single inference step causes an explosion to the number of generated
clauses it may therefore happen that a given time limit is significantly exceeded.
.ie n .IP """\-DocSST""" 4
.el .IP "\f(CW\-DocSST\fR" 4
.IX Item "-DocSST"
Enables/disables documentation output for static soft typing. 
The used sort theory as well as the (failed) proof attempt for
the sort constraint is printed.
Default is 0.
.ie n .IP """\-DocProof""" 4
.el .IP "\f(CW\-DocProof\fR" 4
.IX Item "-DocProof"
Enables/disables proof documentation. If \s-1SPASS\s0 finds a proof it is eventually
printed. If \s-1SPASS\s0 finds a saturation, the saturated set of clauses is eventually printed.
Enabling proof documentation may significantly decrease \s-1SPASS\s0's performance, because
the prover must store clauses that can be thrown away otherwise. Default is 0.
.ie n .IP """\-DocSplit""" 4
.el .IP "\f(CW\-DocSplit\fR" 4
.IX Item "-DocSplit"
Enables/disables the documentation of split backtracking steps where the
current backtracking level is printed.
Default is 0.
.ie n .IP """\-Loops""" 4
.el .IP "\f(CW\-Loops\fR" 4
.IX Item "-Loops"
Sets the maximal number of mainloop iterations for \s-1SPASS\s0.
Default is \-1.
.ie n .IP """\-PSub""" 4
.el .IP "\f(CW\-PSub\fR" 4
.IX Item "-PSub"
Enables/disables printing of subsumed clauses.
Default is 0.
.ie n .IP """\-PRew""" 4
.el .IP "\f(CW\-PRew\fR" 4
.IX Item "-PRew"
Enables/disables printing of rewrite applications.
Default is 0.
.ie n .IP """\-PCon""" 4
.el .IP "\f(CW\-PCon\fR" 4
.IX Item "-PCon"
Enables/disables printing of condensation applications.
Default is 0.
.ie n .IP """\-PTaut""" 4
.el .IP "\f(CW\-PTaut\fR" 4
.IX Item "-PTaut"
Enables/disables printing of tautology deletion applications.
Default is 0.
.ie n .IP """\-PObv""" 4
.el .IP "\f(CW\-PObv\fR" 4
.IX Item "-PObv"
Enables/disables printing of obvious reduction applications.
Default is 0.
.ie n .IP """\-PSSi""" 4
.el .IP "\f(CW\-PSSi\fR" 4
.IX Item "-PSSi"
Enables/disables printing of sort simplification applications.
Default is 0.
.ie n .IP """\-PSST""" 4
.el .IP "\f(CW\-PSST\fR" 4
.IX Item "-PSST"
Enables/disables printing of static soft typing applications.
All deleted clauses are printed.
Default is 0.
.ie n .IP """\-PMRR""" 4
.el .IP "\f(CW\-PMRR\fR" 4
.IX Item "-PMRR"
Enables/disables printing of matching replacement resolution applications.
Default is 0.
.ie n .IP """\-PUnC""" 4
.el .IP "\f(CW\-PUnC\fR" 4
.IX Item "-PUnC"
Enables/disables printing of unit conflict applications.
Default is 0.
.ie n .IP """\-PAED""" 4
.el .IP "\f(CW\-PAED\fR" 4
.IX Item "-PAED"
Enables/disables printing of clauses where redundant
equations have been removed (assignment equation deletion).
.ie n .IP """\-PDer""" 4
.el .IP "\f(CW\-PDer\fR" 4
.IX Item "-PDer"
Enables/disables printing of clauses derived by inferences.
Default is 0.
.ie n .IP """\-PGiven """ 4
.el .IP "\f(CW\-PGiven \fR" 4
.IX Item "-PGiven "
Enables/disables printing of the given clause, selected
to perform inferences.
Default is 0.
.ie n .IP """\-PLabels""" 4
.el .IP "\f(CW\-PLabels\fR" 4
.IX Item "-PLabels"
Enables/disables printing of labels. If the \-DocProof is
set and no labels for formulae are provided by the input,
\&\s-1SPASS\s0 generates generic labels that are then printed by enabling this option.
Default is 0.
.ie n .IP """\-PKept""" 4
.el .IP "\f(CW\-PKept\fR" 4
.IX Item "-PKept"
Enables/disables printing of kept clauses. These are clauses
generated by inferences (backtracking) that are not redundant.
Clauses derived during input reduction/saturation are not printed.
Default is 0.
.ie n .IP """\-PProblem""" 4
.el .IP "\f(CW\-PProblem\fR" 4
.IX Item "-PProblem"
Enables/disables printing of the input clause set.
Default is 1.
.ie n .IP """\-PEmptyClause""" 4
.el .IP "\f(CW\-PEmptyClause\fR" 4
.IX Item "-PEmptyClause"
Enables/disables printing of derived empty clauses.
Default is 0.
.ie n .IP """\-PStatistic""" 4
.el .IP "\f(CW\-PStatistic\fR" 4
.IX Item "-PStatistic"
Enables/disables printing of a final statistics on derived/backtracked/kept clauses,
used time and used space.
Default is 1.
.ie n .IP """\-FPModel""" 4
.el .IP "\f(CW\-FPModel\fR" 4
.IX Item "-FPModel"
Enables/disables the output of an eventually found model to a file. If set
to 1, all clauses in the final set are printed. If set to 2, only
potentially productive clauses are printed, that are clauses with no selected
negative literal and a maximal positive one. If <problemfile> is the name
of the input problem and the eventually generated set is saturated, the
saturation is printed to the file <problemfile>.model, for otherwise
to <problemfile>.clauses. The latter case may, e.g., be caused by a time limit.
Default is 0.
.ie n .IP """\-FPDFGProof""" 4
.el .IP "\f(CW\-FPDFGProof\fR" 4
.IX Item "-FPDFGProof"
Enables/disables the output of an eventually found proof to a file. Using this
option requires to set the option \-DocProof. If <problemfile> is the name
of the input problem the proof is printed to <problemfile>.prf.
Default is 0.
.ie n .IP """\-PFlags""" 4
.el .IP "\f(CW\-PFlags\fR" 4
.IX Item "-PFlags"
Enables/disables the output of all flag values. The flag settings are
printed at the end of a \s-1SPASS\s0 run in form of a DFG-Syntax input section.
Default is 0.
.ie n .IP """\-POptSkolem""" 4
.el .IP "\f(CW\-POptSkolem\fR" 4
.IX Item "-POptSkolem"
Enables/disables the output of optimized Skolemization applications.
Default is 0.
.ie n .IP """\-PStrSkolem""" 4
.el .IP "\f(CW\-PStrSkolem\fR" 4
.IX Item "-PStrSkolem"
Enables/disables the output of strong Skolemization applications.
Default is 0.
.ie n .IP """\-PBDC""" 4
.el .IP "\f(CW\-PBDC\fR" 4
.IX Item "-PBDC"
Enables/disables the output of clauses deleted because of
bound restrictions. 
Default is 0.
.ie n .IP """\-PBInc""" 4
.el .IP "\f(CW\-PBInc\fR" 4
.IX Item "-PBInc"
Enables/disables the output of bound restriction changes. 
Default is 0.
.ie n .IP """\-PApplyDefs """ 4
.el .IP "\f(CW\-PApplyDefs \fR" 4
.IX Item "-PApplyDefs "
Enables/disables printing of expansions of atom definitions.
Default is 0.
.ie n .IP """\-Select""" 4
.el .IP "\f(CW\-Select\fR" 4
.IX Item "-Select"
Sets the selection strategy for \s-1SPASS\s0. If set to 0 no selection
of negative literals is done, if set to 1 negative literals in
clauses with more than one maximal literal are selected, if set
to 2 negative literals are always selected. The latter case results
in an ordered hyperresolution like behavior of ordered resolution.
Default is 1.
.ie n .IP """\-RInput""" 4
.el .IP "\f(CW\-RInput\fR" 4
.IX Item "-RInput"
Enables/disables the reduction of the initial clause set.
Default is 1.
.ie n .IP """\-Sorts""" 4
.el .IP "\f(CW\-Sorts\fR" 4
.IX Item "-Sorts"
Determines the monadic literals that built the sort constraint
for the initial clause set.
If set to 0, no sort constraint is built. If set to 1, all negative
monadic literals with a variable as argument form the sort constraint.
If set to 2, all negative monadic literals form the sort constraint.
Setting \-Sorts to 2 may harm completeness, since sort constraints are
subject to the basic strategy and to static soft typing.
Default is 1.
.ie n .IP """\-SatInput""" 4
.el .IP "\f(CW\-SatInput\fR" 4
.IX Item "-SatInput"
Enables/disables input saturation. The saturation is incomplete
but is guaranteed to terminate.
Default is 0.
.ie n .IP """\-WDRatio""" 4
.el .IP "\f(CW\-WDRatio\fR" 4
.IX Item "-WDRatio"
Sets the ratio between given clauses selected by
weight or the depth in the search space. The weight is the
sum of all symbol weights determined by the \-FuncWeight and
\&\-VarWeight options. The depth of all initial clauses is 0 and
clauses generated by inferences get the maximal depth of a parent
clause plus 1.
Default is 5, meaning
that 4 clauses are selected by weight and the fifth clause is
selected by depth.
.ie n .IP """\-PrefCon""" 4
.el .IP "\f(CW\-PrefCon\fR" 4
.IX Item "-PrefCon"
Sets the ratio to compute the weight for conjecture clauses
and therefore allows to prefer those. Default is 0 meaning that
the weight computation for conjecture clauses is not changed.
.ie n .IP """\-FullRed""" 4
.el .IP "\f(CW\-FullRed\fR" 4
.IX Item "-FullRed"
Enables/disables full reduction. If set to 0, only the set of worked
off clauses is completely inter\-reduced. If set to 1, all currently
hold clauses (worked off and usable) are completely inter\-reduced.
Default is 1.
.ie n .IP """\-FuncWeight """ 4
.el .IP "\f(CW\-FuncWeight \fR" 4
.IX Item "-FuncWeight "
Sets the weight of function/predicate symbols. The weight of
clauses is the sum of all symbol weights. This weight is considered
for the selection of the given clause. Default is 1.
.ie n .IP """\-VarWeight """ 4
.el .IP "\f(CW\-VarWeight \fR" 4
.IX Item "-VarWeight "
Sets the weight of variable symbols (see \-FuncWeight).
Default is 1.
.ie n .IP """\-PrefVar """ 4
.el .IP "\f(CW\-PrefVar \fR" 4
.IX Item "-PrefVar "
Enables/disables the preference for clauses with many variables.
While clauses are selected by weight, if this option is set and
two clauses have the same weight, the clause with more variable
occurrences is preferred.
Default is 0.
.ie n .IP """\-BoundMode""" 4
.el .IP "\f(CW\-BoundMode\fR" 4
.IX Item "-BoundMode"
Selects the mode for bound restrictions. Mode 0 means no
restriction, if set to 1 all newly generated clauses are restricted by weight
(see \-BoundStart) and if set to 2 clauses are restricted
by depth. Default is 0.
.ie n .IP """\-BoundStart""" 4
.el .IP "\f(CW\-BoundStart\fR" 4
.IX Item "-BoundStart"
The start restriction of the selected bound mode. For example,
if bound mode is 1 and bound start set to 5, all clauses with
a weight larger than 5 are deleted until the set is saturated.
This causes an increase of the used bound value that is
determined by the minimal increase saving a before deleted
clause. Default is \-1 meaning no bound restriction.
.ie n .IP """\-BoundLoops """ 4
.el .IP "\f(CW\-BoundLoops \fR" 4
.IX Item "-BoundLoops "
The number of loops applying the actions restrictions/increasing bound.
If the number of loops is exceeded all bound restrictions are
cancelled. Default is 1.
.ie n .IP """\-ApplyDefs""" 4
.el .IP "\f(CW\-ApplyDefs\fR" 4
.IX Item "-ApplyDefs"
Sets the maximal number of applications of atom definitions to input formulae.
Default is 0, meaning no applications at all.
.ie n .IP """\-Ordering """ 4
.el .IP "\f(CW\-Ordering \fR" 4
.IX Item "-Ordering "
Sets the term ordering. If 0 then \s-1KBO\s0 is selected,
if 1 the \s-1RPOS\s0 is selected. Default is 0.          
.ie n .IP """\-CNFOptSkolem  """ 4
.el .IP "\f(CW\-CNFOptSkolem  \fR" 4
.IX Item "-CNFOptSkolem  "
Enables/disables optimized Skolemization.
Default is 1.
.ie n .IP """\-CNFStrSkolem """ 4
.el .IP "\f(CW\-CNFStrSkolem \fR" 4
.IX Item "-CNFStrSkolem "
Enables/disables Strong Skolemization.
Default is 1.
.ie n .IP """\-CNFProofSteps""" 4
.el .IP "\f(CW\-CNFProofSteps\fR" 4
.IX Item "-CNFProofSteps"
Sets the maximal number of proof steps
in an optimized Skolemization proof attempt.
Default is 100.      
.ie n .IP """\-CNFRenaming  """ 4
.el .IP "\f(CW\-CNFRenaming  \fR" 4
.IX Item "-CNFRenaming  "
Enables/disables formula renaming.
Default is 1.
.ie n .IP """\-CNFPRenaming    """ 4
.el .IP "\f(CW\-CNFPRenaming    \fR" 4
.IX Item "-CNFPRenaming    "
Enables/disables the printing of formula renaming applications.
Default is 0.
.ie n .IP """\-CNFFEqR""" 4
.el .IP "\f(CW\-CNFFEqR\fR" 4
.IX Item "-CNFFEqR"
Enables/disables certain equality reduction techniques
on the formula level. Default is 1.
.ie n .IP """\-IEmS  """ 4
.el .IP "\f(CW\-IEmS  \fR" 4
.IX Item "-IEmS  "
Enables/disables the inference rule Empty Sort.
Default is 0.
.ie n .IP """\-ISoR  """ 4
.el .IP "\f(CW\-ISoR  \fR" 4
.IX Item "-ISoR  "
Enables/disables the inference rule Sort Resolution.
Default is 0. 
.ie n .IP """\-IEqR""" 4
.el .IP "\f(CW\-IEqR\fR" 4
.IX Item "-IEqR"
Enables/disables the inference rule Equality Resolution.
Default is 0. 
.ie n .IP """\-IERR""" 4
.el .IP "\f(CW\-IERR\fR" 4
.IX Item "-IERR"
Enables/disables the inference rule Reflexivity Resolution.
Default is 0. 
.ie n .IP """\-IEqF   """ 4
.el .IP "\f(CW\-IEqF   \fR" 4
.IX Item "-IEqF   "
Enables/disables the inference rule Equality Factoring.
Default is 0.       
.ie n .IP """\-IMPm  """ 4
.el .IP "\f(CW\-IMPm  \fR" 4
.IX Item "-IMPm  "
Enables/disables the inference rule Merging Paramodulation.
Default is 0.             
.ie n .IP """\-ISpR   """ 4
.el .IP "\f(CW\-ISpR   \fR" 4
.IX Item "-ISpR   "
Enables/disables the inference rule Superposition Right.
Default is 0.    
.ie n .IP """\-IOPm""" 4
.el .IP "\f(CW\-IOPm\fR" 4
.IX Item "-IOPm"
Enables/disables the inference rule Ordered Paramodulation.
Default is 0.      
.ie n .IP """\-ISPm   """ 4
.el .IP "\f(CW\-ISPm   \fR" 4
.IX Item "-ISPm   "
Enables/disables the inference rule Standard Paramodulation.
Default is 0.    
.ie n .IP """\-ISpL               """ 4
.el .IP "\f(CW\-ISpL               \fR" 4
.IX Item "-ISpL               "
Enables/disables the inference rule Superposition Left.
Default is 0.
.ie n .IP """\-IORe""" 4
.el .IP "\f(CW\-IORe\fR" 4
.IX Item "-IORe"
Enables/disables the inference rule Ordered Resolution.
If set to 1, Ordered Resolution is enabled but no resolution
inferences with equations are generated. If set to 2, equations
are considered for Ordered Resolution steps as well.
Default is 0. 
.ie n .IP """\-ISRe""" 4
.el .IP "\f(CW\-ISRe\fR" 4
.IX Item "-ISRe"
Enables/disables the inference rule Standard Resolution.
If set to 1, Standard Resolution is enabled but no resolution
inferences with equations are generated. If set to 2, equations
are considered for Standard Resolution steps as well.
Default is 0.   
.ie n .IP """\-ISHy """ 4
.el .IP "\f(CW\-ISHy \fR" 4
.IX Item "-ISHy "
Enables/disables the inference rule Standard Hyper\-Resolution.
Default is 0.     
.ie n .IP """\-IOHy""" 4
.el .IP "\f(CW\-IOHy\fR" 4
.IX Item "-IOHy"
Enables/disables the inference rule Ordered Hyper\-Resolution.
Default is 0.  
.ie n .IP """\-IURR""" 4
.el .IP "\f(CW\-IURR\fR" 4
.IX Item "-IURR"
Enables/disables the inference rule Unit Resulting Resolution.
Default is 0.
.ie n .IP """\-IOFc""" 4
.el .IP "\f(CW\-IOFc\fR" 4
.IX Item "-IOFc"
Enables/disables the inference rule Ordered Factoring.
If set to 1, Ordered Factoring is enabled but only factoring
inferences with positive literals are generated. If set to 2,
negative literals are considered for inferences as well.
Default is 0. 
.ie n .IP """\-ISFc""" 4
.el .IP "\f(CW\-ISFc\fR" 4
.IX Item "-ISFc"
Enables/disables the inference rule Standard Factoring.
Default is 0. 
.ie n .IP """\-IUnR""" 4
.el .IP "\f(CW\-IUnR\fR" 4
.IX Item "-IUnR"
Enables/disables the inference rule Unit Resolution.
Default is 0.        
.ie n .IP """\-IBUR""" 4
.el .IP "\f(CW\-IBUR\fR" 4
.IX Item "-IBUR"
Enables/disables the inference rule Bounded Depth Unit Resolution.
Default is 0.      
.ie n .IP """\-IDEF""" 4
.el .IP "\f(CW\-IDEF\fR" 4
.IX Item "-IDEF"
Enables/disables the inference rule Apply Definitions.
Currently not supported.
Default is 0.               
.ie n .IP """\-RFRew""" 4
.el .IP "\f(CW\-RFRew\fR" 4
.IX Item "-RFRew"
Enables/disables the reduction rule Forward Rewriting.
Default is 0.   
.ie n .IP """\-RBRew""" 4
.el .IP "\f(CW\-RBRew\fR" 4
.IX Item "-RBRew"
Enables/disables the reduction rule Backward Rewriting.
Default is 0.    
.ie n .IP """\-RFMRR""" 4
.el .IP "\f(CW\-RFMRR\fR" 4
.IX Item "-RFMRR"
Enables/disables the reduction rule Forward Matching Replacement Resolution.
Default is 0.              
.ie n .IP """\-RBMRR""" 4
.el .IP "\f(CW\-RBMRR\fR" 4
.IX Item "-RBMRR"
Enables/disables the reduction rule Backward Matching Replacement Resolution.
Default is 0.   
.ie n .IP """\-RObv""" 4
.el .IP "\f(CW\-RObv\fR" 4
.IX Item "-RObv"
Enables/disables the reduction rule Obvious Reduction.
Default is 0.                
.ie n .IP """\-RUnC""" 4
.el .IP "\f(CW\-RUnC\fR" 4
.IX Item "-RUnC"
Enables/disables the reduction rule Unit Conflict.
Default is 0. 
.ie n .IP """\-RTer """ 4
.el .IP "\f(CW\-RTer \fR" 4
.IX Item "-RTer "
Enables/disables the terminator by setting the maximal number
of non-unit clauses to be used during the search.   
Default is 0.
.ie n .IP """\-RTaut""" 4
.el .IP "\f(CW\-RTaut\fR" 4
.IX Item "-RTaut"
Enables/disables the reduction rule Tautology Deletion. If
set to 1, only syntactic tautologies are detected and
deleted. If
set to 2, additionally semantic tautologies are removed.
Default is 0.              
.ie n .IP """\-RSST""" 4
.el .IP "\f(CW\-RSST\fR" 4
.IX Item "-RSST"
Enables/disables the reduction rule Static Soft Typing.
Default is 0.            
.ie n .IP """\-RSSi""" 4
.el .IP "\f(CW\-RSSi\fR" 4
.IX Item "-RSSi"
Enables/disables the reduction rule Sort Simplification.
Default is 0.               
.ie n .IP """\-RFSub""" 4
.el .IP "\f(CW\-RFSub\fR" 4
.IX Item "-RFSub"
Enables/disables the reduction rule Forward Subsumption Deletion.
Default is 0.              
.ie n .IP """\-RBSub""" 4
.el .IP "\f(CW\-RBSub\fR" 4
.IX Item "-RBSub"
Enables/disables the reduction rule Backward Subsumption Deletion.
Default is 0.  
.ie n .IP """\-RAED""" 4
.el .IP "\f(CW\-RAED\fR" 4
.IX Item "-RAED"
Enables/disables the reduction rule Assignment Equation Deletion.
This rule removes particular occurrences of equations from clauses.
If set to 1, the reduction is guaranteed to be sound.
If set to 2, the reduction is only sound if any potential model
of the considered problem has a non-trivial domain.
Default is 0.
.ie n .IP """\-RCon""" 4
.el .IP "\f(CW\-RCon\fR" 4
.IX Item "-RCon"
Enables/disables the reduction rule Condensation.
Default is 0.               
.ie n .IP """\-TDfg2OtterOptions""" 4
.el .IP "\f(CW\-TDfg2OtterOptions\fR" 4
.IX Item "-TDfg2OtterOptions"
Enables/disables the inclusion of an Otter options
header. This option only applies to dfg2otter. If
set to 1 it includes a setting that makes Otter nearly
complete. If set to 2 it activates auto modus and if
set to 3 it activates the auto2 modus.
Default is 0.
.SH "EXAMPLES"
.IX Header "EXAMPLES"
To run \s-1SPASS\s0 on a single file without options:
.PP
.Vb 1
\&        SPASS  I<filename>
.Ve
To disable all \s-1SPASS\s0 output expect for the final result:
.PP
.Vb 1
\&        SPASS  -PGiven=0 -PProblem=0 I<filename>
.Ve
.SH "NOTES"
.IX Header "NOTES"
You can also specify options for \s-1SPASS\s0 in the input problem.
In the \s-1DFG\s0 syntax, you would use
.PP
.Vb 5
\&        list_of_settings(SPASS).
\&        {*
\&          set_flag(DocProof,1).
\&        *}
\&        end_of_list.
.Ve
to set the DocProof flag.
.PP
There are three types of options you can set in the input:
.ie n .IP """set_flag(<flag>,<value>).""" 4
.el .IP "\f(CWset_flag(<flag>,<value>).\fR" 4
.IX Item "set_flag(<flag>,<value>)."
Sets a flag to a value. Valid flags and values are described
in the \s-1OPTIONS\s0 section.
.ie n .IP """set_precedence(<comma\-separated list of function and/or predicate symbols>).""" 4
.el .IP "\f(CWset_precedence(<comma\-separated list of function and/or predicate symbols>).\fR" 4
.IX Item "set_precedence(<comma-separated list of function and/or predicate symbols>)."
Sets the precedence for the listed symbols. The precedence is
decreasing from left to right, i.e. the leftmost symbol has
the highest precedence.
.Sp
Every entry in the list has the form
.Sp
.Vb 1
\&        SYMBOL | (SYMBOL, WEIGHT [, {l, r, m}])
.Ve
You can use the second form to assign weights to symbols (for \s-1KBO\s0) or a
status (for \s-1RPOS\s0). Status is either \f(CW@t\fR{l} for left\-to\-right, \f(CW@t\fR{m} for
multiset, or \f(CW@t\fR{r} for right\-to\-left. Weight is given as an integer.
.ie n .IP """set_DomPred(<comma\-separated list of predicate symbols>).""" 4
.el .IP "\f(CWset_DomPred(<comma\-separated list of predicate symbols>).\fR" 4
.IX Item "set_DomPred(<comma-separated list of predicate symbols>)."
Listed predicate (\fIDomPred\fR for dominant predicate) symbols are
first ordered according to their precedence, not according to
their argument lists. Only in case of equal predicates, the
arguments are examined. For example, if we add the option
.Sp
.Vb 1
\&        set_DomPred(P).
.Ve
then in the clause
.Sp
.Vb 1
\&         -> R(f(x,y),a), P(x,a).
.Ve
the atom \fIP(x,a)\fR is strictly maximal.
Predicates listed by the \fIset_DomPred\fR option are
compared according to the precedence.
.SH "SEE ALSO"
.IX Header "SEE ALSO"
\&\fIcheckstat\fR\|(1), \fIfilestat\fR\|(1), \fIpcs\fR\|(1), \fIpgen\fR\|(1), \fIrescmp\fR\|(1), \fItpform\fR\|(1), \fItpget\fR\|(1), \fIdeprose\fR\|(1), \fIdfg2otter\fR\|(1), \fIdfg2otterpl\fR\|(1), \fIdfg2dfg\fR\|(1)
.SH "AUTHORS"
.IX Header "AUTHORS"
Contact : Thomas Hillenbrand <hillen@mpi\-sb.mpg.de>
          Christoph Weidenbach <weidenb@mpi\-sb.mpg.de>