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 5414-5414 | 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 30281-30281 | 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 30280-30280 | immediate instance is a subrelation of instance |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 30279-30279 | 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 3193-3193 | ?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 1205-1212 | For all ?AGENT, ?VOTER,, , ?ELECTION and ?VOTING
|
No TPTP formula. May not be expressible in strict first order. | Government.kif 887-895 | For all ?COUNTRY, ?ELECTION,, , ?VOTING and ?VOTER
|
No TPTP formula. May not be expressible in strict first order. | Government.kif 1056-1067 | For all ?POLITY, ?AGENT,, , ?ELECTION,, , ?VOTINGAGE and ?AGE
|
No TPTP formula. May not be expressible in strict first order. | Government.kif 1124-1138 | 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 18460-18477 | 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 31999-32004 | 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 31977-31982 | 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 4559-4564 | 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 4566-4569 | 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 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 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 2838-2838 | 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 6421-6421 | AVPU alert status is an instance of AVPU status |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 6461-6461 | AVPU pain status is an instance of AVPU status |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 6484-6484 | AVPU unconscious status is an instance of AVPU status |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 6439-6439 | 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 2966-2966 | 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 3851-3851 | 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 |