| No TPTP formula. May not be expressible in strict first order. | Catalog.kif 130-137 | |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 1496-1518 |
|
| No TPTP formula. May not be expressible in strict first order. | Catalog.kif 139-150 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2084-2084 | 时距 是 时间位置 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14848-14848 | 假日 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 19091-19091 | 上午 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 19104-19104 | 发布meridiem 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 19118-19118 | 周末 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 19131-19131 | 一年的季节 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8738-8738 | 年 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8765-8765 | Decade 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8857-8857 | 一天的时间 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8862-8862 | 日出 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8866-8866 | 日落 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8888-8888 | 晚上的时间 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8987-8987 | QuarterYear 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9043-9043 | 月 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9230-9230 | 日 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9332-9332 | 星期 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9340-9340 | 小时 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9350-9350 | 分钟 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9360-9360 | 秒钟 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 1849-1849 | BreakfastTime 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 1861-1861 | LunchTime 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 1878-1878 | DinnerTime 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | ArabicCulture.kif 26-26 | 斋月 是 时距 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | ArabicCulture.kif 112-112 | Dhu al hijjah 是 时距 的 subclass |
|
|