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:

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

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

Password required: