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 8334-8335 | |
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 8331-8331 | 在这时间内 的 1 数量 是 时距 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8332-8332 | 在这时间内 的 2 数量 是 时距 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8328-8328 | 在这时间内 是 二元谓语 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8329-8329 | 在这时间内 是 非自反关系 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8327-8327 | 在这时间内 是 传递关系 的 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 30650-30671 |
|
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 8944-8951 | |
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 2724-2744 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 2746-2767 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8337-8341 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8280-8282 | |
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 30211-30224 | 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 30259-30267 | 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 2573-2589 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30230-30241 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 10576-10592 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 8386-8399 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8862-8867 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8962-8967 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8846-8851 | |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 1904-1923 |
|
No TPTP formula. May not be expressible in strict first order. | Cars.kif 1874-1893 |
|
No TPTP formula. May not be expressible in strict first order. | Cars.kif 1949-1971 |
|
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 |
![]() |
![]() |