No TPTP formula. May not be expressible in strict first order. | Merge.kif 3398-3398 | Binary function is a subclass of function |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3399-3399 | Binary function is a subclass of ternary relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3400-3400 | Binary function is a subclass of inheritable relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3409-3409 | Associative function is a subclass of binary function |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3430-3430 | Commutative function is a subclass of binary function |