| 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 1943-1943 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1940-1940 | Positive integer is a subclass of nonnegative integer |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1941-1941 | 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 8496-8496 | 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 15240-15240 | 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 2912-2912 | 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 4886-4886 | 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 14131-14131 | 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 8876-8876 | 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 8574-8574 | 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 14086-14086 | 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 8858-8858 | 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 3446-3446 | 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 13533-13533 | 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 3461-3461 | 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 21193-21193 | 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 2513-2513 | 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 2501-2501 | 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 6364-6364 | 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 2630-2630 | 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 2706-2706 | 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 2694-2694 | 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 |
|
|
|
|
|