No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 2563-2564 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 7021-7024 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 1266-1268 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 7018-7018 |
Lumen is an instance of composite unit of measure |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 7019-7019 |
Lumen is an instance of systeme international unit |