| 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 1909-1909 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1906-1906 | Positive integer is a subclass of nonnegative integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1907-1907 | 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 951-951 |
| appearance as argument number 3 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8077-8077 | 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 14390-14390 | 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 2871-2871 | 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 4777-4777 | 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 12434-12434 | 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 8446-8446 | The number 1 argument of QuarterFn is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8155-8155 | 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 12389-12389 | 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 8428-8428 | The number 1 argument of WeekFn is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | FinancialOntology.kif 3378-3378 | The number 2 argument of account number is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 12794-12794 | 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 3395-3395 | 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 1214-1214 | 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 207-207 | 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 229-229 | 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 19541-19541 | 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 2328-2328 | 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 2506-2506 | 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 2494-2494 | 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 6339-6339 | 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 2623-2623 | 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 2699-2699 | 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 2687-2687 | 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 1592-1592 | The number 3 argument of industry rank by output is an instance of positive integer |
| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 740-740 | The number 2 argument of maximum replications is an instance of positive 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. | UXExperimentalTerms.kif 987-1005 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1911-1913 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2976-2992 | A list is equal to the list composed of another list and a third list and the other list is not equal to null list and the third list is not equal to null list if and only if for all a positive integer and another positive integer
|
|
|
|