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 14784-14785 | |
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 3116-3116 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 3115-3115 | |
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 14783-14783 | Human is exhaustively partitioned into man and woman |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14782-14782 | Human is a subclass of cognitive agent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14781-14781 | 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 21622-21622 | 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 25357-25357 | 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 25358-25358 | 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 14787-14787 | 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 14794-14794 | Woman is a subclass of human |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1002-1002 | Woman is a subclass of human |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 1216-1216 | Woman is a subclass of human |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 679-679 | Woman is a subclass of human |
No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 210-210 | Woman is a subclass of human |
No TPTP formula. May not be expressible in strict first order. | terms-it.txt 213-213 | Woman is a subclass of human |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2363-2363 | Woman is a subclass of human |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 631-631 | Woman is a subclass of human |
No TPTP formula. May not be expressible in strict first order. | terms-cb.txt 215-215 | Woman is a subclass of human |
No TPTP formula. May not be expressible in strict first order. | terms-cz.txt 247-247 | Woman is a subclass of human |
No TPTP formula. May not be expressible in strict first order. | terms-de.txt 506-506 | Woman is a subclass of 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 | connected body parts abdominal aorta, thoracic aorta and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 1658-1658 | connected body parts 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 | connected body parts acromial artery, thoracoacromial artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 1465-1465 | connected body parts afferent arteriole, interlobular artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 252-252 | connected body parts anterior ethmoidal artery, anterior meningeal artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 257-257 | connected body parts anterior ethmoidal artery, anterior nasal artery branch and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 267-267 | connected body parts anterior ethmoidal artery, inferior palpebral arch artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 262-262 | connected body parts anterior ethmoidal artery, superior palpebral arch artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 1016-1016 | connected body parts anterior humeral circumflex artery, axillary artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 820-820 | connected body parts anterior inferior cerebellar artery, basilar artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 1169-1169 | connected body parts anterior interosseous artery, ulnar artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 79-79 | connected body parts anterior interventricular artery, anterior interventricular diagonal artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 73-73 | connected body parts anterior interventricular artery, anterior interventricular septal artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 1885-1885 | connected body parts anterior lateral malleolar artery, anterior tibial artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 1880-1880 | connected body parts anterior medial malleolar artery, anterior tibial artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 795-795 | connected body parts anterior spinal artery, vertebral artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 1863-1863 | connected body parts anterior tibial artery, popliteal artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 1873-1873 | connected body parts anterior tibial recurrent artery, anterior tibial artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 1148-1148 | connected body parts anterior ulnar recurrent artery, ulnar artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 371-371 | connected body parts anterolateral central artery, external striate artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 366-366 | connected body parts anterolateral central artery, internal striate artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 164-164 | connected body parts aortic arch, left common carotid artery and human |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 1454-1454 | connected body parts arcuate artery, interlobar artery and human |
No TPTP formula. May not be expressible in strict first order. | Anatomy.kif 1600-1600 | connected body parts auditory canal, middle ear and human |
No TPTP formula. May not be expressible in strict first order. | Anatomy.kif 1650-1650 | connected body parts 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 998-1002 | 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 17414-17422 | 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 229-236 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 22235-22257 |
|
No TPTP formula. May not be expressible in strict first order. | Anatomy.kif 1962-1978 |
|
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 8748-8755 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 26716-26725 |
|
No TPTP formula. May not be expressible in strict first order. | Government.kif 1751-1757 |
|
No TPTP formula. May not be expressible in strict first order. | Government.kif 1759-1765 |
|
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 14197-14203 |
|
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 12347-12352 |
|
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 7117-7125 |
|
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 677-685 |
|
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 642-650 |
|
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 509-520 |
|
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
consequent |
![]() |
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 930-939 | 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 953-964 | 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 33417-33422 | 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 991-1004 | 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 15011-15011 | Food is equal to food for human |
![]() |
![]() |