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 14716-14717 | |
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 14715-14715 | Human is exhaustively partitioned into man and woman |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14714-14714 | Human is a subclass of cognitive agent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14713-14713 | 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 20936-20936 | 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 24640-24640 | 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 24641-24641 | 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 14719-14719 | 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 14726-14726 | 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 | 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 1564-1564 | connectedBodyPartTypes auditory canal, middle ear and human |
No TPTP formula. May not be expressible in strict first order. | Anatomy.kif 1614-1614 | 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 17346-17354 | 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 21519-21541 |
|
No TPTP formula. May not be expressible in strict first order. | Anatomy.kif 1922-1938 |
|
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 8262-8269 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25983-25992 |
|
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 13672-13678 |
|
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 12283-12288 |
|
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 6637-6645 |
|
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 674-682 |
|
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 639-647 |
|
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 507-518 |
|
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 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 32664-32669 | 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 14943-14943 | Food is equal to food for human |
![]() |
![]() |