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
Beagle---SAT-0.9.47
Bliksem---1.12
CiME---2.01
cocATP---0.2.0
CVC4---TFF-1.5.1
CVC4---TFN-1.5.1
CVC4---FOF-1.5.1
CVC4---FNT-1.5.1
Darwin---1.4.5
DarwinFM---1.4.5
E---2.0
ePrincess---1.0
E-Darwin---1.5
EQP---0.9e
Equinox---5.0
ET---0.2
Fampire---1.3
Fiesta---2
Geo-III---2016C
GrAnDe---1.1
Infinox---1.0
iProver---2.5
iProver---SAT-2.5
iProverMo---0.7-0.3
Isabelle---2016
Isabelle-HOT---2016
leanCoP---2.2
LEO-II---1.7.0
Leo-III---1.0
Leo+III---1.0
Mace4---1109a
Matita---1.0
Metis---2.3
Muscadet---4.5
Nitpick---2016
Otter---3.3
Princess---160606
Prover9---1109a
Satallax---3.0
Satallax-MaLeS---1.3
SInE---0.4
SNARK---20120808r022
SOS---2.0
SPASS---3.9
SPASS+T---2.2.22
tWEE---1.0
Vampire---4.1
Vampire---SAT-4.1
Waldmeister---710
Z3---4.4.1
Zenon---0.7.1
ZenonModulo---0.4.1
Zipperpin---FOF-0.4
Zipperpin---TFF-0.4
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