No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16524-16524 | License is a subclass of certificate |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16557-16557 | Passport is a subclass of license |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 16878-16878 | Drivers license is a subclass of license |