equal |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1391-1392 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 48-49 | |
No TPTP formula. May not be expressible in strict first order. | spanish_format.kif 53-54 |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 297-297 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 302-302 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 171-171 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 96-96 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1991-1991 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 123-123 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 179-179 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 387-387 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 136-136 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 191-191 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 178-178 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 205-205 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 298-298 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 22317-22317 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 22316-22316 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 206-206 |
antecedent |
consequent |
statement |
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. | 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. | Mid-level-ontology.kif 13333-13336 | RealNumber 等於 測量 RealNumber and OunceMass and 測量 部 RealNumber and 16.0 and 磅質量 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4736-4737 | Integer 等於 前任 Integer and 減法 Integer and 1 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4720-4721 | Integer 等於 接班人 Integer and 加成 Integer and 1 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3037-3040 | @ROW Entity 等於 列表長度 名單 @ROW and entity and 接班人 列表長度 名單 @ROW |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3042-3046 | @ROW Entity 等於 清單順序 名單 @ROW and Entity and 列表長度 名單 @ROW and Entity and Entity |
No TPTP formula. May not be expressible in strict first order. | Government.kif 2915-2915 | 等於 大六 and 6人小組 |
appearance as argument number 0 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5265-5265 | 等於 ArcCosineFn 餘弦 RealNumber and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5275-5275 | 等於 ArcSineFn 正弦 RealNumber and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5255-5255 | 等於 ArcTangentFn 切線 RealNumber and RealNumber |
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. | Merge.kif 14182-14182 | 等於 基數 Continent and 7 |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2003-2003 | 等於 基數 NativityMagi and 3 |
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. | Economy.kif 2008-2008 | 等於 測量 1 and 千瓦時 and 測量 3.6 and 兆 焦耳 |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 2009-2009 | 等於 測量 1 and 千瓦時 and 測量 3600000.0 and 焦耳 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7112-7114 | 等於 測量 1 and 週持續時間 and 測量 7 and 一天長度 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7139-7141 | 等於 測量 1 and 年持續時間 and 測量 365 and 一天長度 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 382-382 | 等於 測量 1.0 and 圓周角度 and 測量 60.0 and 弧分 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 401-401 | 等於 測量 1.0 and 弧分 and 測量 60.0 and 弧秒 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3842-3842 | 等於 測量 1.0 and 推測 and 測量 6.0 and 腳長 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13601-13603 | 等於 測量 1.0 and 公噸 and 測量 2205.0 and 磅質量 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3865-3867 | 等於 測量 1.0 and 海裡 and 測量 1852.0 and 儀表 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 3861-3863 | 等於 測量 1.0 and 海裡 and 測量 6076.1 and 腳長 |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13696-13700 | 等於 測量 1.0 and 平方英里 and 測量 1.0 and 英里 是 測量 1.0 and 英里 的 per |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13706-13710 | 等於 測量 1.0 and 方碼 and 測量 1.0 and 院子長度 是 測量 1.0 and 院子長度 的 per |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 402-402 | 等於 測量 RealNumber and 弧分 and 測量 乘法 60.0 and RealNumber and 弧秒 |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 383-383 | 等於 測量 RealNumber and 圓周角度 and 測量 乘法 60.0 and RealNumber and 弧分 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7151-7153 | 等於 測量 RealNumber and amu and 測量 乘法 RealNumber and 1.6605402E-24 and 公克 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7173-7175 | 等於 測量 RealNumber and 埃 and 測量 乘法 RealNumber and 1.0E-10 and 儀表 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7367-7369 | 等於 測量 RealNumber and 圓周角度 and 測量 乘法 RealNumber and 部 Pi and 180.0 and 弧度 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 7353-7355 | 等於 測量 RealNumber and 英國熱量單位 and 測量 乘法 RealNumber and 1055.05585262 and 焦耳 |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |