| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16354-16354 | Business is a subclass of commercial agent |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16355-16355 | Business is a subclass of organization |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 8264-8264 | Agency is a subclass of business |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 8274-8274 | Entertainment company is a subclass of business |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 8287-8287 | Financial company is a subclass of business |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 8307-8307 | Insurance company is a subclass of business |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 8335-8335 | Transportation company is a subclass of business |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 8373-8373 | Partnership is a subclass of business |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 8437-8437 | Restaurant is a subclass of business |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 8465-8465 | Proprietorship is a subclass of business |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 16363-16363 | Corporation is a subclass of business |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 1699-1699 | Funeral arranger is a subclass of business |
| No TPTP formula. May not be expressible in strict first order. | Media.kif 1704-1704 | Crematorium is a subclass of business |
| No TPTP formula. May not be expressible in strict first order. | Dining.kif 65-65 | Bakery is a subclass of business |
|
|