| No TPTP formula. May not be expressible in strict first order. | Food.kif 2170-2172 | |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2672-2674 | |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 3397-3399 | |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2403-2405 |
|
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2584-2586 | |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2427-2429 | |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2529-2531 | |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 3360-3362 | |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2733-2735 | |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 3483-3485 |
|
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2696-2698 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 9355-9355 | 子類 HerbaceousPlant and FloweringPlant |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 9371-9371 | 子類 草 and HerbaceousPlant |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 9380-9380 | 子類 煙草 and HerbaceousPlant |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4229-4229 | 子類 CucumberPlant and HerbaceousPlant |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4257-4257 | 子類 CabbagePlant and HerbaceousPlant |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4283-4283 | 子類 EggplantPlant and HerbaceousPlant |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4506-4506 | 子類 向日葵 and HerbaceousPlant |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4820-4820 | 子類 AlfalfaPlant and HerbaceousPlant |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4834-4834 | 子類 CloverPlant and HerbaceousPlant |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4860-4860 | 子類 罌粟 and HerbaceousPlant |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4866-4866 | 子類 蘭花 and HerbaceousPlant |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4870-4870 | 子類 菊花 and HerbaceousPlant |
|
|