@article(bonacina1995clause,
 author       = {Maria Paola Bonacina and Jieh Hsiang},
 year         = {1995},
 title        = {The Clause-Diffusion methodology for distributed deduction},
 journal      = {Fundamenta Informaticae},
 volume       = {24},
 number       = {1, 2},
 pages        = {177--207},
 doi          = {10.3233/FI-1995-24128},
)
@inproceedings(10.1007/3-540-61708-6_45,
 author       = {J{\"o}rg Denzinger and Martin Kronenburg},
 year         = {1996},
 title        = {Planning for distributed theorem proving: The teamwork approach},
 editor       = {G{\"u}nther G{\"o}rz and Steffen H{\"o}lldobler},
 booktitle    = {KI-96: Advances in Artificial Intelligence},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {43--56},
 doi          = {10.1007/3-540-61708-6\_45},
)
@inbook(Korovin2013,
 author       = {Konstantin Korovin},
 year         = {2013},
 title        = {Inst-Gen -- A Modular Approach to Instantiation-Based Automated Reasoning},
 pages        = {239--270},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 doi          = {10.1007/978-3-642-37651-1\_10},
)
@inproceedings(DBLP:conf/cav/KovacsV13,
 author       = {Laura Kov{\'{a}}cs and Andrei Voronkov},
 year         = {2013},
 title        = {First-Order Theorem Proving and Vampire},
 booktitle    = {Computer Aided Verification - 25th International Conference, {CAV} 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings},
 pages        = {1--35},
 doi          = {10.1007/978-3-642-39799-8\_1},
)
@article(Nelson:1979:SCD:357073.357079,
 author       = {Greg Nelson and Derek C. Oppen},
 year         = {1979},
 title        = {Simplification by Cooperating Decision Procedures},
 journal      = {ACM Trans. Program. Lang. Syst.},
 volume       = {1},
 number       = {2},
 pages        = {245--257},
 doi          = {10.1145/357073.357079},
)
@inproceedings(DBLP:conf/cade/RegerSV15,
 author       = {Giles Reger and Martin Suda and Andrei Voronkov},
 year         = {2015},
 title        = {Playing with {AVATAR}},
 booktitle    = {Automated Deduction - {CADE-25} - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings},
 pages        = {399--415},
 doi          = {10.1007/978-3-319-21401-6\_28},
)
@inproceedings(Vampire2014and2015:Challenges_of_Evaluating_New,
 author       = {Giles Reger and Martin Suda and Andrei Voronkov},
 year         = {2016},
 title        = {The Challenges of Evaluating a New Feature in Vampire},
 editor       = {Kov\textbackslash{}'acs, Laura and Andrei Voronkov},
 booktitle    = {Proceedings of the 1st and 2nd Vampire Workshops},
 series       = {EPiC Series in Computing},
 volume       = {38},
 publisher    = {EasyChair},
 pages        = {70--74},
 doi          = {10.29007/1ffk},
)
@inproceedings(DBLP:conf/sat/Reger0V16,
 author       = {Giles Reger and Martin Suda and Andrei Voronkov},
 year         = {2016},
 title        = {Finding Finite Models in Multi-sorted First-Order Logic},
 booktitle    = {Theory and Applications of Satisfiability Testing - {SAT} 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings},
 pages        = {323--341},
 doi          = {10.1007/978-3-319-40970-2\_20},
)
@inproceedings(DBLP:conf/cade/RegerTV15,
 author       = {Giles Reger and Dmitry Tishkovsky and Andrei Voronkov},
 year         = {2015},
 title        = {Cooperating Proof Attempts},
 booktitle    = {Automated Deduction - {CADE-25} - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings},
 pages        = {339--355},
 doi          = {10.1007/978-3-319-21401-6\_23},
)
@article(Tammet1997,
 author       = {Tanel Tammet},
 year         = {1997},
 title        = {Gandalf},
 journal      = {Journal of Automated Reasoning},
 volume       = {18},
 number       = {2},
 pages        = {199--204},
 doi          = {10.1023/A:1005887414560},
)
@inproceedings(DBLP:conf/cav/Voronkov14,
 author       = {Andrei Voronkov},
 year         = {2014},
 title        = {{AVATAR:} The Architecture for First-Order Theorem Provers},
 booktitle    = {Computer Aided Verification - 26th International Conference, {CAV} 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna, Austria, July 18-22, 2014. Proceedings},
 pages        = {696--710},
 doi          = {10.1007/978-3-319-08867-9\_46},
)
@inproceedings(ARCADE2017:Do_Portfolio_Solvers_Harm,
 author       = {Christoph Weidenbach},
 year         = {2017},
 title        = {Do Portfolio Solvers Harm?},
 editor       = {Giles Reger and Dmitriy Traytel},
 booktitle    = {ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements},
 series       = {EPiC Series in Computing},
 volume       = {51},
 publisher    = {EasyChair},
 pages        = {76--81},
 doi          = {10.29007/vpxm},
)