No TPTP formula. May not be expressible in strict first order. 
Merge.kif 47484748 
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 46984698 
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 46994699 
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 52455245 
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 52555255 
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 52355235 
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 47694769 
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 47964796 
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 47284728 
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 47294729 
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 48054805 
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 48144814 
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 49094909 
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 49614961 
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 63346334 
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 46854685 
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 46864686 
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 50225022 
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 50565056 
The number 1 argument of 互相 is an instance of real number 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 51565156 
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 51755175 
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 51975197 
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 52055205 
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 47124712 
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 47134713 
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 