Before the main activity: choose which logic engine solves the puzzle underneath, and which set of clues you'll be working from. Every combination shares the same interface below — only the engine doing the real work, and the specific clues, change.
1. Choose an engine
2. Choose a clue-set
The iGEM Chronology Puzzle
Clues
What's known so far
Year
Country
Organism
Project
Award
Engine trace (last action)
No action taken yet.
Action-effect log
Every clue application, in order, and every fact it revealed — including facts revealed again after already being known. The first time any fact is revealed is bolded.
Fitch proof (FitchFX, driven by the engine)
This is a genuine, independent, unmodified open-source Fitch-style proof
system — FitchFX (MIT license, github.com/mrieppel/FitchFX), embedded below
exactly as published. Unlike ndt93/Proof-Editor (used in earlier versions), it supports real
first-order logic, including quantifier rules (∀-Elim, ∀-Intro, ∃-Elim, ∃-Intro)
with proper name-flagging and subproof handling — not just propositional atoms.
For clue-set A only, applying one of the 13 "simple" clues below (a single universal
premise plus one already-known fact) automatically translates that real derivation into FitchFX's
plain-text proof format and imports it — FitchFX's own parser and rule-checker validate it, and
FitchFX's own renderer draws it. The organism-year block and a few other clue types aren't translated
yet (see the note above the clue list for which).
Notation legend (for reference)
All clues, in FOL
Derivations available to view as a Fitch proof
Apply a translatable clue in clue-set A above to see it here.