{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:28:49Z","timestamp":1725488929651},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439318"},{"type":"electronic","value":"9783540456209"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45620-1_23","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T03:18:26Z","timestamp":1186888706000},"page":"280-284","source":"Crossref","is-referenced-by-count":0,"title":["System Description: GrAnDe 1.0"],"prefix":"10.1007","author":[{"given":"Stephan","family":"Schulz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Geoff","family":"Sutcliffe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"key":"23_CR1","unstructured":"DIMACS. Satisfiability Suggested Format. ftp:\/\/dimacs.rutgers.edu\/ pub\/challenge\/satisfiability\/doc\/satformat.tex ."},{"key":"23_CR2","unstructured":"H. Hoos and T. St\u00fctzle. SATLIB: An Online Resource for Research on SAT. In I. Gent, H. van Maaren, and T. Walsh, editors, Proc. of the 3rd Workshop on the Satisfiability Problem, 2001. http:\/\/www.satlib.org\/ ."},{"issue":"1","key":"23_CR3","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/BF00247825","volume":"9","author":"S.-J. Lee","year":"1992","unstructured":"S-J. Lee and D.A. Plaisted. Eliminating Duplication with the Hyper-Linking Strategy. Journal of Automated Reasoning, 9(1):25\u201342, 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an Efficient SAT Solver. In D. Blaauw and L. Lavagno, editors, Proc. of the 39th Design Automation Conference, pages 530\u2013535, 2001.","DOI":"10.1145\/378239.379017"},{"issue":"3","key":"23_CR5","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1023\/A:1006376231563","volume":"25","author":"D.A. Plaisted","year":"2000","unstructured":"D.A. Plaisted and Y. Zhu. Ordered Semantic Hyper-linking. Journal of Automated Reasoning, 25(3):167\u2013217, 2000.","journal-title":"Journal of Automated Reasoning"},{"key":"23_CR6","doi-asserted-by":"crossref","unstructured":"A. Riazanov and A. Voronkov. Vampire. In H. Ganzinger, editor, Proc. of the 16th International Conference on Automated Deduction, number 1632 in Lecture Notes in Artificial Intelligence, pages 292\u2013296. Springer, 1999.","DOI":"10.1007\/3-540-48660-7_26"},{"key":"23_CR7","unstructured":"A. Riazanov and A. Voronkov. Splitting without Backtracking. In B. Nebel, editor, Proc. of the 17th International Joint Conference on Artificial Intelligence, pages 611\u2013617. Morgan Kaufmann, 2001."},{"key":"23_CR8","unstructured":"S. Schulz. A Comparison of Different Techniques for Grounding Near-Propositional CNF Formulae. In S. Haller and G. Simmons, editors, Proc. of the 15th Florida Artificial Intelligence Research Symposium. AAAI Press, 2002. To appear."},{"key":"23_CR9","doi-asserted-by":"crossref","unstructured":"G. Stenz and R. Letz. DCTP-A Disconnection Calculus Theorem Prover. In R. Gore, A. Leitsch, and T. Nipkow, editors, Proc. of the International Joint Conference on Automated Reasoning, number 2083 in Lecture Notes in Artificial Intelligence, pages 381\u2013385. Springer, 2001.","DOI":"10.1007\/3-540-45744-5_30"},{"issue":"2","key":"23_CR10","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"G. Sutcliffe and C.B. Suttner. The TPTP Problem Library: CNF Release v1.2.1. Journal of Automated Reasoning, 21(2):177\u2013203, 1998.","journal-title":"Journal of Automated Reasoning"},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"G. Sutcliffe, C. Suttner, and J. Pelletier. The IJCAR ATP System Competition. Journal of Automated Reasoning, To appear, 2002.","DOI":"10.1023\/A:1015736313131"},{"key":"23_CR12","unstructured":"G. Sutcliffe. CASC-JC. http:\/\/www.cs.miami.edu\/ tptp\/CASC\/JC\/ , 2001."},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"C. Weidenbach, et al. SPASS Version 1.0.0. In H. Ganzinger, editor, Proc. of the 16th International Conference on Automated Deduction, number 1632 in Lecture Notes in Artificial Intelligence, pages 378\u2013382. Springer, 1999.","DOI":"10.1007\/3-540-48660-7_34"},{"issue":"1\/2","key":"23_CR14","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1023\/A:1006351428454","volume":"24","author":"H. Zhang","year":"2000","unstructured":"H. Zhang and M. Stickel. Implementing the Davis-Putnam Method. Journal of Automated Reasoning, 24(1\/2):277\u2013296, 2000.","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-18"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45620-1_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T19:55:50Z","timestamp":1556740550000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45620-1_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439318","9783540456209"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-45620-1_23","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}