| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1633-1633 | 子類 DualObjectProcess and Process |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 11471-11471 | 子類 Substituting and DualObjectProcess |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 11832-11832 | 子類 Transaction and DualObjectProcess |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 12131-12131 | 子類 Comparing and DualObjectProcess |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 12369-12369 | 子類 Attaching and DualObjectProcess |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 12421-12421 | 子類 Detaching and DualObjectProcess |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 12478-12478 | 子類 Combining and DualObjectProcess |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 12504-12504 | 子類 Separating and DualObjectProcess |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 12753-12753 | 子類 翻譯 and DualObjectProcess |
|
|