TPTP2T Results Generation
Change number of sets of Solution Properties
Problem Properties (TPTP Constraints)
Domains
Any
~
Only domains:
Logical Form
Any
~
THF
TXF
TFF
FOF
TH1
TH0
TX1
TX0
TF1
TF0
CNF
#
NHF
NXF
NH1
NH0
NX1
NX0
First-order Subform
Any
~
Propositional
Effectively Prop.
Finite HU
Real 1st order
Status
Any
~
Theorem
ContradictoryAxioms
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
Types
Any
~
0
1
>1
Min:
Max:
Symbols
Any
~
1
>1
Min:
Max:
Predicates
Any
~
1
>1
Min:
Max:
Predicate arity
Any
~
0
1
>1
Min:
Max:
Functions
Any
~
0
1
>1
Min:
Max:
Function arity
Any
~
0
1
>1
Min:
Max:
Variables
Any
~
None
Some
~
^
!
?
!>
Arithmetic
Any
~
No arithmetic
With arithmetic
Solution Properties (TSTP Constraints): Set 1
System
None
~
System name:
ANY---ANY
agsyHOL---1.0
Beagle---0.9.51
Bliksem---1.12
cocATP---0.2.0
ConnectPP---0.6.0
CSE_E---1.6
cvc5---1.1.3
cvc5-SAT---1.1.3
Darwin---1.4.5
DarwinFM---1.4.5
Drodi---3.6.0
Duper---1.0
E---3.2.0
E-SAT---3.2.0
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
Goeland---1.0.0
GKC---0.8
GrAnDe---1.1
HOLyHammer---0.21
Infinox---1.0
iProver---3.9
iProver-SAT---3.9
iProverMo---2.5-0.1
Lash---1.13
lazyCoP---0.1
leanCoP---2.2
LEO-II---1.7.0
Leo-III---1.7.16
MaedMax---1.4
Matita---1.0
Metis---2.4
Moca---0.1
Muscadet---4.5
nanoCoP---2.0
Otter---3.3
Paradox---4.0
Princess---230619
Prover9---1109a
PyRes---1.5
RPx---1.0
Satallax---3.5
SATCoP---0.1
SnakeForV---1.0
SnakeForV-SAT---1.0
SNARK---20120808r022
SPASS---3.9
SPASS+T---2.2.22
Twee---2.5.0
Vampire---4.9
Vampire-SAT---4.9
Waldmeister---710
Z3---4.13.1
Zenon---0.7.1
ZenonModulo---0.5.0
ZenonModuloLP---0.5.0
ZenonModuloDK---0.5.0
Zipperpin---2.1
Result
Any
~
SUC
THM
CAX
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 depth/Domain size
Any
~
Min:
Max:
Solution leaves
Any
~
Min:
Max:
Solution formulae
Any
~
Min:
Max:
Solution equality
Any
~
No equality
With equality
Solution arithmetic
Any
~
No arithmetic
With arithmetic
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