No TPTP formula. May not be expressible in strict first order. | Merge.kif 16173-16173 | Commercial agent is a subclass of agent |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 16179-16179 | Business is a subclass of commercial agent |