No TPTP formula. May not be expressible in strict first order. |
Economy.kif 3840-3845 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 30030-30060 |
- If a process is an instance of breaking record and an agent is an agent of the process,
- then there exist a set, a class,, , another process,, , a time point,, , a case role,, , an object and an entity such that the set is an instance of set and the agent is an element of the set and the class is a subclass of process and the object is an instance 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 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 the object and there don't exist another entity and a third entity such that the other entity is an instance of the set and the other entity is not equal to the agent and the third entity is an instance of the class and the other entity plays role in event the case role for the third entity and the third entity is located at the object 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. |
Mid-level-ontology.kif 129-137 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 1053-1058 |
|
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 2288-2295 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 15400-15407 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 13516-13527 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 16905-16909 |
|
No TPTP formula. May not be expressible in strict first order. |
Cars.kif 3447-3476 |
|
No TPTP formula. May not be expressible in strict first order. |
MilitaryProcesses.kif 2032-2042 |
|
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 3904-3909 |
|
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 1263-1267 |
|
No TPTP formula. May not be expressible in strict first order. |
Catalog.kif 98-107 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 6087-6089 |
|
No TPTP formula. May not be expressible in strict first order. |
Medicine.kif 4025-4038 |
|
No TPTP formula. May not be expressible in strict first order. |
ComputingBrands.kif 30-34 |
|
No TPTP formula. May not be expressible in strict first order. |
engineering.kif 826-831 |
|
No TPTP formula. May not be expressible in strict first order. |
Hotel.kif 364-378 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 31387-31394 |
|
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 3934-3939 |
|
No TPTP formula. May not be expressible in strict first order. |
ComputingBrands.kif 93-97 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 29730-29739 |
|
No TPTP formula. May not be expressible in strict first order. |
Transportation.kif 2692-2701 |
|
No TPTP formula. May not be expressible in strict first order. |
Transportation.kif 2019-2024 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 1231-1239 |
|
No TPTP formula. May not be expressible in strict first order. |
Transportation.kif 2617-2622 |
|
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 983-987 |
|
No TPTP formula. May not be expressible in strict first order. |
UXExperimentalTerms.kif 2630-2643 |
|
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 2112-2121 |
|
No TPTP formula. May not be expressible in strict first order. |
MilitaryProcesses.kif 940-949 |
|
No TPTP formula. May not be expressible in strict first order. |
Hotel.kif 294-313 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16379-16384 |
|
No TPTP formula. May not be expressible in strict first order. |
Government.kif 2331-2338 |
|
No TPTP formula. May not be expressible in strict first order. |
Transportation.kif 1572-1580 |
|
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 6201-6209 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 7528-7533 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 15431-15440 |
|
No TPTP formula. May not be expressible in strict first order. |
WMD.kif 2029-2034 |
|
No TPTP formula. May not be expressible in strict first order. |
Dining.kif 189-201 |
|
No TPTP formula. May not be expressible in strict first order. |
Food.kif 3377-3383 |
|
No TPTP formula. May not be expressible in strict first order. |
VirusProteinAndCellPart.kif 600-608 |
|
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 6393-6404 |
|
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 5267-5276 |
|
No TPTP formula. May not be expressible in strict first order. |
MilitaryProcesses.kif 2174-2184 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 18421-18442 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 9671-9676 |
|
No TPTP formula. May not be expressible in strict first order. |
Hotel.kif 281-292 |
|
No TPTP formula. May not be expressible in strict first order. |
Catalog.kif 337-352 |
|
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 4732-4740 |
|
No TPTP formula. May not be expressible in strict first order. |
Government.kif 2324-2329 |
|
No TPTP formula. May not be expressible in strict first order. |
Government.kif 1692-1698 |
|
No TPTP formula. May not be expressible in strict first order. |
Cars.kif 3389-3417 |
|
No TPTP formula. May not be expressible in strict first order. |
Cars.kif 3531-3552 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14624-14638 |
|
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 998-1003 |
|
No TPTP formula. May not be expressible in strict first order. |
Hotel.kif 1186-1201 |
|
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 2583-2592 |
|
No TPTP formula. May not be expressible in strict first order. |
Catalog.kif 354-370 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 137-141 |
|
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 6425-6434 |
|
No TPTP formula. May not be expressible in strict first order. |
ComputingBrands.kif 62-66 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 828-830 |
|
No TPTP formula. May not be expressible in strict first order. |
Dining.kif 208-212 |
|
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 2277-2286 |
|
No TPTP formula. May not be expressible in strict first order. |
Dining.kif 1044-1059 |
|
No TPTP formula. May not be expressible in strict first order. |
Cars.kif 1688-1693 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13798-13807 |
|
No TPTP formula. May not be expressible in strict first order. |
Transportation.kif 2287-2292 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 200-205 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 98-104 |
|
No TPTP formula. May not be expressible in strict first order. |
WMD.kif 1322-1326 |
|
No TPTP formula. May not be expressible in strict first order. |
Medicine.kif 4481-4492 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14789-14798 |
|
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 6191-6199 |
|
No TPTP formula. May not be expressible in strict first order. |
Cars.kif 3482-3509 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 8243-8257 |
|
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 1980-1989 |
|
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 3993-3998 |
|
No TPTP formula. May not be expressible in strict first order. |
UXExperimentalTerms.kif 4467-4480 |
|
No TPTP formula. May not be expressible in strict first order. |
Medicine.kif 698-715 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 21089-21101 |
|
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 4365-4372 |
|
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 989-996 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3910-3916 |
|
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 3963-3968 |
|
No TPTP formula. May not be expressible in strict first order. |
Transportation.kif 2610-2615 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13820-13829 |
|
No TPTP formula. May not be expressible in strict first order. |
Government.kif 619-625 |
|
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 2202-2211 |
|
No TPTP formula. May not be expressible in strict first order. |
Hotel.kif 504-520 |
|
No TPTP formula. May not be expressible in strict first order. |
Biography.kif 730-740 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 1780-1788 |
|
No TPTP formula. May not be expressible in strict first order. |
Dining.kif 219-223 |
|
No TPTP formula. May not be expressible in strict first order. |
Medicine.kif 3984-4004 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 15166-15187 |
|
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 3948-3953 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3005-3010 |
|
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 2280-2290 |
|
No TPTP formula. May not be expressible in strict first order. |
Hotel.kif 396-417 |
|
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 2213-2220 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 16981-16986 |
|
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 3738-3742 |
|
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 6931-6936 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14606-14613 |
|
No TPTP formula. May not be expressible in strict first order. |
Sports.kif 1040-1047 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13809-13818 |
|
No TPTP formula. May not be expressible in strict first order. |
Dining.kif 229-233 |
|
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 2123-2130 |
|
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 2594-2601 |
|
No TPTP formula. May not be expressible in strict first order. |
Dining.kif 178-182 |
|
No TPTP formula. May not be expressible in strict first order. |
MilitaryDevices.kif 35-43 |
|
No TPTP formula. May not be expressible in strict first order. |
Hotel.kif 811-832 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3392-3396 |
|
No TPTP formula. May not be expressible in strict first order. |
UXExperimentalTerms.kif 1496-1518 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 24195-24206 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 8293-8302 |
|
No TPTP formula. May not be expressible in strict first order. |
Hotel.kif 419-438 |
|
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 1991-1998 |
|
No TPTP formula. May not be expressible in strict first order. |
MilitaryDevices.kif 48-56 |
|
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 2271-2278 |
|
No TPTP formula. May not be expressible in strict first order. |
Catalog.kif 372-387 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 24236-24246 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 7351-7365 |
|
No TPTP formula. May not be expressible in strict first order. |
MilitaryProcesses.kif 2193-2203 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 15016-15024 |
|
No TPTP formula. May not be expressible in strict first order. |
Food.kif 1909-1915 |
|
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 3872-3877 |
|
No TPTP formula. May not be expressible in strict first order. |
Food.kif 299-306 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 13547-13558 |
|
No TPTP formula. May not be expressible in strict first order. |
engineering.kif 855-860 |
|
No TPTP formula. May not be expressible in strict first order. |
Catalog.kif 139-150 |
|
No TPTP formula. May not be expressible in strict first order. |
Hotel.kif 317-332 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 18084-18092 |
|
No TPTP formula. May not be expressible in strict first order. |
Hotel.kif 1478-1491 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 21066-21080 |
|
No TPTP formula. May not be expressible in strict first order. |
Catalog.kif 64-76 |
|
No TPTP formula. May not be expressible in strict first order. |
Catalog.kif 51-62 |
|
No TPTP formula. May not be expressible in strict first order. |
Hotel.kif 346-361 |
|
No TPTP formula. May not be expressible in strict first order. |
Transportation.kif 1683-1688 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 3600-3605 |
|
No TPTP formula. May not be expressible in strict first order. |
Languages.kif 14705-14709 |
|
No TPTP formula. May not be expressible in strict first order. |
Hotel.kif 522-538 |
|
No TPTP formula. May not be expressible in strict first order. |
Cars.kif 1772-1786 |
|
No TPTP formula. May not be expressible in strict first order. |
Catalog.kif 130-137 |
|
No TPTP formula. May not be expressible in strict first order. |
Food.kif 1928-1937 |
|
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 2167-2174 |
|
No TPTP formula. May not be expressible in strict first order. |
Medicine.kif 4614-4619 |
|
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 2156-2165 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 143-147 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 12014-12026 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 23260-23267 |
|
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 5485-5493 |
|
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 9561-9574 |
|
No TPTP formula. May not be expressible in strict first order. |
Military.kif 895-906 |
The fit for military service male of a geopolitical area is equal to the number of instances in the class described by a symbolic string |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 129-129 |
subclass is an instance of binary predicate |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 130-130 |
subclass is an instance of partial ordering relation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 18472-18472 |
subclass is an instance of ClosedWorldPredicate |