| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4556-4556 | 子類 植物油 and FoodFromPlant |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4557-4557 | 子類 植物油 and Mixture |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4558-4558 | 子類 植物油 and OilFromPlant |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2486-2486 | 子類 可可脂 and 植物油 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4561-4561 | 子類 棕櫚油 and 植物油 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4562-4562 | 子類 橄欖油 and 植物油 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4565-4565 | 子類 SoybeanOil and 植物油 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4568-4568 | 子類 GrapeSeedOil and 植物油 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4569-4569 | 子類 RapeseedOil and 植物油 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4570-4570 | 子類 CanolaOil and 植物油 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4571-4571 | 子類 SunFlowerOil and 植物油 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4574-4574 | 子類 SafflowerOil and 植物油 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4575-4575 | 子類 GroundnutOil and 植物油 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4578-4578 | 子類 CottonSeedOil and 植物油 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4579-4579 | 子類 CoconutOil and 植物油 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4582-4582 | 子類 AvocadoOil and 植物油 |
|
|