This repository holds a solution to a puzzle first obtained with Prolog, and then verified with the Coq proof assistant.
Ten people (Adam, Cezary, Eliza, Hubert, Irena, Mateusz, Natalia, Sonia, Tadeusz and Urszula) took part in an online Tichu tournament and created 5 pairs.
In the finals of this tournament, the best 2 pairs met and a very interesting round took place, in which each of the four players received a single-color five-card sequence and one special card (Phoenix, Mah-jong, Dogs or Dragon). Each of the four sequences was of a different suit and started with a different card (with a "2", a "3", a "4" or a "5").
Based on the information provided, please determine the tournament pairs, which place each pair took in the tournament, and give the names of the players of the grand finale, their special cards and sequences.
- The Mateusz - Irena pair didn't take the third nor the last place.
- The sequences of both the woman with the Phoenix card, and the only male in the finals, did not start with a "4".
- Natalia was placed higher than Cezary, and Sonia higher than Tadeusz.
- In the winning mixed pair, Eliza had the Mah-jong and their sequences were not blue.
- The lowest sequence was neither red nor green.
- Tadeusz was paired with a woman, and Adam with a man.
- The highest sequence was black, the Dogs were owned by a person with a red sequence, and the sequence of the vice-champion Urszula was green.