Integer |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1748-1748 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1958-1958 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 356-356 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1956-1956 | 劃分 Integer, NegativeInteger and NonnegativeInteger |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1955-1955 | 劃分 Integer, OddInteger and EvenInteger |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1954-1954 | 子類 Integer and RationalNumber |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | Military.kif 866-866 | 範圍 可用於兵役男性 and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5509-5509 | 範圍 基數 and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4784-4784 | 範圍 天花板 and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4811-4811 | 範圍 分母 and Integer |
No TPTP formula. May not be expressible in strict first order. | Military.kif 888-888 | 範圍 適合兵役的男性 and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4829-4829 | 範圍 地板 and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4847-4847 | 範圍 最大公約數 and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4932-4932 | 範圍 最不常見的倍數 and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5037-5037 | 範圍 分子 and Integer |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31693-31693 | 範圍 人口 and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5335-5335 | 範圍 前任 and Integer |
No TPTP formula. May not be expressible in strict first order. | Military.kif 926-926 | 範圍 每年達到軍齡的男性 and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5098-5098 | 範圍 剩餘 and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5190-5190 | 範圍 正負號 and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5302-5302 | 範圍 接班人 and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1960-1960 | 子類 EvenInteger and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1985-1985 | 子類 NegativeInteger and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1975-1975 | 子類 NonnegativeInteger and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1965-1965 | 子類 OddInteger and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1970-1970 | 子類 PrimeNumber and Integer |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 866-866 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 934-934 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 542-542 | |
No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 72-72 | |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
appearance as argument number 3 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4820-4820 | 域 冪, 2 and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4848-4848 | 域 最大公約數, 1 and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4933-4933 | 域 最不常見的倍數, 1 and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5334-5334 | 域 前任, 1 and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5096-5096 | 域 剩餘, 1 and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5097-5097 | 域 剩餘, 2 and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3161-3161 | 域 SubListFn, 1 and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3162-3162 | 域 SubListFn, 2 and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5301-5301 | 域 接班人, 1 and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8555-8555 | 域 年, 1 and Integer |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 3093-3093 | 域 airQualityIndex, 2 and Integer |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 10379-10379 | 域 breathingRate, 3 and Integer |
No TPTP formula. May not be expressible in strict first order. | Hotel.kif 788-788 | 域 capacityByArrangement, 3 and Integer |
No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 699-699 | 域 chromosomeNumber, 2 and Integer |
No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 825-825 | 域 chromosomeSetCount, 3 and Integer |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 3113-3113 | 域 coilCount, 2 and Integer |
No TPTP formula. May not be expressible in strict first order. | Communications.kif 135-135 | 域 區域通信衛星, 3 and Integer |
No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 644-644 | 域 臨界水平, 2 and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 18441-18441 | 域 defaultMaxValue, 2 and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 18424-18424 | 域 defaultMinValue, 2 and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 18458-18458 | 域 defaultValue, 2 and Integer |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2070-2070 | 域 exactCardinality, 2 and Integer |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2071-2071 | 域 exactCardinality, 3 and Integer |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 3522-3522 | 域 fleetSize, 2 and Integer |
No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 790-790 | 域 haploidNumber, 2 and Integer |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
antecedent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5086-5091 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30956-30971 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30898-30908 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30923-30938 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5328-5330 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5324-5326 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5344-5346 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5311-5313 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5082-5084 |
|
consequent |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24236-24246 | |
No TPTP formula. May not be expressible in strict first order. | Biography.kif 69-85 |
|
No TPTP formula. May not be expressible in strict first order. | Biography.kif 99-115 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3392-3396 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24195-24206 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4899-4904 |
|