| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3814-3815 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 8412-8412 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 9042-9042 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3813-3813 | Cereal grass plant is a subclass of grass plant |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4012-4012 | Barley grass is a subclass of cereal grass plant |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3821-3821 | Maize grass is a subclass of cereal grass plant |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4017-4017 | Millet grass is a subclass of cereal grass plant |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4007-4007 | Oat grass is a subclass of cereal grass plant |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3817-3817 | Paddy rice is a subclass of cereal grass plant |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4000-4000 | Rye grass is a subclass of cereal grass plant |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3826-3826 | Sorghum grass is a subclass of cereal grass plant |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 3860-3860 | Wheat grass is a subclass of cereal grass plant |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 13950-13950 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 13949-13949 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 13948-13948 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4031-4033 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4166-4172 |
|
|
|
|