# Resolve Error or Mathematica's Bug?

The following code,

    Resolve[Exists[{n1, n2, n3}, {n1, n2, n3} \[Element]
NonNegativeIntegers,
1/2 (1 + n1 + n2 - n3) \[Element] NonPositiveIntegers]]


gives output True but if I run LaunchKernels[] and then rerun the exact same code above then the output is

Exists[{n1, n2, n3}, Element[n1 | n2 | n3, Integers] &&
n1 >= 0 && n2 >= 0 && n3 >= 0,
Element[(1 + n1 + n2 - n3)/2, Integers] &&
(1 + n1 + n2 - n3)/2 <= 0]



So is this a bug of Mathematica?

Moreover, I also tried to evaluate a similar code.

Resolve[Exists[{n1, n2, n3}, {n1, n2, n3} \[Element]
NonNegativeIntegers,
1/2 (1 + n1 - n2 + n3) \[Element] NonPositiveIntegers]]


where n2 and n3 is swapped. But then the output is True both before and after LaunchKernels[].

So what is the precise reason for this abnormal behavior? Any idea how to solve it?

Note: If we use Reduce instead of Resolve, it will not help.

In[2]:= Resolve[Exists[{n1, n2, n3}, {n1, n2, n3} \[Element] NonNegativeIntegers , (1 + n1 + n2 - n3)<=0 && Mod[1 + n1 + n2 - n3, 2]==0]]//Timing

• Thanks a lot for this precise answer. I tried to check (out of curiosity) if Divisible[1 + n1 + n2 - n3, 2] instead of Mod[1 + n1 + n2 - n3, 2]==0 works or not. But it does not work and cannot give the output True. Do you know why this happens? Because Divisible[] and Mod[]==0 are equivalent statements. – Epsilon Nov 3 '20 at 21:37