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 2998-3003 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3005-3010 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3252-3256 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 295-302 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3083-3102 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3179-3188 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3190-3202 |
|
No TPTP formula. May not be expressible in strict first order. |
Weather.kif 1486-1497 |
|
No TPTP formula. May not be expressible in strict first order. |
Weather.kif 1453-1465 |
|
No TPTP formula. May not be expressible in strict first order. |
Media.kif 2093-2103 |
|
No TPTP formula. May not be expressible in strict first order. |
Media.kif 2075-2090 |
|
No TPTP formula. May not be expressible in strict first order. |
Media.kif 2137-2150 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3232-3237 |
|
No TPTP formula. May not be expressible in strict first order. |
UXExperimentalTerms.kif 2388-2404 |
|
No TPTP formula. May not be expressible in strict first order. |
Media.kif 2210-2223 |
|
No TPTP formula. May not be expressible in strict first order. |
Media.kif 2174-2187 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3212-3217 |
|
No TPTP formula. May not be expressible in strict first order. |
Media.kif 2125-2134 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 519-531 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3113-3116 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 2910-2915 |
|
No TPTP formula. May not be expressible in strict first order. |
Media.kif 2198-2207 |
|
No TPTP formula. May not be expressible in strict first order. |
Media.kif 2161-2170 |
|