|
|
   BinaryFunction
|
|
|
| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1999-1999 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3284-3285 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3280-3280 | Binary function is a subclass of function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3282-3282 | Binary function is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3281-3281 | Binary function is a subclass of ternary relation |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 280-280 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 279-279 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 278-278 | |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2390-2390 | Aborted is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2456-2456 | Aborted launch is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | MilitaryProcesses.kif 2410-2410 | Aborted mission is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4524-4524 | Addition is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Music.kif 920-920 | Album copies function is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1683-1683 | Attr is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | People.kif 90-90 | Births per thousand is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 685-685 | Border is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | VirusProteinAndCellPart.kif 583-583 | Cell part is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | People.kif 446-446 | Children born per woman is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | UXExperimentalTerms.kif 3524-3524 | Click-through rate is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Music.kif 1034-1034 | Contest function is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 8060-8060 | Day is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | People.kif 121-121 | Deaths per thousand is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | People.kif 242-242 | Deaths per thousand live births is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 6357-6357 | Density is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16050-16050 | Department is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16087-16087 | DepartmentOfPreventingFn is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 476-476 | Directional subregion is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4556-4556 | Division is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14372-14372 | Edition is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 4633-4633 | Exponentiation is an instance of binary function |
| Display limited to 25 items. Show next 25 | ||
| Display limited to 25 items. Show next 25 |
| appearance as argument number 3 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3594-3594 | The number 1 argument of distributes is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3595-3595 | The number 2 argument of distributes is an instance of binary function |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 5001-5001 | The number 1 argument of identity element is an instance of binary function |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3287-3289 |
|
|
|
|