No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2482-2482 | Ocean liner is a subclass of passenger ship |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2483-2483 | Ocean liner is a subclass of cargo ship |