Why are there two different `until` ($\cup$) semantics in Timed Computation Tree Logic?
The two definitions are equivalent:

As you point out, the second one implies the first, as if $\phi$ holds, then clearly $\phi\vee \psi$ holds.

Conversely, consider a computation that satisfies the first definition, and assume by way of contradiction that it does not satisfy the second definition.
Thus, there exists some time in which $\psi$ holds, and in all previous times, $\psi\vee \phi$ holds. However, there also exists a previous time $d$ where $\psi\wedge \neg \phi$ holds, otherwise the second definition would hols.

Consider the minimal (or infimum) time $d$ for which this happens. Then in that time, $\psi$ holds, and in all previous times, $\psi\wedge \phi$ holds, so the second definition also holds for time $d$, which implies it for any later time.

Another way of looking on it: assume that the second definition doesn't hold, so either $\psi$ never holds, in which case clearly the first definition fails, or there is some minimal time $d$ where $\phi$ doesn't hold, and $\psi$ doesn't hold before $d$. In the latter case, $\phi\vee \psi$ also doesn't hold at time $d$, so the first definition doesn't hold.