ImmediateFutureFn |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2745-2746 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8531-8533 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1471-1472 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8528-8528 | 紧接未来函数 的 1 数量 是 时间位置 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8525-8525 | 紧接未来函数 是 时间关系 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8527-8527 | 紧接未来函数 是 总值关系 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8526-8526 | 紧接未来函数 是 一元函数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8529-8529 | 紧接未来函数 的 range 是 时距 的实例 |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 463-463 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 469-469 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 268-268 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 137-137 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2058-2058 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 220-220 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 274-274 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 605-605 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 176-176 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 289-289 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 295-295 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 278-278 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 29349-29349 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 464-464 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 29348-29348 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 29347-29347 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 279-279 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 3231-3245 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 9839-9861 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 9900-9922 |
|
No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 1926-1940 | |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 7016-7030 | |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 777-792 |
|
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 1328-1340 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 1332-1355 |
|
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 3972-3986 | |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 3988-4002 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 10555-10570 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 10533-10548 | |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 1987-1999 | |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 7068-7082 |
consequent |
No TPTP formula. May not be expressible in strict first order. | Government.kif 738-753 |
|
No TPTP formula. May not be expressible in strict first order. | Government.kif 714-719 | |
No TPTP formula. May not be expressible in strict first order. | Government.kif 721-726 | |
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. | ComputingBrands.kif 4482-4491 |
|
No TPTP formula. May not be expressible in strict first order. | Cars.kif 1252-1267 | |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 2397-2406 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29758-29765 | |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 767-785 |
|
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 2784-2796 | |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4123-4135 | |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4079-4092 | |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4101-4114 | |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4143-4153 | |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 391-401 | |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4566-4576 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30079-30087 | |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4498-4507 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 10222-10237 | |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 436-453 | |
No TPTP formula. May not be expressible in strict first order. | MilitaryPersons.kif 133-140 | |
No TPTP formula. May not be expressible in strict first order. | engineering.kif 939-952 | |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4451-4461 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25093-25114 |
|
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 1328-1340 |
|
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
statement |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2791-2794 | 时间位置 是 1 day 的 instance 和 安第斯国际社会 是 "Andean Community of Nations" 的 conventional 全名 在 紧接 那个 时间位置 after holdsDuring |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2765-2769 | 时间位置 是 1996 year 的 instance 和 法语社区的代理机构 是 "Agency for the French-Speaking Community" 的 conventional 全名 在 紧接 那个 时间位置 after holdsDuring |