No TPTP formula. May not be expressible in strict first order. 
Merge.kif 51655165 
The arccosine of the cosine of a real number is equal to the real number 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 51755175 
The arcsine of the sine of a real number is equal to the real number 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 51555155 
The arctan of the tangent of a real number is equal to the real number 
No TPTP formula. May not be expressible in strict first order. 
Military.kif 872881 
The available for military service male of a geopolitical area is equal to the number of instances in the class described by a symbolic string 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 1392813928 
The number of instances in continent is equal to 7 
No TPTP formula. May not be expressible in strict first order. 
Media.kif 20012001 
The number of instances in NativityMagi is equal to 3 
No TPTP formula. May not be expressible in strict first order. 
People.kif 469479 
The children born per woman of a geopolitical area and the year an integer is equal to the number of instances in the class described by a symbolic string 
No TPTP formula. May not be expressible in strict first order. 
Military.kif 895906 
The fit for military service male of a geopolitical area is equal to the number of instances in the class described by a symbolic string 
No TPTP formula. May not be expressible in strict first order. 
Economy.kif 20192019 
1 Kilowatt hour(s) is equal to 3.6 1 million joules(s) 
No TPTP formula. May not be expressible in strict first order. 
Economy.kif 20202020 
1 Kilowatt hour(s) is equal to 3600000.0 joule(s) 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 70167018 
1 Week duration(s) is equal to 7 day duration(s) 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 70437045 
1 Year duration(s) is equal to 365 day duration(s) 
No TPTP formula. May not be expressible in strict first order. 
Geography.kif 382382 
1.0 Angular degree(s) is equal to 60.0 arc minute(s) 
No TPTP formula. May not be expressible in strict first order. 
Geography.kif 401401 
1.0 Arc minute(s) is equal to 60.0 arc second(s) 
No TPTP formula. May not be expressible in strict first order. 
Geography.kif 37643764 
1.0 Fathom(s) is equal to 6.0 foot length(s) 
No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 1306713069 
1.0 Metric ton(s) is equal to 2205.0 pound mass(s) 
No TPTP formula. May not be expressible in strict first order. 
Geography.kif 37873789 
1.0 Nautical mile(s) is equal to 1852.0 meter(s) 
No TPTP formula. May not be expressible in strict first order. 
Geography.kif 37833785 
1.0 Nautical mile(s) is equal to 6076.1 foot length(s) 
No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 1316213166 
1.0 Square mile(s) is equal to the per of 1.0 mile(s) and 1.0 mile(s) 
No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 1317213176 
1.0 Square yard(s) is equal to the per of 1.0 yard length(s) and 1.0 yard length(s) 
No TPTP formula. May not be expressible in strict first order. 
Geography.kif 402402 
A real number arc minute(s) is equal to 60.0 and the real number arc second(s) 
No TPTP formula. May not be expressible in strict first order. 
Geography.kif 383383 
A real number angular degree(s) is equal to 60.0 and the real number arc minute(s) 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 70557057 
A real number amu(s) is equal to the real number and 1.6605402E24 gram(s) 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 70777079 
A real number angstrom(s) is equal to the real number and 1.0E10 meter(s) 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 72717273 
A real number angular degree(s) is equal to the real number and pi and 180.0 radian(s) 

Display limited to 25 items. Show next 25 

Display limited to 25 items. Show next 25 