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 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 |
- 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 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 |
|