| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15422-15429 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15403-15403 | 事实文本 是 文本 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14518-14518 | 公告 是 事实文本 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14534-14534 | 表演计划 是 事实文本 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14583-14583 | 记录 是 事实文本 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14766-14766 | 信息 是 事实文本 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14770-14770 | 报告 是 事实文本 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14803-14803 | 信件 是 事实文本 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14882-14882 | 历史记录 是 事实文本 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14913-14913 | 参考书 是 事实文本 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 3462-3462 | Electrocardiogram 是 事实文本 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 2319-2319 | 党的平台 是 事实文本 的 subclass |
|
|