No TPTP formula. May not be expressible in strict first order. 
Merge.kif 51715171 
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 51815181 
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 51615161 
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 1393513935 
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 70227024 
1 Week duration(s) is equal to 7 day duration(s) 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 70497051 
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 1307113073 
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 1316613170 
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 1317613180 
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 70617063 
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 70837085 
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 72777279 
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 