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 equal length of the other list and length of the list and equal 1th element of the other list and 1th element of the list and for all another positive integer and equal the positive integer and length of the other list and equal the real number and 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 3011-3016 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3018-3023 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3265-3269 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 289-296 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3096-3115 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3192-3201 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3203-3215 |
|
No TPTP formula. May not be expressible in strict first order. |
Weather.kif 2211-2222 |
|
No TPTP formula. May not be expressible in strict first order. |
Weather.kif 2178-2190 |
|
No TPTP formula. May not be expressible in strict first order. |
Media.kif 2095-2105 |
|
No TPTP formula. May not be expressible in strict first order. |
Media.kif 2077-2092 |
|
No TPTP formula. May not be expressible in strict first order. |
Media.kif 2139-2152 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3245-3250 |
|
No TPTP formula. May not be expressible in strict first order. |
UXExperimentalTerms.kif 2388-2404 |
- If a process is an instance of search engine optimization and an entity is a patient of the process,
- then the process has the purpose there exist another entity_BEFORE, the other entity_AFTER,, , a third entity,, , a fourth entity,, , a fifth entity and a sixth entity such that the other entity_BEFORE is an instance of search results and the other entity_AFTER is an instance of search results and equal the entity and the third entityth element of the other entity_BEFORE and equal the entity and the fourth entityth element of the other entity_AFTER and the fifth entity is an instance of best match sort and the sixth entity is an instance of best match sort and the time of existence of the fifth entity happens earlier than the time of existence of the sixth entity and the time of existence of the process happens earlier than the time of existence of the sixth entity and the time of existence of the fifth entity happens earlier than the time of existence of the process and the third entity is greater than the fourth entity
|
No TPTP formula. May not be expressible in strict first order. |
Media.kif 2212-2225 |
|
No TPTP formula. May not be expressible in strict first order. |
Media.kif 2176-2189 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3225-3230 |
|
No TPTP formula. May not be expressible in strict first order. |
Media.kif 2127-2136 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 512-524 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3126-3129 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 2923-2928 |
|
No TPTP formula. May not be expressible in strict first order. |
Media.kif 2200-2209 |
|
No TPTP formula. May not be expressible in strict first order. |
Media.kif 2163-2172 |
|