*Post by Charlie-Boo*I have 5 nonnegative real number variables: A B C M N

1. A + B + C = 10

2. A <= M <= A + C

3. B <= N <= B + C

4. M + N = 5

5. B < 2

Here;s hg9ow you find the answer -- automatically.

(1) Generate a large random set of values for (A,B,C,M,N).

(2) For each combination, produce a 5-bit value based on the yes/no answer to 1, 2, 3, 4, 5 for that combination.

(3) Sort the 5-bit values (and eliminate redundancies)

(4) For each value produce the corresponding boolean expression; e.g. (1 yes, 2 no, 3 yes, 4 yes, 5 no would yield I and not II and III and IV and not V).

(5) Let E0, E1, E2, ... be the expressions formed as a result. Take their disjunction E = E0 or E1 or E2 ...

(6) Convert this to disjunctive normal form. The result is an expression of the form E = F0 and F1 and F2 and ..., where each F has a form, such as (not I or not II or not III or IV or V).

Each F is a relation that probably holds between the statements; e.g. not I or not II or not III or IV or V is the conditional: (I and II and III -> IV or V).

Establish each statement F0, F1, F2, ... with a theorem prover (or by hand) .. or seek out a counter example by generating more combinations of (A, B, C, M, N).

There is a way to DIRECTLY incorporate a counter-example into an update of the list of F's; but I won't go into it here.

Prover9 (theorem prover)/Mace 4 (model finder) can be used to find proofs and models. https://www.cs.unm.edu/~mccune/mace4/