| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14244-14244 | 子類 City and GeopoliticalArea |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14245-14245 | 子類 City and LandArea |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 837-837 | 子類 港口城市 and City |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 35-35 | 子類 美國城市 and City |
| No TPTP formula. May not be expressible in strict first order. | CountriesAndRegions.kif 47-47 | 子類 歐洲城市 and City |
|
|