| No TPTP formula. May not be expressible in strict first order. | Government.kif 619-625 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14855-14855 | 固定假期 是 假日 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 336-336 | ChristmasDay 是 固定假期 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 518-518 | Epiphany 是 固定假期 的 subclass |
|
|