| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14859-14859 | MoveableHoliday est une sous-classe de Holiday |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 297-297 | Advent est une sous-classe de MoveableHoliday |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 312-312 | AdventSunday est une sous-classe de MoveableHoliday |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 414-414 | Lent est une sous-classe de MoveableHoliday |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 461-461 | PalmSunday est une sous-classe de MoveableHoliday |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 486-486 | EasterSunday est une sous-classe de MoveableHoliday |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 529-529 | AscensionThursday est une sous-classe de MoveableHoliday |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 550-550 | Pentecost est une sous-classe de MoveableHoliday |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 571-571 | Hanukkah est une sous-classe de MoveableHoliday |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 600-600 | Passover est une sous-classe de MoveableHoliday |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 620-620 | USThanksgivingDay est une sous-classe de MoveableHoliday |
|
|