| No TPTP formula. May not be expressible in strict first order. | Catalog.kif 64-76 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3555-3555 | 子類 Proposition and Abstract |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 1630-1630 | 子類 TPFDD and Proposition |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13732-13732 | 子類 Music and Proposition |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13785-13785 | 子類 LyricalContent and Proposition |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13956-13956 | 子類 協議 and Proposition |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 22772-22772 | 子類 分類方案 and Proposition |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 27173-27173 | 子類 Policy and Proposition |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5622-5622 | 子類 Graph and Proposition |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5819-5819 | 子類 GraphElement and Proposition |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16791-16791 | 子類 FieldOfStudy and Proposition |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16799-16799 | 子類 Procedure and Proposition |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16834-16834 | 子類 爭論 and Proposition |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1541-1541 | 子類 MealPlan and Proposition |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 2725-2725 | 子類 HotelPackage and Proposition |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 647-647 | 子類 憲法 and Proposition |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 863-863 | 子類 區域法 and Proposition |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 899-899 | 子類 選舉法 and Proposition |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 1639-1639 | 子類 經濟指標 and Proposition |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3882-3882 | 子類 銀行對帳單 and Proposition |
| No TPTP formula. May not be expressible in strict first order. | engineering.kif 69-69 | 子類 模型 and Proposition |
| No TPTP formula. May not be expressible in strict first order. | engineering.kif 150-150 | 子類 方程 and Proposition |
| No TPTP formula. May not be expressible in strict first order. | engineering.kif 1240-1240 | 子類 科學法 and Proposition |
| No TPTP formula. May not be expressible in strict first order. | engineering.kif 1266-1266 | 子類 多極假設 and Proposition |
| No TPTP formula. May not be expressible in strict first order. | Catalog.kif 31-31 | 子類 Catalog and Proposition |
| No TPTP formula. May not be expressible in strict first order. | Catalog.kif 184-184 | 子類 PricingScheme and Proposition |
|
|