| 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 1871-1871 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1868-1868 | Positive integer is a subclass of nonnegative integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1869-1869 | 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 | "正整数" is the printable form of positive integer in ChineseLanguage |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 951-951 | "positive integer" is the printable form of positive integer in english language |
| appearance as argument number 3 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7891-7891 | 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 14204-14204 | 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 2834-2834 | 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 4601-4601 | 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 12399-12399 | 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 8259-8259 | 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 7969-7969 | 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 12354-12354 | 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 8241-8241 | 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 3335-3335 | 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 12608-12608 | 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 3352-3352 | 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 19402-19402 | 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 6332-6332 | 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 1873-1875 |
|
|
|
|