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 1952-1952 | |
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 1950-1950 | Integer is exhaustively partitioned into negative integer and nonnegative integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1949-1949 | Integer is exhaustively partitioned into odd integer and even integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1948-1948 | 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 924-924 | 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 5500-5500 | The range of cardinality is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4778-4778 | The range of ceiling is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 6876-6876 | The range of demand is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4805-4805 | The range of denominator is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Military.kif 946-946 | 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 4823-4823 | The range of floor is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4841-4841 | The range of greatest common divisor is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4926-4926 | The range of least common multiple is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5031-5031 | The range of numerator is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 33384-33384 | The range of population is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5329-5329 | The range of predecessor is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Military.kif 984-984 | 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 5092-5092 | The range of remainder is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5184-5184 | The range of signum is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5296-5296 | The range of successor is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Economy.kif 6847-6847 | The range of supply is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1954-1954 | Even integer is a subclass of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1979-1979 | Negative integer is a subclass of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1969-1969 | Nonnegative integer is a subclass of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1959-1959 | Odd integer is a subclass of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1964-1964 | Prime number is a subclass of integer |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 866-866 | Prime number is a subclass of integer |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 934-934 | Prime number is a subclass of integer |
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 4814-4814 | The number 2 argument of exponentiation is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4842-4842 | 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 4927-4927 | 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 5328-5328 | The number 1 argument of predecessor is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5090-5090 | The number 1 argument of remainder is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5091-5091 | The number 2 argument of remainder is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3156-3156 | 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 3157-3157 | 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 5295-5295 | The number 1 argument of successor is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8625-8625 | The number 1 argument of year is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 3075-3075 | The number 2 argument of airQualityIndex is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 11728-11728 | 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 698-698 | 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 824-824 | 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 3173-3173 | 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 750-750 | 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 18575-18575 | 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 18558-18558 | 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 18592-18592 | 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 3991-3991 | The number 2 argument of Fleet Size is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | engineering.kif 837-837 | The number 2 argument of gear tooth count 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 5080-5085 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 32638-32653 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 32580-32590 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 32605-32620 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5322-5324 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5318-5320 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5338-5340 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5305-5307 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5076-5078 |
|
consequent |
![]() |
![]() |
![]() |