Universal (meta-)logical reasoning: The Wise Men Puzzle (Isabelle/HOL dataset) Academic Article