feat: make `grind` diagnostics opt-in via `+verbose`

This PR changes the default of the `grind` option `verbose` to `false`, which also applies to `lia`, `cutsat`, `grind_linarith`, `grind_order`, and `grobner`. Failures now show only the remaining goal and the hint `use `+verbose` to obtain diagnostic information`. Collecting and printing diagnostics took about 38% of the time spent on easy failing `lia` goals.

In interactive mode (`grind => ...`), solver steps no longer print their state, and solver model traces require `+verbose`. `grind?` is unchanged.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>