| PositiveInteger(positive integer) | | 1, 10, 100, 1000, 10000, 100000, 1000000, 1000000000, 1000000000000, 11, 12, 120, 13, 14, 144, 15, 16, 17, 1728, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 3, 30, 4, 40, 5, 50, 500, 6, 60, 7, 70, 78, 8, 80, 9, 90, C, Captain_Hicks, D... |
| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1754-1754 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1974-1974 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1971-1971 | Positive integer is a subclass of nonnegative integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1972-1972 | Positive integer is a subclass of positive real number |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 872-872 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 946-946 |
| appearance as argument number 3 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8553-8553 | The number 1 argument of day is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15359-15359 | The number 2 argument of edition is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2955-2955 | The number 2 argument of list order is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4947-4947 | The number 2 argument of log is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14510-14510 | The number 2 argument of periodical issue is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8933-8933 | The number 1 argument of quarter fn is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8631-8631 | The number 1 argument of second is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 14465-14465 | The number 2 argument of series volume is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8915-8915 | The number 1 argument of week fn is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3453-3453 | The number 2 argument of account number is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 2254-2254 | The number 3 argument of agricultural product type by rank is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 13632-13632 | The number 2 argument of atomic number is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3470-3470 | The number 2 argument of check number is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 1209-1209 | The number 2 argument of data stream slack is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 209-209 | The number 2 argument of domain is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 231-231 | The number 2 argument of domain subclass is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 21658-21658 | The number 2 argument of electron number is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 2335-2335 | The number 3 argument of export commodity type by rank is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 2514-2514 | The number 3 argument of export partner by rank is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 2502-2502 | The number 3 argument of export partner by rank in period is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 6660-6660 | The number 2 argument of human capacity is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 2631-2631 | The number 3 argument of import commodity type by rank is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 2707-2707 | The number 3 argument of import partner by rank is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 2695-2695 | The number 3 argument of import partner by rank in period is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 1599-1599 | The number 3 argument of industry rank by output is an instance of positive integer |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| antecedent |
|
|
|
|
|