| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14408-14408 | 无花植物 是 植物 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14414-14414 | 藻类 是 无花植物 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14437-14437 | 苔藓 是 无花植物 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14441-14441 | 蕨类 是 无花植物 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6322-6322 | 青苔 是 无花植物 的 subclass |
|
|