No TPTP formula. May not be expressible in strict first order. |
People.kif 289-310 |
A real number is an average of a list if and only if there exists another list such that length of the other list is equal to length of the list and 1th element of the other list is equal to 1th element of the list and for all a positive integer and a fourth positive integer is equal to length of the other list and the real number is equal to the fourth positive integerth element of the other list and the fourth positive integer |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 5897-5910 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 5883-5895 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 5014-5025 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3193-3203 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3017-3036 |
|
No TPTP formula. May not be expressible in strict first order. |
Media.kif 3056-3077 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3124-3136 |
|
No TPTP formula. May not be expressible in strict first order. |
Weather.kif 1452-1464 |
|
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 562-567 |
|
No TPTP formula. May not be expressible in strict first order. |
Transportation.kif 510-517 |
|
No TPTP formula. May not be expressible in strict first order. |
Transportation.kif 503-508 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 6174-6182 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16947-16959 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16965-16977 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16929-16941 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16911-16923 |
|