No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 2565-2567 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 7031-7036 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 1269-1272 |
|
No TPTP formula. May not be expressible in strict first order. |
pictureList.kif 6680-6680 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 7028-7028 |
勒克司 是 CompositeUnitOfMeasure 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 7029-7029 |
勒克司 是 国际单位制 的 instance |