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