TimeIntervalFn |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2729-2731 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8415-8418 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1454-1456 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8411-8411 | 时段函数 的 1 数量 是 时点 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8412-8412 | 时段函数 的 2 数量 是 时点 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8408-8408 | 时段函数 是 二元函数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8410-8410 | 时段函数 是 部分值关系 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8409-8409 | 时段函数 是 时间关系 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8413-8413 | 时段函数 的 range 是 时距 的实例 |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 453-453 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 459-459 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 263-263 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 300-300 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2053-2053 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 215-215 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 269-269 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 592-592 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 336-336 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 284-284 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 289-289 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 492-492 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 454-454 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 58124-58124 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 58123-58123 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 58122-58122 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 23889-23903 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8420-8428 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8430-8439 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14040-14046 |
consequent |
No TPTP formula. May not be expressible in strict first order. | Media.kif 1936-1941 | |
No TPTP formula. May not be expressible in strict first order. | Media.kif 1943-1948 | |
No TPTP formula. May not be expressible in strict first order. | Media.kif 1959-1963 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7524-7528 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30030-30060 |
|
No TPTP formula. May not be expressible in strict first order. | Dining.kif 711-724 |
|
No TPTP formula. May not be expressible in strict first order. | Hotel.kif 2951-2963 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8521-8523 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8490-8492 | |
No TPTP formula. May not be expressible in strict first order. | Food.kif 1867-1876 | |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1878-1886 |