| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4287-4287 | Root vegetable is a subclass of fruit or vegetable |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2582-2582 | Garlic is a subclass of root vegetable |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2712-2712 | Onion is a subclass of root vegetable |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 3401-3401 | Shallot is a subclass of root vegetable |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4291-4291 | Radish is a subclass of root vegetable |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4294-4294 | Turnip is a subclass of root vegetable |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4295-4295 | Beets is a subclass of root vegetable |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4297-4297 | Carrot is a subclass of root vegetable |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4298-4298 | Rutabaga is a subclass of root vegetable |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4302-4302 | Diakon is a subclass of root vegetable |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4304-4304 | Parsnip is a subclass of root vegetable |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4321-4321 | Edible tuber is a subclass of root vegetable |
|
|