No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 2547-2549 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 6951-6956 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 1249-1251 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 6741-6741 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 7464-7464 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 6948-6948 |
Ohm is an instance of composite unit of measure |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 6949-6949 |
Ohm is an instance of systeme international unit |