| No TPTP formula. May not be expressible in strict first order. | Food.kif 2325-2325 | CitrusFruit est une sous-classe de Fruit |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2327-2327 | LemonFruit est une sous-classe de CitrusFruit |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2341-2341 | OrangeFruit est une sous-classe de CitrusFruit |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2353-2353 | Lime est une sous-classe de CitrusFruit |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2362-2362 | Grapefruit est une sous-classe de CitrusFruit |
|
|