![]() |
![]() ![]() ![]()
|
![]() |
|
appearance as argument number 1 |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8694-8694 | Afternoon is disjoint from Evening |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8691-8692 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8690-8690 | 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 8693-8693 | Morning is disjoint from afternoon |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8737-8737 | The range of AfternoonFn is an instance of afternoon |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 5775-5775 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 5774-5774 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 5773-5773 |
antecedent |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8742-8747 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8824-8831 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8749-8754 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8697-8703 |
|
![]() |
![]() |