No TPTP formula. May not be expressible in strict first order. |
Economy.kif 4035-4035 |
Lemon fruit is a subclass of citrus fruit |
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 4047-4047 |
Lime is a subclass of citrus fruit |
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 4042-4042 |
Orange fruit is a subclass of citrus fruit |
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 14907-14907 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 14906-14906 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 14905-14905 |
|