LARA This is an old revision of the document! Exercise 06 - DRAFT Build a theorem prover that will win the CASC competition of resolution-based theorem provers. You may wish to consult the following: The design and implementation of VAMPIRE SPASS E: A Braniac Theorem Prover