| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5767-5767 | 子類 巴巴科語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5774-5774 | 子類 andaqui集團的語言 and 巴巴科語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5787-5787 | 子類 cayapa科羅拉多語言 and 巴巴科語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5816-5816 | 子類 coconucan語言 and 巴巴科語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5838-5838 | 子類 普什圖語 and 巴巴科語言 |
|
|