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 6044-6050 |
|
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 427-431 |
|
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 467-474 |
|
No TPTP formula. May not be expressible in strict first order. |
Transportation.kif 1445-1457 |
|
No TPTP formula. May not be expressible in strict first order. |
Transportation.kif 1426-1438 |
|
No TPTP formula. May not be expressible in strict first order. |
Transportation.kif 1407-1419 |
|
No TPTP formula. May not be expressible in strict first order. |
Weather.kif 917-925 |
|
No TPTP formula. May not be expressible in strict first order. |
Weather.kif 906-915 |
|
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 2873-2884 |
|
No TPTP formula. May not be expressible in strict first order. |
Food.kif 571-578 |
|
No TPTP formula. May not be expressible in strict first order. |
Food.kif 495-502 |
|
No TPTP formula. May not be expressible in strict first order. |
Food.kif 533-540 |
|
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 4645-4658 |
|
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 4669-4682 |
|
No TPTP formula. May not be expressible in strict first order. |
Food.kif 1367-1385 |
|
No TPTP formula. May not be expressible in strict first order. |
CountriesAndRegions.kif 59-65 |
|
No TPTP formula. May not be expressible in strict first order. |
Government.kif 1075-1084 |
|
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. |
Weather.kif 2365-2384 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 8985-8989 |
|
No TPTP formula. May not be expressible in strict first order. |
Food.kif 2993-3011 |
|
No TPTP formula. May not be expressible in strict first order. |
Food.kif 3018-3036 |
|
No TPTP formula. May not be expressible in strict first order. |
Food.kif 2851-2869 |
|
No TPTP formula. May not be expressible in strict first order. |
Transportation.kif 453-458 |
|
|
Display limited to 25 items. Show next 25 |
|
Display limited to 25 items. Show next 25 |