| Annotation | Data.TPTP |
| Application | Data.TPTP |
| Assumption | Data.TPTP |
| Assumptions | Data.TPTP |
| Atom | |
| 1 (Type/Class) | Data.TPTP |
| 2 (Data Constructor) | Data.TPTP |
| atom | Data.TPTP.Parse.Combinators |
| Atomic | Data.TPTP |
| Axiom | Data.TPTP |
| Bind | Data.TPTP |
| ByAssumption | Data.TPTP |
| ByAxiomOfChoice | Data.TPTP |
| ByDefinition | Data.TPTP |
| ByTautology | Data.TPTP |
| CAX | Data.TPTP |
| Ceiling | Data.TPTP |
| CEQ | Data.TPTP |
| Clause | |
| 1 (Type/Class) | Data.TPTP |
| 2 (Data Constructor) | Data.TPTP |
| clause | |
| 1 (Function) | Data.TPTP |
| 2 (Function) | Data.TPTP.Parse.Combinators |
| CNF | Data.TPTP |
| CNF_ | Data.TPTP |
| Conjecture | Data.TPTP |
| Conjunction | Data.TPTP |
| Connected | Data.TPTP |
| Connective | Data.TPTP |
| Corollary | Data.TPTP |
| Creator | Data.TPTP |
| CSA | Data.TPTP |
| CSP | Data.TPTP |
| CTH | Data.TPTP |
| CUP | Data.TPTP |
| Declaration | Data.TPTP |
| declarationLanguage | Data.TPTP |
| Defined | Data.TPTP |
| Definition | Data.TPTP |
| Description | Data.TPTP |
| Difference | Data.TPTP |
| Disjunction | Data.TPTP |
| Distinct | Data.TPTP |
| DistinctObject | |
| 1 (Type/Class) | Data.TPTP |
| 2 (Data Constructor) | Data.TPTP |
| distinctObject | Data.TPTP.Parse.Combinators |
| DistinctTerm | Data.TPTP |
| ECS | Data.TPTP |
| ECT | Data.TPTP |
| Equality | Data.TPTP |
| Equivalence | Data.TPTP |
| EQV | Data.TPTP |
| ESA | Data.TPTP |
| ETH | Data.TPTP |
| ExclusiveOr | Data.TPTP |
| Exists | Data.TPTP |
| Expression | |
| 1 (Data Constructor) | Data.TPTP |
| 2 (Type/Class) | Data.TPTP |
| Extended | Data.TPTP |
| extended | Data.TPTP |
| Falsum | Data.TPTP |
| FiDomain | Data.TPTP |
| FiFunctors | Data.TPTP |
| File | Data.TPTP |
| FiPredicates | Data.TPTP |
| FirstOrder | Data.TPTP |
| Floor | Data.TPTP |
| FOF | Data.TPTP |
| FOF_ | Data.TPTP |
| Forall | Data.TPTP |
| Formula | |
| 1 (Data Constructor) | Data.TPTP |
| 2 (Type/Class) | Data.TPTP |
| formulaLanguage | Data.TPTP |
| FSA | Data.TPTP |
| FUN | Data.TPTP |
| Function | |
| 1 (Data Constructor) | Data.TPTP |
| 2 (Type/Class) | Data.TPTP |
| function | Data.TPTP.Parse.Combinators |
| Greater | Data.TPTP |
| Greatereq | Data.TPTP |
| Hypothesis | Data.TPTP |
| I | Data.TPTP |
| Implication | Data.TPTP |
| Include | Data.TPTP |
| Inference | Data.TPTP |
| Info | Data.TPTP |
| info | Data.TPTP.Parse.Combinators |
| InfoNumber | Data.TPTP |
| Infos | Data.TPTP |
| Int | Data.TPTP |
| IntegerConstant | Data.TPTP |
| Intro | Data.TPTP |
| intro | Data.TPTP.Parse.Combinators |
| Introduced | Data.TPTP |
| Iquote | Data.TPTP |
| isAssociative | Data.TPTP |
| IsInt | Data.TPTP |
| IsRat | Data.TPTP |
| isValidAtom | Data.TPTP |
| isValidDistinctObject | Data.TPTP |
| isValidReserved | Data.TPTP |
| isValidVar | Data.TPTP |
| Language | Data.TPTP |
| Lemma | Data.TPTP |
| Less | Data.TPTP |
| Lesseq | Data.TPTP |
| Literal | Data.TPTP |
| literal | Data.TPTP.Parse.Combinators |
| Logical | Data.TPTP |
| MonomorphicFirstOrder | Data.TPTP |
| monomorphicFirstOrder | Data.TPTP.Parse.Combinators |
| monomorphizeFirstOrder | Data.TPTP |
| monomorphizeTFF1Sort | Data.TPTP |
| Name | Data.TPTP |
| name | Data.TPTP |
| Named | Data.TPTP |
| Negated | Data.TPTP |
| NegatedConjecture | Data.TPTP |
| NegatedConjunction | Data.TPTP |
| NegatedDisjunction | Data.TPTP |
| Negative | Data.TPTP |
| NewSymbols | Data.TPTP |
| NOC | Data.TPTP |
| Number | |
| 1 (Data Constructor) | Data.TPTP |
| 2 (Type/Class) | Data.TPTP |
| number | Data.TPTP.Parse.Combinators |
| O | Data.TPTP |
| Parent | |
| 1 (Type/Class) | Data.TPTP |
| 2 (Data Constructor) | Data.TPTP |
| parent | Data.TPTP.Parse.Combinators |
| parseTPTP | |
| 1 (Function) | Data.TPTP.Parse.Text |
| 2 (Function) | Data.TPTP.Parse.Text.Lazy |
| parseTPTPOnly | Data.TPTP.Parse.Text |
| parseTPTPWith | Data.TPTP.Parse.Text |
| parseUnit | |
| 1 (Function) | Data.TPTP.Parse.Text |
| 2 (Function) | Data.TPTP.Parse.Text.Lazy |
| parseUnitOnly | Data.TPTP.Parse.Text |
| parseUnitWith | Data.TPTP.Parse.Text |
| Plain | Data.TPTP |
| PolymorphicFirstOrder | Data.TPTP |
| polymorphicFirstOrder | Data.TPTP.Parse.Combinators |
| Positive | Data.TPTP |
| Predicate | |
| 1 (Data Constructor) | Data.TPTP |
| 2 (Type/Class) | Data.TPTP |
| predicate | Data.TPTP.Parse.Combinators |
| Pretty | Data.TPTP.Pretty |
| pretty | Data.TPTP.Pretty |
| prettyList | Data.TPTP.Pretty |
| Product | Data.TPTP |
| Quantified | Data.TPTP |
| quantified | Data.TPTP |
| QuantifiedSort | |
| 1 (Type/Class) | Data.TPTP |
| 2 (Data Constructor) | Data.TPTP |
| Quantifier | Data.TPTP |
| Quotient | Data.TPTP |
| QuotientE | Data.TPTP |
| QuotientF | Data.TPTP |
| QuotientT | Data.TPTP |
| Rat | Data.TPTP |
| RationalConstant | Data.TPTP |
| Real | Data.TPTP |
| RealConstant | Data.TPTP |
| Refutation | Data.TPTP |
| RemainderE | Data.TPTP |
| RemainderF | Data.TPTP |
| RemainderT | Data.TPTP |
| Reserved | |
| 1 (Data Constructor) | Data.TPTP |
| 2 (Type/Class) | Data.TPTP |
| ReversedImplication | Data.TPTP |
| Role | Data.TPTP |
| Round | Data.TPTP |
| SAP | Data.TPTP |
| SAT | Data.TPTP |
| SCA | Data.TPTP |
| SCC | Data.TPTP |
| Sign | Data.TPTP |
| Sort | |
| 1 (Data Constructor) | Data.TPTP |
| 2 (Type/Class) | Data.TPTP |
| sort | Data.TPTP.Parse.Combinators |
| Sorted | |
| 1 (Type/Class) | Data.TPTP |
| 2 (Data Constructor) | Data.TPTP |
| SortedFirstOrder | Data.TPTP |
| sortedFirstOrder | Data.TPTP.Parse.Combinators |
| SortVariable | Data.TPTP |
| Source | Data.TPTP |
| source | Data.TPTP.Parse.Combinators |
| Standard | Data.TPTP |
| Status | |
| 1 (Data Constructor) | Data.TPTP |
| 2 (Type/Class) | Data.TPTP |
| SUC | Data.TPTP |
| Sum | Data.TPTP |
| TAC | Data.TPTP |
| TAU | Data.TPTP |
| Tautology | Data.TPTP |
| TCA | Data.TPTP |
| Term | |
| 1 (Data Constructor) | Data.TPTP |
| 2 (Type/Class) | Data.TPTP |
| term | Data.TPTP.Parse.Combinators |
| TFF0 | Data.TPTP |
| TFF1 | Data.TPTP |
| TFF1Sort | |
| 1 (Type/Class) | Data.TPTP |
| 2 (Data Constructor) | Data.TPTP |
| tff1Sort | Data.TPTP.Parse.Combinators |
| TFF1Type | Data.TPTP |
| tff1Type | Data.TPTP |
| TFF_ | Data.TPTP |
| Theorem | Data.TPTP |
| Theory | Data.TPTP |
| THM | Data.TPTP |
| ToInt | Data.TPTP |
| ToRat | Data.TPTP |
| ToReal | Data.TPTP |
| TPTP | |
| 1 (Type/Class) | Data.TPTP |
| 2 (Data Constructor) | Data.TPTP |
| tptp | Data.TPTP.Parse.Combinators |
| Truncate | Data.TPTP |
| Type | |
| 1 (Type/Class) | Data.TPTP |
| 2 (Data Constructor) | Data.TPTP |
| type_ | Data.TPTP.Parse.Combinators |
| Typing | Data.TPTP |
| UCA | Data.TPTP |
| Uminus | Data.TPTP |
| UNC | Data.TPTP |
| Unit | |
| 1 (Type/Class) | Data.TPTP |
| 2 (Data Constructor) | Data.TPTP |
| unit | Data.TPTP.Parse.Combinators |
| UnitName | Data.TPTP |
| units | Data.TPTP |
| UnitSource | Data.TPTP |
| Unknown | Data.TPTP |
| UnknownSource | Data.TPTP |
| UNP | Data.TPTP |
| UNS | Data.TPTP |
| Unsorted | |
| 1 (Type/Class) | Data.TPTP |
| 2 (Data Constructor) | Data.TPTP |
| UnsortedFirstOrder | Data.TPTP |
| unsortedFirstOrder | Data.TPTP.Parse.Combinators |
| Var | |
| 1 (Type/Class) | Data.TPTP |
| 2 (Data Constructor) | Data.TPTP |
| var | Data.TPTP.Parse.Combinators |
| Variable | Data.TPTP |
| WCA | Data.TPTP |
| WCC | Data.TPTP |
| WCT | Data.TPTP |
| WEC | Data.TPTP |
| whitespace | Data.TPTP.Parse.Combinators |
| WTC | Data.TPTP |
| WTH | Data.TPTP |
| WUC | Data.TPTP |