**I realized a problem with my 'counterexample', so I no longer claim that the desired inequality does not hold on $\mathrm{SO}(3)$. The proof that it does hold on the quaternions is still OK. I'll point out my error below and will explain how to use the proof for quaternions to prove the result for $\mathrm{SO}(3)$.**

The goal is to prove the inequality $\left\|\log(RS)\right\|\le\left\|\log(R)+\log(S)\right\|$ for all $R,S\in\mathrm{SO}(3)$ for which $\log(RS)$, $\log(R)$, and $\log(S)$ are defined. (In what follows, I'm taking the Frobenius norm to be $\|B\|^2 = \tfrac12\,\mathrm{tr}(B^TB)$, but this normalization clearly does not affect the argument.)

Notice that the function $B\mapsto \left\|\log(B)\right\|$ is actually a continuous function on $\mathrm{SO}(3)$, because of the easily checked identity
$$
\cos\bigl(\left\|\log(B)\right\|\bigr) = \tfrac12\bigl(\operatorname{tr}(B)-1\bigr)
$$
and the fact that $\cos^{-1}:[-1,1]\to[0,\pi]$ is a continuous, strictly decreasing function on $[-1,1]$. So even though $\log(B)$ is not defined when $\mathrm{tr}(B)=-1$, we can extend $\left\|\log(B)\right\|$ continuously (though not smoothly) to $\mathrm{SO}(3)$ by setting $\|\log(B)\|=\pi$ when $\mathrm{tr}(B)=-1$.

Thus, since the inequality trivially holds if $\left\|\log(R)+\log(S)\right\|\ge\pi$, one only needs to consider the cases where $\left\|\log(R)+\log(S)\right\|\le\pi$. **In this case**, because $\cos:[0,\pi]\to[-1,1]$ is a strictly decreasing function on $[0,\pi]$, the desired inequality is equivalent to
$$
\tfrac12\bigl(\operatorname{tr}(RS)-1\bigr)
\ge \cos\bigl(\left\|\log(R)+\log(S)\right\|\bigr).
$$

In my previous (flawed) analysis, I constructed $R$ and $S$ in $\mathrm{SO}(3)$ that violated this latter inequality. **However**, the example that I constructed has $\left\|\log(R)+\log(S)\right\| > \pi$, so it is *not* a counterexample to the original inequality.

I will now explain how one can prove the inequality after
a detour through the quaternions, where the analysis turns out to be easier. We do indeed have $\left|\log(pq)\right|\le \left|\log(p) + \log(q)\right|$
for unit quaternions $p$ and $q$ different from $-1$, so long as we make the convention that $\left|\log(-1)\right| = \pi$, even though $\log(-1)$ cannot be defined continuously.

Consider the quaternions $\mathbb{H}$, i.e., expressions of the form $q = x_0 + x_1\,i + x_2\,j + x_3\,k$, where the $x_i$ are real numbers and $i$, $j$, and $k$ satisfy the usual relations $i^2=j^2=k^2=-1$ and $ij-k=jk-i=ki-j=ji+k=kj+i=ji+k=0$. The *real part* of $q$ is $x_0$ and the *imaginary part* of $q$ is $x_1\,i + x_2\,j + x_3\,k$. As usual, set $|q| = (x_0^2+x_1^2+x_2^2+x_3^2)^{1/2}$. The unit quaternions $S^3\subset \mathbb{H}\simeq\mathbb{R}^4$ form a group. Write $\mathbb{H} = \mathbb{R} \oplus \mathrm{Im}\mathbb{H}$, where $\mathrm{Im}\mathbb{H}\simeq\mathbb{R}^3$ is the quaternions with vanishing real part.

If $u$ is a unit imaginary quaternion then $u^2=-1$, so that, when $a$ is real, we have $\exp(a\,u) = \cos a + \sin a \,u$. Every unit quaternion $q$ other than $-1$ is of the form $\exp(x)$ for some *unique* purely imaginary quaterion $x$ with $|x|<\pi$. Then setting $x := \log q $ defines $\log$ as a smooth function on the unit quaternions minus the single element $-1$. Note that $\left|\log q \right|) = |x| = |a|$, so $\cos\bigl(\left|\log q\right|\bigr) = \cos a $, which is the real part of $q$.

