instance |
appearance as argument number 1 |
![]() |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1359-1361 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 84-87 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 17-20 | |
No TPTP formula. May not be expressible in strict first order. | spanish_format.kif 17-20 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 81-81 | The number 1 argument of instance is an instance of entity |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 82-82 | The number 2 argument of instance is an instance of class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 80-80 | instance is an instance of binary predicate |
appearance as argument number 2 |
![]() |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 305-305 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 310-310 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 175-175 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 149-149 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1995-1995 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 127-127 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 173-173 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 400-400 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 188-188 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 195-195 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 184-184 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 302-302 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1281-1281 | member is internally related to instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5399-5399 | element is a subrelation of instance |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 89-89 | immediate instance is a subrelation of instance |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 30256-30256 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 306-306 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 30255-30255 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 30254-30254 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 303-303 |
antecedent |
![]() |
consequent |
![]() |
statement |
![]() |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3119-3119 | ?D is an instance of the day 23 is an agreement effective date of antarctic treaty |
No TPTP formula. May not be expressible in strict first order. | People.kif 482-495 | 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. | Government.kif 1241-1248 | For all ?AGENT, ?VOTER,, , ?ELECTION and ?VOTING
|
No TPTP formula. May not be expressible in strict first order. | Government.kif 923-931 | For all ?COUNTRY, ?ELECTION,, , ?VOTING and ?VOTER
|
No TPTP formula. May not be expressible in strict first order. | Government.kif 1092-1103 | For all ?POLITY, ?AGENT,, , ?ELECTION,, , ?VOTINGAGE and ?AGE
|
No TPTP formula. May not be expressible in strict first order. | Government.kif 1160-1174 | For all ?POLITY, ?VOTER,, , ?ELECTION,, , ?VOTINGAGE and ?AGE
|
No TPTP formula. May not be expressible in strict first order. | WMD.kif 921-929 | ?SYMPTOM is a biochemical agent syndrome of ?AGENT and ?AGENT biochemical agent antidote ?SUBSTANCE for ?PROCESS and ?SAMPLE is an instance of ?SUBSTANCE and ?THERAPY is an instance of ?PROCESS and ?ORGANISM experiences ?THERAPY and ?SAMPLE is a patient of ?THERAPY decreases likelihood of ?SYMPTOM is an attribute of ?ORGANISM |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 18042-18059 | There exist ?X, ?CUT,, , ?PAPER,, , ?CBO and ?INFO such that ?X is an instance of paper shredder and ?CUT is an instance of cutting and ?X is an instrument for ?CUT and ?PAPER is an instance of paper and ?PAPER is a patient of ?CUT and ?CBO is located at ?PAPER and ?CBO is an instance of visual content bearing object and ?CBO contains information ?INFO decreases likelihood of there exists ?READ such that ?READ is an instance of interpreting and ?INFO is a patient of ?READ and the time of existence of ?CUT happens earlier than the time of existence of ?READ |
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. | People.kif 49-54 | 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. | ComputingBrands.kif 2453-2457 | There exists a time position such that the time position is an instance of the year 1976 and Steve Wozniak is a coworker of Steve Jobs holds during the time position |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2441-2445 | There exists a time position such that the time position is an instance of the year 2002 and Tim Cook is a coworker of Steve Jobs holds during the time position |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 825-826 | There exists an entity such that the entity is an instance of entity |
No TPTP formula. May not be expressible in strict first order. | Media.kif 1970-1978 | There exists a time interval such that the time interval is an instance of time interval and the time interval finishes the time of existence of Jesus of Nazareth and the time interval starts the time of existence of Twelve apostles and for all an entity
|
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 3307-3313 | IBookstore has the purpose there exists ?D such that ?D is an instance of downloading and iBookstore is an instrument for ?D and ?T is an instance of text and the object transferred in ?D is ?T |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2501-2504 | Serbia is an instance of european nation and a time position is an instance of the day 5 holds during after the time position |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2496-2499 | Serbia is an instance of independent state and a time position is an instance of the day 5 holds during after the time position |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2506-2509 | Serbia has name "Republic of Serbia" and a time position is an instance of the day 5 holds during after the time position |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2528-2531 | A time position is an instance of the day 3 and Montenegro is an instance of european nation holds during after the time position |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2523-2526 | A time position is an instance of the day 3 and Montenegro is an instance of independent state holds during after the time position |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2533-2536 | A time position is an instance of the day 3 and Montenegro has name "Montenegro" holds during after the time position |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2546-2550 | A time position is an instance of the day 3 and serbia and montenegro is not an instance of independent state holds during after the time position |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2791-2794 | A time position is an instance of the day 1 and andean community of nations is a conventional long name of "Andean Community of Nations" holds during immediately after the time position |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
appearance as argument number 0 |
![]() |
No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 663-663 | The cell part of a cell and a kind of cell part is an instance of a kind of cell part |
No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 652-652 | The viral part of a virus and a kind of virus part is an instance of a kind of virus part |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 2534-2534 | AAA-rating is an instance of financial rating |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3426-3426 | Average buying price is an instance of unary function |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 4623-4623 | A/B test is an instance of experiment attribute |
No TPTP formula. May not be expressible in strict first order. | Languages.kif 5379-5379 | A pucikwar language is an instance of central great andamanese language |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2874-2874 | ASEAN regional forum is an instance of organization of nations |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3471-3471 | Average buying price is an instance of unary function |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2122-2122 | AT&T corp is an instance of corporation |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2560-2560 | Aaland islands is an instance of archipelago |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2561-2561 | Aaland islands is an instance of dependency or special sovereignty area |
No TPTP formula. May not be expressible in strict first order. | Languages.kif 3771-3771 | Aariya language is an instance of unclassified spoken language |
No TPTP formula. May not be expressible in strict first order. | People.kif 1235-1235 | Abbot is an instance of religious position |
No TPTP formula. May not be expressible in strict first order. | Languages.kif 2923-2923 | Abinomn language is an instance of spoken human language |
No TPTP formula. May not be expressible in strict first order. | Languages.kif 3777-3777 | Abishira language is an instance of unclassified spoken language |
No TPTP formula. May not be expressible in strict first order. | Languages.kif 14550-14550 | Abkhaz language is an instance of north caucasian language |
No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2410-2410 | Aborted is an instance of binary function |
No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2476-2476 | Aborted launch is an instance of binary function |
No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2430-2430 | Aborted mission is an instance of binary function |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16957-16957 | Above is an instance of anti-symmetric positional attribute |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16956-16956 | Above is an instance of positional attribute |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4747-4747 | Absolute value is an instance of total valued relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4746-4746 | Absolute value is an instance of unary function |
No TPTP formula. May not be expressible in strict first order. | Languages.kif 13713-13713 | Abun language is an instance of north birds head language |
No TPTP formula. May not be expressible in strict first order. | Music.kif 518-518 | Acapella is an instance of music genre |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
![]() |
![]() |