YearFn |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2749-2753 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8558-8566 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1475-1480 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8555-8555 | 年函数 的 1 数量 是 整数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8552-8552 | 年函数 是 时间关系 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8554-8554 | 年函数 是 总值关系 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8553-8553 | 年函数 是 一元函数 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8556-8556 | 年函数 的所得值 是 年 的 subclass |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 465-465 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 471-471 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 269-269 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 317-317 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2059-2059 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 221-221 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 275-275 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 608-608 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 351-351 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 290-290 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 296-296 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 509-509 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8739-8739 | 年 和 年函数 是 内部相关 |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 63757-63757 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 466-466 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 63756-63756 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 63755-63755 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | People.kif 357-390 | 年 是 那个 年EAR year 的 instance 和 地缘政治区域 和 那个 年 的 male 出生估计寿命 equal 实数 若且唯若 有存在 串列, 另一个 整数,, , 符号串,, , 实体,, , 另一个 实体, and 和 第三 实体 这样 那个 串列 是 串列 的 instance 和 那个 串列 的长度 是 那个 另外 整数 的 instance 和 对所有 那个 串列ITEM
|
No TPTP formula. May not be expressible in strict first order. | People.kif 82-97 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 每一千的 births equal 实数 若且唯若 那个 地缘政治区域 的 population 和 1000 equal 另一个 实数 和 另一个 整数 equal 符号串 所描述的类别 instance 的数量 和 那个 另外 整数 和 那个 另外 实数 equal 那个 实数 |
No TPTP formula. May not be expressible in strict first order. | People.kif 118-133 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 每一千里的 deaths equal 实数 若且唯若 那个 地缘政治区域 的 population 和 1000 equal 另一个 实数 和 另一个 整数 equal 符号串 所描述的类别 instance 的数量 和 那个 另外 整数 和 那个 另外 实数 equal 那个 实数 |
No TPTP formula. May not be expressible in strict first order. | People.kif 238-264 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 每一千个生存出生里的 deaths equal 实数 若且唯若 另一个 整数 equal 符号串 所描述的类别 instance 的数量 和 那个 另外 整数 和 1000 equal 另一个 实数 和 第三 整数 equal 另一个 符号串 所描述的类别 instance 的数量 和 那个 第三 整数 和 那个 另外 实数 equal 那个 实数 |
No TPTP formula. May not be expressible in strict first order. | People.kif 403-436 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 的 female 出生预期寿命 equal 实数 若且唯若 有存在 串列, 另一个 整数,, , 符号串,, , 实体,, , 另一个 实体, and 和 第三 实体 这样 那个 串列 是 串列 的 instance 和 那个 串列 的长度 是 那个 另外 整数 的 instance 和 对所有 那个 串列ITEM
|
No TPTP formula. May not be expressible in strict first order. | People.kif 310-342 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 的出生预期 life equal 实数 若且唯若 有存在 串列, 另一个 整数,, , 符号串,, , 实体,, , 另一个 实体, and 和 第三 实体 这样 那个 串列 是 串列 的 instance 和 那个 串列 的长度 是 那个 另外 整数 的 instance 和 对所有 那个 串列ITEM
|
No TPTP formula. May not be expressible in strict first order. | People.kif 156-187 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 每一千的 migrants equal 实数 若且唯若 (那个 整数 和 另一个 整数) equal 1 和 实体 是 那个 另外 整数 year 的 instance 和 那个 地缘政治区域 的 population equal 另一个 实数 在 那个 年 holdsDuring 和 那个 另外 实数 和 1000 equal 第三 实数 和 第三 整数 equal 符号串 所描述的类别 instance 的数量 和 第四 整数 equal 那个 符号串 所描述的类别 instance 的数量 和 (那个 第三 整数 和 那个 第四 整数) equal 第四 实数 和 那个 第四 实数 和 那个 第三 实数 equal 那个 实数 |
No TPTP formula. May not be expressible in strict first order. | People.kif 52-64 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 的 population 成长 equal 实数 若且唯若 (那个 整数 和 那个 整数P) equal 1 和 时间位置 是 那个 整数P year 的 instance 和 那个 地缘政治区域 的 population equal 另一个 实数 在 那个 年 holdsDuring 和 那个 地缘政治区域 的 population equal 第三 实数 在 那个 时间位置 holdsDuring 和 那个 另外 实数 和 那个 第三 实数 equal 第四 实数 和 (那个 第四 实数 和 1) equal 那个 实数 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24236-24246 | |
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. | Government.kif 612-617 | |
No TPTP formula. May not be expressible in strict first order. | Government.kif 619-625 | |
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. | Mid-level-ontology.kif 23916-23932 | |
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. | Merge.kif 8731-8736 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14837-14846 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 9001-9009 | |
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. | Merge.kif 8715-8720 | |
No TPTP formula. May not be expressible in strict first order. | Biography.kif 69-85 |
|
No TPTP formula. May not be expressible in strict first order. | Biography.kif 99-115 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8980-8985 | |
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 17206-17212 | |
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. | People.kif 156-187 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 每一千的 migrants equal 实数 若且唯若 (那个 整数 和 另一个 整数) equal 1 和 实体 是 那个 另外 整数 year 的 instance 和 那个 地缘政治区域 的 population equal 另一个 实数 在 那个 年 holdsDuring 和 那个 另外 实数 和 1000 equal 第三 实数 和 第三 整数 equal 符号串 所描述的类别 instance 的数量 和 第四 整数 equal 那个 符号串 所描述的类别 instance 的数量 和 (那个 第三 整数 和 那个 第四 整数) equal 第四 实数 和 那个 第四 实数 和 那个 第三 实数 equal 那个 实数 |
No TPTP formula. May not be expressible in strict first order. | People.kif 52-64 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 的 population 成长 equal 实数 若且唯若 (那个 整数 和 那个 整数P) equal 1 和 时间位置 是 那个 整数P year 的 instance 和 那个 地缘政治区域 的 population equal 另一个 实数 在 那个 年 holdsDuring 和 那个 地缘政治区域 的 population equal 第三 实数 在 那个 时间位置 holdsDuring 和 那个 另外 实数 和 那个 第三 实数 equal 第四 实数 和 (那个 第四 实数 和 1) equal 那个 实数 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 968-975 | 整数 是 机构 的 year 资金 若且唯若 有存在 过程 和 那个 整数EAR 这样 那个 整数EAR 时段 和 那个 过程 出现 的 time 重叠 和 那个 整数EAR 是 那个 整数 year 的 instance 和 那个 过程 是 创建 的 instance 和 那个 机构 是 那个 过程 的 result |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24236-24246 | |
No TPTP formula. May not be expressible in strict first order. | Government.kif 619-625 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14837-14846 |
|
No TPTP formula. May not be expressible in strict first order. | Biography.kif 69-85 |
|
No TPTP formula. May not be expressible in strict first order. | Biography.kif 99-115 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24195-24206 | |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 3003-3011 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 960-963 |
statement |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3192-3192 | 1 Day 是 南极条约 的 agreement 采用日期 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3193-3193 | ?D 是 23 Day 的 instance 是 南极条约 的 agreement 生效日期 |
No TPTP formula. May not be expressible in strict first order. | People.kif 456-469 | 年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 每个女人生的 children equal 符号串 所描述的类别 instance 的数量 |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2994-2994 | 31 Day 是 出口管制协调委员会 的闭幕 date |
No TPTP formula. May not be expressible in strict first order. | Government.kif 3009-3009 | 1 Day 是 共同经济援助理事会 的闭幕 date |
No TPTP formula. May not be expressible in strict first order. | Government.kif 4145-4145 | 25 Day 是 联合国预防性部署部队 的闭幕 date |
No TPTP formula. May not be expressible in strict first order. | Government.kif 4285-4285 | 1 Day 是 华沙协议 的闭幕 date |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2877-2877 | 1994 Year 是 东盟区域论坛 的成立 date |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2750-2750 | 6 Day 是 非洲加勒比和太平洋国家集团 的成立 date |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2757-2757 | 4 Day 是 非洲开发银行 的成立 date |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2771-2771 | 20 Day 是 法语社区的代理机构 的成立 date |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2778-2778 | 14 Day 是 在拉丁美洲和加勒比地区禁止核武器的机构 的成立 date |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2796-2796 | 26 Day 是 安第斯国际社会 的成立 date |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2801-2801 | 23 Day 是 南极条约理事会 的成立 date |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2812-2812 | 18 Day 是 阿拉伯非洲经济发展银行 的成立 date |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2818-2818 | 16 Day 是 阿拉伯合作理事会 的成立 date |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2824-2824 | 16 Day 是 阿拉伯经济和社会发展基金 的成立 date |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2833-2833 | 22 Day 是 阿拉伯联盟 的成立 date |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2842-2842 | 17 Day 是 阿拉伯马格里布联盟 的成立 date |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2851-2851 | 27 Day 是 阿拉伯货币基金 的成立 date |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2857-2857 | 7 Day 是 亚太经济合作 的成立 date |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2863-2863 | 19 Day 是 亚洲开发银行 的成立 date |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2869-2869 | 8 Day 是 东南亚国家联盟 的成立 date |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2883-2883 | 1984 Year 是 澳大利亚集团 的成立 date |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2889-2889 | 1 Day 是 澳大利亚新西兰美国安全条约 的成立 date |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |