TPTP2T Results Generation

Problem Properties (TPTP Constraints)

Domains	Any	~	Only:

Logical Form	Any	~	FOF	TFF	TXF	THF
			CNF	TF0 TF1	TX0 TX1	TH0 TH1
		#	NXF	NHF		DHF
			NX0 NX1	NH0 NH1		DH0 DH1
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:
Datatypes	Any	~	0	1	>1	Min: Max:
Codatatypes	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		None	Some

Solution Properties (TSTP Constraints): Set 1

System	None	~	System name: Any version This version

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: