| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7527-7532 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 13399-13399 | 运动 是 游戏 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 89-89 | Archery 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 91-91 | Badminton 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 95-95 | Curling 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 97-97 | CycleRacing 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 103-103 | Diving 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 112-112 | IceSkating 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 114-114 | Fencing 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 116-116 | FigureSkating 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 126-126 | Lacrosse 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 133-133 | MartialArts 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 184-184 | SwimmingSport 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 186-186 | SquashSport 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 188-188 | ShootingSport 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 198-198 | SailingSport 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 207-207 | Surfing 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 221-221 | KiteSurfing 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 226-226 | Caving 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 229-229 | Skateboarding 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 232-232 | Rafting 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 236-236 | FishingSport 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 239-239 | TableTennis 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 243-243 | Wrestling 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 245-245 | HorseRacing 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 496-496 | RockClimbing 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 585-585 | 拳击 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 600-600 | 体操 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 772-772 | 健美运动 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 852-852 | Tennis 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 889-889 | 高尔夫球 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 1062-1062 | Skiing 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 1103-1103 | Bowling 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 1182-1182 | Equitation 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 1207-1207 | WaterSport 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 1318-1318 | Racquetball 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Sports.kif 1337-1337 | 奥运会 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7534-7534 | 团队运动 是 运动 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7548-7548 | 赛跑 是 运动 的 subclass |
|
|