| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2100-2100 | 函数量 是 物理量 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2112-2112 | 一元常数函数量 是 函数量 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6208-6208 | CompositeUnitOfMeasure 是 函数量 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6267-6267 | 面积测量 是 函数量 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6278-6278 | 体积测量 是 函数量 的 subclass |
|
|