TPTP2T Results Generation
Change number of sets of Solution Properties
Option Level:
Regular
Advanced
Problem Properties (TPTP Constraints)
Problem type
Any
~
FOF
CNF
Status
Any
~
Theorem
CounterSatisfiable
Unknown
Unsatisfiable
Satisfiable
Open
Order
Any
~
Propositional
"Propositional"
Finite HU
Real 1st order
Predicates
Any
~
1 predicate
> 1 predicate
Equality
Any
~
No equality
Some equality
Pure equality
Any equality
Unit equality
Any
~
No
Yes
Horn
Any
~
Horn
Non-Horn
Range restricted
Any
~
Range restricted
Not range restricted
Formulae
Any
~
Small
Medium
Large
XLarge
Clauses
Any
~
Small
Medium
Large
XLarge
Rating
Any
~
Easy
Difficult
Unsolved
Version
Any
~
Standard
Incomplete
Augmented
Especial
Biased
Unbiased
Domains
Any
~
Only domains:
Solution Properties (TSTP Constraints): Set 1
System
None
~
System name:
ANY
Bliksem---1.12
CARINE---0.734
Darwin---1.4.2
DCTP---1.31
E---0.999
E-KRHyper---1.1
EP---0.999
Equinox---1.3
Faust---1.0
FDP---0.9.16
Gandalf---c-2.6
Geo---2007f
iProver---0.3
iProver---0.5crv
leanCoP---2.0
LeanTAP---2.3
Metis---2.1
Otter---3.3
Prover9---1207
randoCoP---2.0
SCOTT---6.1
SETHEO---3.3
SNARK---20070805r043
SOS---2.0
SPASS---3.01
S-SETHEO---0.0
Theo---2006
Vampire---9.0
Result
Any
~
SUC
THM
CSA
UNS
SAT
---
NOS
TMO
GUP
UNK
Output
Any
~
Sln
Ass
Ref
CRf
Mod
FMo
---
Non
Selectivity
Any
~
Low
Medium
High
Girth
Any
~
Fat
Thin
Solution Properties (TSTP Constraints): Set 2
System
None
~
System name:
ANY
Bliksem---1.12
CARINE---0.734
Darwin---1.4.2
DCTP---1.31
E---0.999
E-KRHyper---1.1
EP---0.999
Equinox---1.3
Faust---1.0
FDP---0.9.16
Gandalf---c-2.6
Geo---2007f
iProver---0.3
iProver---0.5crv
leanCoP---2.0
LeanTAP---2.3
Metis---2.1
Otter---3.3
Prover9---1207
randoCoP---2.0
SCOTT---6.1
SETHEO---3.3
SNARK---20070805r043
SOS---2.0
SPASS---3.01
S-SETHEO---0.0
Theo---2006
Vampire---9.0
Result
Any
~
SUC
THM
CSA
UNS
SAT
---
NOS
TMO
GUP
UNK
Output
Any
~
Sln
Ass
Ref
CRf
Mod
FMo
---
Non
Selectivity
Any
~
Low
Medium
High
Girth
Any
~
Fat
Thin
Output Options
Print Problems
Print Solutions
Print Problems and Solutions
Noisy: Print Progress Ticks, Plus Below
Semi-Quiet: Print Headers and Final Count
Quiet: Print Only Content
Password required:
Created by
Alex Roederer
, University of Miami, 2008