No TPTP formula. May not be expressible in strict first order. 
Merge.kif 46974697 
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 46474647 
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 46484648 
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 51905190 
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 52005200 
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 51805180 
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 47184718 
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 47454745 
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 46774677 
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 46784678 
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 47544754 
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 47634763 
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 48584858 
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 49104910 
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 62876287 
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 46344634 
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 46354635 
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 49714971 
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 50055005 
The number 1 argument of 互相 is an instance of real number 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 51015101 
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 51205120 
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 51425142 
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 51505150 
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 46614661 
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 46624662 
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 