| 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 | 子類 Collection and Object |
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 713-713 | 子類 MonoploidChromosomeSet and Collection |
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 859-859 | 子類 HomologousChromosomeSet and Collection |
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 1057-1057 | 子類 高爾基體 and Collection |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 133-133 | 子類 WebListingCategory and Collection |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 1126-1126 | 子類 VisitorProfile and Collection |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2119-2119 | 子類 WebStore and Collection |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 4486-4486 | 子類 MultivariateTest and Collection |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 957-957 | 子類 商船 and Collection |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2049-2049 | 子類 火車 and Collection |
| No TPTP formula. May not be expressible in strict first order. | Music.kif 60-60 | 子類 Discography and Collection |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 669-669 | 子類 腳本 and Collection |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 3512-3512 | 子類 Fleet and Collection |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 5302-5302 | 子類 服裝套裝 and Collection |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7619-7619 | 子類 通訊系統 and Collection |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 11480-11480 | 子類 頭骨 and Collection |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14449-14449 | 子類 MediaSystem and Collection |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 15010-15010 | 子類 行業 and Collection |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 22323-22323 | 子類 護航 and Collection |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25452-25452 | 子類 FireSprinklerSystem and Collection |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 26961-26961 | 子類 SurveillanceSystem and Collection |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16223-16223 | 子類 Group and Collection |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 138-138 | 子類 RoomInventory and Collection |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1718-1718 | 子類 HotelMiniBar and Collection |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3362-3362 | 子類 太陽系 and Collection |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5342-5342 | 子類 內陸水系統 and Collection |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5510-5510 | 子類 河流系統 and Collection |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 5842-5842 | 子類 群島 and Collection |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 1675-1675 | 子類 Meal and Collection |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2507-2507 | 子類 一盒巧克力 and Collection |
| No TPTP formula. May not be expressible in strict first order. | Dining.kif 255-255 | 子類 Buffet and Collection |
| No TPTP formula. May not be expressible in strict first order. | Dining.kif 464-464 | 子類 Outfit and Collection |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 3317-3317 | 子類 ComputerSystem and Collection |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 3773-3773 | 子類 RemoteKeylessSystem and Collection |
|
|