| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4166-4172 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3813-3813 | 子類 穀物草 and 草 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3817-3817 | 子類 水稻 and 穀物草 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3821-3821 | 子類 MaizeGrass and 穀物草 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3826-3826 | 子類 高粱 and 穀物草 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3860-3860 | 子類 WheatGrass and 穀物草 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4000-4000 | 子類 RyeGrass and 穀物草 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4007-4007 | 子類 OatGrass and 穀物草 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4012-4012 | 子類 BarleyGrass and 穀物草 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4017-4017 | 子類 MilletGrass and 穀物草 |
|
|