Afternoon(afternoon) | ![]() | afternoon |
appearance as argument number 1 |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8776-8776 | Afternoon is disjoint from evening |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8773-8774 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8772-8772 | Afternoon is a subclass of day time |
appearance as argument number 2 |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8775-8775 | Morning is disjoint from afternoon |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8819-8819 | The range of afternoon of is an instance of afternoon |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 5771-5771 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 5770-5770 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 5769-5769 |
antecedent |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8824-8829 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8906-8913 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8831-8836 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8779-8785 |
|
![]() |
![]() |