# A simple expression on which Reduce fails

The conditions in x ∉ Integers && y ∈ Integers && y == -(1/2) + x/2 are inconsistent but Reduce does not solve it (I expected False):

cond = x ∉ Integers && y ∈ Integers && y == -(1/2) + x/2;
Reduce[cond, {x, y}]
(*  x ∉ Integers && y ∈ Integers && y == -(1/2) + x/2  *)


I thought that odd, since the proof is simple. I thought I might check that my brain was working correctly by asking for an instance when it's true. To my surprise, FindInstance returned a candidate (a bug apparently), but of course the candidate makes the condition false:

FindInstance[cond, {x, y}]
cond /. %
(*
{{x -> 3909, y -> 1954}}
{False}
*)


It turns out that Reduce can solve an equivalent problem (although FindInstance produces the same spurious result):

Reduce[x ∉ Integers && y ∈ Integers && x == 1 + 2 y]
(*  False  *)


This equivalent condition can be produced with Simplify[cond], but I wanted to avoid (Full)Simplify because some of the transformations are only generically true.

Question: Is there a way to get Reduce or an equivalently rigorous reduction to produce False? The condition cond arose programmatically, so I don't have much control over its form.

• Since there seems to be a bug with FindInstance, I should probably add that I'm using V11.3.0 (Jan 22, 2018), Mac OS. I can add it to the question, if it turns out to be important. – Michael E2 Aug 10 '18 at 16:48
• Reduce[cond] works in place of Reduce[cond, {x, y}]....I guess I'll delete, unless someone argues this would be valuable Q&A. – Michael E2 Aug 10 '18 at 16:58
• Reduce[cond, {y, x}] works, too. It's solving for y first that is the problem (Reduce[cond, {y}] fails). – Michael E2 Aug 10 '18 at 17:05
• Earlier NotElement oddity: mathematica.stackexchange.com/questions/105511/… – kirma Aug 11 '18 at 7:58
• And, FindInstance[cond, {y, x}]  returns an empty list, as it should. – bbgodfrey Aug 12 '18 at 2:17