subclass |
appearance as argument number 1 |
![]() |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1371-1373 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 133-135 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 27-29 | |
No TPTP formula. May not be expressible in strict first order. | spanish_format.kif 28-30 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 131-131 | 域 子類, 1 and Class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 132-132 | 域 子類, 2 and Class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 129-129 | 例 子類 and BinaryPredicate |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 18660-18660 | 例 子類 and ClosedWorldPredicate |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 130-130 | 例 子類 and PartialOrderingRelation |
appearance as argument number 2 |
![]() |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 319-319 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 324-324 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 182-182 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 271-271 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2002-2002 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 134-134 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 175-175 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 419-419 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 308-308 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 202-202 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 192-192 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 463-463 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 22956-22956 | 子關係 子領域 and 子類 |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55708-55708 | 子關係 子領域 and 子類 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 320-320 | 子關係 子領域 and 子類 |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55707-55707 | 子關係 子領域 and 子類 |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55706-55706 | 子關係 子領域 and 子類 |
No TPTP formula. May not be expressible in strict first order. | terms-de.txt 133-133 | 子關係 子領域 and 子類 |
antecedent |
![]() |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 3987-4007 |
|
No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1194-1209 |
|
No TPTP formula. May not be expressible in strict first order. | Biography.kif 738-748 |
|
No TPTP formula. May not be expressible in strict first order. | WMD.kif 789-793 |
|
No TPTP formula. May not be expressible in strict first order. | WMD.kif 976-980 | |
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. | Government.kif 583-589 | |
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. | Hotel.kif 522-538 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14886-14897 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14855-14866 |
|
No TPTP formula. May not be expressible in strict first order. | WMD.kif 957-961 |
|
No TPTP formula. May not be expressible in strict first order. | WMD.kif 963-967 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2352-2361 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2396-2405 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2442-2451 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2220-2229 |
|
No TPTP formula. May not be expressible in strict first order. | Food.kif 2883-2889 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 4967-4972 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 5031-5037 | |
No TPTP formula. May not be expressible in strict first order. | Media.kif 195-200 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 19972-19977 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 5285-5290 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 4503-4509 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 4870-4881 | |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
consequent |
![]() |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 33332-33339 | |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 4203-4227 |
|
No TPTP formula. May not be expressible in strict first order. | Hotel.kif 1489-1502 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25883-25893 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 215-221 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3018-3023 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 238-244 | |
No TPTP formula. May not be expressible in strict first order. | Media.kif 195-200 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 5285-5290 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 4870-4881 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 5599-5606 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 5373-5377 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 5576-5585 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1790-1798 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 4177-4182 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 4300-4305 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 4330-4335 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 12164-12176 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 4241-4246 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 4271-4276 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 4209-4214 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 4285-4290 | |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 5827-5835 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 19655-19663 | |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 3508-3537 |
|
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
statement |
![]() |
No TPTP formula. May not be expressible in strict first order. | Military.kif 963-974 | equal GeopoliticalArea 的 fit 對於軍服務男性 and 基數 卡帕 SymbolicString and 例 SymbolicString and Human attribute SymbolicString and 男 子類 entity and MilitaryProcess entity 是 SymbolicString 的 fit 軍事服務 entity 是 GeopoliticalArea 的 military 年紀 年齡 SymbolicString and entity 大於或等於 entity and entity 棲息 SymbolicString and GeopoliticalArea |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 5170-5173 | Object 子類 Object and HandToolBox manufacturer Object and SortimoCorp |
appearance as argument number 0 |
![]() |
No TPTP formula. May not be expressible in strict first order. | Muscles.kif 778-778 | 子類 ABranchOfDorsalPrimaryDivisionOfSuboccipitalNerve and Nerve |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 28254-28254 | 子類 ACPowerSource and 能量源 |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 3294-3294 | 子類 ADHD and PsychologicalDysfunction |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 27208-27208 | 子類 AMFMAlarmClock and AlarmClock |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 27209-27209 | 子類 AMFMAlarmClock and 無線電接收器 |
No TPTP formula. May not be expressible in strict first order. | Communications.kif 293-293 | 子類 AM廣播電台 and 廣播電台 |
No TPTP formula. May not be expressible in strict first order. | Communications.kif 236-236 | 子類 AM無線電系統 and 無線電系統 |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 4075-4075 | 子類 AOCnumber and SymbolicString |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3601-3601 | 子類 自動提款機 and StationaryArtifact |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3677-3677 | 子類 ATM插槽 and HoleRegion |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 4876-4876 | 子類 ATVTire and Tire |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2169-2169 | 子類 影/音控制傳輸協議 and ComputerProgram |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 6430-6430 | 子類 AVPUStatus and RelationalAttribute |
No TPTP formula. May not be expressible in strict first order. | Food.kif 1994-1994 | 子類 AbaloneMeat and MolluskMeat |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 4952-4952 | 子類 Abatacept and Immunosupressant |
No TPTP formula. May not be expressible in strict first order. | ArabicCulture.kif 527-527 | 子類 阿巴亞 and 披風 |
No TPTP formula. May not be expressible in strict first order. | People.kif 1213-1213 | 子類 僧院 and ReligiousOrganization |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14148-14148 | 子類 Abdomen and 動物解剖結構 |
No TPTP formula. May not be expressible in strict first order. | arteries.kif 1272-1272 | 子類 AbdominalAorta and 動脈 |
No TPTP formula. May not be expressible in strict first order. | Muscles.kif 135-135 | 子類 AbducensNerveCNVI and Nerve |
No TPTP formula. May not be expressible in strict first order. | Anatomy.kif 2046-2046 | 子類 Abducting and BodyMotion |
No TPTP formula. May not be expressible in strict first order. | Anatomy.kif 2047-2047 | 子類 Abducting and MovingAwayFrom |
No TPTP formula. May not be expressible in strict first order. | Muscles.kif 1608-1608 | 子類 AbductorDigitiMinimiMuscle and Muscle |
No TPTP formula. May not be expressible in strict first order. | Muscles.kif 2127-2127 | 子類 AbductorHallucisMuscle and Muscle |
No TPTP formula. May not be expressible in strict first order. | Muscles.kif 1581-1581 | 子類 AbductorPollicisBrevisMuscle and Muscle |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
![]() |
![]() |