@misc(acl2:doc,
 author       = {{ACL2 Community}},
 year         = {Accessed: 2018},
 title        = {{ACL2+Books} Documentation},
 url          = {http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index.html},
)
@article(balyo2015,
 author       = {Tom{\'{a}}{\v{s}} Balyo and Armin Biere and Markus Iser and Carsten Sinz},
 year         = {2016},
 title        = {{SAT} Race 2015},
 journal      = {Artificial Intelligence},
 volume       = {241},
 pages        = {45--65},
 doi          = {10.1016/j.artint.2016.08.007},
)
@book(balyo2017,
 editor       = {Tom{\'{a}}{\v{s}} Balyo and Marijn J. H. Heule and Matti J{\"a}rvisalo},
 year         = {2017},
 title        = {Proceedings of SAT Competition 2017: Solver and Benchmark Descriptions},
 series       = {Publication series B},
 volume       = {B-2017-1},
 publisher    = {University of Helsinki, Department of Computer Science},
 url          = {http://hdl.handle.net/10138/224324},
)
@incollection(boyer1991,
 author       = {Robert S. Boyer and David M. Goldschlag and Matt Kaufmann and J Strother Moore},
 year         = {1991},
 title        = {Functional instantiation in first-order logic},
 editor       = {Vladimir Lifschitz},
 booktitle    = {Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy},
 publisher    = {Academic Press, Inc.},
 pages        = {7--26},
 doi          = {10.1016/B978-0-12-450010-5.50007-4},
)
@inproceedings(EPTCS114.8,
 author       = {Jared Davis and Sol Swords},
 year         = {2013},
 title        = {Verified AIG Algorithms in ACL2},
 editor       = {Ruben Gamboa and Jared Davis},
 booktitle    = {{\rm Proceedings International Workshop on the} ACL2 Theorem Prover and its Applications, {\rm Laramie, Wyoming, USA , May 30-31, 2013}},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {114},
 publisher    = {Open Publishing Association},
 pages        = {95--110},
 doi          = {10.4204/EPTCS.114.8},
)
@inproceedings(EPTCS114.5,
 author       = {Shilpi Goel and Warren A Hunt, Jr. and Matt Kaufmann},
 year         = {2013},
 title        = {Abstract Stobjs and Their Application to ISA Modeling},
 editor       = {Ruben Gamboa and Jared Davis},
 booktitle    = {{\rm Proceedings International Workshop on the} ACL2 Theorem Prover and its Applications, {\rm Laramie, Wyoming, USA , May 30-31, 2013}},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {114},
 publisher    = {Open Publishing Association},
 pages        = {54--69},
 doi          = {10.4204/EPTCS.114.5},
)
@article(KAUFMANN20093,
 author       = {Matt Kaufmann and J Strother Moore and Sandip Ray and Erik Reeber},
 year         = {2009},
 title        = {Integrating external deduction tools with ACL2},
 journal      = {Journal of Applied Logic},
 volume       = {7},
 number       = {1},
 pages        = {3 -- 25},
 doi          = {10.1016/j.jal.2007.07.002},
 note         = {Special Issue: Empirically Successful Computerized Reasoning},
)
@inproceedings(Mishchenko:2006:ICE:1233501.1233679,
 author       = {Alan Mishchenko and Satrajit Chatterjee and Robert Brayton and Niklas Een},
 year         = {2006},
 title        = {Improvements to Combinational Equivalence Checking},
 booktitle    = {Proceedings of the 2006 IEEE/ACM International Conference on Computer-aided Design},
 series       = {ICCAD '06},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {836--843},
 doi          = {10.1145/1233501.1233679},
)
@inproceedings(DBLP:journals/corr/PengG15,
 author       = {Yan Peng and Mark R. Greenstreet},
 year         = {2015},
 title        = {Extending {ACL2} with {SMT} Solvers},
 booktitle    = {Proceedings Thirteenth International Workshop on the {ACL2} Theorem Prover and Its Applications, Austin, Texas, USA, 1-2 October 2015.},
 pages        = {61--77},
 doi          = {10.4204/EPTCS.192.6},
)
@inproceedings(sulfa,
 author       = {Erik Reeber and Warren A. Hunt},
 year         = {2006},
 title        = {A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA)},
 editor       = {Ulrich Furbach and Natarajan Shankar},
 booktitle    = {Automated Reasoning},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {453--467},
 doi          = {10.1007/11814771_38},
)
@inproceedings(4021022,
 author       = {J. Sawada and E. Reeber},
 year         = {2006},
 title        = {ACL2SIX: A Hint used to Integrate a Theorem Prover and an Automated Verification Tool},
 booktitle    = {2006 Formal Methods in Computer Aided Design},
 pages        = {161--170},
 doi          = {10.1109/FMCAD.2006.3},
)
@inproceedings(DBLP:journals/corr/abs-1110-4676,
 author       = {Sol Swords and Jared Davis},
 year         = {2011},
 title        = {Bit-Blasting {ACL2} Theorems},
 booktitle    = {Proceedings 10th International Workshop on the {ACL2} Theorem Prover and its Applications, {ACL2} 2011, Austin, Texas, USA, November 3-4, 2011.},
 pages        = {84--102},
 doi          = {10.4204/EPTCS.70.7},
)
@inbook(Tseitin1983,
 author       = {G. S. Tseitin},
 year         = {1983},
 title        = {Automation of Reasoning: 2: Classical Papers on Computational Logic 1967--1970},
 chapter      = {On the Complexity of Derivation in Propositional Calculus},
 pages        = {466--483},
 publisher    = {Springer},
 address      = {Berlin, Heidelberg},
 doi          = {10.1007/978-3-642-81955-1_28},
)