| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4277-4281 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4223-4227 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4532-4543 | |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2175-2175 | 子類 水果 and FruitOrVegetable |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2179-2179 | 子類 蘋果 and 水果 |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2188-2188 | 子類 日期水果 and 水果 |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2193-2193 | 子類 梨果 and 水果 |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2198-2198 | 子類 漿果 and 水果 |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2281-2281 | 子類 鱷梨 and 水果 |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2286-2286 | 子類 番茄 and 水果 |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2288-2288 | 子類 葡萄 and 水果 |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2290-2290 | 子類 瓜 and 水果 |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2294-2294 | 子類 橄欖 and 水果 |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2325-2325 | 子類 柑橘類水果 and 水果 |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2364-2364 | 子類 熱帶水果 and 水果 |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 2758-2758 | 子類 Peach and 水果 |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 3481-3481 | 子類 Strawberry and 水果 |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 3487-3487 | 子類 TamarindFruit and 水果 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4730-4730 | 子類 釀酒葡萄 and 水果 |
|
|