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
First-order Subform Any ~ Propositional "Propositional" Finite HU Real 1st order

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:

Result Any ~
Result time Any ~ Min: Max:
Output Any ~

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

Password required: