| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2232-2232 | 子類 BinaryRelation and Relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2233-2233 | 子類 BinaryRelation and 可繼承的關係 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16900-16900 | 子類 經濟關係 and BinaryRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2239-2239 | 子類 ReflexiveRelation and BinaryRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2249-2249 | 子類 IrreflexiveRelation and BinaryRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2260-2260 | 子類 SymmetricRelation and BinaryRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2292-2292 | 子類 AntisymmetricRelation and BinaryRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2310-2310 | 子類 TrichotomizingRelation and BinaryRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2333-2333 | 子類 TransitiveRelation and BinaryRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2349-2349 | 子類 IntransitiveRelation and BinaryRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3359-3359 | 子類 UnaryFunction and BinaryRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3479-3479 | 子類 BinaryPredicate and BinaryRelation |
|
|