No TPTP formula. May not be expressible in strict first order. 
Merge.kif 47624762 
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 47124712 
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 47134713 
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 52595259 
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 52695269 
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 52495249 
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 47834783 
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 48104810 
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 47424742 
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 47434743 
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 48194819 
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 48284828 
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 49234923 
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 49754975 
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 63486348 
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 46994699 
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 47004700 
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 50365036 
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 50705070 
The number 1 argument of 互相 is an instance of real number 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 51705170 
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 51895189 
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 52115211 
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 52195219 
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 47264726 
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 47274727 
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 