lessThanOrEqualTo |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1733-1734 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1863-1865 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 341-342 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1860-1860 | 域 小於或等於, 1 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1861-1861 | 域 小於或等於, 2 and RealNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1856-1856 | 例 小於或等於 and BinaryPredicate |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1857-1857 | 例 小於或等於 and PartialOrderingRelation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1858-1858 | 例 小於或等於 and RelationExtendedToQuantities |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1859-1859 | trichotomizing 小於或等於 and RealNumber |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 143-143 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 144-144 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 93-93 | |
No TPTP formula. May not be expressible in strict first order. | relations-it.txt 164-164 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 1920-1920 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 45-45 | |
No TPTP formula. May not be expressible in strict first order. | relations-cz.txt 78-78 | |
No TPTP formula. May not be expressible in strict first order. | relations-de.txt 174-174 | |
No TPTP formula. May not be expressible in strict first order. | relations-hindi.txt 203-203 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 112-112 | |
No TPTP formula. May not be expressible in strict first order. | relations-sv.txt 92-92 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 327-327 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1879-1879 | 逆 大於或等於 and 小於或等於 |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 34151-34151 | |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 144-144 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 34150-34150 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 34149-34149 | |
No TPTP formula. May not be expressible in strict first order. | terms-de.txt 53-53 | |
No TPTP formula. May not be expressible in strict first order. | relations-tg.txt 328-328 |
antecedent |
consequent |
No TPTP formula. May not be expressible in strict first order. | People.kif 272-293 | RealNumber 是 List 的 average List PositiveInteger 等於 列表長度 List and 列表長度 List 等於 清單順序 List and 1 and 清單順序 List and 1 PositiveInteger
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6044-6050 | |
No TPTP formula. May not be expressible in strict first order. | Geography.kif 427-431 |
|
No TPTP formula. May not be expressible in strict first order. | Geography.kif 467-474 |
|
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1445-1457 | |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1426-1438 | |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1407-1419 | |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 917-925 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 906-915 |
|
No TPTP formula. May not be expressible in strict first order. | Geography.kif 2873-2884 | |
No TPTP formula. May not be expressible in strict first order. | Food.kif 571-578 |
|
No TPTP formula. May not be expressible in strict first order. | Food.kif 495-502 |
|
No TPTP formula. May not be expressible in strict first order. | Food.kif 533-540 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 4645-4658 |
|
No TPTP formula. May not be expressible in strict first order. | Economy.kif 4669-4682 |
|
No TPTP formula. May not be expressible in strict first order. | Food.kif 1367-1385 |
|
No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 59-65 |
|
No TPTP formula. May not be expressible in strict first order. | Government.kif 1075-1084 |
|
No TPTP formula. May not be expressible in strict first order. | Government.kif 1062-1073 |
|
No TPTP formula. May not be expressible in strict first order. | Weather.kif 2365-2384 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 8985-8989 |
|
No TPTP formula. May not be expressible in strict first order. | Food.kif 2993-3011 |
|
No TPTP formula. May not be expressible in strict first order. | Food.kif 3018-3036 |
|
No TPTP formula. May not be expressible in strict first order. | Food.kif 2851-2869 |
|
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 453-458 | |
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. | Media.kif 1966-1966 | 小於或等於 基數 TwelveApostles and 12 |