No TPTP formula. May not be expressible in strict first order. | Merge.kif 2232-2232 | Binary relation is a subclass of relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2233-2233 | Binary relation is a subclass of inheritable relation |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16900-16900 | Economic relation is a subclass of binary relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2239-2239 | Reflexive relation is a subclass of binary relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2249-2249 | Irreflexive relation is a subclass of binary relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2260-2260 | Symmetric relation is a subclass of binary relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2292-2292 | Antisymmetric relation is a subclass of binary relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2310-2310 | Trichotomizing relation is a subclass of binary relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2333-2333 | Transitive relation is a subclass of binary relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2349-2349 | Intransitive relation is a subclass of binary relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3359-3359 | Unary function is a subclass of binary relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3479-3479 | Binary predicate is a subclass of binary relation |