SystemeInternationalUnit(systeme international unit) |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6982-6982 | Tesla is an instance of systeme international unit |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6927-6927 | Volt is an instance of systeme international unit |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6890-6890 | Watt is an instance of systeme international unit |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 6972-6972 | Weber is an instance of systeme international unit |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1302-1302 | |
No TPTP formula. May not be expressible in strict first order. | english_format.kif 1821-1821 | |
No TPTP formula. May not be expressible in strict first order. | french_format.kif 980-980 | |
No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 515-515 | |
No TPTP formula. May not be expressible in strict first order. | terms-it.txt 519-519 | |
No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2664-2664 | |
No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 932-932 | |
No TPTP formula. May not be expressible in strict first order. | terms-cz.txt 555-555 | |
No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 1001-1001 |