No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2115-2115 | Locomotive is a subclass of rolling stock |
No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2116-2116 | Locomotive is a subclass of powered vehicle |