No TPTP formula. May not be expressible in strict first order. |
People.kif 357-390 |
年 是 那个 年EAR year 的 instance 和 地缘政治区域 和 那个 年 的 male 出生估计寿命 equal 实数 若且唯若 有存在 串列, 另一个 整数,, , 符号串,, , 实体,, , 另一个 实体, and 和 第三 实体 这样 那个 串列 是 串列 的 instance 和 那个 串列 的长度 是 那个 另外 整数 的 instance 和 对所有 那个 串列ITEM 和 那个 实数 是 那个 串列 的 average |
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 和 那个 实数 是 那个 串列 的 average |
No TPTP formula. May not be expressible in strict first order. |
People.kif 310-342 |
年 是 整数 year 的 instance 和 地缘政治区域 和 那个 年 的出生预期 life equal 实数 若且唯若 有存在 串列, 另一个 整数,, , 符号串,, , 实体,, , 另一个 实体, and 和 第三 实体 这样 那个 串列 是 串列 的 instance 和 那个 串列 的长度 是 那个 另外 整数 的 instance 和 对所有 那个 串列ITEM 和 那个 实数 是 那个 串列 的 average |
No TPTP formula. May not be expressible in strict first order. |
Government.kif 1132-1152 |
|
No TPTP formula. May not be expressible in strict first order. |
Government.kif 1062-1073 |
|
No TPTP formula. May not be expressible in strict first order. |
Government.kif 990-1001 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 21147-21177 |
|
No TPTP formula. May not be expressible in strict first order. |
Military.kif 840-850 |
|
No TPTP formula. May not be expressible in strict first order. |
Hotel.kif 2925-2940 |
|
No TPTP formula. May not be expressible in strict first order. |
Law.kif 573-588 |
|
No TPTP formula. May not be expressible in strict first order. |
Government.kif 1211-1231 |
|
No TPTP formula. May not be expressible in strict first order. |
Government.kif 1040-1050 |
|
No TPTP formula. May not be expressible in strict first order. |
Government.kif 968-978 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 382-390 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 201-209 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 301-309 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 259-267 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 332-340 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16248-16257 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 405-411 |
|
No TPTP formula. May not be expressible in strict first order. |
Government.kif 1191-1209 |
|
No TPTP formula. May not be expressible in strict first order. |
Government.kif 1106-1118 |
|