> In particular, I helped design MARMOSET (Marmoset Automated Reasoner Mostly Only Solves Easy Theorems), a competitive SAT problem solver. [...]

Now that is some good SAT solver name - keeping user's expectations low, I guess? Nice choice! ;)