| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4469-4469 | 子類 食用堅果 and FoodFromPlant |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4470-4470 | 子類 食用堅果 and FruitOrVegetable |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2085-2085 | 子類 AlmondNut and 食用堅果 |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2419-2419 | 子類 腰果 and 食用堅果 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4472-4472 | 子類 核桃 and 食用堅果 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4474-4474 | 子類 山核桃 and 食用堅果 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4476-4476 | 子類 PineNut and 食用堅果 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4482-4482 | 子類 澳洲堅果 and 食用堅果 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4484-4484 | 子類 乳木果 and 食用堅果 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4518-4518 | 子類 棕櫚油堅果 and 食用堅果 |
|
|