Suppose that $q = \cos a + \sin a \,u$
while $p=\cos b + \sin b \,v$ where $0\le a,b<\pi$ and $u$ and $v$ are unit quaternions, with $u\cdot v = \cos c$ for some $c$. Note that the real part of $uv$ is $-\cos c$. Thus, we have the product expansion
$$
qp = (\cos a + \sin a \,u)(\cos b + \sin b \,v)
= (\cos a\cos b-\sin a\sin b\cos c) + X
$$
where $X$ is imaginary. Thus
$$
\cos\bigl(\left|\log(qp)\right|\bigr) = (\cos a\cos b-\sin a\sin b\cos c).
$$
Meanwhile
$$
\left|\log q + \log p\right| = |au+bv| = \sqrt{a^2+2ab\cos c+b^2}.
$$

Since $\left|\log(qp)\right|\le\pi$, in order to verify the inequality $\left|\log(qp)\right|\le \left|\log q + \log p\right|$, one only needs to deal with the cases in which $0\le \left|\log q + \log p\right|\le \pi$, which may as well be assumed. In this case, since $\cos$ is a strictly decreasing function on the interval $[0,\pi]$, the inequality $\left|\log(qp)|\le \right|\log q + \log p|$ is equivalent to $\cos\bigl( \left| \log(qp) \right| \bigr)\ge
\cos\bigl(\left|\log q + \log p\right|\bigr)$, i.e.,
$$
(\cos a\cos b-\sin a\sin b\cos c)
\ge \cos\bigl(\sqrt{a^2+2ab\cos c+b^2}\bigr).
$$
Now, it can be shown that this inequality does indeed hold for all $c$ and all $a$ and $b$ with $|a|,|b|<\pi$ (not just when $a^2+2ab\cos c+b^2\le \pi^2$). (In fact, by continuity, it holds for $|a|,|b|\le \pi$ and all $c$. Moreover, equality holds in this range of the variables only when $a=0$, $b=0$ or $\cos c = \pm 1$.)
[A proof of the above inequality goes as follows: Let
$$F(a,b,t)=
\cos a\cos b-t \sin a\sin b-\cos\bigl(\sqrt{a^2+2abt+b^2}\bigr).
$$
Then $F$ is an analytic function on $\mathbb{R}^3$ that vanishes when $a=0$, $b=0$ or $t=\pm 1$. Since $F(-a,b,-t)=F(a,-b,-t)=F(a,b,t)$ it suffices to prove the inequality for $0<a,b<\pi$.
So fix such $a$ and $b$ and note the easily proved fact that, as a function of $t$, $F(a,b,t)$ vanishes at $t=\pm 1$ and has at most one critical point in the range $|t|<1$. (Just look at $F_t(a,b,t)$.) Thus, $F(a,b,t)$ cannot vanish or change sign when $|t|<1$. Now show that $F(a,b,0) = \cos a\cos b-\cos\bigl(\sqrt{a^2+b^2})$ is positive for small $a,b>0$ (by Taylor expansion). Since $F(a,b,0)$ can never vanish when $0<a,b<\pi$, it must be positive for all such $a,b$, and hence $F(a,b,t)$ must be positive when $|t|<1$.]

Thus, the desired inequality $\left|\log(qp)\right|\le \left|\log q + \log p \right|$ follows.

(Note that $qp=-1$ would imply that $p=-\bar q$, so $\cos(a)+\cos(b)=0$ and $\sin a\,u=\sin b\,v$. But then $|\sin a|=|\sin b|$. This forces $a+b = \pi$ (since we can assume that $0\le a,b <\pi$) and $u=v$, i.e., $c=0$. Thus, the inequality holds even when $\log (qp)$ does not exist.)

To deal with the case of $\mathrm{SO}(3)$, make use of the double covering homomorphism $\rho:S^3\to\mathrm{SO}(3)$ defined by
$$
\rho(q)(x) = q x \bar q
$$
for $q\in S^3$ and $x\in \mathrm{Im}\mathbb{H}$. The homomorphism $\rho$ maps the unit quaterions with positive real part diffeomorphically onto the elements of $\mathrm{SO}(3)$ with trace greater than $-1$.

One then finds that $\log(\rho(q)) = \mathrm{ad}(\log q)$, and this allows one to use the inequality $\left|\log(qp)\right|\le \left|\log q + \log p \right|$ to show the desired inequality
$$\left\|\log(RS)\right\|\le\left\|\log(R)+\log(S)\right\|$$ for all $R,S\in\mathrm{SO}(3)$ for which $\log(RS)$, $\log(R)$, and $\log(S)$ are defined.

5more comments