fix(provers): correct EProver '#'→'%' prefix bug and Z3 get-value parsing bug; add proof_failure diagnostics

EProver uses '%' as its output comment prefix (TPTP convention), not '#'
(shell convention). parse_result was checking '# SZS status ...' so every
EProver result came back inconclusive. Tests updated to match real output.

Z3's parse_smt_result took the last non-empty line as the check-sat answer.
When a (get-value ...) follows the final (check-sat), the last line is a
model term like '(found_2 0))' — not 'sat'/'unsat'. Fixed to scan backward
for the last line that is exactly one of the three answer tokens, skipping
model/value output.

Adds src/rust/diagnostics/proof_failure.rs: a new DiagnosticReport type
with FailureKind taxonomy (ParseMismatch, BackendBug, UnsolvedGoal, TypeError,
SyntaxError, OutOfScope, Timeout, ProverCrash, Satisfiable, ConfigError,
Unknown), per-prover output parsers for EProver/Z3/CVC5/Coq/Agda/Lean/Idris2/
Vampire, location extraction, human-readable display, and A2ML serialisation.
11 unit tests all pass.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

src/rust/diagnostics/mod.rs

@@ -4,7 +4,9 @@
 pub mod corpus_monitor;
 pub mod health;
 pub mod gnn_training;
+pub mod proof_failure;
 
 pub use corpus_monitor::{CorpusMetrics, CorpusMonitor};
 pub use health::{HealthStatus, ProverHealth, ModelHealth, CorpusHealth, DegradationMode};
 pub use gnn_training::{GnnTrainingMetrics, load_training_metrics, update_health_with_metrics};
+pub use proof_failure::{diagnose, DiagnosticReport, FailureKind, SourceLocation};