No TPTP formula. May not be expressible in strict first order. 
Merge.kif 47634763 
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 47134713 
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 47144714 
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 52605260 
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 52705270 
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 52505250 
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 47844784 
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 48114811 
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 47434743 
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 47444744 
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 48204820 
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 48294829 
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 49244924 
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 49764976 
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 63496349 
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 47004700 
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 47014701 
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 50375037 
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 50715071 
The number 1 argument of 互相 is an instance of real number 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 51715171 
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 51905190 
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 52125212 
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 52205220 
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 47274727 
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 47284728 
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 