| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6393-6404 | |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2184-2186 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 5284-5291 |
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6388-6388 | 子類 DeciduousTree and 植物樹 |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6479-6479 | 子類 BalsaTree and DeciduousTree |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6484-6484 | 子類 BeechTree and DeciduousTree |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6489-6489 | 子類 BirchTree and DeciduousTree |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6494-6494 | 子類 BlackCherryTree and DeciduousTree |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6499-6499 | 子類 SweetCherryTree and DeciduousTree |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6503-6503 | 子類 MapleTree and DeciduousTree |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6507-6507 | 子類 奧古曼樹 and DeciduousTree |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6512-6512 | 子類 PoplarTree and DeciduousTree |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6516-6516 | 子類 CottonwoodTree and DeciduousTree |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6519-6519 | 子類 AspenTree and DeciduousTree |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6522-6522 | 子類 RedOakTree and DeciduousTree |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6526-6526 | 子類 SapeleTree and DeciduousTree |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6531-6531 | 子類 WalnutTree and DeciduousTree |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6536-6536 | 子類 WhiteOakTree and DeciduousTree |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6541-6541 | 子類 柳樹 and DeciduousTree |
|
|