| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24236-24246 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24195-24206 | |
| 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 9240-9240 | 星期一 是 日 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9243-9243 | 星期二 是 日 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9256-9256 | 星期三 是 日 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9269-9269 | 星期四 是 日 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9282-9282 | 星期五 是 日 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9295-9295 | 星期六 是 日 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 9308-9308 | 星期日 是 日 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 335-335 | ChristmasDay 是 日 的 subclass |
|
|