Vehicle
|
|
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1748-1748 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1958-1958 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 356-356 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1956-1956 | Integer is exhaustively partitioned into negative integer and nonnegative integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1955-1955 | Integer is exhaustively partitioned into odd integer and even integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1954-1954 | Integer is a subclass of rational number |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | Military.kif 857-857 | The range of available for military service male is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5510-5510 | The range of cardinality is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4785-4785 | The range of ceiling is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4812-4812 | The range of denominator is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Military.kif 879-879 | The range of fit for military service male is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4830-4830 | The range of floor is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4848-4848 | The range of greatest common divisor is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4933-4933 | The range of least common multiple is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5038-5038 | The range of numerator is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31725-31725 | The range of population is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5336-5336 | The range of predecessor is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Military.kif 917-917 | The range of reaching military age annually male is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5099-5099 | The range of remainder is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5191-5191 | The range of signum is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5303-5303 | The range of successor is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1960-1960 | Even integer is a subclass of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1985-1985 | Negative integer is a subclass of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1975-1975 | Nonnegative integer is a subclass of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1965-1965 | Odd integer is a subclass of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1970-1970 | Prime number is a subclass of integer |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 866-866 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 934-934 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 542-542 | |
No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 72-72 | |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
appearance as argument number 3 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4821-4821 | The number 2 argument of exponentiation is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4849-4849 | The number 1 argument of greatest common divisor is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4934-4934 | The number 1 argument of least common multiple is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5335-5335 | The number 1 argument of predecessor is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5097-5097 | The number 1 argument of remainder is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5098-5098 | The number 2 argument of remainder is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3162-3162 | The number 1 argument of sub-list function is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3163-3163 | The number 2 argument of sub-list function is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5302-5302 | The number 1 argument of successor is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 8591-8591 | The number 1 argument of year is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Weather.kif 3076-3076 | The number 2 argument of airQualityIndex is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 10406-10406 | The number 3 argument of breathingRate is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Hotel.kif 788-788 | The number 3 argument of capacity by arrangement is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 698-698 | The number 2 argument of chromosome number is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 824-824 | The number 3 argument of chromosome set count is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 3097-3097 | The number 2 argument of coil count is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Communications.kif 135-135 | The number 3 argument of communication satellite for area is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 644-644 | The number 2 argument of criticality level is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 18520-18520 | The number 2 argument of default max value is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 18503-18503 | The number 2 argument of default min value is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 18537-18537 | The number 2 argument of default value is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2070-2070 | The number 2 argument of exact cardinality is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Media.kif 2071-2071 | The number 3 argument of exact cardinality is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 3515-3515 | The number 2 argument of Fleet Size is an instance of integer |
No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 789-789 | The number 2 argument of haploid number is an instance of 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. | Merge.kif 5087-5092 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30980-30995 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30922-30932 |
|
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30947-30962 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5329-5331 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5325-5327 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5345-5347 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5312-5314 |
|
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5083-5085 |
|
consequent |