Distributed deduction by Clause-Diffusion: the Aquarius prover