| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2194-2194 | 总值关系 是 关系 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2195-2195 | 总值关系 是 可继承的关系 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2368-2368 | 偏序关系 是 总值关系 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6448-6448 | UnitOfMeasureMultiplier 是 总值关系 的 subclass |
|
|