LARA This is an old revision of the document! Finite Models Imply Decidability Prover and counterexample finder running in parallel.