No TPTP formula. May not be expressible in strict first order. |
Geography.kif 4711-4720 |
公海 是 客体 的 attribute 若且唯若 有存在 物理 和 实数 这样 那个 客体 是 盐水区 的 instance 和 那个 客体 不 是 内陆水域 的 instance 和 那个 物理 和 那个 客体 的 distance 是 那个 实数 海里 和 那个 实数 是 greaterThan 5.0 |
No TPTP formula. May not be expressible in strict first order. |
People.kif 272-293 |
实数 是 串列 的 average 若且唯若 有存在 另一个 串列 和 正整数 这样 那个 另外 串列 的长度 equal 那个 串列 的长度 和 那个 另外 串列 的第 1 几个元素 equal 那个 串列 的第 1 几个元素 和 对所有 另一个 正整数 和 那个 正整数 equal 那个 另外 串列 的长度 和 那个 实数 equal 那个 另外 串列 的第 那个 正整数 几个元素 和 那个 正整数 |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 1885-1889 |
实数 是 greaterThanOrEqualTo 另一个 实数 若且唯若 那个 实数 equal 那个 另外 实数 或 那个 实数 是 greaterThan 那个 另外 实数 |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 1937-1941 |
实数 是 正实数 的 instance 若且唯若 那个 实数 是 greaterThan 0 和 那个 实数 是 实数 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 7758-7766 |
客体 larger 另一个 客体 若且唯若 对所有 实数, 另一个 实数, and 和 测量单位 |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 1754-1759 |
|
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 1766-1771 |
|
No TPTP formula. May not be expressible in strict first order. |
Dining.kif 1165-1176 |
|
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. |
Medicine.kif 3984-4004 |
|
No TPTP formula. May not be expressible in strict first order. |
Hotel.kif 1186-1201 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 24236-24246 |
|
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 1538-1544 |
|
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 1522-1530 |
|
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 1597-1603 |
|
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. |
Merge.kif 18446-18451 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 13536-13545 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 13547-13558 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 13486-13497 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 13566-13575 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 18429-18434 |
|
No TPTP formula. May not be expressible in strict first order. |
Cars.kif 2585-2603 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4874-4888 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 18343-18358 |
|
|
Display limited to 25 items. Show next 25 |
|
Display limited to 25 items. Show next 25 |