No TPTP formula. May not be expressible in strict first order. |
People.kif 298-319 |
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 2985-2990 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 2992-2997 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3239-3243 |
|
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 3070-3089 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3166-3175 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3177-3189 |
|
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 3219-3224 |
|
No TPTP formula. May not be expressible in strict first order. |
UXExperimentalTerms.kif 2594-2610 |
- 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 the entity is equal to the third entityth element of the other entity_BEFORE and the entity is equal to 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 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 3199-3204 |
|
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 3100-3103 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 2897-2902 |
|
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 |
|