In: Journal of Automated Reasoning, 47(4), 2011 (Jasmin Christian Blanchette and Alexander Krauss) PDF