| OrangeFruit(orange fruit)
| | Jaffa_orange, Seville_orange, Valencia_orange, bitter_orange, clementine, mandarin, mandarin_orange, navel_orange, orange, satsuma, sour_orange, sweet_orange, tangerine, temple_orange |
| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2343-2344 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 870-870 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 906-906 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 933-933 | |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2342-2342 | Orange fruit is a subclass of food for animal |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2341-2341 | Orange fruit is a subclass of citrus fruit |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 42408-42408 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 42407-42407 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 42406-42406 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2346-2351 |
|
|
|
|