SPASS(1) on Linux
The text 4e477fb1e531, as Debian 9 (Stretch), Debian 8 (Jessie), Debian 7 (Wheezy), Debian 6.0 (Squeeze) shipped it. The page shows this text now.
automated theorem prover for full first-order logic with equality
Flags it lists
-
-ApplyDefs -
-Auto -
-BoundLoops -
-BoundMode -
-BoundStart -
-CNFCon -
-CNFFEqR -
-CNFOptSkolem -
-CNFPRenaming -
-CNFProofSteps -
-CNFQuantExch -
-CNFRedTime -
-CNFRenMatch -
-CNFRenaming -
-CNFStrSkolem -
-CNFSub -
-DocProof -
-DocSST -
-DocSplit -
-EML -
-EML2Rel -
-EMLAuto -
-EMLElimComp -
-EMLFFSorts -
-EMLFuncNary -
-EMLFuncNdeQ -
-EMLPTrans -
-EMLTheory -
-EMLTranslation -
-FPDFGProof -
-FPModel -
-Flotter -
-FullRed -
-FuncWeight -
-IBUR -
-IDEF -
-IERR -
-IEmS -
-IEqF -
-IEqR -
-IMPm -
-IOFc -
-IOHy -
-IOPm -
-IORe -
-ISFc -
-ISHy -
-ISPm -
-ISRe -
-ISoR -
-ISpL -
-ISpR -
-IURR -
-IUnR -
-Interactive -
-Loops -
-Memory -
-Ordering -
-PAED -
-PApplyDefs -
-PBDC -
-PBInc -
-PCon -
-PDer -
-PEmptyClause -
-PFlags -
-PGiven -
-PKept -
-PLabels -
-PMRR -
-PObv -
-POptSkolem -
-PProblem -
-PRew -
-PSST -
-PSSi -
-PStatistic -
-PStrSkolem -
-PSub -
-PTaut -
-PUnC -
-PrefCon -
-PrefVar -
-RAED -
-RBMRR -
-RBRew -
-RBSub -
-RCon -
-RFMRR -
-RFRew -
-RFSub -
-RInput -
-RObv -
-RSST -
-RSSi -
-RTaut -
-RTer -
-RUnC -
-SOS -
-SatInput -
-Select -
-Sorts -
-Splits -
-Stdin -
-TDfg2OtterOptions -
-TPTP -
-TimeLimit -
-VarWeight -
-WDRatio -
-rf