No TPTP formula. May not be expressible in strict first order. | Merge.kif 6242-6242 | Length measure is a subclass of constant quantity |
No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1498-1498 | Altitude measure is a subclass of length measure |