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 |
|