diff --git a/docs/analysis/cryptanalysis/report-mixer-3.md b/docs/analysis/cryptanalysis/report-mixer-3.md
index 06a300705..973bf1f29 100644
--- a/docs/analysis/cryptanalysis/report-mixer-3.md
+++ b/docs/analysis/cryptanalysis/report-mixer-3.md
@@ -31,7 +31,7 @@ Plant rule: a tool is trusted once it has fired on a known-failed shape. Which s
 | Q4 | single-bit linear correlations, random states, 2^26 samples | k = 0 (the identity, fired: c = 1.0 on the diagonal) | no cell beyond 6 sigma (band 0.00073) | day 20729 k = 1..7 and day 20733 k = 1..8: worst c between 0.00055 and 0.00062 (z 4.5 to 5.1; the expected maximum of 262,144 normals is 4.8), 0 cells beyond 6 sigma on every row; day 20729 k = 8 running | PASS from k = 1 (BOUND) |
 | Q4b | t-bit linear correlations on the round-0 input, 2^26 samples | k = 0 (fired: c = 1.0, t bit 0 to s[8] bit 0) | no cell beyond 6 sigma | both days, k = 1..8: worst c 0.00046 to 0.00059 (z 3.7 to 4.9 over 16,384 cells), 0 cells beyond 6 sigma | PASS from k = 1 (BOUND) |
 | Q5 | rotational-XOR, rotations 1, 8, 16, 2^22 samples | `weak0` at k = 1 (fired: 740 zero-difference words of 2^20 at r = 1, 245 at r = 16) | no zero-difference word above 2 of N, no repeated difference above 3 | both days, k = 1, 2, 3, 4 at 2^22 samples: 0 zero-difference words at every rotation (random expects about 0.001), most frequent per-word difference multiplicity 3 (the birthday expectation at 2^22 draws of 32 bits) | PASS from k = 1 (BOUND: the XOR constants and the odd multiply kill the rotational property inside one application) |
-| Q6 | SAT (CaDiCaL) on the round-0 input: find t with a given 22-bit index after k applications | k = 1 solved and verified | solve inside one hour per k, time against the honest 2^10 x k x 130 ops | k = 1: SATISFIABLE in 137 s wall on build-1 (load about 160) and 1,593 s on build-2 (load about 500), the same model t = 0x49880000 both times, verified to the target 0x20eb79 through the real code; k = 2: TIMEOUT at the one-hour cap (68,624 vars, 227,767 clauses); k = 3: TIMEOUT (103,375 vars, 343,206 clauses). Honest: 2^10 trials is under a millisecond at every k | PASS at k = 1, 2, 3 (BOUND: no SAT shortcut, the solver loses to brute force at k = 1 and does not return at k = 2 or 3); k = 4 RUNNING under the cap |
+| Q6 | SAT (CaDiCaL) on the round-0 input: find t with a given 22-bit index after k applications | k = 1 solved and verified | solve inside one hour per k, time against the honest 2^10 x k x 130 ops | k = 1: SATISFIABLE in 137 s wall on build-1 (load about 160) and 1,593 s on build-2 (load about 500), the same model t = 0x49880000 both times, verified to the target 0x20eb79 through the real code; k = 2: TIMEOUT at the one-hour cap (68,624 vars, 227,767 clauses); k = 3: TIMEOUT (103,375 vars, 343,206 clauses); k = 4: TIMEOUT (138,126 vars, 458,645 clauses). Honest: 2^10 trials is under a millisecond at every k | PASS at k = 1..4 on day 20729 (BOUND: no SAT shortcut, the solver loses to brute force at k = 1 and does not return at k = 2, 3 or 4 inside an hour); day 20733 k = 2..4 RUNNING under the cap |
 | Q7 | days: 20733 on every row, 8 fixed day indices on Q1 and Q2 (queue 07, run by the sibling adv-mixer from the shared queue) | as above | as above | day 20733: every row above; day 20730: index uniform at k = 2, 3, 4, 8, sac clean at k = 2, 3; the other seven days pending in queue 07 | RUNNING |
 | GPU | any GPU row | n/a | n/a | no GPU on either box | BLOCKED |
 
@@ -270,7 +270,8 @@ under a millisecond on one core. The solver at k = 1 is five orders slower than
 | 20729 | 1 (queue 08, build-2) | 33,873 | 112,328 | SATISFIABLE | 1,593 s (box at load 500) | the same t |
 | 20729 | 2 | 68,624 | 227,767 | TIMEOUT at the one-hour cap (rc 124), 91.8 MB | 3,600 s | none |
 | 20729 | 3 | 103,375 | 343,206 | TIMEOUT at the one-hour cap (status 124), 149 MB | 3,600 s | none |
-| 20729 | 4 | 138,126 | 458,645 | running since 22:41 UTC (one-hour cap) | | |
+| 20729 | 4 | 138,126 | 458,645 | TIMEOUT at the one-hour cap (status 124), 175 MB | 3,600 s | none |
+| 20733 | 2, 3, 4 | as above (the same shape, the day's constants) | | queued from 23:41 UTC, one-hour cap each | | |
 
 Reading: the one-application model is a 32-variable problem with 112 k clauses of ripple-carry adders (16
 constant multiplies of up to 32 adders each dominate). CaDiCaL needs minutes on it where the honest search needs
@@ -321,7 +322,7 @@ and the 72 per item, on the two real days 20729 and 20733:
 | Single-bit linear correlation (Q4, Q4b), band 0.00073 | no | no | 8 | 72 |
 | Rotational-XOR (Q5), 2^22 samples | no | no | 8 | 72 |
 | Round-0 line-index histogram over all 2^32 t (Q1) | no (uniform from k = 1, through k = 8) | no | 8 | 72 |
-| SAT preimage of the round-0 line index (Q6) | k = 1 solved, 137 s, five orders slower than the honest 2^10 trials | timeout at one hour | not a shortcut at any k | |
+| SAT preimage of the round-0 line index (Q6) | k = 1 solved, 137 s, five orders slower than the honest 2^10 trials | timeout at one hour (k = 2, 3 and 4 alike) | not a shortcut at any k | |
 
 Every statistic that reaches k = 1 is the lowest-set-bit trail through one application (the mechanism in Q2);
 none reaches k = 2 at the bands above. The bound: no distinguisher in this pass survives 2 of the 8 keyed