appearance as argument number 1 |
![]() |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2814-2814 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 9275-9275 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 8013-8013 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 8014-8014 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 6907-6907 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 9273-9273 | Sunday is a subclass of day |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 9001-9001 | Monday is the successor class of Sunday. |
appearance as argument number 2 |
![]() |
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 |
antecedent |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 9277-9284 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 9286-9295 |
|
consequent |
![]() |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 18903-18911 |
|
![]() |
![]() |