# Using Boolean operators in FindInstance

The section on Boolean operators suggests that FindInstance can be applied to them. However, when I try to use it I get a rather confusing error:

Horses :=
(Result == 100 / Speed) &&
((Horse == 1) \[Equivalent] (Speed == 1)) &&
((Horse == 2) \[Equivalent] (Speed == 20))

Result = 5
FindInstance[Horses, {Horse}]


produces the dreaded not a quantified system of equations and inequalities error with no statement of which part is the problem.

Can I not use the relational operator Equivalent in FindInstance, or is what I'm trying to do generally invalid?

• The documentation of FindInstance suggests to me that it can solve satisfiability problems on Boolean statements which contain Boolean-valued variables (I.e. with a True/False value). Your case is trying to solve an algebraic equation with real-valued variables, expressed as a logical statement. I saw no indication that this is possible with FindInstance. Dec 17, 2019 at 4:21
• I saw a comment that <=> isn’t a valid operator. What I actually entered was ESC <=> ESC which I’m not sure how to represent on SO. I’m surprised if using the function call form alone fixes the problem. Dec 17, 2019 at 12:45

Horses := (Result == 100/Speed) &&Equivalent[(Horse == 1), (Speed == 1)] &&

• ... Also, adding && MemberQ[{1,2},Horse] to the Horses system makes it return no instances, even though the instance above makes that true also. Dec 17, 2019 at 20:39