> we tried a few alternatives to Wilkies and didn't find smaller countermodels.

I wish you spent at least a couple words in the paper about that. Even negative results are worth documenting! (even if you didn't get up to size 11, I'd've loved to hear about those other alternatives)

---

by the way, you mentioned that decreasing HSI6/10 from O(n^6) to O(n^5) clauses was slower - how big was the slowdown and how much less total clauses were there in that encoding? if I understand it correctly, that was still the biggest clause maker, but by how much?

---

also, have you tried reordering order of operations in symmetry break? how much did it affect the search? I wonder if unique multiplication table might've been of help had it been disambiguated stronger (or weaker)