| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3398-3398 | Fonction binaire est une sous-classe de function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3399-3399 | Fonction binaire est une sous-classe de relation ternaire |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3400-3400 | Fonction binaire est une sous-classe de InheritableRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3409-3409 | Fonction associative est une sous-classe de fonction binaire |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3430-3430 | Function commutative est une sous-classe de fonction binaire |
|
|