| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3398-3398 | 二元函数 是 函数 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3399-3399 | 二元函数 是 三元关系 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3400-3400 | 二元函数 是 可继承的关系 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3409-3409 | 结合函数 是 二元函数 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3430-3430 | 交换函数 是 二元函数 的 subclass |
|
|