No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 2553-2555 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 6975-6978 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 1255-1257 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 6972-6972 |
Weber is an instance of composite unit of measure |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 6973-6973 |
Weber is an instance of systeme international unit |