Prove this inequality via weighted Jensen inequality The following inequality is derived from this difficult olympiad problem.
Suppose $a,b,c$ are three positive real numbers such that $abc = 8$, show that
$$\frac{1}{\sqrt{a + 1}} + \frac{1}{\sqrt{b + 1}} + \frac{1}{\sqrt{c + 1}} < 2$$
My idea: Note that $\sqrt{x}$ is a concave function on $(0,\infty)$. Let $x,y,z,p,q,r$ be any positive real numbers, then according to weighted Jensen inequality we have
$$\begin{aligned}\sqrt{x} + \sqrt{y} + \sqrt{z} &= \frac{\sqrt{p^2x}}{p} + \frac{\sqrt{q^2y}}{q} + \frac{\sqrt{r^2z}}{r}\\&\leq\sqrt{\left(\frac{1}{p} + \frac{1}{q} + \frac{1}{r}\right)(px + qy + rz)}\end{aligned}$$
Let $x = a,y = b,z = c = \frac{8}{ab}$. If we can find appropriate weights $p,q,r$ such that
$$\left(\frac{1}{p} + \frac{1}{q} + \frac{1}{r}\right)(px + qy + rz) < 4$$
then we are done.
Now if I ask Mathematica
Reduce[ForAll[a, a > 0, ForAll[b, b > 0, Exists[{p, q, r}, p > 0 && q > 0 && r > 0 && (1/p + 1/q + 1/r) (p/(1 + a) + q/(1 + b) + r/(1 + 8/(a b))) < 4]]]]

Mathematica returns True in less than 2 seconds(!!). However, it provides no more details other than a truth value.
If I ask instead
Reduce[ForAll[a, a > 0, ForAll[b, b > 0, Exists[{p, q, r}, p > 0 && q > 0 && r > 0 && (1/p + 1/q + 1/r) (p/(1 + a) + q/(1 + b) + r/(1 + 8/(a b))) < m]]], m]

Mathematical returns m >= 4, although using much longer time.
Which algorithm does Mathematica use to verify the proposition? It is certainly not cylindrical algebra, for CylindricalDecomposition takes much much longer.
Can we find simple expressions for $p,q,r$ that would complete the proof?
Update: I have found a way to carry out quantifier elimination by hand. Therefore the first part of this problem is solved.
 A: The Contradiction method works! 
