No TPTP formula. May not be expressible in strict first order. 
Merge.kif 49894989 
The range of max is an instance of number 
No TPTP formula. May not be expressible in strict first order. 
Weather.kif 16831683 
The range of maximum value is an instance of number 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 50155015 
The range of min is an instance of number 
No TPTP formula. May not be expressible in strict first order. 
Weather.kif 15061506 
The range of standard deviation is an instance of number 
No TPTP formula. May not be expressible in strict first order. 
Weather.kif 14511451 
The range of variance average function is an instance of number 
No TPTP formula. May not be expressible in strict first order. 
Weather.kif 14731473 
The range of variance function is an instance of number 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 20082008 
Complex number is a subclass of number 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 18991899 
Imaginary number is a subclass of number 
No TPTP formula. May not be expressible in strict first order. 
engineering.kif 289289 
Multipole variable is a subclass of number 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 18911891 
Real number is a subclass of number 
No TPTP formula. May not be expressible in strict first order. 
chinese_format.kif 858858 

No TPTP formula. May not be expressible in strict first order. 
english_format.kif 918918 

No TPTP formula. May not be expressible in strict first order. 
french_format.kif 534534 

No TPTP formula. May not be expressible in strict first order. 
termshindi.txt 2222 

No TPTP formula. May not be expressible in strict first order. 
termsit.txt 2424 

No TPTP formula. May not be expressible in strict first order. 
japanese_format.kif 22192219 

No TPTP formula. May not be expressible in strict first order. 
portuguese_format.kif 486486 

No TPTP formula. May not be expressible in strict first order. 
termscb.txt 2525 

No TPTP formula. May not be expressible in strict first order. 
termscz.txt 101101 

No TPTP formula. May not be expressible in strict first order. 
relationsro.kif 555555 

No TPTP formula. May not be expressible in strict first order. 
termstg.txt 2525 
