HourFn |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2764-2768 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8617-8623 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1493-1498 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8613-8613 | 域 小時, 1 and NonnegativeInteger |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8614-8614 | 域子類 小時, 2 and Day |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8611-8611 | 例 小時 and BinaryFunction |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8612-8612 | 例 小時 and PartialValuedRelation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8610-8610 | 例 小時 and TemporalRelation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8615-8615 | 範圍子類 小時 and Hour |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 471-471 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 477-477 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 272-272 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 133-133 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2062-2062 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 224-224 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 278-278 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 614-614 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 172-172 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 293-293 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 299-299 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 272-272 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 9341-9341 | 相關的內部概念 Hour and 小時 |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 28707-28707 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 472-472 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 28706-28706 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 28705-28705 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 273-273 |
antecedent |
consequent |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3691-3711 |
|
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3735-3755 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8795-8801 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 19095-19102 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8807-8813 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 19109-19116 |
|
No TPTP formula. May not be expressible in strict first order. | Food.kif 1867-1876 |
|
statement |
No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 2143-2143 | 等於 unix時代 and 第二 0 and 分 0 and 小時 0 and 天 1 and 月 January and 年 1970 |