lessThan |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1729-1730 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1839-1840 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 337-338 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1836-1836 | 域 少於, 1 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1837-1837 | 域 少於, 2 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1831-1831 | 例 少於 and BinaryPredicate |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1833-1833 | 例 少於 and IrreflexiveRelation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1834-1834 | 例 少於 and RelationExtendedToQuantities |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1832-1832 | 例 少於 and TransitiveRelation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1835-1835 | trichotomizing 少於 and RealNumber |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 141-141 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 142-142 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 92-92 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 163-163 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1919-1919 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 44-44 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 76-76 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 172-172 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 202-202 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 111-111 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 91-91 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 325-325 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1850-1850 | 逆 比較多 and 少於 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 142-142 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 34144-34144 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 34143-34143 | |
No TPTP formula. May not be expressible in strict first order. | terms-de.txt 52-52 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 326-326 |
antecedent |
consequent |
No TPTP formula. May not be expressible in strict first order. | People.kif 238-264 | 例 年 and 年 Integer 等於 GeopoliticalArea 和 年 每一千個生存出生裡的 deaths and RealNumber 等於 Integer and 基數 卡帕 SymbolicString and 例 SymbolicString and Birth 體驗者 SymbolicString and entity 例 entity and Human 期間 何時 SymbolicString and 年 等於 哪裡 SymbolicString and 何時 SymbolicString and GeopoliticalArea 等於 部 Integer and 1000 and RealNumber 等於 entityDEATHCOUNT and 基數 卡帕 SymbolicString and 例 SymbolicString and Death 體驗者 SymbolicString and entity 例 entity and Human 年齡 entity and 測量 entity and 年持續時間 少於 entity and 1 期間 何時 SymbolicString and 年 等於 哪裡 SymbolicString and 何時 SymbolicString and GeopoliticalArea 等於 部 entityDEATHCOUNT and RealNumber and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1948-1952 | 例 RealNumber and NegativeRealNumber 少於 RealNumber and 0 例 RealNumber and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1867-1871 | 小於或等於 RealNumber and RealNumber 等於 RealNumber and RealNumber 少於 RealNumber and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 172-187 | |
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 155-170 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 18728-18737 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 18743-18753 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 18759-18769 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 18775-18785 |
|
No TPTP formula. May not be expressible in strict first order. | Dining.kif 1148-1156 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2623-2628 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13577-13586 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13505-13514 |
|
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 13467-13477 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4958-4972 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 4868-4872 |
|
No TPTP formula. May not be expressible in strict first order. | Dining.kif 772-795 |
|
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1391-1400 | |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 1940-1954 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 892-898 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 882-890 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 4698-4708 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 10961-10974 |
|
No TPTP formula. May not be expressible in strict first order. | Medicine.kif 620-630 | |
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. | Merge.kif 6099-6106 | GraphPath GraphPath 例 GraphPath and 切集 Graph 例 GraphPath and 最小割集 Graph 路徑長度 GraphPath and PositiveInteger 路徑長度 GraphPath and PositiveInteger 少於 PositiveInteger and PositiveInteger |