No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 3762-3762 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 3761-3761 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 3760-3760 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 7548-7548 |
高度 是 linearExtent 的 subrelation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 7557-7557 |
长度 是 linearExtent 的 subrelation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 7543-7543 |
宽度 是 linearExtent 的 subrelation |
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 65866-65866 |
|