Afternoon
|
|
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8814-8814 | 下午 和 % 2 是 disjoint |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8811-8812 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8810-8810 | 下午 是 一天的时间 的 subclass |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8813-8813 | 早上 和 % 2 是 disjoint |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8857-8857 | AfternoonFn 的 range 是 下午 的实例 |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 5766-5766 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 5765-5765 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 5764-5764 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8862-8867 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8944-8951 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8869-8874 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8817-8823 |