| No TPTP formula. May not be expressible in strict first order. | Media.kif 264-264 | ChristianHoliday 是 假日 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 296-296 | Advent 是 ChristianHoliday 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 310-310 | AdventSunday 是 ChristianHoliday 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 334-334 | ChristmasDay 是 ChristianHoliday 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 413-413 | Lent 是 ChristianHoliday 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 459-459 | PalmSunday 是 ChristianHoliday 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 484-484 | EasterSunday 是 ChristianHoliday 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 516-516 | Epiphany 是 ChristianHoliday 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 528-528 | AscensionThursday 是 ChristianHoliday 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 549-549 | Pentecost 是 ChristianHoliday 的 subclass |
|
|