No TPTP formula. May not be expressible in strict first order. 
Merge.kif 46664666 
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 46164616 
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 46174617 
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 51595159 
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 51695169 
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 51495149 
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 46874687 
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 47144714 
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 46464646 
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 46474647 
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 47234723 
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 47324732 
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 48274827 
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 48794879 
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 62526252 
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 46034603 
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 46044604 
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 49404940 
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 49744974 
The number 1 argument of 互相 is an instance of real number 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 50705070 
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 50895089 
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 51115111 
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 51195119 
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 46304630 
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 46314631 
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 