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
cocATP---0.2.0
CSE---1.4
cvc5---1.0
cvc5---SAT-1.0
Darwin---1.4.5
DarwinFM---1.4.5
Drodi---3.1
E---2.6
E---FNT-2.6
Ehoh---2.7
Enigma---0.5.1
ePrincess---1.0
Etableau---0.67
EQP---0.9e
Equinox---6.0.1a
Fampire---1.3
Fiesta---2
Geo-III---2018C
GKC---0.7
GrAnDe---1.1
HOLyHammer---0.21
Infinox---1.0
iProver---3.5
iProver---SAT-3.5
iProverMo---2.5-0.1
Isabelle---2016
Isabelle-HOT---2016
lazyCoP---0.1
leanCoP---2.2
LEO-II---1.7.0
Leo-III---1.6
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
PyRes---1.3
RPx---1.0
Satallax---3.5
Satallax-MaLeS---1.3
SATCoP---0.1
SNARK---20120808r022
SOS---2.0
SPASS---3.9
SPASS+T---2.2.22
Twee---2.4
Vampire---4.6.1
Vampire-SAT---4.6.1
Waldmeister---710
Z3---4.8.9.0
Zenon---0.7.1
ZenonModulo---0.4.2
Zipperpin---2.1
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