Integer(integer) | ![]() | 0, 1, 10, 100, 1000, 101, 105, 11, 110, 115, 12, 120, 125, 13, 130, 135, 14, 140, 145, 15, 150, 155, 16, 160, 165, 17, 170, 175, 18, 180, 19, 190, 2, 20, 200, 21, 22, 23, 24, 25, 26, 27, 28, 29, 3, 30, 300, 31, 32, 33... |
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 is exhaustively partitioned into negative integer and nonnegative integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1955-1955 | Integer is exhaustively partitioned into odd integer and even integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1954-1954 | Integer is a subclass of rational number |
appearance as argument number 2 |
![]() |
No TPTP formula. May not be expressible in strict first order. | Military.kif 866-866 | The range of available for military service male is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5509-5509 | The range of cardinality is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4784-4784 | The range of ceiling is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4811-4811 | The range of denominator is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Military.kif 888-888 | The range of fit for military service male is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4829-4829 | The range of floor is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4847-4847 | The range of greatest common divisor is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4932-4932 | The range of least common multiple is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5037-5037 | The range of numerator is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | People.kif 30-30 | The range of population is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5335-5335 | The range of predecessor is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Military.kif 926-926 | The range of reaching military age annually male is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5098-5098 | The range of remainder is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5190-5190 | The range of signum is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5302-5302 | The range of successor is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1960-1960 | Even integer is a subclass of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1985-1985 | Negative integer is a subclass of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1975-1975 | Nonnegative integer is a subclass of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1965-1965 | Odd integer is a subclass of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1970-1970 | Prime number is a subclass of 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 | The number 2 argument of exponentiation is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4848-4848 | The number 1 argument of greatest common divisor is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4933-4933 | The number 1 argument of least common multiple is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5334-5334 | The number 1 argument of predecessor is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5096-5096 | The number 1 argument of remainder is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5097-5097 | The number 2 argument of remainder is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3161-3161 | The number 1 argument of sub-list function is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3162-3162 | The number 2 argument of sub-list function is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5301-5301 | The number 1 argument of successor is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8555-8555 | The number 1 argument of year is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 10351-10351 | The number 3 argument of breathingRate is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Hotel.kif 788-788 | The number 3 argument of capacity by arrangement is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 699-699 | The number 2 argument of chromosome number is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 825-825 | The number 3 argument of chromosome set count is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 3113-3113 | The number 2 argument of coil count is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Communications.kif 135-135 | The number 3 argument of communication satellite for area is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 644-644 | The number 2 argument of criticality level is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 18411-18411 | The number 2 argument of default max value is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 18394-18394 | The number 2 argument of default min value is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 18428-18428 | The number 2 argument of default value is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2070-2070 | The number 2 argument of exact cardinality is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2071-2071 | The number 3 argument of exact cardinality is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 3494-3494 | The number 2 argument of Fleet Size is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 790-790 | The number 2 argument of haploid number is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 10309-10309 | The number 3 argument of heart rate is an instance of 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 30873-30888 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30815-30825 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30840-30855 |
|
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 |
![]() |
![]() |
![]() |