# Why did Resolve[] fail to verify a statement whose counter-example was proven to be nonexistant by FindInstance[]?

I wanted to know whether the following statement is correct.

Let $$a$$, $$b$$, $$c$$, $$d$$ be positive real numbers such that $$abcd=1$$, then $$\frac{(3 a+1) (d-1)}{a+1}+\frac{(a-1) (3 d+1)}{d+1}+\frac{(3 b+1) (c-1)}{b+1}+\frac{(b-1) (3 c+1)}{c+1}\geq 0$$ always holds.

I tried to use FindInstance[] to find a counterexample,

FindInstance[{((a - 1) (3 d + 1))/(d + 1) + ((b - 1) (3 c + 1))/(
c + 1) + ((c - 1) (3 b + 1))/(b + 1) + ((d - 1) (3 a + 1))/(
a + 1) < 0, a b c d == 1}, {a, b, c, d}, PositiveReals]


The output came quickly and it was an empty list {}.

I then tried to use Resolve[] to verify it,

Resolve[ForAll[{a, b, c,
d}, {a b c d == 1}, ((a - 1) (3 d + 1))/(
d + 1) + ((b - 1) (3 c + 1))/(c + 1) + ((c - 1) (3 b + 1))/(
b + 1) + ((d - 1) (3 a + 1))/(a + 1) >= 0], PositiveReals]


But the evaluation lasted for a long time.

Why is it so?

• The software failed to evaluate the second code. The kernel quit for some reason (perhaps out of memory) Commented Aug 14 at 11:10

Do not use more variables than necessary. If you eliminate one variable using "a b c d ==1", Resolve evaluates quickly to True:

Resolve[ForAll[{a, b,
c}, ((a - 1) (3 d + 1))/(d + 1) + ((b - 1) (3 c + 1))/(c +
1) + ((c - 1) (3 b + 1))/(b + 1) + ((d - 1) (3 a + 1))/(a +
1) >= 0 /. d -> 1/(a b c)], PositiveReals]

True


One can work with four variables, considering the negation of the implication..

Resolve[Exists[{a, b, c, d},  a  b  c  d ==
1 && ((a - 1)  (3  d + 1))/(d + 1) + ((b - 1)  (3  c + 1))/(c +
1) + ((c - 1)  (3  b + 1))/(b +
1) + ((d - 1)  (3  a + 1))/(a + 1) < 0], PositiveReals]


False

Addition. In 14.1 on Windows 10

Resolve[ForAll[{a, b, c, d},  Implies[a b c d ==
1, ((a - 1) (3 d + 1))/(d + 1) + ((b - 1) (3 c + 1))/(c +
1) + ((c - 1) (3 b + 1))/(b + 1) + ((d - 1) (3 a + 1))/(a +
1) >= 0]], PositiveReals]


True

in few minutes.

• See Wiki concerning the negation of the implication. Commented Aug 14 at 13:30
• I'll try the code later. So Exists[] is more efficient than ForAll[]? Commented Aug 14 at 14:30
• @youthdoo: More exactly, the negation of the quantified implication appears simpler for Resolve than that implication. Commented Aug 14 at 14:54
In[1]:= Implies[a b c d ==
1, ((a - 1) (3 d + 1))/(d + 1) + ((b - 1) (3 c + 1))/(c +
1) + ((c - 1) (3 b + 1))/(b + 1) + ((d - 1) (3 a + 1))/(a +
1) >= 0]//BooleanConvert//InputForm

Out[1]//InputForm=
a*b*c*d != 1 || ((1 + 3*b)*(-1 + c))/(1 + b) + ((-1 + b)*(1 + 3*c))/(1 + c) +
((1 + 3*a)*(-1 + d))/(1 + a) + ((-1 + a)*(1 + 3*d))/(1 + d) >= 0


Hence you no longer have an equation that can be used to eliminate a variable. One more variable in an algorithm that is doubly exponential in the number of variables makes a difference.