Let $\frac{1}{\sqrt{a+1}}=p,$ $\frac{1}{\sqrt{b+1}}=q$ and $\frac{1}{\sqrt{c+1}}=r.$
Thus, $\{p,q,r\}\subset(0,1),$ $\frac{(1-p^2)(1-q^2)(1-r^2)}{p^2q^2r^2}=8$ and we need to prove that:
$$p+q+r<2.$$
Indeed, let $p+q+r\geq2,$ $r=kr'$ such that $k>0$ and $p+q+r'=2$.
Thus, $$p+q+kr'\geq2=p+q+r',$$ which gives $k\geq1.$
Thus, $$8=\frac{(1-p^2)(1-q^2)}{p^2q^2}\cdot\left(\frac{1}{k^2r'^2}-1\right)\leq\frac{(1-p^2)(1-q^2)}{p^2q^2}\cdot\left(\frac{1}{r'^2}-1\right),$$ which is a contradiction because we'll prove now that
$$8>\frac{(1-p^2)(1-q^2)}{p^2q^2}\cdot\left(\frac{1}{r'^2}-1\right).$$
Indeed, we need to prove that
$$8p^2q^2r'^2>(1-p^2)(1-q^2)(1-r'^2)$$ or
$$512p^2q^2r'^2>((p+q+r')^2-4p^2)((p+q+r')^2-4q^2)((p+q+r')^2-4r'^2)$$ or
$$512p^2q^2r'^2>(3p+q+r')(3q+p+r')(3r'+p+q)(p+q-r')(p+r'-q)(q+r'-p).$$
Now, if $(p+q-r')(p+r'-q)(q+r'-p)\leq0$, so our inequality is true, which says that it's enough to prove it for $(p+q-r')(p+r'-q)(q+r'-p)>0$.
Also, if $p+q-r'<0$ and $p+r'-q<0,$ so $p<0$, which is a contradiction.
Thus, we can assume that $p+q-r'=z>0,$ $p+r'-q=y>0$ and $q+r'-p=x>0$, which gives
$p=\frac{y+z}{2},$ $q=\frac{x+z}{2},$ $r'=\frac{x+y}{2}$ and we need to prove that
$$8(x+y)^2(x+z)^2(y+z)^2>xyz\prod_{cyc}(x+2y+2z),$$
which is obviously true after full expanding.
Done!
It's interesting that even the following is true.

Let $x$, $y$ and $z$ be non-negative numbers. Prove that:
  $$125(x+y)^2(x+z)^2(y+z)^2\geq64xyz(x+2y+2z)(2x+y+2z)(2x+2y+z).$$

A: Update: This problem turned out to be simple enough that quantifier elimination can be carried out "by hand" (with CAS software, of course).
I found a way to solve it.
Remember that the goal is to prove $\forall a > 0, b > 0$ there exists $p > 0, q > 0, r > 0$ such that
$$\left(\frac{1}{p} + \frac{1}{q} + \frac{1}{r}\right)\left(\frac{1}{a + 1} + \frac{1}{b + 1} + \frac{1}{\frac{8}{ab} + 1}\right) < 4$$
Reducing the LHS (using Mathematica!), we get
$$\frac{(8 p + 8 b p + a b p + a b^2 p + 8 q + 8 a q + a b q + a^2 b q + 
     a b r + a^2 b r + a b^2 r + a^2 b^2 r) (p q + p r + q r)}{(1 + 
     a) (1 + b) (8 + a b) p q r} < 4$$
Now move the denominator to the RHS, and subtract RHS from both sides, we get
$$F(a,b,p,q,r) < 0$$
where $F$ is an enormous polynomial. Now put $q = k_1 p, r = k_2p$, and define $G = F/p^3$. $G$ is also a polynomial, and depends only on $a,b,k_1,k_2$. In fact, $G$ is a quadratic function in $k_1$. Assume that
$$G = Uk_1^2 + Vk_1 + W$$
We can easily see that $U > 0,W > 0$. Therefore the following constraints guarantee the existence of a positive $k_1$ such that $G < 0$:
$$\left\{\begin{aligned}\Delta = V^2 - 4UW &> 0\\V &< 0\end{aligned}\right.$$
Furthermore, this set of inequalities depend only on $a,b,k_2$. From now on we use techniques from algebra.
1) $V$ is a quadratic function in $k_2$. Assume that
$$V = Ak_2^2 + Bk_2 + C$$
We can easily see that $A > 0,B < 0,C > 0,\Delta_V = B^2 - 4AC > 0$. Therefore for any positive $a,b$ there are two positive real numbers $w_1,w_2$ such that
$$V < 0 \Leftrightarrow w_1 < k_2 < w_2$$
2) $\Delta$ is a quartic function in $k_2$. Assume that
$$\Delta = z_0k_2^4 + z_1k_2^3 + z_2k_2^2 + z_3k_2 + z_4$$
We can easily see that $z_0 > 0,z_1 < 0,z_2 > 0,z_3 < 0,z_4 > 0$. Therefore all real roots of $\Delta$ are positive.
3) Let $\Delta'$ be the derivative of $\Delta$ w.r.t. $k_2$. The resultant of $\Delta,\Delta'$ is always positive. Thus $\Delta$ has no repeated roots.
4) Using Sturm's theorem, we can easily see that $\Delta$ has four distinct real roots. Let them be $r_1,r_2,r_3,r_4$, ordered from smallest to largest.
5) The resultant of $\Delta,V$ is always positive. Thus $\Delta$ and $V$ have no common roots.
6) We now use Tarski's theorem to calculate the Cauchy index of $\Delta'V/\Delta$ and $V'\Delta/V$. It turns out that the Cauchy index of $\Delta'V/\Delta$ is always $0$, and that of $V'\Delta/V$ always $-2$. From here we can deduce that
$$0 < r_1 < w_1 < r_2 < r_3 < w_2 < r_4$$
Therefore if we take any $r_2 < k_2 < r_3$, we can guarantee that $\Delta > 0,V < 0$.
Done.
