| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9851-9851 | 洞 是 地区 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 959-959 | 高尔夫球洞 是 洞 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 6142-6142 | Glottis 是 洞 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 12047-12047 | BodyOrifice 是 洞 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 12121-12121 | Pupil 是 洞 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6012-6012 | 洞穴 是 洞 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6027-6027 | 地洞 是 洞 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3659-3659 | ATM插槽 是 洞 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 311-311 | InternalCombustionChamber 是 洞 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 324-324 | Crankcase 是 洞 的 subclass |
|
|