| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3350-3350 | 子類 Function and SingleValuedRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3351-3351 | 子類 Function and 可繼承的關係 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3358-3358 | 子類 UnaryFunction and Function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3398-3398 | 子類 BinaryFunction and Function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3450-3450 | 子類 TernaryFunction and Function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3461-3461 | 子類 QuaternaryFunction and Function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3472-3472 | 子類 ContinuousFunction and Function |
|
|