| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7528-7533 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7524-7524 | 运动队 是 一群人 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 503-503 | BasketballTeam 是 运动队 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 505-505 | VolleyballTeam 是 运动队 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 507-507 | SoccerTeam 是 运动队 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 509-509 | RugbyTeam 是 运动队 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 511-511 | LacrosseTeam 是 运动队 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 513-513 | CarRacingTeam 是 运动队 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 514-514 | MotorcycleRacingTeam 是 运动队 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 750-750 | 棒球队 是 运动队 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 843-843 | 足球队 是 运动队 的 subclass |
|
|