| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16980-16985 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 13394-13394 | 游戏 是 比赛 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 13395-13395 | 游戏 是 娱乐或锻炼 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 465-465 | Chess 是 游戏 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 467-467 | Darts 是 游戏 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 469-469 | GoGame 是 游戏 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 471-471 | Poker 是 游戏 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 473-473 | Snooker 是 游戏 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 475-475 | Blackjack 是 游戏 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 25858-25858 | VideoGame 是 游戏 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 13399-13399 | 运动 是 游戏 的 subclass |
|
|