| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14860-14860 | 可动的假期 是 假日 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 297-297 | Advent 是 可动的假期 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 312-312 | AdventSunday 是 可动的假期 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 414-414 | Lent 是 可动的假期 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 461-461 | PalmSunday 是 可动的假期 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 486-486 | EasterSunday 是 可动的假期 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 529-529 | AscensionThursday 是 可动的假期 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 550-550 | Pentecost 是 可动的假期 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 571-571 | Hanukkah 是 可动的假期 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 600-600 | Passover 是 可动的假期 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 620-620 | USThanksgivingDay 是 可动的假期 的 subclass |
|
|