Run on https://w4eg.de/malvin/illc/smcdelweb/index.html (see also https://lipsum.dev/2025-09-1-enigme-logique-epistemique/)

BlueEyedPuzzle.smcdel.txt

-- Boolean variables for "Agent i has blue eyes?"
VARS 1,2,3,4,5

LAW Top

-- Agents can see each other eyes, but not their own
OBS a: 2, 3, 4, 5
    b: 1, 3, 4, 5
    c: 1, 2, 4, 5
    d: 1, 2, 3, 5
    e: 1, 2, 3, 4

WHERE?
   -- Monday: Visitor announces seeing someone with blue eyes
   < ! (1 | 2 | 3 | 4 | 5) >
   -- Tuesday: Nothing special at noon.
   < ! (
         ~(a knows that 1)
         & ~(b knows that 2)
         & ~(c knows that 3)
         & ~(d knows that 4)
         & ~(e knows that 5)
      ) >
    -- Wesdnesday: Nothing special at noon.
    < ! (
         ~(a knows that 1)
         & ~(b knows that 2)
         & ~(c knows that 3)
         & ~(d knows that 4)
         & ~(e knows that 5)
      ) >
   -- Thursday: a, b, c commit suicide.
   (
      a knows that 1
      & b knows that 2
      & c knows that 3
      & ~(d knows that 4)
      & ~(e knows that 5)
   )

TRUE?
   {1, 2, 3}
   a knows that (1 | 2 | 3 | 4 | 5)
   & b knows that (1 | 2 | 3 | 4 | 5)
   & c knows that (1 | 2 | 3 | 4 | 5)
   & d knows that (1 | 2 | 3 | 4 | 5)
   & e knows that (1 | 2 | 3 | 4 | 5)

TRUE?
   {1, 2, 3}
   a knows that a knows that (1 | 2 | 3 | 4 | 5)
   & a knows that b knows that (1 | 2 | 3 | 4 | 5)
   & a knows that c knows that (1 | 2 | 3 | 4 | 5)
   & a knows that d knows that (1 | 2 | 3 | 4 | 5)
   & a knows that e knows that (1 | 2 | 3 | 4 | 5)

TRUE?
   {1, 2, 3}
   ~(a knows that b knows that c knows that (1 | 2 | 3 | 4 | 5))

TRUE?
   {1, 2, 3}
   ~((a, b, c, d, e) comknow that (1 | 2 | 3 | 4 | 5))