I'm one of the authors of the arXiv paper. Thanks for bringing this to our attention! We were fully unaware of this repository, and it unfortunately did not come up during our literature search. Our approaches to the lower bound are pretty similar, although some technical differences make ours more efficient. For example, to show that there is no counterexample of size 10, we generate a formula with ~50k variables and ~2.7M clauses, which takes about 85 seconds to solve with Kissat. The encoder from this repository generates a formula with ~2k variables and ~33M clauses, which takes about 50 minutes to solve. We have sent an email to the authors of the Zenodo artifact to decide how to proceed!

I think you are right, it's weird that the paper doesn't mention it