But I mean, what happens if you just chuck those 39,000 clauses into Z3 and let it spin to see what happens? Solvers use a bunch of cute backtracking heuristics to not explore too much of the state space, and they keep getting better at it. Particularly, SAT is sort of like the halting problem, with a class of easily identifiable satisfiable instances and a class of easily identifiable unsatisfiable ones. The difficult instances are a narrow band between the other two classes. SAT solvers are so successful because so many naturally occurring instances turn out to be easy.