|
|
   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 1871-1871 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1869-1869 | Integer is exhaustively partitioned into negative integer and nonnegative integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1868-1868 | Integer is exhaustively partitioned into odd integer and even integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1867-1867 | 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 861-861 | 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 5227-5227 | The range of cardinality is an instance of integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4601-4601 | The range of ceiling is an instance of integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4628-4628 | The range of denominator is an instance of integer |
| No TPTP formula. May not be expressible in strict first order. | Military.kif 883-883 | 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 4646-4646 | The range of floor is an instance of integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4664-4664 | The range of greatest common divisor is an instance of integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4737-4737 | The range of least common multiple is an instance of integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4831-4831 | 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 5058-5058 | The range of predecessor is an instance of integer |
| No TPTP formula. May not be expressible in strict first order. | Military.kif 921-921 | 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 4892-4892 | The range of remainder is an instance of integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4946-4946 | The range of signum is an instance of integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5025-5025 | The range of successor is an instance of integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1873-1873 | Even integer is a subclass of integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1898-1898 | Negative integer is a subclass of integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1888-1888 | Nonnegative integer is a subclass of integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1878-1878 | Odd integer is a subclass of integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1883-1883 | 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 939-939 |
| appearance as argument number 3 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4637-4637 | The number 2 argument of exponentiation is an instance of integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4665-4665 | 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 4738-4738 | 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 5057-5057 | The number 1 argument of predecessor is an instance of integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4890-4890 | The number 1 argument of remainder is an instance of integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4891-4891 | The number 2 argument of remainder is an instance of integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3054-3054 | 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 3055-3055 | 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 5024-5024 | The number 1 argument of successor is an instance of integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8029-8029 | The number 1 argument of year is an instance of integer |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 761-761 | The number 3 argument of capacity by arrangement is an instance of integer |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 3088-3088 | The number 2 argument of coilCount 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 642-642 | 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 17106-17106 | The number 2 argument of defaultMaxValue is an instance of integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 17089-17089 | The number 2 argument of defaultMinValue is an instance of integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 17122-17122 | The number 2 argument of defaultValue is an instance of integer |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2072-2072 | The number 2 argument of exactCardinality is an instance of integer |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2073-2073 | The number 3 argument of exactCardinality is an instance of integer |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 4061-4061 | The number 2 argument of Fleet Size is an instance of integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5002-5002 | The number 2 argument of identity element is an instance of integer |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2190-2190 | The number 2 argument of maxCardinality is an instance of integer |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2191-2191 | The number 3 argument of maxCardinality is an instance of integer |
| No TPTP formula. May not be expressible in strict first order. | Hotel.kif 453-453 | The number 2 argument of maximum capacity is an instance of integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 17072-17072 | The number 2 argument of maxValue 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 4880-4885 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5051-5053 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5047-5049 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5067-5069 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5034-5036 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4876-4878 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3274-3278 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4704-4709 |
|
|
|
|