| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14244-14244 | 城市 是 地缘政治区域 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14245-14245 | 城市 是 土地面积 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 837-837 | 港口城市 是 城市 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 35-35 | 美国城市 是 城市 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 47-47 | 欧洲城市 是 城市 的 subclass |
|
|