|
|
   Procedure
|
|
|
| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 5280-5280 | Hardwood 和 % 2 是 disjoint |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 5281-5282 | |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 5279-5279 | Hardwood 详尽无遗地 partition 成 Softwood |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 5278-5278 | Hardwood 是 WoodProduct 的 subclass |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 5293-5293 | BalsaWood 是 Hardwood 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 5303-5303 | BeechWood 是 Hardwood 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 5313-5313 | BirchWood 是 Hardwood 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 5323-5323 | CherryWood 是 Hardwood 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 5335-5335 | MapleWood 是 Hardwood 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 5345-5345 | OkoumeWood 是 Hardwood 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 5355-5355 | PoplarWood 是 Hardwood 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 5365-5365 | RedOakWood 是 Hardwood 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 5375-5375 | SapeleWood 是 Hardwood 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 5385-5385 | WalnutWood 是 Hardwood 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 5395-5395 | WhiteOakWood 是 Hardwood 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 64967-64967 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 5284-5291 |
|
|
|
|