TPTP2T Results Generation
Change number of sets of Solution Properties
Problem Properties (TPTP Constraints)
Domains
Any
~
Only domains:
Logical Form
Any
~
THF
TFF
FOF
CNF
TH1
TH0
TF1
TF0
First-order Subform
Any
~
Propositional
"Propositional"
Finite HU
Real 1st order
Version
Any
~
Standard
Incomplete
Augmented
Especial
Biased
Unbiased
Status
Any
~
Theorem
CounterSatisfiable
Unknown
Unsatisfiable
Satisfiable
Open
Rating
Any
~
Easy
Difficult
Unsolved
Min:
Max:
Formulae
Any
~
Min:
Max:
Unit formulae
Any
~
Min:
Max:
Atoms (Literals in CNF)
Any
~
Min:
Max:
Equality
Any
~
No equality
Some equality
Pure equality
Any equality
Unit equality
Any
No
Yes
Predicates
Any
~
1
>1
Min:
Max:
Minimal predicate arity
Any
~
0
1
2
Min:
Maximal predicate arity
Any
~
Max:
2
1
0
Functions
Any
~
0
1
>1
Min:
Max:
Minimal function arity
Any
~
0
1
2
Min:
Maximal function arity
Any
~
Max:
2
1
0
Variables
Any
~
No
Yes
PI Variables
Any
~
No
Yes
Arithmetic
Any
~
No arithmetic
With arithmetic
Solution Properties (TSTP Constraints): Set 1
System
None
~
System name:
ANY---ANY
agsyHOL---1.0
Beagle---0.9.47
Bliksem---1.12
CiME---2.01
cocATP---0.2.0
CSE---1.0
CSE_E---1.0
CVC4---1.7
CVC4---SAT-1.7
Darwin---1.4.5
DarwinFM---1.4.5
E---2.4
E---FNT-2.4
Enigma---0.4
ePrincess---1.0
E-Darwin---1.5
EQP---0.9e
Equinox---6.0.1a
Fampire---1.3
Fiesta---2
Geo-III---2018C
Etableau---0.1
GKC---0.4
GrAnDe---1.1
Infinox---1.0
iProver---3.0
iProver---SAT-3.0
iProverMo---2.5-0.1
Isabelle---2016
Isabelle-HOT---2016
leanCoP---2.2
LEO-II---1.7.0
Leo-III---1.4
Mace4---1109a
MaedMax---1.3
Matita---1.0
Metis---2.4
Moca---0.1
Muscadet---4.5
nanoCoP---1.1
Nitpick---2016
Otter---3.3
Paradox---4.0
Princess---170717
Prover9---1109a
RPx---1.0
Satallax---3.4
Satallax-MaLeS---1.3
SInE---0.4
SNARK---20120808r022
SOS---2.0
SPASS---3.9
SPASS+T---2.2.22
Twee---2.2
Vampire---THF-4.4
Vampire---4.4
Vampire---SAT-4.4
Waldmeister---710
Z3---4.4.1
Zenon---0.7.1
ZenonModulo---0.4.2
Zipperpin---1.5
Result
Any
~
SUC
THM
CSA
UNS
SAT
---
NOS
TMO
GUP
ERR
UNK
Result time
Any
~
Min:
Max:
Output
Any
~
Sol
Prf
Ref
CRf
Mod
FMo
Sat
Ass
---
Non
Solution formulae
Any
~
Min:
Max:
Solution depth
Any
~
Min:
Max:
Solution leaves
Any
~
Min:
Max:
Solution equality
Any
~
No equality
Any equality
Selectivity
Any
~
Low
Medium
High
Min:
Max:
Girth
Any
~
Fat
Thin
Min:
Max:
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