| No TPTP formula. May not be expressible in strict first order. | Economy.kif 5409-5416 |
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6555-6555 | 子類 Conifers and EvergreenTree |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6559-6559 | 子類 松樹 and Conifers |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6570-6570 | 子類 CedarTree and Conifers |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6575-6575 | 子類 CypressTree and Conifers |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6582-6582 | 子類 FirTree and Conifers |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6587-6587 | 子類 LarchTree and Conifers |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6592-6592 | 子類 SpruceTree and Conifers |
|
|