| No TPTP formula. May not be expressible in strict first order. | Languages.kif 7105-7105 | 德系语 是 印度欧洲语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 7112-7112 | 东德语 是 德系语 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 7130-7130 | 北方的德语 是 德系语 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 7313-7313 | 西德语 是 德系语 的 subclass |
|
|