| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1491-1491 | 口语人类语言 是 人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13139-13139 | 音调语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 1402-1402 | 克里奥尔语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 3312-3312 | 混合语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 3468-3468 | 洋泾浜语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 3765-3765 | 非语言口语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 4602-4602 | 非洲亚洲语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5063-5063 | Alacalufan语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5093-5093 | Algic 语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5100-5100 | 阿尔泰语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5329-5329 | Amto musan 语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5359-5359 | Andamanese语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5501-5501 | Aruan语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5587-5587 | Araucanian语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5625-5625 | 阿拉瓦坎语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5632-5632 | Arutani sape 语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5667-5667 | 澳大利亚语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5706-5706 | 奥斯特亚洲语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5714-5714 | 奥地利语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5721-5721 | Aymaran语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5767-5767 | 巴巴科语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5866-5866 | 巴斯克语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5928-5928 | Bayono awbono 语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5954-5954 | Caddoan语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6049-6049 | Cahuapanan语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6075-6075 | Cant 语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6120-6120 | 加勒比语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6126-6126 | Chachapacura wanham pacura语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6193-6193 | Chibchan语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6199-6199 | Chimakuan语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6216-6216 | Choco语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6222-6222 | Chon语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6246-6246 | Chukotko kamchatkan 语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6351-6351 | Chumash集团的语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6413-6413 | Coahuiltecan语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6430-6430 | 德拉威语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6436-6436 | 东鸟头语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6471-6471 | 东papuan语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6478-6478 | 爱斯基摩人阿拉伯语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6485-6485 | Geelvink湾语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6491-6491 | Guahiban语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6569-6569 | 海湾语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6606-6606 | 哈拉克贝特语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6650-6650 | Hokan语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6656-6656 | Huavean语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 11310-11310 | 日本语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 11520-11520 | Jivaroan语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 11578-11578 | Katukinan语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 11609-11609 | Keres语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 11645-11645 | 科伊桑语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 11652-11652 | Kiowa 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 11726-11726 | Left may语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 11804-11804 | 较低的mamberamo语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 11843-11843 | Lule vilela 语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 11861-11861 | Macro ge语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 11868-11868 | Maku语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 11944-11944 | Mascoian语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12018-12018 | Mataco guaicuru 语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12166-12166 | 玛雅语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12173-12173 | Misumalpan语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12249-12249 | Mixe zoque 语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12256-12256 | 莫斯特南语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12274-12274 | Mura语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12293-12293 | Muskogean语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12394-12394 | Na dene 语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12401-12401 | Nambiquaran语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12456-12456 | 尼日尔刚果语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12464-12464 | Nilo撒哈拉语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12509-12509 | 北方白种人语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12517-12517 | Oto manguean 语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12524-12524 | Paezan语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12545-12545 | 全盘语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12552-12552 | Peba yaguan 语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12579-12579 | Penutian语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12587-12587 | Quechuan语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12595-12595 | 萨利珊语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12602-12602 | Salivan语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12638-12638 | Sepik ramu 语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12661-12661 | Siouan语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12953-12953 | Sko语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13033-13033 | 南方白种人语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13145-13145 | Subtiaba tlapanec 语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13200-13200 | 塔卡语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13306-13306 | Tai kadai 语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13314-13314 | 托里切利语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13321-13321 | 托博纳坎语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13456-13456 | 反式新几内亚语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13526-13526 | Tucanoan语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13534-13534 | 图皮语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13541-13541 | Uralic语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13547-13547 | Uru chipaya 语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13577-13577 | Uto aztecan 语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13584-13584 | 瓦卡山语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13659-13659 | 西papuan语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 14042-14042 | Witotoan语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 14164-14164 | Yanomami语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 14229-14229 | Yenisei ostyak 语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 14258-14258 | Yukaghir语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 14312-14312 | Yuki组语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 14333-14333 | Zamucoan语言 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 14363-14363 | 萨帕罗语 是 口语人类语言 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 14592-14592 | ChineseLanguage 是 口语人类语言 的 subclass |
|
|