| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1491-1491 | 子類 口語人類語言 and HumanLanguage |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 13139-13139 | 子類 音調語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 1402-1402 | 子類 克里奧爾語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 3312-3312 | 子類 混合語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 3468-3468 | 子類 洋涇浜語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 3765-3765 | 子類 非語言口語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 4602-4602 | 子類 非洲亞洲語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5063-5063 | 子類 alacalufan語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5093-5093 | 子類 algic 語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5100-5100 | 子類 阿爾泰語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5329-5329 | 子類 amto musan 語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5359-5359 | 子類 andamanese語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5501-5501 | 子類 aruan語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5587-5587 | 子類 araucanian語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5625-5625 | 子類 阿拉瓦坎語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5632-5632 | 子類 arutani sape 語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5667-5667 | 子類 澳大利亞語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5706-5706 | 子類 奧斯特亞洲語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5714-5714 | 子類 奧地利語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5721-5721 | 子類 aymaran語言 and 口語人類語言 |
| 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 5866-5866 | 子類 巴斯克語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5928-5928 | 子類 bayono awbono 語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 5954-5954 | 子類 caddoan語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6049-6049 | 子類 cahuapanan語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6075-6075 | 子類 cant 語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6120-6120 | 子類 加勒比語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6126-6126 | 子類 chapacura wanham 語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6193-6193 | 子類 chibchan語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6199-6199 | 子類 chimakuan語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6216-6216 | 子類 choco語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6222-6222 | 子類 chon語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6246-6246 | 子類 chukotko kamchatkan 語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6351-6351 | 子類 chumash集團的語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6413-6413 | 子類 coahuiltecan語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6430-6430 | 子類 德拉威語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6436-6436 | 子類 東鳥頭語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6471-6471 | 子類 東papuan語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6478-6478 | 子類 愛斯基摩人阿拉伯語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6485-6485 | 子類 geelvink灣語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6491-6491 | 子類 guahiban語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6569-6569 | 子類 海灣語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6606-6606 | 子類 哈拉克貝特語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6650-6650 | 子類 hokan語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 6656-6656 | 子類 huavean語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 11310-11310 | 子類 日本語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 11520-11520 | 子類 jivaroan語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 11578-11578 | 子類 katukinan語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 11609-11609 | 子類 keres語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 11645-11645 | 子類 科伊桑語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 11652-11652 | 子類 kiowa and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 11726-11726 | 子類 left may語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 11804-11804 | 子類 較低的mamberamo語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 11843-11843 | 子類 lule vilela 語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 11861-11861 | 子類 macro ge語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 11868-11868 | 子類 maku語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 11944-11944 | 子類 mascoian語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12018-12018 | 子類 mataco guaicuru 語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12166-12166 | 子類 瑪雅語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12173-12173 | 子類 misumalpan語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12249-12249 | 子類 mixe zoque 語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12256-12256 | 子類 莫斯特南語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12274-12274 | 子類 mura語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12293-12293 | 子類 muskogean語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12394-12394 | 子類 na dene 語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12401-12401 | 子類 nambiquaran語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12456-12456 | 子類 尼日爾剛果語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12464-12464 | 子類 nilo撒哈拉語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12509-12509 | 子類 北方白種人語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12517-12517 | 子類 oto manguean 語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12524-12524 | 子類 paezan語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12545-12545 | 子類 全盤語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12552-12552 | 子類 peba yaguan 語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12579-12579 | 子類 penutian語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12587-12587 | 子類 quechuan語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12595-12595 | 子類 薩利珊語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12602-12602 | 子類 salivan語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12638-12638 | 子類 sepik ramu 語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12661-12661 | 子類 siouan語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 12953-12953 | 子類 sko語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13033-13033 | 子類 南方白種人語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13145-13145 | 子類 subtiaba tlapanec 語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13200-13200 | 子類 塔卡語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13306-13306 | 子類 tai kadai 語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13314-13314 | 子類 托里切利語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13321-13321 | 子類 托博納坎語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13456-13456 | 子類 反式新幾內亞語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13526-13526 | 子類 tucanoan語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13534-13534 | 子類 圖皮語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13541-13541 | 子類 uralic語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13547-13547 | 子類 uru chipaya 語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13577-13577 | 子類 uto aztecan 語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13584-13584 | 子類 瓦卡山語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 13659-13659 | 子類 西papuan語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 14042-14042 | 子類 witotoan語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 14164-14164 | 子類 yanomami語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 14229-14229 | 子類 yenisei ostyak 語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 14258-14258 | 子類 yukaghir語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 14312-14312 | 子類 yuki組語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 14333-14333 | 子類 zamucoan語言 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 14363-14363 | 子類 薩帕羅語 and 口語人類語言 |
| No TPTP formula. May not be expressible in strict first order. | Languages.kif 14592-14592 | 子類 ChineseLanguage and 口語人類語言 |
|
|