during |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 2720-2721 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8312-8313 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1444-1445 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8309-8309 | 在这时间内 的 1 数量 是 时距 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8310-8310 | 在这时间内 的 2 数量 是 时距 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8306-8306 | 在这时间内 是 二元谓语 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8307-8307 | 在这时间内 是 非自反关系 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8305-8305 | 在这时间内 是 传递关系 的 instance |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 433-433 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 439-439 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 251-251 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 86-86 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2045-2045 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 203-203 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 257-257 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 565-565 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 126-126 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 272-272 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 275-275 | |
No TPTP formula. May not be expressible in strict first order. | relations-cb.txt 120-120 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 434-434 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 20694-20694 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 20693-20693 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 20692-20692 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 188-188 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 367-385 |
|
No TPTP formula. May not be expressible in strict first order. | Cars.kif 809-825 |
|
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 6470-6482 | |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 6447-6459 | |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 1500-1512 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30662-30683 |
|
No TPTP formula. May not be expressible in strict first order. | Media.kif 437-444 | |
No TPTP formula. May not be expressible in strict first order. | Media.kif 446-453 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8922-8929 | |
No TPTP formula. May not be expressible in strict first order. | ArabicCulture.kif 65-84 |
|
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 466-482 |
|
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. | Medicine.kif 5997-6017 |
|
No TPTP formula. May not be expressible in strict first order. | Media.kif 387-394 | |
No TPTP formula. May not be expressible in strict first order. | Media.kif 396-403 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3668-3704 |
|
No TPTP formula. May not be expressible in strict first order. | Media.kif 538-547 | |
No TPTP formula. May not be expressible in strict first order. | Media.kif 473-482 | |
No TPTP formula. May not be expressible in strict first order. | Media.kif 559-568 | |
No TPTP formula. May not be expressible in strict first order. | Anatomy.kif 1758-1780 |
|
No TPTP formula. May not be expressible in strict first order. | Anatomy.kif 1708-1729 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 2728-2748 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 2750-2771 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8315-8319 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8258-8260 | |
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 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. | Mid-level-ontology.kif 30223-30236 | Alone 是 实体 的 attribute 在 时距 holdsDuring 若且唯若 不存在 那个 实体2 和 过程 这样 那个 实体 不 equal 那个 实体2 和 那个 实体2 是 施事体 的 instance 和 那个 过程 是 社交 的 instance 和 那个 过程 出现 的 time 在 那个 时距 时段内发生 和 那个 实体 是事件 那个 过程 的 involved 和 那个 实体2 是事件 那个 过程 的 involved |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30271-30279 | Mute 是 施事体 的 attribute 在 时距 holdsDuring 若且唯若 不存在 过程 这样 那个 过程 是 说话 的 instance 和 那个 过程 出现 的 time 在 那个 时距 时段内发生 和 那个 施事体 是 那个 过程 的 agent |
No TPTP formula. May not be expressible in strict first order. | ArabicCulture.kif 204-223 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3534-3543 | |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3582-3591 | |
No TPTP formula. May not be expressible in strict first order. | emotion.kif 161-172 |
|
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 6470-6482 | |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 6447-6459 | |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 2567-2583 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30242-30253 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 10577-10593 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 8387-8400 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8840-8845 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8940-8945 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8824-8829 | |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 1898-1917 |
|
No TPTP formula. May not be expressible in strict first order. | Cars.kif 1868-1887 |
|
No TPTP formula. May not be expressible in strict first order. | Cars.kif 1943-1965 |
|
No TPTP formula. May not be expressible in strict first order. | emotion.kif 1583-1597 |
|
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |