| appearance as argument number 1 |
|
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7247-7248 | |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7249-7249 | The number 1 argument of headquarters of organization is an instance of organization |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7250-7250 | The number 2 argument of headquarters of organization is an instance of geopolitical area |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7251-7251 | headquarters of organization is an instance of binary predicate |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 7252-7252 | headquarters of organization is a subrelation of located |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 3627-3627 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 3626-3626 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 3625-3625 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 27723-27723 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 27722-27722 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 27721-27721 |
| appearance as argument number 0 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4731-4731 | The headquarters of British Seagull corp is in united kingdom |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4571-4571 | The headquarters of ByteDance is in Beijing |
| No TPTP formula. May not be expressible in strict first order. | Government.kif 2259-2259 | The headquarters of CCP is in china |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 5162-5162 | The headquarters of Cosworth Corporation is in England |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4637-4637 | The headquarters of eBay is in california |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4498-4498 | The headquarters of General Motors is in united states |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4579-4579 | The headquarters of Harley Davidson is in united states |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4501-4501 | The headquarters of Holden Corporation is in australia |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 5010-5010 | The headquarters of Peterbilt is in texas |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4713-4713 | The headquarters of RoverGroup is in united kingdom |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4840-4840 | The headquarters of SimmonsCorp is in australia |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 5110-5110 | The headquarters of Sortimo Corporation is in germany |
|
Show full definition with tree view
Show simplified definition (without tree view)
Show simplified definition (with tree view)
|
|
Sigma web home Suggested Upper Merged Ontology (SUMO) web home
Sigma version 3.0 is open source software produced by Articulate Software and its partners