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 14372-14374 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14370-14370 | 居住 的 1 数量 是 生物 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14371-14371 | 居住 的 2 数量 是 客体 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14369-14369 | 居住 是 非对称关系 的 instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14368-14368 | 居住 是 二元谓语 的 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 14384-14384 | 家 是 居住 的 subrelation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14391-14391 | 停留 是 居住 的 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 14472-14476 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14431-14435 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14484-14488 | |
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 14376-14382 |
|
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 30120-30127 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30104-30112 | |
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 25035-25044 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 17352-17368 |
|
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 30388-30395 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14418-14423 | |
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 15743-15753 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14573-14578 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30636-30643 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 6997-7004 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 6280-6282 |
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 31712-31717 | 地缘政治区域 的 population equal 符号串 所描述的类别 instance 的数量 |
No TPTP formula. May not be expressible in strict first order. | Military.kif 933-946 | 地缘政治区域 和 年 每年的 reaching 军事男性年龄 equal 符号串 所描述的类别 instance 的数量 |