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