| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1543-1543 | 字词 是 语言式表达 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 2504-2504 | SearchTerm 是 字词 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15248-15248 | 名词 是 字词 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15253-15253 | 动词 是 字词 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15257-15257 | 形容词 是 字词 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15261-15261 | 副词 是 字词 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15265-15265 | 助词 是 字词 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 3092-3092 | Palindrome 是 字词 的 subclass |
|
|