No TPTP formula. May not be expressible in strict first order. | Merge.kif 9269-9269 | Thursday is a subclass of day |
No TPTP formula. May not be expressible in strict first order. | Media.kif 530-530 | Ascension thursday is a subclass of Thursday |
No TPTP formula. May not be expressible in strict first order. | Media.kif 621-621 | US thanksgiving day is a subclass of Thursday |