| No TPTP formula. May not be expressible in strict first order. | Merge.kif 11775-11775 | 获得 是 改变所有权 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Military.kif 51-51 | 食品配送业务 是 获得 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 11787-11787 | 单方面获得 是 获得 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 11803-11803 | 借入 是 获得 的 subclass |
|
|