Human
|
|
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 3438-3438 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14692-14693 | |
No TPTP formula. May not be expressible in strict first order. | pictureList-ImageNet.kif 259-259 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 3117-3117 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 3116-3116 | |
No TPTP formula. May not be expressible in strict first order. | pictureList-ImageNet.kif 257-257 | |
No TPTP formula. May not be expressible in strict first order. | pictureList-ImageNet.kif 258-258 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14691-14691 | Human is exhaustively partitioned into man and woman |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14690-14690 | Human is a subclass of cognitive agent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14689-14689 | Human is a subclass of hominid |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | WMD.kif 1586-1586 | Human is a biological agent carrier of bordetella pertussis |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 20045-20045 | Domestic animal is disjoint from human |
No TPTP formula. May not be expressible in strict first order. | Media.kif 35-35 | Organization is disjoint from human |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 786-786 | Every vocal cords is initially part of a human |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 23749-23749 | Instance of brain are always initially part of instances of human |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 23750-23750 | Instance of heart are always initially part of instances of human |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2447-2447 | Steve Jobs is an instance of human |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2459-2459 | Steve Wozniak is an instance of human |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2435-2435 | Tim Cook is an instance of human |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 178-178 | Human adult is a subclass of human |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 241-241 | Human youth is a subclass of human |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14695-14695 | Man is a subclass of human |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 313-313 | Teenager is a subclass of human |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14702-14702 | Woman is a subclass of human |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1002-1002 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 1216-1216 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 679-679 | |
No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 210-210 | |
No TPTP formula. May not be expressible in strict first order. | terms-it.txt 213-213 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2363-2363 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 631-631 | |
No TPTP formula. May not be expressible in strict first order. | terms-cb.txt 215-215 | |
No TPTP formula. May not be expressible in strict first order. | terms-cz.txt 247-247 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 700-700 | |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
appearance as argument number 3 |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 1280-1280 | connectedBodyPartTypes abdominal aorta, thoracic aorta and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 1658-1658 | connectedBodyPartTypes accompanying artery of ischiadic nerve, inferior gluteal artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 986-986 | connectedBodyPartTypes acromial artery, thoracoacromial artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 1465-1465 | connectedBodyPartTypes afferent arteriole, interlobular artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 252-252 | connectedBodyPartTypes anterior ethmoidal artery, anterior meningeal artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 257-257 | connectedBodyPartTypes anterior ethmoidal artery, anterior nasal artery branch and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 267-267 | connectedBodyPartTypes anterior ethmoidal artery, inferior palpebral arch artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 262-262 | connectedBodyPartTypes anterior ethmoidal artery, superior palpebral arch artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 1016-1016 | connectedBodyPartTypes anterior humeral circumflex artery, axillary artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 820-820 | connectedBodyPartTypes anterior inferior cerebellar artery, basilar artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 1169-1169 | connectedBodyPartTypes anterior interosseous artery, ulnar artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 79-79 | connectedBodyPartTypes anterior interventricular artery, anterior interventricular diagonal artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 73-73 | connectedBodyPartTypes anterior interventricular artery, anterior interventricular septal artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 1885-1885 | connectedBodyPartTypes anterior lateral malleolar artery, anterior tibial artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 1880-1880 | connectedBodyPartTypes anterior medial malleolar artery, anterior tibial artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 795-795 | connectedBodyPartTypes anterior spinal artery, vertebral artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 1863-1863 | connectedBodyPartTypes anterior tibial artery, popliteal artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 1873-1873 | connectedBodyPartTypes anterior tibial recurrent artery, anterior tibial artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 1148-1148 | connectedBodyPartTypes anterior ulnar recurrent artery, ulnar artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 371-371 | connectedBodyPartTypes anterolateral central artery, external striate artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 366-366 | connectedBodyPartTypes anterolateral central artery, internal striate artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 164-164 | connectedBodyPartTypes aortic arch, left common carotid artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 1454-1454 | connectedBodyPartTypes arcuate artery, interlobar artery and human |
No TPTP formula. May not be expressible in strict first order. | Anatomy.kif 1565-1565 | connectedBodyPartTypes auditory canal, middle ear and human |
No TPTP formula. May not be expressible in strict first order. | Anatomy.kif 1615-1615 | connectedBodyPartTypes pinna, auditory canal and human |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 996-1000 | A cognitive agent holds account a financial account and the cognitive agent is an instance of human if and only if the financial account is an instance of personal account |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17325-17333 | An entity is an instance of human and for all another entity the other entity doesn't employ the entity holds during a time position if and only if unemployed person is an attribute of the entity holds during the time position |
No TPTP formula. May not be expressible in strict first order. | Biography.kif 223-230 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 20628-20650 |
|
No TPTP formula. May not be expressible in strict first order. | Anatomy.kif 1923-1939 |
|
No TPTP formula. May not be expressible in strict first order. | Government.kif 223-234 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7589-7596 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25092-25101 |
|
No TPTP formula. May not be expressible in strict first order. | Government.kif 1753-1759 |
|
No TPTP formula. May not be expressible in strict first order. | Government.kif 1761-1767 |
|
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 44-59 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 12875-12881 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 279-285 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 12258-12263 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3923-3934 |
|
No TPTP formula. May not be expressible in strict first order. | MilitaryPersons.kif 285-296 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 6155-6163 |
|
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 686-694 |
|
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 651-659 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 335-341 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 212-218 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 262-267 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 385-390 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 304-311 |
|
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 519-530 |
|
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
consequent |
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
|
No TPTP formula. May not be expressible in strict first order. | People.kif 82-97 | A year is an instance of the year an integer and the births per thousand of a geopolitical area and the year is equal to a real number if and only if the population of the geopolitical area and 1000 is equal to another real number and another integer is equal to the number of instances in the class described by a symbolic string and the other integer and the other real number is equal to the real number |
No TPTP formula. May not be expressible in strict first order. | People.kif 118-133 | A year is an instance of the year an integer and the deaths per thousand of a geopolitical area and the year is equal to a real number if and only if the population of the geopolitical area and 1000 is equal to another real number and another integer is equal to the number of instances in the class described by a symbolic string and the other integer and the other real number is equal to the real number |
No TPTP formula. May not be expressible in strict first order. | People.kif 238-264 | A year is an instance of the year an integer and the deaths per thousand live births of a geopolitical area and the year is equal to a real number if and only if another integer is equal to the number of instances in the class described by a symbolic string and the other integer and 1000 is equal to another real number and a third integer is equal to the number of instances in the class described by another symbolic string and the third integer and the other real number is equal to the real number |
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
|
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
|
No TPTP formula. May not be expressible in strict first order. | People.kif 156-187 | A year is an instance of the year an integer and the migrants per thousand of a geopolitical area and the year is equal to a real number if and only if (the integer and another integer) is equal to 1 and an entity is an instance of the year the other integer and the population of the geopolitical area is equal to another real number holds during the year and the other real number and 1000 is equal to a third real number and a third integer is equal to the number of instances in the class described by a symbolic string and a fourth integer is equal to the number of instances in the class described by the symbolic string and (the third integer and the fourth integer) is equal to a fourth real number and the fourth real number and the third real number is equal to the real number |
No TPTP formula. May not be expressible in strict first order. | People.kif 206-223 | The male to female ratio of a geopolitical area is equal to a real number if and only if an integer is equal to the number of instances in the class described by a symbolic string and another integer is equal to the number of instances in the class described by another symbolic string and the integer and the other integer is equal to the real number |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29558-29570 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30144-30151 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17315-17319 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30128-30136 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 4195-4204 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 20628-20650 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2579-2583 |
|
No TPTP formula. May not be expressible in strict first order. | Government.kif 4546-4554 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 8024-8028 |
|
No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2663-2669 |
|
No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2534-2538 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16309-16313 |
|
No TPTP formula. May not be expressible in strict first order. | Cars.kif 3432-3461 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1562-1575 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 17397-17401 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3428-3455 |
|
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 381-388 |
|
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
statement |
No TPTP formula. May not be expressible in strict first order. | People.kif 456-469 | A year is an instance of the year an integer and the children born per woman of a geopolitical area and the year is equal to the number of instances in the class described by a symbolic string |
No TPTP formula. May not be expressible in strict first order. | Military.kif 863-872 | The available for military service male of a geopolitical area is equal to the number of instances in the class described by a symbolic string |
No TPTP formula. May not be expressible in strict first order. | Military.kif 886-897 | The fit for military service male of a geopolitical area is equal to the number of instances in the class described by a symbolic string |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31744-31749 | The population of a geopolitical area is equal to the number of instances in the class described by a symbolic string |
No TPTP formula. May not be expressible in strict first order. | Military.kif 924-937 | The reaching military age annually male of a geopolitical area and a year is equal to the number of instances in the class described by a symbolic string |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14919-14919 | Food is equal to food for human |