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 1280-1280 | member is internally related to 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 30276-30276 | immediate instance is a subrelation of instance |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 306-306 | immediate instance is a subrelation of instance |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 30275-30275 | immediate instance is a subrelation of instance |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 30274-30274 | immediate instance is a subrelation of instance |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 303-303 | immediate instance is a subrelation of instance |
antecedent |
consequent |
statement |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3181-3181 | ?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 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. | Government.kif 1203-1210 | For all ?AGENT, ?VOTER,, , ?ELECTION and ?VOTING
|
No TPTP formula. May not be expressible in strict first order. | Government.kif 885-893 | For all ?COUNTRY, ?ELECTION,, , ?VOTING and ?VOTER
|
No TPTP formula. May not be expressible in strict first order. | Government.kif 1054-1065 | For all ?POLITY, ?AGENT,, , ?ELECTION,, , ?VOTINGAGE and ?AGE
|
No TPTP formula. May not be expressible in strict first order. | Government.kif 1122-1136 | 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 18492-18509 | 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 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 32032-32037 | Individuals of type an organism in a geographic area. is equal to the number of instances in the class described by the organismI |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 32010-32015 | 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. | Medicine.kif 4547-4552 | There exist a process and an entity such that the process is an instance of disseminating and Netflix Corp. is an agent of the process and the entity is a patient of the process and the entity is an instance of motion picture |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 4554-4557 | There exists a process such that the process is an instance of film making and Netflix Corp. is an agent of the process |
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 824-825 | 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 3309-3315 | 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 |
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 1177-1177 | 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 1166-1166 | 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 2520-2520 | AAA_Rating is an instance of financial rating |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3220-3220 | Average buying price is an instance of unary function |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 4417-4417 | 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 2836-2836 | ASEAN regional forum is an instance of organization of nations |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3265-3265 | 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. | Medicine.kif 6405-6405 | AVPU alert status is an instance of AVPU status |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 6445-6445 | AVPU pain status is an instance of AVPU status |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 6468-6468 | AVPU unconscious status is an instance of AVPU status |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 6423-6423 | AVPU verbal status is an instance of AVPU status |
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. | Medicine.kif 2954-2954 | AbbVie is an instance of corporation |
No TPTP formula. May not be expressible in strict first order. | People.kif 1209-1209 | Abbot is an instance of religious position |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 3839-3839 | Abbott is an instance of corporation |
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 2528-2528 | 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 |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |