SpeedFn |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2483-2485 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6661-6664 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1178-1180 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6657-6657 | 速率函数 的 1 数量 是 长度测量 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6658-6658 | 速率函数 的 2 数量 是 持续时间 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6656-6656 | 速率函数 是 二元函数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6655-6655 | 速率函数 是 总值关系 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6659-6659 | 速率函数 的 range 是 函数量 的实例 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6654-6654 | 速率函数 是 每 的 subrelation |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 659-659 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 662-662 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 396-396 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 267-267 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2126-2126 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 348-348 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 862-862 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 304-304 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 418-418 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 439-439 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 459-459 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 54606-54606 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 660-660 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 54605-54605 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 54604-54604 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 2884-2902 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 11158-11166 | |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 148-157 | |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 4899-4903 | |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 115-123 | |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1718-1736 |
|
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3929-3937 |
consequent |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1702-1708 | 函数量 equal 实数 英里每小時 若且唯若 那个 函数量 equal 那个 实数 英里 除以 1 小时 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 17143-17164 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 17171-17191 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 125-130 | |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 148-157 | |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 4899-4903 | |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3939-3945 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6679-6681 |