| No TPTP formula. May not be expressible in strict first order. | Media.kif 3203-3205 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1261-1261 | 群体 是 客体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 713-713 | MonoploidChromosomeSet 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 859-859 | HomologousChromosomeSet 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 1057-1057 | 高尔基体 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 133-133 | WebListingCategory 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 1126-1126 | VisitorProfile 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2119-2119 | WebStore 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 4486-4486 | MultivariateTest 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 957-957 | 商船 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2049-2049 | 火车 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Music.kif 60-60 | Discography 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 669-669 | 脚本 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 3512-3512 | Fleet 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 5302-5302 | 服装套装 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7619-7619 | 通讯系统 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 11480-11480 | 头骨 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14449-14449 | MediaSystem 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 15010-15010 | 行业 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 22323-22323 | 护航 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25452-25452 | FireSprinklerSystem 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 26961-26961 | SurveillanceSystem 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16223-16223 | 群组 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 138-138 | RoomInventory 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1718-1718 | HotelMiniBar 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3362-3362 | 太阳系 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5342-5342 | 内陆水系统 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5510-5510 | 河流系统 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5842-5842 | 群岛 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 1675-1675 | Meal 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2507-2507 | 一盒巧克力 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Dining.kif 255-255 | Buffet 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Dining.kif 464-464 | Outfit 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 3317-3317 | ComputerSystem 是 群体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 3773-3773 | RemoteKeylessSystem 是 群体 的 subclass |
|
|