| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14860-14860 | Moveable holiday is a subclass of holiday |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 297-297 | Advent is a subclass of moveable holiday |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 312-312 | Advent sunday is a subclass of moveable holiday |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 414-414 | Lent is a subclass of moveable holiday |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 461-461 | Palm sunday is a subclass of moveable holiday |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 486-486 | Easter sunday is a subclass of moveable holiday |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 529-529 | Ascension thursday is a subclass of moveable holiday |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 550-550 | Pentecost is a subclass of moveable holiday |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 571-571 | Hanukkah is a subclass of moveable holiday |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 600-600 | Passover is a subclass of moveable holiday |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 620-620 | US thanksgiving day is a subclass of moveable holiday |
|
|