| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15979-15979 | 乐器 是 设备 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Music.kif 1186-1186 | 弦乐器 是 乐器 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Music.kif 1198-1198 | 管乐器 是 乐器 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Music.kif 1215-1215 | 喇叭乐器 是 乐器 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Music.kif 1220-1220 | 打击乐器 是 乐器 的 subclass |
|
|