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 14705-14706 | |
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 14704-14704 | Human is exhaustively partitioned into man and woman |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14703-14703 | Human is a subclass of cognitive agent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 14702-14702 | 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 20308-20308 | 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 24012-24012 | 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 24013-24013 | 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 14708-14708 | 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 14715-14715 | 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. | relations-ro.kif 700-700 | 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 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 17335-17343 | 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 20891-20913 |
|
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 7780-7787 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25355-25364 |
|
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 13066-13072 |
|
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 12272-12277 |
|
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 29823-29835 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30409-30416 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 17325-17329 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30393-30401 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 4310-4319 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 20891-20913 |
|
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 4544-4552 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 8215-8219 |
|
No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2715-2721 |
|
No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2586-2590 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16319-16323 |
|
No TPTP formula. May not be expressible in strict first order. | Cars.kif 3507-3536 |
|
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 17660-17664 |
|
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 32009-32014 | 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 14932-14932 | Food is equal to food for human |