|
|
   ChristianHoliday
|
|
|
| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Media.kif 265-267 | |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 264-264 | ChristianHoliday is a subclass of holiday |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Media.kif 296-296 | Advent is a subclass of ChristianHoliday |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 310-310 | AdventSunday is a subclass of ChristianHoliday |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 528-528 | AscensionThursday is a subclass of ChristianHoliday |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 334-334 | ChristmasDay is a subclass of ChristianHoliday |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 484-484 | EasterSunday is a subclass of ChristianHoliday |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 516-516 | Epiphany is a subclass of ChristianHoliday |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 413-413 | Lent is a subclass of ChristianHoliday |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 459-459 | PalmSunday is a subclass of ChristianHoliday |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 549-549 | Pentecost is a subclass of ChristianHoliday |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Media.kif 269-274 |
|
|
|
|