No TPTP formula. May not be expressible in strict first order. |
People.kif 383-416 |
A year is an instance of the year the yearEAR and the male life expectancy at birth of a geopolitical area and the year is equal to a real number if and only if there exist a list, another integer,, , a symbolic string,, , an entity,, , another entity and a third entity such that the list is an instance of list and length of the list is an instance of the other integer and for all the listITEM and the real number is an average of the list |
No TPTP formula. May not be expressible in strict first order. |
People.kif 429-462 |
A year is an instance of the year an integer and the female life expectancy at birth of a geopolitical area and the year is equal to a real number if and only if there exist a list, another integer,, , a symbolic string,, , an entity,, , another entity and a third entity such that the list is an instance of list and length of the list is an instance of the other integer and for all the listITEM and the real number is an average of the list |
No TPTP formula. May not be expressible in strict first order. |
People.kif 336-368 |
A year is an instance of the year an integer and the life expectancy at birth of a geopolitical area and the year is equal to a real number if and only if there exist a list, another integer,, , a symbolic string,, , an entity,, , another entity and a third entity such that the list is an instance of list and length of the list is an instance of the other integer and for all the listITEM and the real number is an average of the list |
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. |
Music.kif 280-287 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 7563-7578 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4832-4843 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4845-4859 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4917-4927 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4929-4943 |
|
No TPTP formula. May not be expressible in strict first order. |
Music.kif 935-945 |
|
No TPTP formula. May not be expressible in strict first order. |
Weather.kif 2005-2017 |
|
No TPTP formula. May not be expressible in strict first order. |
Media.kif 801-812 |
|
No TPTP formula. May not be expressible in strict first order. |
Weather.kif 1532-1547 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 5336-5341 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 464-468 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 2927-2932 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 2934-2943 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 574-578 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4825-4830 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4910-4915 |
|
No TPTP formula. May not be expressible in strict first order. |
Weather.kif 1685-1692 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 509-517 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 2917-2925 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 558-562 |
|
|
Display limited to 25 items. Show next 25 |
|
Display limited to 25 items. Show next 25 |