instance |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1359-1361 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 84-87 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 17-20 | |
No TPTP formula. May not be expressible in strict first order. | spanish_format.kif 17-20 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 81-81 | 域 例, 1 and Entity |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 82-82 | 域 例, 2 and Class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 80-80 | 例 例 and BinaryPredicate |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 305-305 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 310-310 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 175-175 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 149-149 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1995-1995 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 127-127 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 173-173 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 400-400 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 188-188 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 195-195 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 184-184 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 302-302 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1281-1281 | 相關的內部概念 會員 and 例 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5413-5413 | 子關係 元件 and 例 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 89-89 | 子關係 立即實例 and 例 |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 30247-30247 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 306-306 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 30246-30246 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 30245-30245 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 303-303 |
antecedent |
consequent |
statement |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3193-3193 | 例 ?D and 天 23 and 月 June and 年 1961 是 南極條約 的 agreement 生效日期 |
No TPTP formula. May not be expressible in strict first order. | People.kif 456-469 | 例 年 and 年 Integer 等於 GeopoliticalArea 和 年 每個女人生的 children and 基數 卡帕 SymbolicString and 例 entity and Birth 體驗者 entity and SymbolicString agent entity and entity 例 entity and Human attribute entity and 女 持有期間 年 and 棲息 entity and GeopoliticalArea |
No TPTP formula. May not be expressible in strict first order. | Government.kif 1241-1248 | 包含信息 ?AGENT ?VOTER, ?ELECTION and ?VOTING
|
No TPTP formula. May not be expressible in strict first order. | Government.kif 923-931 | 包含信息 ?COUNTRY ?ELECTION, ?VOTING and ?VOTER
|
No TPTP formula. May not be expressible in strict first order. | Government.kif 1092-1103 | 包含信息 ?POLITY ?AGENT, ?ELECTION, ?VOTINGAGE and ?AGE
|
No TPTP formula. May not be expressible in strict first order. | Government.kif 1160-1174 | 包含信息 ?POLITY ?VOTER, ?ELECTION, ?VOTINGAGE and ?AGE
|
No TPTP formula. May not be expressible in strict first order. | WMD.kif 921-929 | 降低可能性 ?SYMPTOM 是 ?AGENT 的 biochemical 病毒徵兆 ?AGENT biochemical 病毒解毒製劑 ?SUBSTANCE 對於 ?PROCESS 例 ?SAMPLE and ?SUBSTANCE 例 ?THERAPY and ?PROCESS 體驗者 ?THERAPY and ?ORGANISM 患者 ?THERAPY and ?SAMPLE and attribute ?ORGANISM and ?SYMPTOM |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 18202-18219 | 降低可能性 ?X ?CUT, ?PAPER, ?CBO and ?INFO 例 ?X and PaperShredder 例 ?CUT and Cutting 儀器 ?CUT and ?X 例 ?PAPER and 紙 患者 ?CUT and ?PAPER 位於 ?CBO and ?PAPER 例 ?CBO and VisualContentBearingObject 包含信息 ?CBO and ?INFO and ?READ 例 ?READ and 解讀 患者 ?READ and ?INFO 早期 何時 ?CUT and 何時 ?READ |
No TPTP formula. May not be expressible in strict first order. | Military.kif 872-881 | 等於 GeopoliticalArea 的 available 軍事服務男性 and 基數 卡帕 SymbolicString and 例 SymbolicString and Human attribute SymbolicString and 男 entity 是 GeopoliticalArea 的 military 年紀 年齡 SymbolicString and entity 大於或等於 entity and entity 棲息 SymbolicString and GeopoliticalArea |
No TPTP formula. May not be expressible in strict first order. | Military.kif 895-906 | 等於 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. | Mid-level-ontology.kif 31734-31739 | 等於 OrganismPopulationFn Organism and GeographicArea and 基數 卡帕 OrganismI and 例 OrganismI and Organism 位於 OrganismI and GeographicArea |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31712-31717 | 等於 GeopoliticalArea 的 population and 基數 卡帕 SymbolicString and 例 SymbolicString and Human 棲息 SymbolicString and GeopoliticalArea |
No TPTP formula. May not be expressible in strict first order. | Military.kif 933-946 | 等於 GeopoliticalArea 和 年 每年的 reaching 軍事男性年齡 and 基數 卡帕 SymbolicString and 例 SymbolicString and Human attribute SymbolicString and 男 entity 是 GeopoliticalArea 的 military 年紀 等於 entity and 減法 entity and 1 持有期間 年 and 年齡 SymbolicString and entity 年齡 SymbolicString and entity 等於 entity and entity 棲息 SymbolicString and GeopoliticalArea |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 4559-4564 | Process Entity 例 Process and Disseminating agent Process and Netflix 患者 Process and Entity 例 Entity and MotionPicture |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 4566-4569 | Process 例 Process and 電影製作 agent Process and Netflix |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2453-2457 | TimePosition 例 TimePosition and 年 1976 持有期間 TimePosition and 斯蒂夫·沃茲尼亞克 是 史蒂芬·賈伯斯 的 coworker |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2441-2445 | TimePosition 例 TimePosition and 年 2002 持有期間 TimePosition and 提姆·庫克 是 史蒂芬·賈伯斯 的 coworker |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 825-826 | Entity 例 Entity and Entity |
No TPTP formula. May not be expressible in strict first order. | Media.kif 1970-1978 | TimeInterval 例 TimeInterval and TimeInterval 飾面 TimeInterval and 何時 JesusOfNazareth 啟動 TimeInterval and 何時 TwelveApostles entity
|
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 3309-3315 | 有目的 iBookstore and ?D 例 ?D and 下載 儀器 ?D and iBookstore 例 ?T and Text objectTransferred ?D and ?T |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2501-2504 | 持有期間 未來 TimePosition and 例 Serbia and 歐洲國家 例 TimePosition and 天 5 and 月 June and 年 2006 |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2496-2499 | 持有期間 未來 TimePosition and 例 Serbia and 獨立國家 例 TimePosition and 天 5 and 月 June and 年 2006 |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2506-2509 | 持有期間 未來 TimePosition and 名 "Republic of Serbia" and Serbia 例 TimePosition and 天 5 and 月 June and 年 2006 |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2528-2531 | 持有期間 未來 TimePosition and 例 TimePosition and 天 3 and 月 June and 年 2006 例 Montenegro and 歐洲國家 |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2523-2526 | 持有期間 未來 TimePosition and 例 TimePosition and 天 3 and 月 June and 年 2006 例 Montenegro and 獨立國家 |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
appearance as argument number 0 |
No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 1176-1176 | 例 Cell 和 細胞部分 的 cell 部分 and 細胞部分 |
No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 1165-1165 | 例 Virus 和 病毒部分 的 viral 部分 and 病毒部分 |
No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 2520-2520 | 例 AAA評級 and 財務評級 |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3220-3220 | 例 ABPFn and UnaryFunction |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 4417-4417 | 例 ABTest and ExperimentAttribute |
No TPTP formula. May not be expressible in strict first order. | Languages.kif 5379-5379 | 例 一種 pucikwar 語言 and 中央偉大的andamanese語言 |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2874-2874 | 例 東盟區域論壇 and 國際組織 |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3265-3265 | 例 ASPFn and UnaryFunction |
No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 2122-2122 | 例 ATandTCorp and Corporation |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 6421-6421 | 例 AVPUAlertStatus and AVPUStatus |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 6461-6461 | 例 AVPUPainStatus and AVPUStatus |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 6484-6484 | 例 AVPUUnresponsiveStatus and AVPUStatus |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 6439-6439 | 例 AVPUVerbalStatus and AVPUStatus |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2560-2560 | 例 AalandIslands and 群島 |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2561-2561 | 例 AalandIslands and 依賴或特殊主權領域 |
No TPTP formula. May not be expressible in strict first order. | Languages.kif 3771-3771 | 例 aariya語言 and 非語言口語 |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 2966-2966 | 例 AbbVie and Corporation |
No TPTP formula. May not be expressible in strict first order. | People.kif 1209-1209 | 例 方丈 and 宗教立場 |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 3851-3851 | 例 AbbottLaboratories and Corporation |
No TPTP formula. May not be expressible in strict first order. | Languages.kif 2923-2923 | 例 abinomn語言 and 口語人類語言 |
No TPTP formula. May not be expressible in strict first order. | Languages.kif 3777-3777 | 例 abishira語言 and 非語言口語 |
No TPTP formula. May not be expressible in strict first order. | Languages.kif 14550-14550 | 例 AbkhazLanguage and 北方白種人語言 |
No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2410-2410 | 例 中止 and BinaryFunction |
No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2476-2476 | 例 中止發射 and BinaryFunction |
No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2430-2430 | 例 任務中止 and BinaryFunction |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |