| 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 1905-1905 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1902-1902 | Positive integer is a subclass of nonnegative integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1903-1903 | 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 8025-8025 | 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 14338-14338 | 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 2867-2867 | 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 4732-4732 | 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 12459-12459 | 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 8393-8393 | 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 8103-8103 | 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 12414-12414 | 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 8375-8375 | 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 3336-3336 | 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 12742-12742 | 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 3353-3353 | 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 19562-19562 | 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 985-1003 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1907-1909 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2972-2988 | 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
|
|
|
|