Version 0.42. A real Fitch-style proof: single uppercase predicate letters (Country, Organism, Title, Award), grounded facts written with the year as a subscript (e.g. C₂₀₂₃(HK)), ∀-Elimination and Modus Ponens shown as two separate lines, and genuine nested Fitch boxes for the reductio arguments that pin down the organism years. Six background axioms (bijectivity of each relation, unique names, and the total order on years) sit alongside the 23 clues as premises — nothing here is derivable, they're assumed.
| Year | Country | Organism | Project | Award |
|---|
Clues 1–5 have no prerequisites of their own — apply them in whatever order you like. (Clue 1 does need to happen at some point before you try the case analysis below, since it's what rules out peptide-sensor bacteria landing anywhere but the last slot — but it doesn't have to be your first click.)
Same lines, same numbers, in prose. For the four reductio arguments below, we just say "by reductio ad absurdum" rather than re-explaining the mechanics of proof-by-contradiction each time.