TPTP2T Results Generation

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:

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: