EndFn |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2699-2700 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8035-8036 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1422-1423 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8032-8032 | 结束函数 的 1 数量 是 时距 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8029-8029 | 结束函数 是 时间关系 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8031-8031 | 结束函数 是 总值关系 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8030-8030 | 结束函数 是 一元函数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8033-8033 | 结束函数 的 range 是 时点 的实例 |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 451-451 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 457-457 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 262-262 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 92-92 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2052-2052 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 214-214 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 268-268 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 589-589 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 132-132 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 283-283 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 288-288 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 199-199 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 22042-22042 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 452-452 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 22041-22041 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 22040-22040 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 200-200 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8108-8116 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8076-8084 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 22919-22924 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29583-29592 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 12405-12419 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3759-3784 |
|
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 1087-1099 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 11669-11676 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 12453-12462 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2456-2466 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8376-8386 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 1496-1518 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8284-8289 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8291-8301 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 12826-12832 | |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 2669-2685 | |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 2623-2639 | |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 2687-2703 | |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 2641-2659 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8047-8052 | |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 834-842 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8404-8406 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8038-8045 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8361-8365 | |
No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 1270-1284 |
|
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
consequent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 12488-12495 | 过程 是 结合 的 instance 和 客体 是 那个 过程 的 resource 和 实体 是 那个 过程 的 result 若且唯若 那个 客体 不 是 那个 实体 的 part 在 那个 过程 出现 的 time 的开始 holdsDuring 和 那个 客体 是 那个 实体 的 part 在 那个 过程 出现 的 time 的结束 holdsDuring |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 655-667 | |
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. | Merge.kif 15537-15554 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 21494-21505 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 17142-17163 |
|
No TPTP formula. May not be expressible in strict first order. | ComputerInput.kif 2268-2277 |
|
No TPTP formula. May not be expressible in strict first order. | ComputerInput.kif 2332-2343 |
|
No TPTP formula. May not be expressible in strict first order. | ComputerInput.kif 2347-2354 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 12678-12691 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 12638-12651 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 1326-1342 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 12382-12389 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16342-16352 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 17385-17396 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 17426-17438 | |
No TPTP formula. May not be expressible in strict first order. | Food.kif 468-478 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16362-16372 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 21394-21402 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 13955-13963 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 23767-23778 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 23788-23799 | |
No TPTP formula. May not be expressible in strict first order. | Food.kif 3076-3094 | |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 754-765 | |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |