| No TPTP formula. May not be expressible in strict first order. | Media.kif 2233-2233 | 子類 CodeMap and 分類方案 |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 3130-3130 | 子類 AirlineCodeMap and CodeMap |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2242-2242 | 子類 LanguageCodeMap and CodeMap |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2249-2249 | 子類 CurrencyCodeMap and CodeMap |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2256-2256 | 子類 GeographicCodeMap and CodeMap |
|
|