Sigma KB Term Intersection

No TPTP formula. May not be expressible in strict first order.	Catalog.kif 136-145	If an agent offers items for sale in a catalog during a kind of time interval and a kind of entity is in the catalog and a kind of entity is a subclass of object and a process is an instance of another kind of process and another kind of process is a subclass of process and another entity is an instance of the kind of entity and the other entity is a patient of the process, then the agent is capable of being a agent in the other kind of process during a kind of time interval
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4051-4054	If a kind of OrganismRemains is equal to a dead tropical fruit, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Merge.kif 2878-2883	If a class is disjointly decomposed into @ROW, then for all a third class if the third class is a member of (@ROW), then the third class is a subclass of the class
No TPTP formula. May not be expressible in strict first order.	WMD.kif 950-954	If a disease or syndrome is disease treatment a kind of biologically active substance for a kind of process and another kind of process is a subclass of a kind of process, then the disease or syndrome is disease treatment a kind of biologically active substance for another kind of process
No TPTP formula. May not be expressible in strict first order.	WMD.kif 2019-2024	If a kind of biochemical agent is a subclass of tick borne encephalitis virus, then there exists a disease or syndrome such that the disease or syndrome is an instance of tick borne encephalitis and the disease or syndrome is a biochemical agent syndrome of a kind of biochemical agent
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 1683-1688	If an object is an instance of river and a kind of self connected object is a trafficable for traffic type of the object and a kind of self connected object is a subclass of water vehicle, then the object is an instance of waterway
No TPTP formula. May not be expressible in strict first order.	Dining.kif 204-208	If a catalog is an instance of drinks menu and a kind of entity is in the catalog, then a kind of entity is a subclass of beverage
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 7332-7338	If an agent is an instance of medical clinic, then there doesn't exist an object such that the agent possesses the object and the object is a subclass of temporary residence
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 374-396	If renters of a kind of hotel unit can pay to use a class and the class is a subclass of object, then if a temporary residence is an instance of a kind of hotel unit and a human stays at the temporary residence and the temporary residence is an element of belongings of an agent and an object is an instance of the class and the object is located at the temporary residence and a process is an instance of process and the human is an agent of the process and the process is located at the object or the object is a patient of the process or the object is an instrument for the process or the object is a resource for the process, then the process is price the processRICE an unit of measure(s) for the agent and the unit of measure is an instance of UnitOfCurrency and the processRICE is greater than 0
No TPTP formula. May not be expressible in strict first order.	Geography.kif 6088-6096	If a kind of plant is found in a geographic area and a kind of plant is a subclass of plant and the geographic area is an instance of geographic area, then there exists a physical such that the physical is an instance of the kind of plant and the physical is located at the geographic area
No TPTP formula. May not be expressible in strict first order.	WMD.kif 1279-1281	If a disease or syndrome is disease treatment oral antibiotic for a kind of process, then a kind of process is a subclass of ingesting
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4093-4096	If a kind of OrganismRemains is equal to a dead mango, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Cars.kif 1674-1681	If an entity is an instance of Charcoal, then there exist a class and an object such that the class is a subclass of combustion and the object is an instance of wood and the entity is a result of the class and the object is a resource for the class
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 3552-3557	If a corpuscular object is an instance of currency coin, then there exists a kind of substance such that a kind of substance is a subclass of metal and the corpuscular object is made of the kind of substance
No TPTP formula. May not be expressible in strict first order.	WMD.kif 1384-1387	If a kind of biological agent is equal to the biological agent of coccidiodes posadasii, then a kind of biological agent is a subclass of life threatening agent
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2288-2297	If a geopolitical area export total in period a currency measure for a kind of time interval and a kind of time interval is a subclass of year or the kind of time interval is a subclass of the fiscal year of the geopolitical area, then there exists a time position such that the time position is an instance of the kind of time interval and the currency measure is an annual export total of the geopolitical area holds during the time position
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2134-2141	If a physical quantity is an annual electricity consumption of a geopolitical area holds during a time position and the time position is an instance of a kind of time interval and a kind of time interval is a subclass of year or the kind of time interval is a subclass of the fiscal year of the geopolitical area, then the geopolitical area is electricity consumption in period the physical quantity for the kind of time interval
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 16344-16348	If a relation is an instance of economic relation and the number 1 argument of the relation is an instance of a class, then the class is a subclass of geopolitical area
No TPTP formula. May not be expressible in strict first order.	Merge.kif 14895-14911	If an object is an instance of the objectC and another object is an instance of the other objectC and the objectC is not equal to the other objectC and the objectC is not a subclass of the other objectC and the other objectC is not a subclass of the objectC and the object is adjacent to the other object, then the statement there exists an entity such that the entity is an instance of connective tissue and the entity is between the object and the other object has the modal force of likely
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 276-287	If a kind of physical is an amenity in a kind of hotel unit and a kind of physical is a subclass of object, then for all an object if the object is an instance of a kind of hotel unit, then there exists another physical such that the object is an instance of the kind of hotel unit and the other physical is an instance of the kind of physical and the other physical is located at the object
No TPTP formula. May not be expressible in strict first order.	Food.kif 237-243	If an object is an instance of meat, then there exist another object and a kind of organism such that the other object is an instance of a dead a kind of organism and the object is a part of the other object and the kind of organism is a subclass of animal
No TPTP formula. May not be expressible in strict first order.	UXExperimentalTerms.kif 1703-1725	If a time interval is an instance of the time interval_CLASS and the time interval_CLASS is a subclass of process and an AccessingWebPage is an instance of AccessingWebPage and an agent is an instance of agent and the agent is an agent of the time interval and the agent is an agent of the AccessingWebPage and the time interval takes place during the AccessingWebPage and a physical is an instance of time interval and there doesn't exist the time interval2 such that the time interval2 is an instance of the time interval_CLASS and the agent is an agent of the time interval2 and the time interval2 takes place during the AccessingWebPage and the beginning of the time of existence of the time interval2 happens before the beginning of the time of existence of the time interval and the beginning of the time of existence of the AccessingWebPage is equal to the beginning of the time of existence of the physical and the beginning of the time of existence of the time interval is equal to the end of the time of existence of the physical, then the time of the AccessingWebPage in the class the time interval_CLASS is equal to the physical
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3995-3998	If a kind of OrganismRemains is equal to a dead grape, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Economy.kif 1638-1642	If a kind of object is an organization product type of an organization and a kind of object is a subclass of another kind of object, then another kind of object is an organization product type of the organization
No TPTP formula. May not be expressible in strict first order.	Dining.kif 997-1012	If an agent believes another agent is quick and the agent believes a third agent is slow and a process is an instance of a class and another process is an instance of the class and the class is a subclass of process and the other agent is an agent of the process and the third agent is an agent of the other process, then an unit of measure is an instance of UnitOfDuration and duration of the time of existence of the process is a real number the unit of measure(s) and duration of the time of existence of the other process is another real number the unit of measure(s) and the other real number is greater than the real number
No TPTP formula. May not be expressible in strict first order.	Media.kif 1849-1853	If an agent is the author of a kind of musical composition and a kind of musical composition is a subclass of musical composition, then the agent composed the kind of musical composition
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4100-4103	If a kind of OrganismRemains is equal to a dead papaw, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Cars.kif 1772-1786	If an object is an instance of a kind of compound substance and a kind of compound substance is a subclass of compound substance and there doesn't exist another object such that the other object is an instance of the kind of compound substance and the other object is a part of the object and the number of molecules of a kind of elemental substance in a molecule of the kind of compound substance is an integer and a collection is an instance of group and a third object is a member of the collection and the third object is a part of the object and the third object is an instance of a kind of elemental substance, then the integer is a member count of the collection
No TPTP formula. May not be expressible in strict first order.	Food.kif 804-810	If an object is an instance of seafood, then there exist another object and a kind of organism such that the other object is an instance of a dead a kind of organism and the object is a part of the other object and the kind of organism is a subclass of fish
No TPTP formula. May not be expressible in strict first order.	Geography.kif 2283-2293	If a kind of physical is a natural hazard type in area of a geographic area and a kind of physical is a subclass of process, then there exists another physical such that the other physical is an instance of the kind of physical and the other physical is located at the geographic area and the time of existence of the geographic area overlaps the time of existence of the other physical
No TPTP formula. May not be expressible in strict first order.	Catalog.kif 36-41	If an abstract is an instance of catalog, then there exists an agent such that the agent is a subclass of agent and the agent offers items for sale in the abstract
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2604-2611	If a currency measure is an annual import total of a geopolitical area holds during a time position and the time position is an instance of a kind of time interval and a kind of time interval is a subclass of year or the kind of time interval is a subclass of the fiscal year of the geopolitical area, then the geopolitical area import total in period the currency measure for the kind of time interval
No TPTP formula. May not be expressible in strict first order.	Government.kif 2328-2335	If a kind of content bearing object is a subclass of party platform and a cognitive agent is the author of a kind of content bearing object and the cognitive agent is an instance of political party and a content bearing physical is an instance of the kind of content bearing object and the content bearing physical contains information a formula, then the cognitive agent believes the formula
No TPTP formula. May not be expressible in strict first order.	Merge.kif 15437-15439	If a kind of artifact is a version of another kind of artifact, then a kind of artifact is a subclass of another kind of artifact
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 17793-17814	If a physical is an instance of Protecting, then the physical has the purpose there exists an entity such that the entity is an instance of object and object is a patient of the physical and another entity is a subclass of the class described by a third entity and the physical prevents the occurrence of the other entity or the physical hinders the other entity
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2123-2132	If a geopolitical area is electricity consumption in period a physical quantity for a kind of time interval and a kind of time interval is a subclass of year or the kind of time interval is a subclass of the fiscal year of the geopolitical area, then there exists a time position such that the time position is an instance of the kind of time interval and the physical quantity is an annual electricity consumption of the geopolitical area holds during the time position
No TPTP formula. May not be expressible in strict first order.	Merge.kif 242-248	If the number a positive integer argument of a relation is a subclass of a class and the number the positive integer argument of the relation is a subclass of another class, then the class is a subclass of the other class or the other class is a subclass of the class
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 7846-7860	If a process is an instance of recreation or exercise and the processM is an instrument for the process and the processM is an instance of ergometer and an agent experiences the process and the processOW is an instance of rowing and the processMOT is a subprocess of the process and a class is a subclass of body motion and the processMOT is an instance of the class, then there exists the processOWMOT such that the processOWMOT is an instance of the class and the processOWMOT is a subprocess of the process and the agent is an agent of the processOWMOT
No TPTP formula. May not be expressible in strict first order.	Media.kif 195-200	If a kind of getting is equal to receiving a a kind of object and another kind of getting is equal to receiving a another kind of object and a kind of object is a subclass of another kind of object, then a kind of getting is a subclass of another kind of getting
No TPTP formula. May not be expressible in strict first order.	Merge.kif 219-225	If the number a positive integer argument of a relation is an instance of a class and the number the positive integer argument of the relation is an instance of another class, then the class is a subclass of the other class or the other class is a subclass of the class
No TPTP formula. May not be expressible in strict first order.	Cars.kif 3533-3555	If a physical is an instance of respirator, then the physical has the purpose if an entity is an instance of animal and the entity wears the physical, then there exist another entity, a third entity and a fourth entity such that the fourth entity is an instance of process and the physical is an instrument for the fourth entity and the fourth entity prevents the occurrence of the third entity and the third entity is a subclass of the class described by a fifth entity
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3829-3835	If a case role is an instance of case role and the case role an entity and an object and the entity is an instance of a kind of process and a kind of process is a subclass of process, then the object is capable of doing the kind of process as a the case role
No TPTP formula. May not be expressible in strict first order.	MilitaryProcesses.kif 940-949	If a kind of content bearing object is a subclass of joint publication and a content bearing physical is an instance of a kind of content bearing object and the content bearing physical contains information a formula and an agent is the author of the kind of content bearing object, then there exists an organization such that the organization is a part of the organization US military and the agent obligates the organization to perform task of the type the formula
No TPTP formula. May not be expressible in strict first order.	Media.kif 1892-1896	If an entity publishes a class holds during a time position and the class is a subclass of text, then information industry is an attribute of the entity holds during the time position
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3880-3883	If a kind of OrganismRemains is equal to a dead sweet pepper, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3918-3921	If a kind of OrganismRemains is equal to a dead squash, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 26058-26061	If a kind of uniform is a subclass of uniform, then there exists a group such that the group has uniform a kind of uniform
No TPTP formula. May not be expressible in strict first order.	Catalog.kif 332-347	If a process is an instance of buying and an entity is a patient of the process and the process originates at a cognitive agent and the price of another kind of entity from the cognitive agent according to a pricing scheme is a currency measure or the unit price charged the cognitive agent under the pricing scheme for a function quantity is another kind of entity and the other kind of entity is a subclass of physical and the entity is an immediate instance of the other kind of entity and a kind of payment is a valid payment under the pricing scheme, then the statement there exists a kind of paymentMENT such that the kind of paymentMENT is an instance of the kind of payment and the kind of paymentMENT is a subprocess of the process has the modal force of likely
No TPTP formula. May not be expressible in strict first order.	WMD.kif 969-973	If a kind of organism is a biological agent carrier of a kind of biological agent and another kind of organism is a subclass of a kind of organism, then another kind of organism is a biological agent carrier of a kind of biological agent
No TPTP formula. May not be expressible in strict first order.	Catalog.kif 367-382	If the price of a kind of entity from a cognitive agent according to a pricing scheme is a currency measure or the unit price charged the cognitive agent under the pricing scheme for a function quantity is a kind of entity and the kind of entity is a subclass of physical and another entity is an immediate instance of the kind of entity and the pricing scheme is valid during a time interval, then the statement if a third entity is an instance of selling and the cognitive agent is an agent of the third entity and the other entity is a patient of the third entity, then the currency measure is a transaction amount of the third entity has the modal force of likely holds during the time interval
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1005-1010	If a class is a subclass of substance and a substance is an instance of the class and another substance is a piece of the substance, then the other substance is an instance of the class
No TPTP formula. May not be expressible in strict first order.	Merge.kif 158-165	If a class is an immediate subclass of another class, then there doesn't exist a third class such that the third class is a subclass of the other class and the class is a subclass of the third class and the other class is not equal to the third class and the class is not equal to the third class
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3873-3876	If a kind of OrganismRemains is equal to a dead eggplant, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Media.kif 1886-1890	If an entity publishes a class holds during a time position and the class is a subclass of musical composition, then music publishers is an attribute of the entity holds during the time position
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3951-3954	If a kind of OrganismRemains is equal to a dead cassava, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Geography.kif 1269-1273	If a geographic area is an instance of a kind of climate zone and a kind of climate zone is a subclass of climate zone, then the kind of climate zone is a climate type in area of the geographic area
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3845-3848	If a kind of OrganismRemains is equal to a dead leafy green vegetable, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	WMD.kif 956-960	If a disease or syndrome is disease treatment a kind of biologically active substance for a kind of process and another kind of biologically active substance is a subclass of a kind of biologically active substance, then the disease or syndrome is disease treatment another kind of biologically active substance for a kind of process
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4110-4113	If a kind of OrganismRemains is equal to a dead papaya, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Catalog.kif 97-106	If an agent offers items for sale in a catalog and a kind of entity is in the catalog and a kind of entity is a subclass of object and a process is an instance of another kind of process and another kind of process is a subclass of process and another entity is an instance of the kind of entity and the other entity is a patient of the process, then the agent is capable of doing the other kind of process as a agent
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 13013-13024	If the maximum expected value of a kind of object is a real number an unit of measure(s) and a class is a subclass of NonCompositeUnitOfMeasure and the unit of measure is an instance of the class, then the statement there exist an entity, the real numberUANTITY and a third entity such that the entity is an instance of a kind of object and the measure of the entity is the real numberUANTITY the third entity(s) and the third entity is an instance of the class and the real numberUANTITY the third entity(s) is greater than the real number the unit of measure(s) has the modal force of unlikely
No TPTP formula. May not be expressible in strict first order.	WMD.kif 313-315	If batrachotoxin is a secretes toxin of a kind of organism, then a kind of organism is a subclass of amphibian
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1720-1728	If a kind of object is equal to the attr of another kind of object and an attribute and a third object is an instance of a kind of object, then the third object is an instance of another kind of object and the kind of object is a subclass of the other kind of object and the attribute is an attribute of the third object
No TPTP formula. May not be expressible in strict first order.	engineering.kif 853-858	If a corpuscular object is an instance of resistor element, then there exists a kind of substance such that a kind of substance is a subclass of insulator substance and the corpuscular object is made of the kind of substance
No TPTP formula. May not be expressible in strict first order.	WMD.kif 789-793	If a kind of process is a biochemical agent delivery of a kind of biochemical agent and another kind of process is a subclass of a kind of process, then another kind of process is a biochemical agent delivery of a kind of biochemical agent
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 14070-14077	If a kind of series is a subclass of news program and a kind of text is equal to volume a positive integer in the series a kind of series, then there exists a process such that the process is an instance of disseminating and a kind of text is a patient of the process
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 289-308	If a human is a guest at a cognitive agent and the human stays at a temporary residence and the temporary residence is an element of belongings of the cognitive agent and the temporary residence is an instance of the temporary residenceOOM and a kind of physical is an amenity in the temporary residenceOOM and a kind of physical is a subclass of object, then there exists another physical such that the other physical is an instance of the kind of physical and the other physical is located at the temporary residence and the cognitive agent allows the human to perform task of the type there exists an entity such that the human is an agent of the entity and the other physical is an instrument for the entity or the other physical is a patient of the entity or the other physical is a resource for the entity
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2224-2231	If a physical quantity is an annual electricity import of a geopolitical area holds during a time position and the time position is an instance of a kind of time interval and a kind of time interval is a subclass of year or the kind of time interval is a subclass of the fiscal year of the geopolitical area, then the geopolitical area is electricity import in period the physical quantity for the kind of time interval
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 2624-2629	If a kind of self connected object is a trafficable for traffic type of a region and a kind of self connected object is a subclass of agent and an object is an instance of the kind of self connected object, then translocation capable at location agent for the object with the region
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 502-518	If a cognitive agent is a customer of another cognitive agent and the cognitive agent has a kind of physical and a kind of physical is a subclass of process, then the statement there exist an entity and another entity such that the other entity is an element of belongings of the cognitive agent and the cognitive agent is an agent of the entity and the other cognitive agent is a patient of the entity and the entity is an instance of the kind of physical or a third entity is an instance of a fourth entity and the entity is a subprocess of the third entity and the entity is located at the other entity has the modal force of possibility
No TPTP formula. May not be expressible in strict first order.	Dining.kif 215-219	If a catalog is an instance of cocktail menu and a kind of entity is in the catalog, then a kind of entity is a subclass of alcoholic beverage
No TPTP formula. May not be expressible in strict first order.	Merge.kif 16104-16109	If an organism is a parent of another organism and a class is a subclass of organism and the organism is an instance of the class, then the other organism is an instance of the class
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4072-4075	If a kind of OrganismRemains is equal to a dead breadfruit, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Economy.kif 1991-2000	If a geopolitical area is electricity production in period a physical quantity for a kind of time interval and a kind of time interval is a subclass of year or the kind of time interval is a subclass of the fiscal year of the geopolitical area, then there exists a time position such that the time position is an instance of the kind of time interval and the physical quantity is an annual electricity production of the geopolitical area holds during the time position
No TPTP formula. May not be expressible in strict first order.	Dining.kif 178-182	If a catalog is an instance of menu and a kind of entity is in the catalog, then a kind of entity is a subclass of food for human
No TPTP formula. May not be expressible in strict first order.	Cars.kif 1688-1693	If a corpuscular object is an instance of charcoal filter, then there exists a kind of substance such that a kind of substance is a subclass of Charcoal and the corpuscular object is made of the kind of substance
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2299-2306	If a currency measure is an annual export total of a geopolitical area holds during a time position and the time position is an instance of a kind of time interval and a kind of time interval is a subclass of year or the kind of time interval is a subclass of the fiscal year of the geopolitical area, then the geopolitical area export total in period the currency measure for the kind of time interval
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 16420-16425	If an object is an instance of game artifact, then there exists a kind of process such that a kind of process is a subclass of game and the object is capable of doing the kind of process as a instrument
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4079-4082	If a kind of OrganismRemains is equal to a dead coconut, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4131-4134	If a kind of OrganismRemains is equal to a dead plantain, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4065-4068	If a kind of OrganismRemains is equal to a dead banana, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Government.kif 1689-1695	If an agent is an instance of agent and the election of the agent is a subclass of election, then the agent is an instance of organization or the agent is an instance of geopolitical area
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 14088-14102	If a kind of series is a subclass of periodical and volume a positive integer in the series a kind of series is equal to a kind of text and volume another positive integer in the series the kind of series is equal to another kind of text and the other positive integer is greater than the positive integer and a process is an instance of publication and another process is an instance of publication and an entity is an instance of a kind of text and another entity is an instance of another kind of text and the entity is a patient of the process and the other entity is a patient of the other process and date of the process is a day and date of the other process is another day, then the end of the day happens before the end of the other day
No TPTP formula. May not be expressible in strict first order.	MilitaryDevices.kif 35-43	If a military vehicle %is weapon carrying capability a kind of weapon for a positive integer and an object is an instance of a kind of weapon and the object is capable of doing a kind of process as a a case role and a kind of process is a subclass of shooting or the kind of process is a subclass of damaging, then the military vehicle is capable of doing the kind of process as a the case role
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 1572-1580	If a kind of transportation device is a subclass of transportation device and the transportation of a kind of transportation device is a subclass of transportation and a process is an instance of the transportation of the kind of transportation device, then there exists an object such that the object is an instance of the kind of transportation device and the object is an instrument for the process
No TPTP formula. May not be expressible in strict first order.	Geography.kif 1005-1010	If a geographic area is an instance of a kind of maritime claim area and a kind of maritime claim area is a subclass of maritime claim area and a geopolitical area is a claimed territory of the geographic area, then the kind of maritime claim area is a maritime claim type of the geopolitical area
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 8759-8761	If a class is an instance of biological species, then the class is a subclass of organism
No TPTP formula. May not be expressible in strict first order.	Merge.kif 337-341	If the values returned by a function are subclasses of a kind of class and the function(@ROW) is equal to another class, then the other class is a subclass of a kind of class
No TPTP formula. May not be expressible in strict first order.	Merge.kif 12613-12617	If a process is an instance of publication and a class is a patient of the process, then the class is a subclass of text
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 14478-14488	If a collection is an instance of industry, then if a physical is a member of the collection and another physical is a member of the collection, then there exists a class such that the class is a subclass of corporation and the physical is an immediate instance of the class and the other physical is an immediate instance of the class
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 1164-1179	If oversized is an attribute of an object and the object is an immediate instance of a class and the class is a subclass of hotel unit, then there exist a physical, a real number,, , another real number and an unit of measure such that the physical is an immediate instance of the class and the unit of measure is an instance of UnitOfArea and the measure of the physical is the real number the unit of measure(s) and the measure of the object is the other real number the unit of measure(s) and the real number is an instance of area measure and the other real number is an instance of area measure and the other real number is greater than the real number
No TPTP formula. May not be expressible in strict first order.	Geography.kif 6098-6106	If not a kind of plant is found in a geographic area and a kind of plant is a subclass of plant and the geographic area is an instance of geographic area, then there doesn't exist a physical such that the physical is an instance of the kind of plant and the physical is located at the geographic area
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 29138-29147	If a physical is a subclass of a covering for a kind of body part, then the physical has the purpose there exist an entity, a kind of body partI and the physicalI such that the entity is an instance of covering and the kind of body partI is an instance of the kind of body part and the physicalI is an instance of the physical and the entity ends up at the kind of body partI and the physicalI is a patient of the entity
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 2617-2622	If a kind of self connected object is a trafficable for traffic type of a region and a kind of self connected object is a subclass of transportation device and an object is an instance of the kind of self connected object, then transportation capable at location instrument for the object with the region
No TPTP formula. May not be expressible in strict first order.	Media.kif 2877-2883	If a symbolic string in ISO-4217-A denotes an UnitOfCurrency and another symbolic string in ISO-3166-1-alpha-2 denotes a class and the class is a subclass of geopolitical area and the other symbolic string is equal to the sub-string of the symbolic string from 0 to 2, then the UnitOfCurrency is a currency type of the class
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 790-811	If use of a kind of physical is free for a kind of hotel function room and an entity is an instance of a kind of hotel function room and the entity is an element of belongings of an agent and a process is an instance of renting and the entity is a patient of the process and the agent is an agent of the process and the process ends up at another entity and a kind of physical is a subclass of object, then the statement there exist a third entity and a fourth entity such that the third entity is an instance of the kind of physical and the fourth entity is an instance of process and the third entity is a resource for the fourth entity or the third entity is an instrument for the fourth entity or the third entity is a patient of the fourth entity and the other entity is an agent of the fourth entity or the other entity experiences the fourth entity has the modal force of possibility
No TPTP formula. May not be expressible in strict first order.	Catalog.kif 64-75	If an agent offers items for sale in a catalog and a kind of entity is in the catalog and a kind of entity is a subclass of proposition, then the statement there exist another entity and a third entity such that the third entity expresses the content of the kind of entity and the other entity is an instance of selling and the third entity is a patient of the other entity and the agent is an agent of the other entity has the modal force of possibility
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4000-4003	If a kind of OrganismRemains is equal to a dead melon, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2593-2602	If a geopolitical area import total in period a currency measure for a kind of time interval and a kind of time interval is a subclass of year or the kind of time interval is a subclass of the fiscal year of the geopolitical area, then there exists a time position such that the time position is an instance of the kind of time interval and the currency measure is an annual import total of the geopolitical area holds during the time position
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 17778-17787
No TPTP formula. May not be expressible in strict first order.	Catalog.kif 87-92	If an agent offers items for sale in a catalog and a kind of entity is in the catalog and a kind of entity is a subclass of process, then the agent is capable of doing the kind of entity as a agent
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 7011-7025	If an object is an instance of auditorium seat and the object is a part of another object and a third object is a part of the other object and the other object is an instance of auditorium and the third object is an instance of performance stage and a fourth object is located at the object and the fourth object is an instance of human and a kind of process is a subclass of seeing and for all another process if the other process is an instance of a kind of process, then the third object is a patient of the other process , then the fourth object is capable of doing the kind of process as a agent
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2178-2185	If a physical quantity is an annual electricity export of a geopolitical area holds during a time position and the time position is an instance of a kind of time interval and a kind of time interval is a subclass of year or the kind of time interval is a subclass of the fiscal year of the geopolitical area, then the geopolitical area is electricity export in period the physical quantity for the kind of time interval
No TPTP formula. May not be expressible in strict first order.	WMD.kif 401-404	If a kind of biological agent is equal to the biological agent of yersinia pestis, then a kind of biological agent is a subclass of life threatening agent
No TPTP formula. May not be expressible in strict first order.	Merge.kif 3320-3324	If a function is an instance of sequence function and the range of the function is an instance of a class, then the class is a subclass of integer
No TPTP formula. May not be expressible in strict first order.	Languages.kif 14705-14709	If a symbolic string in ISO-639-1 denotes a class, then the class is an instance of human language or the class is a subclass of human language
No TPTP formula. May not be expressible in strict first order.	Merge.kif 13552-13561	If an object is an instance of a kind of pure substance and a kind of pure substance is a subclass of pure substance and a real number inch mercury(s) is a barometric pressure of the object and 29.92 is greater than the real number and another real number kelvin degree(s) is a boiling point of the kind of pure substance and the measure of the object is a third real number kelvin degree(s) and the third real number is greater than the other real number, then gas is an attribute of the object
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3944-3947	If a kind of OrganismRemains is equal to a dead yam tuber, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3911-3914	If a kind of OrganismRemains is equal to a dead carrot, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 122-130	If an entity is an instance of organic object and a process is an instance of death and an agent experiences the process and the agent is an instance of the agentTYPE and the agent is a subclass of organism and the entity is a result of the process, then the entity is an instance of a dead the agentTYPE
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4030-4033	If a kind of OrganismRemains is equal to a dead citrus fruit, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 310-325	If a kind of physical is an amenity in a kind of hotel unit and a kind of hotel unit is a part of an object and a kind of physical is a subclass of process, then the statement there exist an entity and another entity such that the entity is an instance of the kind of hotel unit and the object is an agent of the other entity and the other entity is an instance of the kind of physical or a third entity is an instance of the kind of physical and the other entity is a subprocess of the third entity and the other entity is located at the entity has the modal force of possibility
No TPTP formula. May not be expressible in strict first order.	Merge.kif 13574-13583	If an object is an instance of a kind of pure substance and a kind of pure substance is a subclass of pure substance and a real number kelvin degree(s) is a melting point of the kind of pure substance and another real number inch mercury(s) is a barometric pressure of the object and the other real number is greater than 29.92 and the measure of the object is a third real number kelvin degree(s) and the third real number is less than the real number, then solid is an attribute of the object
No TPTP formula. May not be expressible in strict first order.	Merge.kif 15125-15132	If a content bearing physical is an instance of a kind of content bearing object and a kind of content bearing object is a subclass of factual text and a cognitive agent is the author of the kind of content bearing object and the content bearing physical subsumes the content of a formula and the formula is an instance of formula, then the cognitive agent believes the formula
No TPTP formula. May not be expressible in strict first order.	Media.kif 1898-1902	If an entity publishes a class holds during a time position and the class is a subclass of book, then book publishers is an attribute of the entity holds during the time position
No TPTP formula. May not be expressible in strict first order.	Catalog.kif 349-365	If the price of a kind of entity from a cognitive agent according to a pricing scheme is a currency measure or the unit price charged the cognitive agent under the pricing scheme for a function quantity is a kind of entity and the kind of entity is a subclass of physical and another entity is an immediate instance of the kind of entity and the pricing scheme is valid for a kind of agent and a third entity is an instance of a kind of agent, then the statement if a fourth entity is an instance of buying and the third entity is an agent of the fourth entity and the fourth entity originates at the cognitive agent and the other entity is a patient of the fourth entity, then the currency measure is a transaction amount of the fourth entity has the modal force of likely
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 2294-2299	If a kind of transportation device is a subclass of water vehicle and a process is an instance of the transportation of a kind of transportation device and the process is located at 2, then an entity is an instance of water area
No TPTP formula. May not be expressible in strict first order.	WMD.kif 1306-1308	If a disease or syndrome is disease treatment topical antibiotic for a kind of process, then a kind of process is a subclass of covering
No TPTP formula. May not be expressible in strict first order.	Merge.kif 198-203	If a relation is a subrelation of another relation and the other relation is an instance of a class and the class is a subclass of inheritable relation, then the relation is an instance of the class
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 351-365	If use of a class is free for a kind of hotel unit and the class is a subclass of process and a temporary residence is an instance of a kind of hotel unit and a human stays at the temporary residence and the temporary residence is an element of belongings of an agent and the human is a patient of a process and the process is an instance of the class or another process is an instance of the class and the process is a subprocess of the other process and the process is located at the temporary residence, then the process is price 0.0 united states dollar(s) for the agent
No TPTP formula. May not be expressible in strict first order.	Government.kif 2321-2326	If a kind of content bearing object is a subclass of party platform and an agent is the author of a kind of content bearing object and the agent is an instance of organization, then the agent is an instance of political party
No TPTP formula. May not be expressible in strict first order.	Geography.kif 6619-6624	If a geopolitical area is an instance of all the instances of a kind of geographic area in another geopolitical area and a kind of geographic area is a subclass of geopolitical area and the other geopolitical area is an instance of geopolitical area, then the geopolitical area is a geopolitical part of the other geopolitical area
No TPTP formula. May not be expressible in strict first order.	Geography.kif 6609-6611	If a kind of geographic area is equal to all the instances of another kind of geographic area in a third geographic area, then a kind of geographic area is a subclass of another kind of geographic area
No TPTP formula. May not be expressible in strict first order.	Government.kif 617-623	If the day a positive integer is a commemorates date of a kind of holiday and an entity is an instance of a kind of holiday and the kind of holiday is a subclass of fixed holiday and an integer is less than or equal to another entity-YEAR, then the entity is an instance of the day the positive integer
No TPTP formula. May not be expressible in strict first order.	Food.kif 256-265	If an entity is an instance of a kind of organic object and a kind of organic object is a subclass of seafood, then there exist an organism and the entityEA such that the kind of organic object is the meat of a kind of animal and the organism is an instance of a kind of animal and the entityEA is an instance of body of water and the organism lives in the entityEA
No TPTP formula. May not be expressible in strict first order.	Merge.kif 96-102	If an entity is an immediate instance of a class, then there doesn't exist another class such that the other class is a subclass of the class and the other class is not equal to the class and the entity is an instance of the other class
No TPTP formula. May not be expressible in strict first order.	Merge.kif 5991-5993	If a graph is an instance of graph, then the set of minimal paths that partition the graph into two separate graphs is a subclass of the set of paths that partition the graph into two separate graphs
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3988-3991	If a kind of OrganismRemains is equal to a dead tomato, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4179-4182	If a kind of OrganismRemains is equal to a dead groundnut, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 12982-12993	If the minimum expected value of a kind of object is a real number an unit of measure(s) and a class is a subclass of NonCompositeUnitOfMeasure and the unit of measure is an instance of the class, then the statement there exist an entity, the real numberUANTITY and a third entity such that the entity is an instance of a kind of object and the measure of the entity is the real numberUANTITY the third entity(s) and the third entity is an instance of the class and the real numberUANTITY is less than the real number has the modal force of unlikely
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4086-4089	If a kind of OrganismRemains is equal to a dead date fruit, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2167-2176	If a geopolitical area is electricity export in period a physical quantity for a kind of time interval and a kind of time interval is a subclass of year or the kind of time interval is a subclass of the fiscal year of the geopolitical area, then there exists a time position such that the time position is an instance of the kind of time interval and the physical quantity is an annual electricity export of the geopolitical area holds during the time position
No TPTP formula. May not be expressible in strict first order.	Merge.kif 135-139	If a class is a subclass of another class, then the class is an instance of class and the other class is an instance of class
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4016-4019	If a kind of OrganismRemains is equal to a dead apple, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 29428-29458	If a process is an instance of BreakingRecord and an agent is an agent of the process, then there exist a class, another class,, , another process,, , a time point,, , a case role,, , a third class and an entity such that the class is an instance of set and the agent is an instance of the class and the other class is a subclass of process and the third class is a subclass of region and the time point is an instance of time point and the entity is an instance of quantity and the other process is an instance of the other class and the process includes a reference to the entity and the entity includes a reference to the other process and the agent plays role in event the case role for the other process and the other process is located at 2 and there don't exist another entity and a third entity such that the other entity is an instance of the class and the other entity is not equal to the agent and the third entity is an instance of the other class and the other entity plays role in event the case role for the third entity and the third entity is located at 2 holds during interval between the time point and the end of the time of existence of the process
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3937-3940	If a kind of OrganismRemains is equal to a dead taro tuber, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3866-3869	If a kind of OrganismRemains is equal to a dead cauliflower, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2213-2222	If a geopolitical area is electricity import in period a physical quantity for a kind of time interval and a kind of time interval is a subclass of year or the kind of time interval is a subclass of the fiscal year of the geopolitical area, then there exists a time position such that the time position is an instance of the kind of time interval and the physical quantity is an annual electricity import of the geopolitical area holds during the time position
No TPTP formula. May not be expressible in strict first order.	Merge.kif 141-145	If a class is a subclass of another class and an entity is an instance of the class, then the entity is an instance of the other class
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 2699-2708	If a kind of process is a subclass of process and another process is an instance of a kind of process and the other process is located at 2 and a case role is an instance of case role and an object is an instance of object and a region is an instance of geographic area and the case role the other process and the object, then the kind of process capable at location the case role for the object with the region
No TPTP formula. May not be expressible in strict first order.	WMD.kif 1372-1375	If a kind of biological agent is equal to the biological agent of coccidioides immitis, then a kind of biological agent is a subclass of life threatening agent
No TPTP formula. May not be expressible in strict first order.	Cars.kif 3448-3478	If a physical is an instance of hearing protection, then the physical has the purpose if an entity is an instance of human and the entity wears the physical, then there exist another entity and a third entity such that the other entity is an instance of process and the third entity is a subclass of the class described by a fourth entity and the other entity prevents the occurrence of the third entity and the physical is an instrument for the other entity
No TPTP formula. May not be expressible in strict first order.	Transportation.kif 2027-2032	If a transportation device is an instance of truck, then there exists a kind of object such that a kind of object is a subclass of object and the kind of object is a cargo type of the transportation device
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3930-3933	If a kind of OrganismRemains is equal to a dead sweet potato tuber, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 7204-7209	If an object is an instance of sports team, then there exists a kind of process such that a kind of process is a subclass of sport and the object is capable of doing the kind of process as a agent
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 22703-22710	If an object plays role in event a case role for a process and the process is an instance of another kind of process and another kind of process is a subclass of process and the process exists during a time position and the process is located at 2, then the object plays role in event of type the case role for the other kind of process with the time position and another object
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3852-3855	If a kind of OrganismRemains is equal to a dead cucumber, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	engineering.kif 824-829	If a corpuscular object is an instance of ElectricalConductor, then there exists a kind of substance such that a kind of substance is a subclass of conductor substance and the corpuscular object is made of the kind of substance
No TPTP formula. May not be expressible in strict first order.	Media.kif 1910-1914	If an entity publishes a class holds during a time position and the class is a subclass of newspaper, then newspaper publishers is an attribute of the entity holds during the time position
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4172-4175	If a kind of OrganismRemains is equal to a dead peanut, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Economy.kif 1678-1682	If a kind of intentional process is an organization service type of an organization and a kind of intentional process is a subclass of another kind of intentional process, then another kind of intentional process is an organization service type of the organization
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 29795-29798	If a kind of organism inhabits a geographic area, then a kind of organism is not a subclass of domestic animal
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 398-418	If renters of a kind of hotel unit can pay to use a class and the class is a subclass of process, then if a temporary residence is an instance of a kind of hotel unit and a human stays at the temporary residence and the temporary residence is an element of belongings of an agent and the human is a patient of a process and the process is an instance of the class or another process is an instance of the class and the process is a subprocess of the other process and the process is located at the temporary residence, then the process is price the processRICE an unit of measure(s) for the agent and the unit of measure is an instance of UnitOfCurrency and the processRICE is greater than 0
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4653-4656	If a kind of OrganismRemains is equal to a dead botanical tree, then a kind of OrganismRemains is a subclass of timber
No TPTP formula. May not be expressible in strict first order.	Merge.kif 349-355	If the values returned by a function are subclasses of a kind of class and the values returned by the function are subclasses of another kind of class, then a kind of class is a subclass of another kind of class or the other kind of class is a subclass of the kind of class
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 20373-20380	If medical doctor is an attribute of an object, then there exist a kind of process and another kind of process such that a kind of process is a subclass of diagnostic process and another kind of process is a subclass of therapeutic process and the object is capable of doing the kind of process as a agent and the object is capable of doing the other kind of process as a agent
No TPTP formula. May not be expressible in strict first order.	Merge.kif 322-328	If the range of a function is an instance of a class and the range of the function is an instance of another class, then the class is a subclass of the other class or the other class is a subclass of the class
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4157-4160	If a kind of OrganismRemains is equal to a dead edible nut, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Cars.kif 3485-3511	If a physical is an instance of protective eyewear, then the physical has the purpose if the physicalRSON is an instance of human and the physicalRSON wears the physical, then there exist another entity, a third entity and a fourth entity such that the other entity is an instance of process and the physical is an instrument for the other entity and the fourth entity is a subclass of the class described by a fifth entity and the other entity prevents the occurrence of the fourth entity
No TPTP formula. May not be expressible in strict first order.	CountriesAndRegions.kif 871-878	If an unit of measure is a subclass of area measure and the measure of alaska is a real number the unit of measure(s) and the measure of a physical is another real number the unit of measure(s) and the physical is an instance of american state and alaska is not equal to the physical, then the other real number is less than the real number
No TPTP formula. May not be expressible in strict first order.	Merge.kif 15156-15165	If a content bearing physical is an instance of a kind of content bearing object and a kind of content bearing object is a subclass of fictional text and a cognitive agent is the author of the kind of content bearing object, then there exists a formula such that the content bearing physical subsumes the content of the formula and the formula is an instance of formula and the cognitive agent doesn't believe the formula
No TPTP formula. May not be expressible in strict first order.	Media.kif 3191-3193	If a symbolic string is the title in a language for instances of a class, then the class is a subclass of collection
No TPTP formula. May not be expressible in strict first order.	Cars.kif 3389-3418	If a physical is an instance of safety harness, then the physical has the purpose if an entity is an instance of animal and the entity wears the physical, then there exist another entity and a third entity such that the other entity is an instance of process and the physical is an instrument for the other entity and the entity is a patient of the other entity and the third entity is a subclass of the class described by a fourth entity and the other entity prevents the occurrence of the third entity
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 14253-14262	If a class is a subclass of newspaper and a time position is an instance of week, then there exist a process and an entity such that the process is an instance of publication and the time of existence of the process is a part of the time position and the entity is a result of the process and the entity is an instance of the class
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4009-4012	If a kind of OrganismRemains is equal to a dead berry, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4117-4120	If a kind of OrganismRemains is equal to a dead passion fruit, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 17772-17776
No TPTP formula. May not be expressible in strict first order.	Media.kif 1904-1908	If an entity publishes a class holds during a time position and the class is a subclass of periodical, then periodical publishers is an attribute of the entity holds during the time position
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 12079-12085	If an object is an instance of caterpillar, then larval is an attribute of the object and the object is a subclass of moth or a class is a subclass of Butterfly
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 334-349	If use of a class is free for a kind of hotel unit and the class is a subclass of object and a temporary residence is an instance of a kind of hotel unit and a human stays at the temporary residence and the temporary residence is an element of belongings of an agent and an object is an instance of the class and the object is located at the temporary residence and a process is an instance of process and the human is an agent of the process and the object is a patient of the process or the object is an instrument for the process or the object is a resource for the process, then the process is price 0 united states dollar(s) for the agent
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1183-1191	If a corpuscular object is an instance of corpuscular object, then there exist a kind of substance and another kind of substance such that a kind of substance is a subclass of substance and another kind of substance is a subclass of substance and the corpuscular object is made of the kind of substance and the corpuscular object is made of the other kind of substance and the kind of substance is not equal to the other kind of substance
No TPTP formula. May not be expressible in strict first order.	Catalog.kif 51-62	If an agent offers items for sale in a catalog and a kind of entity is in the catalog and a kind of entity is a subclass of physical, then the statement there exist another entity and a third entity such that the third entity is an instance of the kind of entity and the other entity is an instance of selling and the agent is an agent of the other entity and the third entity is a patient of the other entity has the modal force of possibility
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4124-4127	If a kind of OrganismRemains is equal to a dead pineapple, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3977-3980	If a kind of OrganismRemains is equal to a dead sugar cane, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 9239-9244	If a kind of medicine is a subclass of antibiotic, then there exists a disease or syndrome such that the disease or syndrome is an instance of bacterial disease and a kind of medicine is medicine for the disease or syndrome
No TPTP formula. May not be expressible in strict first order.	Hotel.kif 484-500	If a cognitive agent is a customer of another cognitive agent and the cognitive agent has a kind of physical and a kind of physical is a subclass of object and an entity is an instance of the kind of physical, then the cognitive agent allows the other cognitive agent to perform task of the type there exists another entity such that the other entity is an instance of process and the entity is a resource for the other entity or the entity is an instrument for the other entity or the entity is a patient of the other entity and the other cognitive agent is an agent of the other entity or the other cognitive agent experiences the other entity
No TPTP formula. May not be expressible in strict first order.	Merge.kif 811-813	If a class is an instance of class, then the class is a subclass of entity
No TPTP formula. May not be expressible in strict first order.	Merge.kif 2933-2938	If the number a positive integer argument of a relation is a subclass of a class and the relation is an instance of predicate and the relation @ROW, then the positive integerth element of (@ROW) is a subclass of the class
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4023-4026	If a kind of OrganismRemains is equal to a dead olive, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	Merge.kif 13563-13572	If an object is an instance of a kind of pure substance and a kind of pure substance is a subclass of pure substance and a real number kelvin degree(s) is a boiling point of the kind of pure substance and another real number kelvin degree(s) is a melting point of the kind of pure substance and the measure of the object is a third real number kelvin degree(s) and the third real number is greater than the other real number and the third real number is less than the real number, then liquid is an attribute of the object
No TPTP formula. May not be expressible in strict first order.	Economy.kif 2002-2009	If a physical quantity is an annual electricity production of a geopolitical area holds during a time position and the time position is an instance of a kind of time interval and a kind of time interval is a subclass of year or the kind of time interval is a subclass of the fiscal year of the geopolitical area, then the geopolitical area is electricity production in period the physical quantity for the kind of time interval
No TPTP formula. May not be expressible in strict first order.	Catalog.kif 129-134	If an agent offers items for sale in a catalog during a kind of time interval and a kind of entity is in the catalog and a kind of entity is a subclass of process, then the agent is capable of being a agent in the kind of entity during a kind of time interval
No TPTP formula. May not be expressible in strict first order.	WMD.kif 1362-1365	If a kind of biological agent is equal to the biological agent of serratia marcenscens, then a kind of biological agent is a subclass of life threatening agent
No TPTP formula. May not be expressible in strict first order.	Mid-level-ontology.kif 30774-30781	If an object can be an argument to a relation and the object is an instance of the objectC and the number 1 argument of the relation is an instance of another class, then the objectC is equal to the other class or the objectC is a subclass of the other class
No TPTP formula. May not be expressible in strict first order.	Geography.kif 990-994	If a geopolitical area is an instance of landlocked area and a kind of maritime claim area is a subclass of maritime claim area, then a kind of maritime claim area is not a maritime claim type of the geopolitical area
No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 88-90	If a class is a subclass of IOS, then Apple created the class
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3904-3907	If a kind of OrganismRemains is equal to a dead turnip, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	MilitaryDevices.kif 48-56	If an object is capable of doing a kind of process as a a case role and a kind of process is a subclass of shooting, then there exists another object such that the other object is an instance of weapon and the other object is a part of the object and the other object is capable of doing the kind of process as a the case role
No TPTP formula. May not be expressible in strict first order.	Dining.kif 225-229	If a catalog is an instance of wine list and a kind of entity is in the catalog, then a kind of entity is a subclass of wine list
No TPTP formula. May not be expressible in strict first order.	Economy.kif 3859-3862	If a kind of OrganismRemains is equal to a dead cabbage, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	WMD.kif 2009-2012	If a kind of biological agent is equal to the biological agent of tick borne encephalitis virus, then a kind of biological agent is a subclass of life threatening agent
No TPTP formula. May not be expressible in strict first order.	Geography.kif 996-1003	If a kind of maritime claim area is a maritime claim type of a geopolitical area and a kind of maritime claim area is a subclass of maritime claim area, then there exists a geographic area such that the geographic area is an instance of the kind of maritime claim area and the geopolitical area is a claimed territory of the geographic area
No TPTP formula. May not be expressible in strict first order.	Geography.kif 2274-2281	If a kind of physical is a natural hazard type in area of a geographic area and a kind of physical is a subclass of object, then there exists another physical such that the other physical is an instance of the kind of physical and the other physical is located at the geographic area
No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 29-31	If a class is a subclass of Android, then Alphabet created the class
No TPTP formula. May not be expressible in strict first order.	Economy.kif 4058-4061	If a kind of OrganismRemains is equal to a dead avocado, then a kind of OrganismRemains is a subclass of grocery produce
No TPTP formula. May not be expressible in strict first order.	ComputingBrands.kif 59-61	If a class is a subclass of WindowsOS, then Microsoft created the class
No TPTP formula. May not be expressible in strict first order.	Cars.kif 5112-5115	There exists an agent such that the agent is a subclass of tool box and the maker of Sortimo Corporation is the agent

Sigma web home Suggested Upper Merged Ontology (SUMO) web home
Sigma version 3.0 is open source software produced by Articulate Software and its partners