| 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. | Economy.kif 4693-4699 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4629-4634 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4839-4843 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15036-15036 | 子類 種子 and ReproductiveBody |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 15037-15037 | 子類 種子 and 植物解剖結構 |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 3391-3391 | 子類 芝麻 and 種子 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4026-4026 | 子類 穀物 and 種子 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4112-4112 | 子類 豌豆 and 種子 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4497-4497 | 子類 諾福克島松籽 and 種子 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4500-4500 | 子類 kentia棕櫚種子 and 種子 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4503-4503 | 子類 葵花籽 and 種子 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4509-4509 | 子類 油籽 and 種子 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4624-4624 | 子類 咖啡豆 and 種子 |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 4686-4686 | 子類 可可豆 and 種子 |
|
|