| No TPTP formula. May not be expressible in strict first order. | Food.kif 299-306 | |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 1633-1639 | |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 294-294 | FoodFromPlant 是 Food 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 1029-1029 | CoffeeGrind 是 FoodFromPlant 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 1470-1470 | 面粉 是 FoodFromPlant 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 3323-3323 | Raisin 是 FoodFromPlant 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 3509-3509 | Tofu 是 FoodFromPlant 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4149-4149 | Grain 是 FoodFromPlant 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4307-4307 | CerealStarch 是 FoodFromPlant 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4312-4312 | 根淀粉 是 FoodFromPlant 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4360-4360 | 香料 是 FoodFromPlant 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4469-4469 | 食用坚果 是 FoodFromPlant 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4556-4556 | 植物油 是 FoodFromPlant 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4625-4625 | 咖啡豆 是 FoodFromPlant 的 subclass |
|
|