pub fn answer_question(input: &str) -> Result<Vec<String>, ParseError>Expand description
ANSWER a wh-question theorem (“Given: … Prove: Who is a lawyer?”). A wh-goal
converts to ∃x.φ(x); the ANSWER is the witness. We find it the same way the
puzzle is meant to be solved — by the GENERAL kernel-certified prover, applied
per candidate: enumerate the domain individuals named in the premises and prove
each candidate goal φ(c); the c’s that prove are the answer (usually one, for a
puzzle with a unique solution). No question-specific reasoning — every step is
the same prove_certify_check that proves Socrates.