appearance as argument number 1 |
![]() |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1737-1738 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1835-1837 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 11751-11751 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 10233-10233 | |
No TPTP formula. May not be expressible in strict first order. | pictureList.kif 11750-11750 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1832-1832 | Real number is exhaustively partitioned into negative real number and nonnegative real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1833-1833 | Real number is exhaustively partitioned into rational number and irrational number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1831-1831 | Real number is a subclass of number |
appearance as argument number 2 |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1949-1949 | Complex number is disjoint from real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1765-1765 | Number is exhaustively partitioned into real number, imaginary number, and complex number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4618-4618 | The range of addition is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5160-5160 | The range of arccosine is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5170-5170 | The range of arcsine is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5150-5150 | The range of arctangent is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3201-3201 | The range of average function is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | People.kif 97-97 | The range of births per thousand is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | People.kif 456-456 | The range of children born per woman is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3539-3539 | The range of click-through rate is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4706-4706 | The range of cosine is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | People.kif 128-128 | The range of deaths per thousand is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | People.kif 249-249 | The range of deaths per thousand live births is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4648-4648 | The range of division is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4725-4725 | The range of exponentiation is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | People.kif 411-411 | The range of female life expectancy at birth is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | People.kif 316-316 | The range of life expectancy at birth is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 4756-4756 | The range of lift is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3170-3170 | The range of the &%sum of elements in %1 is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4881-4881 | The range of log is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | People.kif 363-363 | The range of male life expectancy at birth is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | People.kif 212-212 | The range of male to female ratio is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | People.kif 162-162 | The range of migrants per thousand is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4605-4605 | The range of multiplication is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3295-3295 | The range of qualifying purchases per user per interval is an instance of real number |
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 4666-4666 | The number 1 argument of absolute value is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4616-4616 | The number 1 argument of addition is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4617-4617 | The number 2 argument of addition is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5159-5159 | The number 1 argument of arccosine is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5169-5169 | The number 1 argument of arcsine is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5149-5149 | The number 1 argument of arctangent is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4687-4687 | The number 1 argument of ceiling is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4714-4714 | The number 1 argument of denominator is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4646-4646 | The number 1 argument of division is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4647-4647 | The number 2 argument of division is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4723-4723 | The number 1 argument of exponentiation is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4732-4732 | The number 1 argument of floor is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4827-4827 | The number 1 argument of integer square root is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4879-4879 | The number 1 argument of log is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6252-6252 | The number 1 argument of measure is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4603-4603 | The number 1 argument of multiplication is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4604-4604 | The number 2 argument of multiplication is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4940-4940 | The number 1 argument of numerator is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4974-4974 | The number 1 argument of 互相 is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5070-5070 | The number 1 argument of round is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5089-5089 | The number 1 argument of signum is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5111-5111 | The number 1 argument of sine is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5119-5119 | The number 1 argument of square root is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4630-4630 | The number 1 argument of subtraction is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 4631-4631 | The number 2 argument of subtraction is an instance of real number |
Display limited to 25 items. Show next 25 | ||
Display limited to 25 items. Show next 25 |
antecedent |
![]() |
consequent |
![]() |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1888-1892 | A real number is an instance of negative real number if and only if the real number is less than 0 and the real number is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1866-1870 | A real number is an instance of nonnegative real number if and only if the real number is greater than or equal to 0 and the real number is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1877-1881 | A real number is an instance of positive real number if and only if the real number is greater than 0 and the real number is an instance of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5269-5274 |
|
![]() |
![]() |