There are 4 fair coins and 5 men. Each of the men picks a number that he believe will be the number of heads in total after 4 flips. Each man has a different number picked.

The story goes like this:

- First coin is flipped => man #2 announces that he lost
- Second coin is flipped => man #0 announces that he lost; man #3 announces that his chances to win decreased a lot
- Third coin is flipped => man #3 announced that he lost; man #1 believe that he can still win
- Fourth coin is flipped and is revealed to be tails => man #4 is the winner (man #1 loses)

A declaration of loss means that a man cannot win i.e. his picked number of heads is impossible to obtain. A win means that the total number of heads after four flips is exactly matching a picked integer.

What needs to be inferred:

- Each men's pick (total number of heads)
- Coin state for flip 1, 2 and 3 (flip 4 is observed).

Here I assume "heads" = "True" and "tails" = "False".

I have couple of questions here:

- How to encode that each man's pick is distinct (an integer from range 0 to 4)?
- How to encode an event such as "man #3 announces that his chances to win decreased"?
- How to encode an event of loss/win for a particular man?
- Coin flips need to be counted, my idea was to use a VariableArray<bool>. I realized that the last coin flip is observed and this cannot done with only one element of an array. Is there a way to count total number of heads from separate variables?

I found the puzzle on stackexchange to be interesting. Even though Infer.NET is overkill for this sort of problem, I asked myself whether I could write this model and do the inference in it.