inhabits |
appearance as argument number 1 |
![]() |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 3373-3374 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14394-14396 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14392-14392 | 居住 的 1 数量 是 生物 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14393-14393 | 居住 的 2 数量 是 客体 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14391-14391 | 居住 是 非对称关系 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14390-14390 | 居住 是 二元谓语 的 instance |
appearance as argument number 2 |
![]() |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 521-521 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 526-526 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 308-308 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 143-143 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2076-2076 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 260-260 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 314-314 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 677-677 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 182-182 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 329-329 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 336-336 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 290-290 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14406-14406 | 家 是 居住 的 subrelation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14413-14413 | 停留 是 居住 的 subrelation |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 522-522 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 30073-30073 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 30072-30072 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 30071-30071 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 291-291 |
antecedent |
![]() |
No TPTP formula. May not be expressible in strict first order. | MilitaryPersons.kif 26-47 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14494-14498 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14453-14457 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14506-14510 | |
No TPTP formula. May not be expressible in strict first order. | MilitaryPersons.kif 70-78 | |
No TPTP formula. May not be expressible in strict first order. | MilitaryPersons.kif 92-99 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14398-14404 |
|
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 206-223 | 地缘政治区域 的 male 对母性比率 equal 实数 若且唯若 整数 equal 符号串 所描述的类别 instance 的数量 和 另一个 整数 equal 另一个 符号串 所描述的类别 instance 的数量 和 那个 整数 和 那个 另外 整数 equal 那个 实数 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30108-30115 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30092-30100 | |
No TPTP formula. May not be expressible in strict first order. | MilitaryPersons.kif 26-47 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25034-25043 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 17351-17367 |
|
No TPTP formula. May not be expressible in strict first order. | Food.kif 1928-1937 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30376-30383 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14440-14445 | |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 6042-6046 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 15765-15775 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14595-14600 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30624-30631 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 6996-7003 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 6279-6281 |
statement |
![]() |
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. | Military.kif 872-881 | 地缘政治区域 的 available 军事服务男性 equal 符号串 所描述的类别 instance 的数量 |
No TPTP formula. May not be expressible in strict first order. | Military.kif 895-906 | 地缘政治区域 的 fit 对于军服务男性 equal 符号串 所描述的类别 instance 的数量 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31708-31713 | 地缘政治区域 的 population equal 符号串 所描述的类别 instance 的数量 |
No TPTP formula. May not be expressible in strict first order. | Military.kif 933-946 | 地缘政治区域 和 年 每年的 reaching 军事男性年龄 equal 符号串 所描述的类别 instance 的数量 |
![]() |
![]() |