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 14646-14647 | |
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 14645-14645 | Human is exhaustively partitioned into man and woman |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14644-14644 | Human is a subclass of cognitive agent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14643-14643 | 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 20018-20018 | 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 793-793 | Every vocal cords is initially part of a 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 185-185 | Human adult is a subclass of human |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 248-248 | Human youth is a subclass of human |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14649-14649 | Man is a subclass of human |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 320-320 | Teenager is a subclass of human |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14656-14656 | 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 | |
No TPTP formula. May not be expressible in strict first order. | terms-tg.txt 214-214 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 791-791 | A vocal cords is typically a part of a human |
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 17254-17262 | 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 20601-20623 |
|
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 7562-7569 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25035-25044 |
|
No TPTP formula. May not be expressible in strict first order. | Government.kif 1789-1795 |
|
No TPTP formula. May not be expressible in strict first order. | Government.kif 1797-1803 |
|
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 12848-12854 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 286-292 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 12212-12217 |
|
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 6161-6169 |
|
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 342-348 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 219-225 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 269-274 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 392-397 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 311-318 |
|
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 29507-29519 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30120-30127 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17244-17248 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30104-30112 |
|
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 20601-20623 |
|
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 4582-4590 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7997-8001 |
|
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 16238-16242 |
|
No TPTP formula. May not be expressible in strict first order. | Cars.kif 3447-3476 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 1579-1592 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 17370-17374 |
|
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 872-881 | 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 895-906 | 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 31712-31717 | 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 933-946 | 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 14873-14873 | Food is equal to food for human |