| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1336-1336 | 子類 SymbolicString and 內容承載物理 |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2410-2410 | 子類 SearchQuery and SymbolicString |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 3169-3169 | 子類 AOCnumber and SymbolicString |
| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 218-218 | 子類 實際地址 and SymbolicString |
| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 1851-1851 | 子類 數字數據 and SymbolicString |
| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 2047-2047 | 子類 用戶名 and SymbolicString |
| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 2083-2083 | 子類 電腦密碼 and SymbolicString |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 19455-19455 | 子類 音節 and SymbolicString |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24846-24846 | 子類 PostalAddressText and SymbolicString |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24874-24874 | 子類 TelecomNumber and SymbolicString |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29928-29928 | 子類 AccountNumber and SymbolicString |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 29939-29939 | 子類 InvoiceNumber and SymbolicString |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 30012-30012 | 子類 PurchaseOrderNumber and SymbolicString |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1340-1340 | 子類 Character and SymbolicString |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 1580-1580 | 子類 UnicodeString and SymbolicString |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2901-2901 | 子類 AlphabeticString and SymbolicString |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2911-2911 | 子類 DecimalDigitString and SymbolicString |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 2938-2938 | 子類 AlphaNumericString and SymbolicString |
|
|