adv-mixer: cadical lease released for the class v5 census; ledger and SAT row updated

Internal adversarial pass, not an independent review.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

docs/analysis/cryptanalysis/report-mixer.md

@@ -240,8 +240,11 @@ outcome inside the hour: the instance is a preimage-shaped search on a 2^512 spa
 reach only and is no evidence either way. The CNF stays on box 2 at
 /srv/builds/_adv-adv-mixer/logs/adv-mixer-commute-20729.cnf (6.8 MB) for a re-queue through `lease pool` once
 that subcommand exists (at 20:21 BST `lease --help` offered `lease cores` and `lease status` only). Re-queued
-through `lease pool 1` at 20:22 BST the minute the subcommand landed (log sat-commute-20729-lease.log); RUNNING
-under a fresh one-hour cap; the row lands here.
+through `lease pool 1` at 20:22 BST the minute the subcommand landed (log sat-commute-20729-lease.log), then
+RELEASED at 20:41 BST on main's order so the class v5 census (owner class-v5, 88 cores, the 0.3.24 critical path)
+can take box 2's pool: 1,106 s run, no SAT or UNSAT. Two cadical runs total 2,855 s of solving on this instance
+with no decision, which is the expected shape for a preimage-sized search. Status: BLOCKED on pool priority, to
+be re-queued after the census is confirmed running.
 
 ## Q1 consolidated verdict (internal adversarial pass, not an independent review)
 
@@ -316,6 +319,7 @@ wall times above are under heavy sharing.
 | 19:3x | drop SIGSTOP yield, run on cores 8-95 only | no yield was ever added; run-box.sh band set to 8-95; direct nohup runs at nice 10 |
 | 20:20 | main: every hand-started sweep is killed by its pid file now and re-queued through `lease pool`; release builds and the class v5 suites outrank sweeps | killed cadical (box 2, 29 min lost, no result) and sibling 07 (box 1, 6 of 56 steps done, claim released); nothing started since; `lease pool` absent at 20:21, so the re-queue waits on it |
 | 20:22 | `lease pool` live on both boxes (lease sha f814b447) | cadical re-queued the same minute through `lease pool 1 --owner adv-mixer --nice 10`, core 8, 1 h cap |
+| 20:41 | main: box 2's pool must show 0 adv-* holders for the class v5 census; the yield to a class-v5 waiter is mechanical at shard end from now | released the cadical lease by pid file; nothing held on either box |
 | 20:2x | pool rule: a sweep lease asks for at most 48 cores with --min at the least usable; the yield test is by OWNER (refined at 20:3x): yield to a waiter whose owner is class-v5, or whose owner is attack-pass with "v5" in its label, never to a waiter whose owner starts with adv-; on a yield, finish the shard in hand and release; release builds and v5 suites outrank every sweep | adopted for any further lease; the one-core cadical lease is cleared by main to its 21:23 BST cap |
 
 ### Kill ledger (main's rule, 20:20 BST)
@@ -324,6 +328,7 @@ wall times above are under heavy sharing.
 |---|---|---|---|---|---|
 | cadical on adv-mixer-commute-20729.cnf | 2 | sat-commute-20729.log.pid | 19:20:41Z | 1,749 s of a 3,600 s cap, no SAT or UNSAT | RE-QUEUED 19:22:46Z (20:22 BST) through `lease pool 1 --owner adv-mixer --nice 10` the minute the subcommand landed; holding 1 pool core, 1 h cap; pid file sat-commute-20729-lease.log.pid |
 | 07-adv-mixer-3-days.sh (owner adv-mixer-3) | 1 | queue-07-adv-mixer-3-days.sh.log.pid | 19:20:47Z | 50 of 56 steps unrun; the 6 done are in the owner's logs | claim released; owner or next free lane |
+| cadical, the leased re-run (lease pool 1, core 8) | 2 | sat-commute-20729-lease.log.pid | 19:41:11Z (20:41 BST), main's order so the class v5 census takes box 2's pool | 1,106 s of a fresh 3,600 s cap, no SAT or UNSAT; 2,494 s of cap lost | re-queue through `lease pool 1 --min 1` after main confirms the census is running; the yield to class-v5 waiters is mechanical from now |
 
 Both kills were the wrapper pid from the pid file plus its descendants (one cadical, one adv-mixer-3), TERM then
 KILL; no process of this lane remained on either box afterwards.