However, modern sat-solvers do both. That is, although they are called "sat-solvers", they can actually output both "sat" and "unsat". In software verification

However, modern sat-solvers do both. That is, although they are called "sat-solvers", they can actually output both "sat" and "unsat". In software verification they are used for the "unsat" side: you produce a logical formula P stating that your software is correct, and then you ask the sat-solver about ¬P. Hopefully it returns "unsat", meaning that it has proved P is true; otherwise it will return a satisfying assignment, which is a counterexample to your proposed theorem. So I guess you could say that a theorem prover for propositional logic, like Logic Theorist, is "half" of a modern solver like Z3, it can produce proofs but not counterexamples. :)