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 数量 是 非负整数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8614-8614 | 时函数 的 2 数量 是 日 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8611-8611 | 时函数 是 二元函数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8612-8612 | 时函数 是 部分值关系 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8610-8610 | 时函数 是 时间关系 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8615-8615 | 时函数 的所得值 是 小时 的 subclass |
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 | 小时 和 时函数 是 内部相关 |
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 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8629-8634 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17206-17212 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17218-17224 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17194-17200 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17182-17188 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8625-8627 |
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时代 equal 0 second |