| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15400-15407 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15381-15381 | 子類 事實文本 and Text |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14519-14519 | 子類 公告 and 事實文本 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14535-14535 | 子類 表演計劃 and 事實文本 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14584-14584 | 子類 記錄 and 事實文本 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14767-14767 | 子類 信息 and 事實文本 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14771-14771 | 子類 報告 and 事實文本 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14804-14804 | 子類 信件 and 事實文本 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14883-14883 | 子類 歷史記錄 and 事實文本 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14914-14914 | 子類 參考書 and 事實文本 |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 3462-3462 | 子類 Electrocardiogram and 事實文本 |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 2319-2319 | 子類 黨的平台 and 事實文本 |
|
|