No TPTP formula. May not be expressible in strict first order. |
Media.kif 311-311 |
Advent sunday is a subclass of Sunday |
No TPTP formula. May not be expressible in strict first order. |
Media.kif 485-485 |
Easter sunday is a subclass of Sunday |
No TPTP formula. May not be expressible in strict first order. |
Media.kif 460-460 |
Palm sunday is a subclass of Sunday |
No TPTP formula. May not be expressible in strict first order. |
Media.kif 551-551 |
Pentecost is a subclass of Sunday |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 1296-1296 |
|
No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1809-1809 |
|
No TPTP formula. May not be expressible in strict first order. |
french_format.kif 974-974 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 509-509 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 511-511 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2658-2658 |
|
No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 926-926 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cb.txt 515-515 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 549-549 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 995-995 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 514-514 |
|