No TPTP formula. May not be expressible in strict first order. |
People.kif 357-390 |
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 403-436 |
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 310-342 |
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 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 7794-7802 |
An object is larger than another object if and only if for all a real number, another real number and an unit of measure |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 1297-1302 |
A collection is a proper sub-collection of another collection if and only if for all a physical |
No TPTP formula. May not be expressible in strict first order. |
Hotel.kif 171-176 |
|
No TPTP formula. May not be expressible in strict first order. |
Hotel.kif 233-238 |
|
No TPTP formula. May not be expressible in strict first order. |
Hotel.kif 218-223 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 4984-4992 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 17767-17776 |
|
No TPTP formula. May not be expressible in strict first order. |
Government.kif 1096-1116 |
|
No TPTP formula. May not be expressible in strict first order. |
Hotel.kif 147-154 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4862-4873 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4875-4889 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4947-4957 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4959-4973 |
|
No TPTP formula. May not be expressible in strict first order. |
Music.kif 936-946 |
|
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 9930-9937 |
|
No TPTP formula. May not be expressible in strict first order. |
UXExperimentalTerms.kif 992-1008 |
|
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 7142-7162 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 12957-12968 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 10258-10273 |
|
No TPTP formula. May not be expressible in strict first order. |
Food.kif 1012-1026 |
|
|
Display limited to 25 items. Show next 25 |
|
Display limited to 25 items. Show next 25 |