@ARTICLE{MPB-JH:JSC:1995:aquarius, AUTHOR = "Maria Paola Bonacina and Jieh Hsiang", TITLE = "Distributed deduction by {C}lause-{D}iffusion: distributed contraction and the {A}quarius prover", JOURNAL = "Journal of Symbolic Computation", VOLUME = 19, PAGES = "245--267", MONTH = "March", DOI = "10.1006/jsco.1995.1014", YEAR = 1995}