( ! [V__SPEED,V__NUM] :
(((s__instance(V__SPEED,s__FunctionQuantity) &
s__instance(V__NUM,s__RealNumber))
=>
((((V__SPEED = s__MeasureFn(V__NUM,s__MilesPerHour))
=>
(V__SPEED = s__SpeedFn(s__MeasureFn(V__NUM,s__Mile),s__MeasureFn(n__1,s__HourDuration))))
&
((V__SPEED = s__SpeedFn(s__MeasureFn(V__NUM,s__Mile),s__MeasureFn(n__1,s__HourDuration)))
=>
(V__SPEED = s__MeasureFn(V__NUM,s__MilesPerHour))))))
)
)

Weather.kif 17011707 
A function quantity is equal to a real number miles per hour(s) if and only if the function quantity is equal to the real number mile(s) per 1 hour duration(s) 
( ! [V__TIME2,V__TIME1] :
(((s__instance(V__TIME2,s__Number) &
s__instance(V__TIME2,s__TimePosition) &
s__instance(V__TIME1,s__Number) &
s__instance(V__TIME1,s__TimePosition))
=>
(((s__RelativeTimeFn(V__TIME1,s__CentralTimeZone) = V__TIME2)
=>
((V__TIME2 = s__AdditionFn(V__TIME1,s__MeasureFn(n__6,s__HourDuration)))))))
)
)

Merge.kif 1652416526 

( ! [V__TIME2,V__TIME1] :
(((s__instance(V__TIME2,s__Number) &
s__instance(V__TIME2,s__TimePosition) &
s__instance(V__TIME1,s__Number) &
s__instance(V__TIME1,s__TimePosition))
=>
(((s__RelativeTimeFn(V__TIME1,s__EasternTimeZone) = V__TIME2)
=>
((V__TIME2 = s__AdditionFn(V__TIME1,s__MeasureFn(n__5,s__HourDuration)))))))
)
)

Merge.kif 1653216534 

( ! [V__TIME2,V__TIME1] :
(((s__instance(V__TIME2,s__Number) &
s__instance(V__TIME2,s__TimePosition) &
s__instance(V__TIME1,s__Number) &
s__instance(V__TIME1,s__TimePosition))
=>
(((s__RelativeTimeFn(V__TIME1,s__MountainTimeZone) = V__TIME2)
=>
((V__TIME2 = s__AdditionFn(V__TIME1,s__MeasureFn(n__7,s__HourDuration)))))))
)
)

Merge.kif 1651616518 

( ! [V__TIME2,V__TIME1] :
(((s__instance(V__TIME2,s__Number) &
s__instance(V__TIME2,s__TimePosition) &
s__instance(V__TIME1,s__Number) &
s__instance(V__TIME1,s__TimePosition))
=>
(((s__RelativeTimeFn(V__TIME1,s__PacificTimeZone) = V__TIME2)
=>
((V__TIME2 = s__AdditionFn(V__TIME1,s__MeasureFn(n__8,s__HourDuration)))))))
)
)

Merge.kif 1650516510 

( ! [V__SPEED,V__NUM] :
(((s__instance(V__SPEED,s__FunctionQuantity) &
s__instance(V__NUM,s__RealNumber))
=>
(((V__SPEED = s__MeasureFn(V__NUM,s__KnotUnitOfSpeed))
=>
((V__SPEED = s__SpeedFn(s__MeasureFn(V__NUM,s__NauticalMile),s__MeasureFn(n__1,s__HourDuration)))))))
)
)

Geography.kif 37783780 

( ! [V__FLOOD] :
((s__instance(V__FLOOD,s__FlashFlooding) =>
(( ? [V__WATER, V__HOUR] :
((s__instance(V__HOUR,s__RealNumber) &
(s__instance(V__WATER,s__WaterMotion) &
s__causes(V__WATER,V__FLOOD)
&
s__meetsTemporally(s__WhenFn(V__WATER)
,s__WhenFn(V__FLOOD))
&
s__duration(s__WhenFn(V__WATER)
,s__MeasureFn(V__HOUR,s__HourDuration))
&
s__lessThan(V__HOUR,n__6)))))))
)
)

Weather.kif 16291641 

( ! [V__HOUR] :
((s__instance(V__HOUR,s__Hour) =>
(s__duration(V__HOUR,s__MeasureFn(n__1,s__HourDuration))))
)
)

Merge.kif 89838985 

No TPTP formula. May not be expressible in strict first order. 
Weather.kif 11091123 

No TPTP formula. May not be expressible in strict first order. 
Weather.kif 26202633 

No TPTP formula. May not be expressible in strict first order. 
Weather.kif 29332948 
