See https://news.ycombinator.com/item?id=21543377 discussion

Hackernews puzzle.py

import z3
answers = [z3.Bool(f"answer{i}") for i in range(1,7)]
implications = [
  z3.And(answers[1:]),         # All of the below
  z3.Not(z3.Or(answers[2:])),  # None of the below
  z3.And(answers[:2]),         # All of the above
  z3.Or(answers[:3]),          # Any of the above
  z3.Not(z3.Or(answers[:4])),  # None of the above
  z3.Not(z3.Or(answers[:5]))]  # None of the above

# An answer should be True if and only if its "implication" is true
constraints = [ans == impl for ans, impl in zip(answers, implications)]

z3.solve(constraints) # Prints the right solution


# Try to find another solution by rejecting the previous one
constraints.append(z3.Or(*answers[:4], z3.Not(answers[4]), answers[5]))
z3.solve(constraints) # no solution