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 206-223 |
地缘政治区域 的 male 对母性比率 equal 实数 若且唯若 整数 equal 符号串 所描述的类别 instance 的数量 和 另一个 整数 equal 另一个 符号串 所描述的类别 instance 的数量 和 那个 整数 和 那个 另外 整数 equal 那个 实数 |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 20200-20204 |
客体 是 公牛 的 instance 若且唯若 那个 客体 是 牛 的 instance 和 女 是 那个 客体 的 attribute |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 20232-20236 |
客体 是 母鸡 的 instance 若且唯若 那个 客体 是 鸡 的 instance 和 女 是 那个 客体 的 attribute |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 12859-12863 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 18117-18122 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 24131-24137 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 23880-23887 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 23934-23936 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 19844-19846 |
|
No TPTP formula. May not be expressible in strict first order. |
Hotel.kif 1243-1254 |
|
No TPTP formula. May not be expressible in strict first order. |
Hotel.kif 1042-1050 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16444-16446 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 24010-24017 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 12647-12651 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 10870-10877 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 14659-14661 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16414-16416 |
|