No TPTP formula. May not be expressible in strict first order. |
People.kif 272-293 |
A real number is an average of a list if and only if there exist another list and a positive integer 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 another positive integer and the positive integer is equal to length of the other list and the real number is equal to the positive integerth element of the other list and the positive integer |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 5993-6006 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 5979-5991 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 5104-5115 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3258-3268 |
|
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. |
Media.kif 3068-3089 |
|
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 1453-1465 |
|
No TPTP formula. May not be expressible in strict first order. |
Food.kif 1248-1262 |
|
No TPTP formula. May not be expressible in strict first order. |
Biography.kif 69-85 |
|
No TPTP formula. May not be expressible in strict first order. |
Biography.kif 99-115 |
|
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 555-560 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 17206-17212 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 17218-17224 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 17194-17200 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 17182-17188 |
|
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 6501-6509 |
|