BeginFn |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2697-2698 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7985-7986 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1420-1421 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7982-7982 | 开始函数 的 1 数量 是 时距 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7979-7979 | 开始函数 是 时间关系 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7981-7981 | 开始函数 是 总值关系 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7980-7980 | 开始函数 是 一元函数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7983-7983 | 开始函数 的 range 是 时点 的实例 |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 449-449 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 455-455 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 261-261 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 34-34 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2051-2051 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 213-213 | |
No TPTP formula. May not be expressible in strict first order. | relations-cb.txt 68-68 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 267-267 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 586-586 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 78-78 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 282-282 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 287-287 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 84-84 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 10559-10559 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 450-450 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 10558-10558 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 10557-10557 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 85-85 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8086-8094 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8054-8062 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 22920-22925 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29595-29604 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 23916-23932 | |
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. | Mid-level-ontology.kif 501-514 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 12383-12397 | |
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. | ComputerInput.kif 2332-2343 |
|
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 11647-11654 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 12431-12440 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8722-8729 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2421-2430 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2432-2445 |
|
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. | Media.kif 587-597 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8354-8364 | |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 1399-1404 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8706-8713 | |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 1753-1773 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 19583-19595 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 17638-17656 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 17616-17634 |
|
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 12466-12473 | 过程 是 结合 的 instance 和 客体 是 那个 过程 的 resource 和 实体 是 那个 过程 的 result 若且唯若 那个 客体 不 是 那个 实体 的 part 在 那个 过程 出现 的 time 的开始 holdsDuring 和 那个 客体 是 那个 实体 的 part 在 那个 过程 出现 的 time 的结束 holdsDuring |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 6231-6244 | |
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. | Hotel.kif 684-695 | |
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. | Communications.kif 202-214 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30692-30698 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3836-3843 | |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1966-1973 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 23710-23719 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 23737-23745 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 21495-21506 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 1042-1055 | |
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. | ComputerInput.kif 2268-2277 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 12656-12669 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 12616-12629 |
|
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 12360-12367 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16343-16353 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 17386-17397 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 17427-17439 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16363-16373 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 21395-21403 | |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |