The article is spot on. Some finds it counterintuitive that SAT solver often can solve problems with redundant clauses (hence larger problems) faster than minim

The article is spot on. Some finds it counterintuitive that SAT solver often can solve problems with redundant clauses (hence larger problems) faster than minimal ones. But you can find the proof faster if you have appropriate lemmas. Since lemmas can be derived from axioms, strictly speaking, all lemmas are redundant. But they help. Note: the author maintains a state-of-the-art SAT solver.