TPTP2T Results Generation
Change number of sets of Solution Properties
Option Level:
Regular
Advanced
Problem Properties (TPTP Constraints)
Problem type
Any
~
THF
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---ANY
Ayane---1.1
Bliksem---1.12
CARINE---0.734
CiME---2.01
Darwin---1.4.5
DarwinFM---1.4.5
DCTP---1.31
E---1.1
EP---1.1
E-Darwin---1.2
E-KRHyper---1.1.3
EQP---0.9e
Equinox---4.1
Fampire---1.3
FDP---0.9.16
Fiesta---2
Geo---2007f
GrAnDe---1.1
Infinox---1.0
iProver---0.7
iProver-SAT---0.7
IsabelleP---2009
IsabelleM---2009
IsabelleN---2009
leanCoP---2.1
randoCoP---1.1
LeanTAP---2.3
LEO-II---1.1
Mace2---2.2
Mace4---0908
Matita---1.0
Metis---2.2
Muscadet---3.0
Otter---3.3
Paradox---3.0
Prover9---0908
S-SETHEO---0.0
SETHEO---3.3
SInE---0.4
SNARK---20080805r005
SOS---2.0
SPASS---3.01
SRASS---0.1
Theo---2006
TPS---3.080227G1d
Vampire---9.0
VampireLT---10.0
Vampire---11.0
Waldmeister---C09a
zChaff---04.11.15
Zenon---0.5.0
Result
Any
~
SUC
THM
CSA
UNS
SAT
---
NOS
TMO
GUP
ERR
UNK
Output
Any
~
Sol
Prf
Ref
CRf
Mod
FMo
Sat
Ass
---
Non
Solution equality
Any
~
No equality
Any equality
Selectivity
Any
~
Low
Medium
High
Girth
Any
~
Fat
Thin
Solution Properties (TSTP Constraints): Set 2
System
None
~
System name:
ANY---ANY
Ayane---1.1
Bliksem---1.12
CARINE---0.734
CiME---2.01
Darwin---1.4.5
DarwinFM---1.4.5
DCTP---1.31
E---1.1
EP---1.1
E-Darwin---1.2
E-KRHyper---1.1.3
EQP---0.9e
Equinox---4.1
Fampire---1.3
FDP---0.9.16
Fiesta---2
Geo---2007f
GrAnDe---1.1
Infinox---1.0
iProver---0.7
iProver-SAT---0.7
IsabelleP---2009
IsabelleM---2009
IsabelleN---2009
leanCoP---2.1
randoCoP---1.1
LeanTAP---2.3
LEO-II---1.1
Mace2---2.2
Mace4---0908
Matita---1.0
Metis---2.2
Muscadet---3.0
Otter---3.3
Paradox---3.0
Prover9---0908
S-SETHEO---0.0
SETHEO---3.3
SInE---0.4
SNARK---20080805r005
SOS---2.0
SPASS---3.01
SRASS---0.1
Theo---2006
TPS---3.080227G1d
Vampire---9.0
VampireLT---10.0
Vampire---11.0
Waldmeister---C09a
zChaff---04.11.15
Zenon---0.5.0
Result
Any
~
SUC
THM
CSA
UNS
SAT
---
NOS
TMO
GUP
ERR
UNK
Output
Any
~
Sol
Prf
Ref
CRf
Mod
FMo
Sat
Ass
---
Non
Solution equality
Any
~
No equality
Any equality
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