| No TPTP formula. May not be expressible in strict first order. | Languages.kif 7941-7941 | 子類 上德語 and 德語小組語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 7947-7947 | 子類 alemannic語言 and 上德語 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 8022-8022 | 子類 土耳其語 and 上德語 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 8059-8059 | 子類 巴伐利亞奧地利語言 and 上德語 |
|
|