@Book{AMR93,
    Author       = "Abraham, R. and Marsden, J. and Ratiu, T.",
    Year         = "1993",
    Title        = "{Manifolds, Tensor Analysis, and Applications}",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@InProceedings{AAR11,
    Author       = "Alberti, F. and Armando, A. and Ranise, S.",
    Year         = "2011",
    Title        = "{An Automated Symbolic Analysis of Security Policies}",
    Editor       = "Bj{\o}rner, N. and Sofronie-Stokkermans, V.",
    BookTitle    = "{Proceedings of the 23rd International Conference on
                    Automated Deduction}",
    Place        = "Wroclaw, Poland",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "6803",
    Pages        = "26-33",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@InProceedings{AAR11-ASIACCS,
    Author       = "Alberti, F. and Armando, A. and Ranise, S.",
    Year         = "2011",
    Title        = "{Efficient Symbolic Automated Analysis of Administrative
                    Attribute-based RBAC-Policies}",
    Editor       = "Sandhu, R. and Wong, D.",
    BookTitle    = "{Proceedings of the 6th ACM Symposium on Information,
                    Computer and Communications Security}",
    Place        = "Hong Kong",
    Pages        = "165-175",
    Publisher    = "ACM Press",
    Comment      = "TPTPRef"
}

@InProceedings{AM+01,
    Author       = "Alechina, N. and Mendler, M. and de Paiva, V. and Ritter,
                    E.",
    Year         = "2001",
    Title        = "{Categorical and Kripke Semantics for Constructive S4 Modal
                    Logic}",
    Editor       = "Fribourg, L.",
    BookTitle    = "{Proceedings of the 15th International Workshop on Computer
                    Science Logic}",
    Place        = "Paris, France",
    Series       = "Lecture Notes in Computer Science",
    Number       = "2142",
    Pages        = "292-307",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@PhDThesis{Ale95,
    Author       = "Alexander, G.",
    Year         = "1995",
    Title        = "{Proving First-Order Equality Theorems with
                    Hyper-Linking}",
    School       = "University of North Carolina at Chapel Hill",
    Address      = "Chapel Hill, USA",
    Comment      = "TPTPRefForResults,TPTPCite,TPTPData"
}

@Book{AK+91,
    Author       = "Allen, J.F. and Kautz, H.A. and Pelavin, R.N. and
                    Tenenberg, J.D.",
    Year         = "1991",
    Title        = "{Reasoning about Plans}",
    Publisher    = "Morgan Kaufmann Publishers",
    Comment      = "TPTPRef"
}

@InProceedings{AGR18,
    Author       = "Alvez, J. and Gonzalez-Dios, I. and Rigau, G.",
    Year         = "2018",
    Title        = "{Cross-checking WordNet and SUMO Using Meronymy}",
    Editor       = "Calzolari, N. and Choukri, K. and Cieri, C. and Declerck,
                    T. and Goggi, S. and Hasida, K. and Isahara, H. and
                    Maegaard, B. and Mariani, J. and Mazo, H. and Moreno, A.
                    and Odijk, J. and Piperidis, S. and Tokunaga, T.",
    BookTitle    = "{Proceedings of the 11th Language Resources and Evaluation
                    Conference}",
    Place        = "Miyazaki, Japan",
    Comment      = "TPTPRef"
}

@Article{ALR12,
    Author       = "Alvez, J. and Lucio, P. and Rigau, G.",
    Year         = "2012",
    Title        = "{Adimen-SUMO: Reengineering an Ontology for First-Order
                    Reasoning}",
    Journal      = "International Journal on Semantic Web and Information
                    Systems",
    Volume       = "8",
    Number       = "3",
    Pages        = "80-116",
    Publisher    = "IGI Global",
    Comment      = "TPTPRef"
}

@Book{AMS92,
    Author       = "American Mathematical Society",
    Year         = "1992",
    Title        = "{Mathematical Subject Classification}",
    Pages        = "S1-S35",
    Publisher    = "American Mathematical Society",
    Comment      = "TPTPRef"
}

@InProceedings{AB90,
    Author       = "Anantharaman, S. and Bonacina, M.P.",
    Year         = "1990",
    Title        = "{An Application of the Theorem Prover SBR3 to Many-Valued
                    Logic}",
    Editor       = "Okada, M. and Kaplan, S.",
    BookTitle    = "{Proceedings of the 2nd International Workshop on
                    Conditional and Typed Rewriting Systems}",
    Place        = "Montreal, Canada",
    Series       = "Lecture Notes in Computer Science",
    Number       = "516",
    Pages        = "156-161",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Article{AH90,
    Author       = "Anantharaman, S. and Hsiang, J.",
    Year         = "1990",
    Title        = "{Automated Proofs of the Moufang Identities in Alternative
                    Rings}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "6",
    Number       = "1",
    Pages        = "79-110",
    Comment      = "TPTPRef"
}

@Article{And89,
    Author       = "Andrews, P.B.",
    Year         = "1989",
    Title        = "{On Connections and Higher-Order Logic}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "5",
    Number       = "3",
    Pages        = "257-291",
    Comment      = "TPTPRef"
}

@Book{And86,
    Author       = "Andrews, P.B.",
    Year         = "1986",
    Title        = "{An Introduction to Mathematical Logic and Type Theory: To
                    Truth Through Proof}",
    Publisher    = "Academic Press",
    Comment      = "TPTPRef"
}

@Article{And72,
    Author       = "Andrews, P.B.",
    Year         = "1972",
    Title        = "{General Models and Extensionality}",
    Journal      = "Journal of Symbolic Logic",
    Volume       = "37",
    Number       = "2",
    Pages        = "395-397",
    Comment      = "TPTPRef"
}

@Article{And71,
    Author       = "Andrews, P.B.",
    Year         = "1971",
    Title        = "{Resolution in Type Theory}",
    Journal      = "Journal of Symbolic Logic",
    Volume       = "36",
    Number       = "3",
    Pages        = "414-432",
    Comment      = "TPTPRef"
}

@Article{AZ89,
    Author       = "Angshuman, G. and Zhang, H.",
    Year         = "1989",
    Title        = "{Andrews' Challenge Problem: Clause Conversion and
                    Solutions}",
    Journal      = "AAR Newsletter",
    Volume       = "14",
    Pages        = "5-8",
    Comment      = "TPTPRef"
}

@Unpublished{ANL,
    Author       = "Argonne National Laboratory",
    Title        = "{Argonne National Laboratory Problem Library}",
    Note         = "Available by anonymous ftp from info.msc.anl.gov, Maths
                    and Computer Science Division, Argonne National
                    Laboratory, Argonne, IL.",
    Comment      = "TPTPRef"
}

@Article{AB+09,
    Author       = "Armando, A. and Bonacina, M. and Ranise, S. and Schulz,
                    S.",
    Year         = "2009",
    Title        = "{New Results on Rewrite-based Satisfiability Procedures}",
    Journal      = "ACM Transactions on Computational Logic",
    Volume       = "10",
    Number       = "1:4",
    Comment      = "TPTPRef"
}

@InProceedings{AR10,
    Author       = "Armando, A. and Ranise, S.",
    Year         = "2010",
    Title        = "{Automated Symbolic Analysis of ARBAC Policies}",
    Editor       = "Cuellar, J. and Lopez, J.",
    BookTitle    = "{Proceedings of the 6th International Workshop on Security
                    and Trust Management}",
    Place        = "Athens, Greece",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@InCollection{AO13,
    Author       = "Arthan, R. and Olica, P.",
    Year         = "2013",
    Title        = "{Dual Hoops Have Unique Halving}",
    Editor       = "Bonacina, M.P. and Stickel, M.",
    BookTitle    = "{Automated Reasoning and Mathematics: Essays in Memory of
                    William McCune}",
    Series       = "Lecture Notes in Artificial Intelligence",
    Pages        = "To appear",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Article{AKP06,
    Author       = "Aschbacher, M. and Kinyon, M. and Phillips, J.D.",
    Year         = "2006",
    Title        = "{Finite Bruck Loops}",
    Journal      = "Transactions of the American Mathematical Society",
    Volume       = "358",
    Pages        = "3061-3075",
    Comment      = "TPTPRef"
}

@TechReport{Ast92,
    Author       = "Astrachan, O.L.",
    Year         = "1992",
    Title        = "{METEOR: Exploring Model Elimination Theorem Proving}",
    Number       = "CS-1992-22",
    Institution  = "Department of Computer Science, Duke University",
    Address      = "Durham, USA",
    Comment      = "TPTPRef, linear systems"
}

@InProceedings{ADF95,
    Author       = "Avenhaus, J. and Denzinger, J. and Fuchs, M.",
    Year         = "1995",
    Title        = "{DISCOUNT: A  System for Distributed Equational
                    Deduction}",
    Editor       = "Hsiang J.",
    BookTitle    = "{Proceedings of the 6th International Conference on
                    Rewriting Techniques and Applications}",
    Place        = "Kaiserslautern, Germany",
    Pages        = "397-402",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRefForResults"
}

@Unpublished{ADM08,
    Author       = "Avigad, J. and Dean, E. and Mumma, J.",
    Year         = "2008",
    Title        = "{A Formal System for Euclid's Elements}",
    Note         = "arXiv:0810.4315v3",
    Comment      = "TPTPRef"
}

@Book{BN99,
    Author       = "Baader, F. and Nipkow, T.",
    Year         = "1999",
    Title        = "{Term Rewriting and All That}",
    Publisher    = "Cambridge University Press",
    Comment      = "TPTPRef"
}

@Article{BH+08,
    Author       = "Baaz, M. and Hetzl, S. and Leitsch, A. and Richter, C. and
                    Spohr, H.",
    Year         = "2008",
    Title        = "{CERES: An Analysis of F{\"u}rstenberg's Proof of the
                    Infinity of Primes}",
    Journal      = "Theoretical Computer Science",
    Comment      = "TPTPRef"
}

@InProceedings{BD86,
    Author       = "Bachmair, L. and Dershowitz, N.",
    Year         = "1986",
    Title        = "{Commutation, Transformation, and Termination}",
    Editor       = "Siekmann, J.",
    BookTitle    = "{Proceedings of the 8th International Conference on
                    Automated Deduction}",
    Place        = "Oxford, United Kingdom",
    Series       = "Lecture Notes in Computer Science",
    Number       = "230",
    Pages        = "5-20",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@InProceedings{Bac89,
    Author       = "Back, R.",
    Year         = "1989",
    Title        = "{A Method for Refining Atomicity in Parallel Algorithms}",
    Editor       = "Odijk, E. and Rem, M. and Syr, J.",
    BookTitle    = "{Proceedings of Parallel Architectures and Languages
                    Europe}",
    Place        = "Eindhoven, Netherlands",
    Series       = "Lecture Notes in Computer Science",
    Number       = "366",
    Pages        = "199-216",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Book{BvW98,
    Author       = "Back, R. and von Wright, J.",
    Year         = "998",
    Title        = "{Refinement Calculus: A Systematic Introduction}",
    Series       = "Graduate Texts in Computer Science",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@MastersThesis{Bac10-Thesis,
    Author       = "Backes, J.",
    Year         = "2010",
    Title        = "{Tableaux for Higher-Order Logic with If-Then-Else,
                    Description and Choice}",
    School       = "Saarland University",
    Address      = "Saarbruecken, Germany",
    Comment      = "TPTPRef"
}

@Article{BB93,
    Author       = "Bailin, S. and Barker-Plummer, D.",
    Year         = "1993",
    Title        = "{L-match: An Inference Rule for Incrementally Elaborating
                    Set Instantiations}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "11",
    Number       = "3",
    Pages        = "391-428",
    Comment      = "TPTPRef"
}

@PhDThesis{Bal98,
    Author       = "Baldoni, M.",
    Year         = "1998",
    Title        = "{Normal Multimodal Logics: Automatic Deduction and Logic
                    Programming Extensions}",
    School       = "Universita degli studi di Torino",
    Address      = "Torino, Italy",
    Comment      = "TPTPRef"
}

@Article{BHS00,
    Author       = "Balsiger, P. and Heuerding, A. and Schwendimann, S.",
    Year         = "2000",
    Title        = "{A Benchmark Method for the Propositional Modal Logics K,
                    KT, S4}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "24",
    Number       = "3",
    Pages        = "297-317",
    Comment      = "TPTPRef,TPTPCite,Evaluation"
}

@Article{Ban01-JFM,
    Author       = "Bancerek, G.",
    Year         = "2001",
    Title        = "{Duality Based on the Galois Connection. Part I}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "9",
    Number       = "4",
    Pages        = "767-778",
    Comment      = "TPTPRef,WAYBEL34"
}

@Article{Ban97-JFM-BP,
    Author       = "Bancerek, G.",
    Year         = "1997",
    Title        = "{Bounds in Posets and Relational Substructures}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "6",
    Number       = "1",
    Pages        = "81-91",
    Comment      = "TPTPRef"
}

@Article{Ban97-JFM-DS,
    Author       = "Bancerek, G.",
    Year         = "1997",
    Title        = "{Directed Sets, Nets, Ideals, Filters, and Maps}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "6",
    Number       = "1",
    Pages        = "93-107",
    Comment      = "TPTPRef"
}

@Article{Ban97-JFM-PIF,
    Author       = "Bancerek, G.",
    Year         = "1997",
    Title        = "{Prime Ideals and Filters}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "6",
    Number       = "2",
    Pages        = "241-247",
    Comment      = "TPTPRef"
}

@Article{Ban96-JFM,
    Author       = "Bancerek, G.",
    Year         = "1996",
    Title        = "{Ideals}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "5",
    Number       = "2",
    Pages        = "149-156",
    Comment      = "TPTPRef,FILTER_2"
}

@Article{Ban91-JFM-CL,
    Author       = "Bancerek, G.",
    Year         = "1991",
    Title        = "{Complete Lattices}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "2",
    Number       = "5",
    Pages        = "719-725",
    Comment      = "TPTPRef"
}

@Article{Ban91-JFM-F2,
    Author       = "Bancerek, G.",
    Year         = "1991",
    Title        = "{Filters - Part II. Quotient Lattices Modulo Filters and
                    Direct Product of Two Lattices}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "2",
    Number       = "3",
    Pages        = "433-438",
    Comment      = "TPTPRef"
}

@Article{Ban90-JFL-ON,
    Author       = "Bancerek, G.",
    Year         = "1990",
    Title        = "{The Ordinal Numbers}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "1",
    Number       = "1",
    Pages        = "91-96",
    Comment      = "TPTPRef"
}

@Article{Ban90-JFM-WOR,
    Author       = "Bancerek, G.",
    Year         = "1990",
    Title        = "{The Well Ordering Relations}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "1",
    Number       = "1",
    Pages        = "123-129",
    Comment      = "TPTPRef"
}

@Article{Ban90-JFM-ZF,
    Author       = "Bancerek, G.",
    Year         = "1990",
    Title        = "{Zermelo Theorem and Axiom of Choice}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "1",
    Number       = "2",
    Pages        = "265-267",
    Comment      = "TPTPRef"
}

@Article{BE01-JFM,
    Author       = "Bancerek, G. and Endou, N.",
    Year         = "2001",
    Title        = "{Compactness of Lim-inf Topology}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "9",
    Number       = "4",
    Pages        = "739-743",
    Comment      = "TPTPRef,WAYBEL33"
}

@Article{BES01,
    Author       = "Bancerek, G. and Endou, N. and Sakai, Y.",
    Year         = "2001",
    Title        = "{On the Characterizations of Compactness}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "9",
    Number       = "4",
    Pages        = "733-738",
    Comment      = "TPTPRef"
}

@Article{Bar46,
    Author       = "Barcan, R.",
    Year         = "1946",
    Title        = "{A Functional Calculus of First Order Based on Strict
                    Implication}",
    Journal      = "Journal of Symbolic Logic",
    Volume       = "11",
    Pages        = "1-16",
    Comment      = "TPTPRef"
}

@Book{Bar81,
    Author       = "Barendregt, H.P.",
    Year         = "1981",
    Title        = "{The Lambda Calculus: Its Syntax and Semantics}",
    Publisher    = "North-Holland",
    Comment      = "TPTPRef"
}

@Article{Bar92,
    Author       = "Barker-Plummer, D",
    Year         = "1992",
    Title        = "{Gazing: An Approach to the Problem of Definition and Lemma
                    Use}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "8",
    Number       = "3",
    Pages        = "311-344",
    Comment      = "TPTPRef"
}

@InProceedings{Bau15,
    Author       = "Baumgartner, P.",
    Year         = "2015",
    Title        = "{SMTtoTPTP - A Converter for Theorem Proving Formats}",
    Editor       = "Felty, A. and Middeldorp, A.",
    BookTitle    = "{Proceedings of the 25th International Conference on
                    Automated Deduction}",
    Place        = "Berlin, Germany",
    Series       = "Lecture Notes in Computer Science",
    Number       = "9195",
    Pages        = "285-294",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Unpublished{Bau99,
    Author       = "Baumgartner, P.",
    Year         = "1999",
    Title        = "{FTP'2000 - Problem Sets}",
    Note         = "ftp://ftphost.uni-koblenz.de/outgoing/agki/FTP2000/ProblemSets/index.html",
    Comment      = "TPTPRef"
}

@Article{Bau96,
    Author       = "Baumgartner, P.",
    Year         = "1996",
    Title        = "{Linear and Unit-Resulting Refutations for Horn Theories}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "16",
    Number       = "3",
    Pages        = "241-319",
    Comment      = "TPTPRefForResults,TPTPCite,TPTPData"
}

@InProceedings{Bau94,
    Author       = "Baumgartner, P.",
    Year         = "1994",
    Title        = "{Refinements of Theory Model Elimination and a Variant
                    without Contrapositives}",
    Editor       = "Cohn, A.G.",
    BookTitle    = "{Proceedings of the 11th European Conference on Artificial
                    Intelligence}",
    Pages        = "90-94",
    Publisher    = "Wiley and Sons",
    Comment      = "TPTPRefForResults,TPTPCite"
}

@InProceedings{BB13,
    Author       = "Baumgartner, P. and Bax, J.",
    Year         = "2013",
    Title        = "{Proving Infinite Satisfiability}",
    Editor       = "McMillan, K. and Middeldorp, A. and Voronkov, A.",
    BookTitle    = "{Proceedings of the 19th International Conference on Logic
                    for Programming, Artificial Intelligence, and Reasoning}",
    Place        = "Stellenbosch, South Africa",
    Series       = "Lecture Notes in Computer Science",
    Number       = "8312",
    Pages        = "86-95",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@InProceedings{BF94,
    Author       = "Baumgartner, P. and Furbach, U.",
    Year         = "1994",
    Title        = "{PROTEIN: A {\em PRO}ver with a {\em T}heory {\em
                    E}xtension {\em IN}terface}",
    Editor       = "Bundy, A.",
    BookTitle    = "{Proceedings of the 12th International Conference on
                    Automated Deduction}",
    Place        = "Nancy, France",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "814",
    Pages        = "769-773",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRefForResults,linear systems,TPTPCite,TPTPData"
}

@Article{BF94-JAR-13,
    Author       = "Baumgartner, P. and Furbach, U.",
    Year         = "1994",
    Title        = "{Model Elimination without Contrapositives and its
                    Application to PTTP}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "13",
    Number       = "3",
    Pages        = "339-359",
    Comment      = "TPTPRefForResults,TPTPCite"
}

@Article{BFS97,
    Author       = "Baumgartner, P. and Furbach, U. and Stolzenburg, F.",
    Year         = "1997",
    Title        = "{Computing Answers with Model Elimination}",
    Journal      = "Artificial Intelligence",
    Volume       = "90",
    Pages        = "135-176",
    Comment      = "TPTPRefForResults,TPTPCite, TPTPData, TPTPRef"
}

@InProceedings{BFS95,
    Author       = "Baumgartner, P. and Furbach, U. and Stolzenburg, F.",
    Year         = "1995",
    Title        = "{Model Elimination, Logic Programming and Computing
                    Answers}",
    Editor       = "Mellish, C.S.",
    BookTitle    = "{Proceedings of the 14th International Joint Conference on
                    Artificial Intelligence}",
    Pages        = "335-340",
    Publisher    = "Morgan Kaufmann",
    Comment      = "TPTPCite, TPTPRef"
}

@InProceedings{BS09-FTP,
    Author       = "Baumgartner, P. and Slaney, J.",
    Year         = "2009",
    Title        = "{Constraint Modelling: A Challenge for Automated
                    Reasoning}",
    Editor       = "Peltier, N. and Sofronie-Stokkermans, V.",
    BookTitle    = "{Proceedings of the 7th International Workshop on
                    First-Order Theorem Proving}",
    Place        = "Oslo, Norway",
    Series       = "CEUR Workshop Proceedings",
    Number       = "556",
    Pages        = "4-18",
    Comment      = "TPTPRef"
}

@Book{BHS07,
    Author       = "Beckert, B. and Hahnle, R. and Schmitt, P.",
    Year         = "2007",
    Title        = "{Verification of Object-Oriented Software: The KeY
                    Approach}",
    Series       = "Lecture Notes in Computer Science",
    Number       = "4334",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Article{BP95,
    Author       = "Beckert, B. and Posegga, J.",
    Year         = "1995",
    Title        = "{leanTAP: Lean, Tableau-based Deduction}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "15",
    Number       = "3",
    Pages        = "339-358",
    Comment      = "TPTPRef"
}

@Article{BW17,
    Author       = "Beeson, M. and Wos, L.",
    Year         = "2017",
    Title        = "{Finding Proofs in Tarskian Geometry}",
    Journal      = "Journal of Automated Reasoning",
    Pages        = "To appear",
    Comment      = "TPTPRef"
}

@Article{Bel97,
    Author       = "Belinfante, J.G.F.",
    Year         = "1997",
    Title        = "{On Quaife's Development of Class Theory}",
    Journal      = "AAR Newsletter",
    Volume       = "37",
    Pages        = "1-4",
    Comment      = "TPTPRef"
}

@Article{Ben92,
    Author       = "Benanav, D.",
    Year         = "1992",
    Title        = "{Recognising Unnecessary Clauses in Resolution Based
                    Systems}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "9",
    Number       = "1",
    Pages        = "43-76",
    Comment      = "TPTPRef"
}

@Article{Ben89,
    Author       = "Bennett, F.E.",
    Year         = "1989",
    Title        = "{Quasigroup Identities and Mendelsohn Designs}",
    Journal      = "Canadian Journal of Mathematics",
    Volume       = "41",
    Number       = "2",
    Pages        = "341-368",
    Comment      = "TPTPRef"
}

@InCollection{BZ92-CDT,
    Author       = "Bennett, F.E. and Zhu, L.",
    Year         = "1992",
    Title        = "{Conjugate-Orthogonal Latin Squares and Related
                    Structures}",
    Editor       = "Dinitz, J.H. and Douglas, R.S.",
    BookTitle    = "{Contemporary Design Theory: A Collection of Surveys}",
    Pages        = "41-96",
    Publisher    = "Wiley and Sons",
    Comment      = "TPTPRef"
}

@Article{Ben11,
    Author       = "Benzm{\"u}ller, C.",
    Year         = "2011",
    Title        = "{Combining and Automating Classical and Non-Classical
                    Logics in Classical Higher-Order Logics Theory}",
    Journal      = "Annals of Mathematics and Artificial Intelligence",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@InProceedings{Ben10,
    Author       = "Benzm{\"u}ller, C.",
    Year         = "2010",
    Title        = "{Simple Type Theory as a Framework for Combining Logics}",
    BookTitle    = "{Proceedings of the 3rd World Congress and School on
                    Universal Logic}",
    Place        = "Lisbon, Portugal",
    Pages        = "To appear",
    Comment      = "TPTPRef"
}

@TechReport{Ben08-TR,
    Author       = "Benzm{\"u}ller, C.",
    Year         = "2008",
    Title        = "{Automating Access Control Logics in Simple Type Theory
                    with LEO-II}",
    Number       = "SEKI Technical Report SR-2008-01",
    Institution  = "Universit{\"a}t des Saarlandes",
    Address      = "Saarbr{\"u}cken, Germany",
    Comment      = "TPTPRef, TPTPCite"
}

@PhDThesis{Ben99-PhD,
    Author       = "Benzm{\"u}ller, C.",
    Year         = "1999",
    Title        = "{Equality and Extensionality in Higher-Order Theorem
                    Proving}",
    School       = "Department of Computer Science, Saarland University",
    Address      = "Saarbruecken, Germany",
    Comment      = "TPTPRef"
}

@InCollection{BB07,
    Author       = "Benzm{\"u}ller, C. and Brown, C.E.",
    Year         = "2007",
    Title        = "{The Curious Inference of Boolos in MIZAR and OMEGA}",
    Editor       = "Matuszewski, R. and Zalewska, A.",
    BookTitle    = "{Festschrift in Honour of Andrzej Trybulec}",
    Journal      = "Studies in Logic, Grammar, and Rhetoric",
    Volume       = "10",
    Number       = "23",
    Pages        = "299-388",
    Comment      = "TPTPRef"
}

@InProceedings{BB05,
    Author       = "Benzm{\"u}ller, C. and Brown, C.E.",
    Year         = "2005",
    Title        = "{A Structured Set of Higher-Order Problems}",
    Editor       = "Hurd, J. and Melham, T.",
    BookTitle    = "{Proceedings of the 18th International Conference on
                    Theorem Proving in Higher Order Logics}",
    Place        = "Oxford, United Kingdom",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "3606",
    Pages        = "66-81",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@InProceedings{BC+97,
    Author       = "Benzm{\"u}ller, C. and Cheikhrouhou, L. and Fehrer, D. and
                    Fiedler, A. and Huang, X. and Kerber, M. and Kohlhase, M.
                    and Konrad, K. and Meier, A. and Melis, E. and
                    Schaarschmidt, W. and Siekmann, J. and Sorge, V.",
    Year         = "1997",
    Title        = "{OMEGA: Towards a Mathematical Assistant}",
    Editor       = "McCune, W.W.",
    BookTitle    = "{Proceedings of the 14th International Conference on
                    Automated Deduction}",
    Place        = "Townsville, Australia",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "1249",
    Pages        = "252-255",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRefForResults,TPTPCite"
}

@Article{BP13,
    Author       = "Benzm{\"u}ller, C. and Paulson, L.",
    Year         = "2013",
    Title        = "{Quantified Multimodal Logics in Simple Type Theory}",
    Journal      = "Logica Universalis",
    Volume       = "7",
    Number       = "1",
    Pages        = "7-20",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Article{BP10,
    Author       = "Benzm{\"u}ller, C. and Paulson, L.",
    Year         = "2010",
    Title        = "{Multimodal and Intuitionistic Logics in Simple Type
                    Theory}",
    Journal      = "Logic Journal of the IGPL",
    Publisher    = "Oxford University Press",
    Comment      = "TPTPRef"
}

@InCollection{BP08,
    Author       = "Benzm{\"u}ller, C. and Paulson, L.",
    Year         = "2008",
    Title        = "{Exploring Properties of Normal Multimodal Logics in Simple
                    Type Theory with LEO-II}",
    Editor       = "Benzm{\"u}ller, C. and Brown, C.E. and Siekmann, J. and
                    Statman, R.",
    BookTitle    = "{Reasoning in Simple Type Theory: Festschrift in Honour of
                    Peter B. Andrews on his 70th Birthday}",
    Series       = "Studies in Logic, Mathematical Logic and Foundations",
    Number       = "17",
    Pages        = "401-422",
    Publisher    = "College Publications",
    Comment      = "TPTPRef"
}

@InProceedings{BP10-PAAR,
    Author       = "Benzm{\"u}ller, C. and Pease, A.",
    Year         = "2010",
    Title        = "{Progress in Automating Higher-order Ontology Reasoning}",
    BookTitle    = "{Proceedings of IJACR 2010 Workshop on Practical Aspects of
                    Automated Reasoning}",
    Place        = "Edinburgh, United Kingdom",
    Comment      = "TPTPRef,TPTPCite"
}

@Article{BS+08,
    Author       = "Benzm{\"u}ller, C. and Sorge, V. and Jamnik, M. and
                    Kerber, M.",
    Year         = "2008",
    Title        = "{Combined Reasoning by Automated Cooperation}",
    Journal      = "Journal of Applied Logic",
    Volume       = "6",
    Number       = "3",
    Pages        = "318-342",
    Comment      = "TPTPRef"
}

@InProceedings{BS+05,
    Author       = "Benzm{\"u}ller, C. and Sorge, V. and Jamnik, M. and
                    Kerber, M.",
    Year         = "2005",
    Title        = "{Can a Higher-Order and a First-Order Theorem Prover
                    Cooperate?}",
    Editor       = "Baader, F. and Voronkov, A.",
    BookTitle    = "{Proceedings of the 11th International Conference on Logic
                    for Programming, Artificial Intelligence, and Reasoning}",
    Place        = "Montevideo, Uruguay",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "3452",
    Pages        = "415-431",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef,TPTPData"
}

@InProceedings{BCO06,
    Author       = "Berdine, J. and Calcagno, C. and O'Hearn, P.",
    Year         = "2006",
    Title        = "{Smallfoot: Modular Automatic Assertion Checking with
                    Separation Logic}",
    Editor       = "de Boer, F. and Bonsangue, M. and Graf, S. and de Roever,
                    W-P.",
    BookTitle    = "{Proceedings of the 4th International Symposium on Formal
                    Methods for Components and Objects}",
    Place        = "Amsterdam, The Netherlands",
    Series       = "Lecture Notes in Computer Science",
    Number       = "4111",
    Pages        = "115-137",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@InProceedings{BCO05,
    Author       = "Berdine, J. and Calcagno, C. and O'Hearn, P.",
    Year         = "2005",
    Title        = "{Symbolic Execution with Separation Logic}",
    Editor       = "Yi, K.",
    BookTitle    = "{Proceedings of the 3rd Asian Symposium on Programming
                    Languages and Systems}",
    Place        = "Tsukuba, Japan",
    Series       = "Lecture Notes in Computer Science",
    Number       = "3780",
    Pages        = "52-68",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Book{BB70,
    Author       = "Birkhoff, G. and Bartee, T.",
    Year         = "1970",
    Title        = "{Modern Applied Algebra}",
    Publisher    = "McGraw-Hill",
    Comment      = "TPTPRef"
}

@Book{BM65,
    Author       = "Birkhoff, G. and MacLane, S.",
    Year         = "1965",
    Title        = "{A Survey of Modern Algebra}",
    Publisher    = "Macmillan",
    Comment      = "TPTPRef"
}

@Book{BG80,
    Author       = "Bishop, R. and Goldberg, S.",
    Year         = "1980",
    Title        = "{Tensor Analysis on Manifolds}",
    Publisher    = "Dover",
    Comment      = "TPTPRef"
}

@Article{Bla15,
    Author       = "Blanchette, J.",
    Year         = "2015",
    Title        = "{The Editor's Corner}",
    Journal      = "AAR Newsletter",
    Volume       = "112",
    Note         = "http://www.aarinc.org/Newsletters/112-2015-09.html",
    Comment      = "TPTPRef"
}

@Article{Bla09,
    Author       = "Blanchette, J.",
    Year         = "2009",
    Title        = "{Proof Pearl: Mechanizing the Textbook Proof of Huffman's
                    Algorithm}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "43",
    Number       = "1",
    Pages        = "1-18",
    Comment      = "TPTPRef"
}

@Article{Bla08,
    Author       = "Blanchette, J.",
    Year         = "2008",
    Title        = "{The Textbook Proof of Huffman's Algorithm}",
    Journal      = "Archive of Formal Proofs",
    Note         = "http://isa-afp.org/entries/Huffman.shtml",
    Comment      = "TPTPRef"
}

@InProceedings{BBP11,
    Author       = "Blanchette, J. and Boehme, S. and Paulson, L.",
    Year         = "2011",
    Title        = "{Extending Sledgehammer with SMT Solvers}",
    Editor       = "Bj{\o}rner, N. and Sofronie-Stokkermans, V.",
    BookTitle    = "{Proceedings of the 23rd International Conference on
                    Automated Deduction}",
    Place        = "Wroclaw, Poland",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "6803",
    Pages        = "116-130",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@InProceedings{BH+14,
    Author       = "Blanchette, J. and H{\"o}lzl, J. and Lochbihler, A. and
                    Panny, L. and Popescu, A. and Traytel, D.",
    Year         = "2014",
    Title        = "{Truly Modular (Co)datatypes for Isabelle/HOL}",
    Editor       = "Klein, G. and Gamboa, R.",
    BookTitle    = "{Proceedings of the 5th International Conference on
                    Interactive Theorem Proving}",
    Place        = "Vienna, Austria",
    Series       = "Lecture Notes in Computer Science",
    Number       = "8558",
    Pages        = "93-110",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Article{BPT14,
    Author       = "Blanchette, J. and Popescu, A. and Traytel, D.",
    Year         = "2014",
    Title        = "{Abstract Completeness}",
    Journal      = "Archive of Formal Proofs",
    Note         = "http://isa-afp.org/entries/Abstract_Completeness.shtml",
    Comment      = "TPTPRef"
}

@Article{Ble90,
    Author       = "Bledsoe, W.W.",
    Year         = "1990",
    Title        = "{Challenge Problems in Elementary Calculus}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "6",
    Number       = "3",
    Pages        = "341-359",
    Comment      = "TPTPRef"
}

@Article{Ble77,
    Author       = "Bledsoe, W.W.",
    Year         = "1977",
    Title        = "{Non-resolution Theorem Proving}",
    Journal      = "Artificial Intelligence",
    Volume       = "9",
    Pages        = "1-35",
    Comment      = "TPTPRef, non-resolution"
}

@Article{BBH72,
    Author       = "Bledsoe, W.W. and Boyer, R.S. and Henneman, W.H.",
    Year         = "1972",
    Title        = "{Computer Proofs of Limit Theorems}",
    Journal      = "Artificial Intelligence",
    Volume       = "3",
    Pages        = "27-60",
    Comment      = "TPTPRef, proofs"
}

@Article{BF93,
    Author       = "Bledsoe, W.W. and Feng, G.",
    Year         = "1993",
    Title        = "{SET-VAR}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "11",
    Number       = "3",
    Pages        = "293-314",
    Comment      = "TPTPRef"
}

@Book{BV94,
    Author       = "Blyth, I.S. and Varlet I.C.",
    Year         = "1994",
    Title        = "{Ockham Algebras}",
    Publisher    = "Oxford Science Publications",
    Comment      = "TPTPRef"
}

@Unpublished{BF+URL,
    Author       = "Bobot, F. and Filliatre, J-C. and Marche, C. and
                    Melquiond, G. and Paskevich, A.",
    Year         = "",
    Title        = "{Toccata: Certified Programs and Certified Tools}",
    Note         = "http://toccata.lri.fr/gallery/why3.en.html",
    Comment      = "TPTPRef"
}

@Article{BG05,
    Author       = "Bock, C. and Gruninger, M.",
    Year         = "2005",
    Title        = "{PSL: A Semantic Domain for Flow Models}",
    Journal      = "Journal of Software and Systems Modeling",
    Volume       = "4",
    Number       = "2",
    Pages        = "209-231",
    Comment      = "TPTPRef"
}

@Article{BE04,
    Author       = "Boeva, V. and Ekenberg, L.",
    Year         = "2004",
    Title        = "{A Transition Logic for Schemata Conflicts}",
    Journal      = "Data and Knowledge Engineering",
    Volume       = "51",
    Number       = "3",
    Pages        = "277-294",
    Comment      = "TPTPRef"
}

@Article{Bon91,
    Author       = "Bonacina, M.P.",
    Year         = "1991",
    Title        = "{Problems in \Lukasiewicz Logic}",
    Journal      = "AAR Newsletter",
    Volume       = "18",
    Pages        = "5-12",
    Comment      = "TPTPRef"
}

@Article{BA01,
    Author       = "Bond, M. and Anderson, R.",
    Year         = "2001",
    Title        = "{API-Level Attacks on Embedded Systems}",
    Journal      = "Computer",
    Volume       = "34",
    Number       = "10",
    Pages        = "67-75",
    Comment      = "TPTPRef"
}

@Article{Boo87,
    Author       = "Boolos, G.",
    Year         = "1987",
    Title        = "{A Curious Inference}",
    Journal      = "Journal of Philosophical Logic",
    Volume       = "16",
    Pages        = "1-12",
    Comment      = "TPTPRef"
}

@Book{BBJ03,
    Author       = "Boolos, G. and Burgess, J. and Jeffrey, R.",
    Year         = "2003",
    Title        = "{Computability and Logic}",
    Publisher    = "Cambridge University Press",
    Comment      = "TPTPRef"
}

@Book{Bou89,
    Author       = "Bourbaki, N.",
    Year         = "1989",
    Title        = "{Algebra I - Chapters 1-3}",
    Publisher    = "Springer Verlag",
    Comment      = "TPTPRef"
}

@InProceedings{BCP94,
    Author       = "Bourely, C. and Caferra, R. and Peltier, N.",
    Year         = "1994",
    Title        = "{A Method for Building Models Automatically. Experiments
                    with an Extension of Otter}",
    Editor       = "Bundy, A.",
    BookTitle    = "{Proceedings of the 12th International Conference on
                    Automated Deduction}",
    Place        = "Nancy, France",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "814",
    Pages        = "72-86",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Article{BL+86,
    Author       = "Boyer, R. and Lusk E.L. and McCune, W.W. and Overbeek, R.
                    and Stickel, M.E. and Wos, L.",
    Year         = "1986",
    Title        = "{Set Theory in First-Order Logic: Clauses for Godel's
                    Axioms}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "2",
    Number       = "3",
    Pages        = "287-327",
    Comment      = "TPTPRef"
}

@Article{BM88,
    Author       = "Boyer, R. and Moore J.",
    Year         = "1988",
    Title        = "{Integrating Decision Procedures into Heuristic Theorem
                    Provers: A Case Study of Linear Arithmetic}",
    Journal      = "Machine Intelligence",
    Volume       = "11",
    Pages        = "83-124",
    Comment      = "TPTPRef"
}

@Article{BRH96,
    Author       = "Bronsard, F. and Reddy, U. and Hasker, R.",
    Year         = "1996",
    Title        = "{Induction using Term Orders}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "16",
    Number       = "1-2",
    Pages        = "3-37",
    Comment      = "TPTPRef"
}

@InProceedings{Bro11,
    Author       = "Brown, C.E.",
    Year         = "2011",
    Title        = "{Reducing Higher-Order Theorem Proving to a Sequence of SAT
                    Problems}",
    Editor       = "Bj{\o}rner, N. and Sofronie-Stokkermans, V.",
    BookTitle    = "{Proceedings of the 23rd International Conference on
                    Automated Deduction}",
    Place        = "Wroclaw, Poland",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "6803",
    Pages        = "147-161",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@InCollection{Bro08,
    Author       = "Brown, C.E.",
    Year         = "2008",
    Title        = "{M-Set Models}",
    Editor       = "Benzm{\"u}ller, C. and Brown, C.E. and Siekmann, J. and
                    Statman, R.",
    BookTitle    = "{Reasoning in Simple Type Theory: Festschrift in Honour of
                    Peter B. Andrews on his 70th Birthday}",
    Series       = "Studies in Logic, Mathematical Logic and Foundations",
    Number       = "17",
    Pages        = "175-186",
    Publisher    = "College Publications",
    Comment      = "TPTPRef"
}

@InProceedings{BS09,
    Author       = "Brown, C.E. and Smolka, G.",
    Year         = "2009",
    Title        = "{Terminating Tableaux for the Basic Fragment of Simple Type
                    Theory}",
    Editor       = "Giese, M. and Waaler, A.",
    BookTitle    = "{Proceedings of the 18th International Conference on
                    Automated Reasoning with Analytic Tableaux and Related
                    Methods}",
    Place        = "Oslo, Norway",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "5697",
    Pages        = "138-151",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@InProceedings{BS09-TPHOLs,
    Author       = "Brown, C.E. and Smolka, G.",
    Year         = "2009",
    Title        = "{Extended First-Order Logic}",
    Editor       = "Nipkow, T. and Urban, C.",
    BookTitle    = "{Proceedings of the 22nd International Conference on
                    Theorem Proving in Higher Order Logics}",
    Place        = "Munich, Germany",
    Series       = "Lecture Notes in Computer Science",
    Number       = "5674",
    Pages        = "164-179",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Article{Bru91,
    Author       = "Brushi, M.",
    Year         = "1991",
    Title        = "{The Halting Problem}",
    Journal      = "AAR Newsletter",
    Volume       = "17",
    Pages        = "7-12",
    Comment      = "TPTPRef"
}

@TechReport{BH96,
    Author       = "Buch, A. and Hillenbrand, T.",
    Year         = "1996",
    Title        = "{Waldmeister: Development of a High Performance
                    Completion-Based Theorem Prover}",
    Number       = "SEKI-Report SR-96-01",
    Institution  = "AG Effiziente Algorithmen, Universit{\"a}t
                    Kaiserslautern",
    Address      = "Kaiserslautern, Germany",
    Comment      = "TPTPRefForResults"
}

@InProceedings{BHF96,
    Author       = "Buch, A. and Hillenbrand, T. and Fettig, R.",
    Year         = "1996",
    Title        = "{Waldmeister: High Performance Equational Theorem
                    Proving}",
    Editor       = "Calmet, J. and Limongelli, C.",
    BookTitle    = "{Proceedings of the International Symposium on Design and
                    Implementation of Symbolic Computation Systems}",
    Place        = "Karlsruhe, Germany",
    Series       = "Lecture Notes in Computer Science",
    Number       = "1128",
    Pages        = "63-64",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRefForResults"
}

@InProceedings{Bum65,
    Author       = "Bumcroft, R.",
    Year         = "1965",
    Title        = "{}",
    BookTitle    = "{Proceedings of the Glasgow Mathematical Association
                    7(1)}",
    Comment      = "TPTPRef"
}

@TechReport{Bun99,
    Author       = "Bundy, A.",
    Year         = "1999",
    Title        = "{The Advantages of Binary Sinks}",
    Number       = "Blue Book Note 1311",
    Institution  = "University of Edinburgh, Mathematical Reasoning Group",
    Address      = "Edinburgh, United Kingdom",
    Comment      = "TPTPRef"
}

@TechReport{Bun97,
    Author       = "Bundy, A.",
    Year         = "1997",
    Title        = "{Non-structural Inductions and Rippling}",
    Number       = "Blue Book Note 1188",
    Institution  = "University of Edinburgh, Mathematical Reasoning Group",
    Address      = "Edinburgh, United Kingdom",
    Comment      = "TPTPRef"
}

@TechReport{Bun95,
    Author       = "Bundy, A.",
    Year         = "1995",
    Title        = "{Rippling in Harald's Problem}",
    Number       = "Blue Book Note 978",
    Institution  = "University of Edinburgh, Mathematical Reasoning Group",
    Address      = "Edinburgh, United Kingdom",
    Comment      = "TPTPRef"
}

@TechReport{Bun94,
    Author       = "Bundy, A.",
    Year         = "1994",
    Title        = "{Shankar's Arithmetic/Geometic Mean Proof}",
    Number       = "Blue Book Note 951",
    Institution  = "University of Edinburgh, Mathematical Reasoning Group",
    Address      = "Edinburgh, United Kingdom",
    Comment      = "TPTPRef"
}

@TechReport{Bun92,
    Author       = "Bundy, A.",
    Year         = "1992",
    Title        = "{How to Prove Pete's Nasty Theorem}",
    Number       = "Blue Book Note 725",
    Institution  = "University of Edinburgh, Mathematical Reasoning Group",
    Address      = "Edinburgh, United Kingdom",
    Comment      = "TPTPRef"
}

@TechReport{Bun89,
    Author       = "Bundy, A.",
    Year         = "1989",
    Title        = "{An Analysis of the Arithmetic/Geometric Mean Theorem}",
    Number       = "Blue Book Note 524",
    Institution  = "University of Edinburgh, Mathematical Reasoning Group",
    Address      = "Edinburgh, United Kingdom",
    Comment      = "TPTPRef"
}

@Book{Bun83,
    Author       = "Bundy, A.",
    Year         = "1983",
    Title        = "{The Computer Modelling of Mathematical Reasoning}",
    Publisher    = "Academic Press",
    Comment      = "TPTPRef, general reasoning"
}

@Article{Bur87,
    Author       = "Burkholder, L.",
    Year         = "1987",
    Title        = "{A 76th Automated Theorem Proving Problem}",
    Journal      = "AAR Newsletter",
    Volume       = "8",
    Pages        = "6-7",
    Comment      = "TPTPRef"
}

@Article{Bur87-SIGCSE,
    Author       = "Burkholder, L.",
    Year         = "1987",
    Title        = "{The Halting Problem}",
    Journal      = "SIGCSE bulletin",
    Comment      = "TPTPRef"
}

@Article{BAN89,
    Author       = "Burrows, M. and Abadi, M. and Needham, R.",
    Year         = "1989",
    Title        = "{A Logic of Authentication}",
    Journal      = "Proceedings of the Royal Society",
    Volume       = "426",
    Number       = "1871",
    Comment      = "TPTPRef"
}

@Article{Byl90,
    Author       = "Bylinski, C.",
    Year         = "1990",
    Title        = "{Functions and Their Basic Properties}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "1",
    Number       = "1",
    Pages        = "55-65",
    Comment      = "TPTPRef"
}

@Article{Byl90-Sets,
    Author       = "Bylinski, C.",
    Year         = "1990",
    Title        = "{Some Basic Properties of Sets}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "1",
    Number       = "1",
    Pages        = "47-53",
    Comment      = "TPTPRef"
}

@Article{Byl90,
    Author       = "Byli{\'n}ski, C.",
    Year         = "1990",
    Title        = "{Functions from a Set to a Set}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "1",
    Number       = "1",
    Pages        = "153-164",
    Comment      = "TPTPRef"
}

@InProceedings{BN10,
    Author       = "B{\"o}hme, S. and Nipkow, T.",
    Year         = "2010",
    Title        = "{Sledgehammer: Judgement Day}",
    Editor       = "Giesl, J. and Haehnle, R.",
    BookTitle    = "{Proceedings of the 5th International Joint Conference on
                    Automated Reasoning}",
    Place        = "Edinburgh, United Kingdom",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "6173",
    Pages        = "107-121",
    Comment      = "TPTPRef"
}

@Book{Bor01,
    Author       = "B{\"o}rger, E. and Gr{\"a}del, E. and Gurevich, Y.",
    Year         = "2001",
    Title        = "{The Classical Decision Problem}",
    Pages        = "33",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@InProceedings{CD+07,
    Author       = "Calvanese, D. and De Giacomo, G. and Lembo, D. and
                    Lenzerini, M. and Rosati, R.",
    Year         = "2007",
    Title        = "{EQL-Lite: Effective First-Order Query Processing in
                    Description Logics}",
    Editor       = "Velosco, M.",
    BookTitle    = "{Proceedings of the 20th International Joint Conference on
                    Artificial Intelligence}",
    Place        = "Hyderabad, India",
    Pages        = "274-279",
    Comment      = "TPTPRef"
}

@InProceedings{CK+15,
    Author       = "Caminati, M. and Kerber, M. and Lange, C. and Rowat, C.",
    Year         = "2015",
    Title        = "{Sound Auction Specification and Implementation}",
    Editor       = "Feldman, M. and Schwarz, M. and Roughgarden, T.",
    BookTitle    = "{Proceedings of the 16th ACM Conference on Economics and
                    Computation}",
    Place        = "Portland, USA",
    Pages        = "547-564",
    Publisher    = "ACM Press",
    Comment      = "TPTPRef"
}

@Book{CH00,
    Author       = "Carroll, G.R. and Hannan, M.T.",
    Year         = "2000",
    Title        = "{The Demography of Corporations and Industries}",
    Publisher    = "Princeton University Press",
    Comment      = "TPTPRef"
}

@Book{Car86,
    Author       = "Carroll, L.",
    Year         = "1986",
    Title        = "{Lewis Carroll's Symbolic Logic}",
    Publisher    = "C.N. Potter",
    Comment      = "TPTPRef"
}

@PhDThesis{Cer15,
    Author       = "Cerna, D.",
    Year         = "2015",
    Title        = "{Advances in Schematic Cut Elimination}",
    School       = "Technical University of Vienna",
    Comment      = "TPTPRef"
}

@InProceedings{CL16,
    Author       = "Cerna, D. and Leitsch, A.",
    Year         = "2016",
    Title        = "{Schematic Cut Elimination and the Ordered Pigeonhole
                    Principle}",
    Editor       = "Olivetti, N. and Tiwari, A.",
    BookTitle    = "{Proceedings of the 8th International Joint Conference on
                    Automated Reasoning}",
    Place        = "Coimbra, Portugal",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "9706",
    Pages        = "241-256",
    Comment      = "TPTPRef"
}

@Article{Cha70,
    Author       = "Chang, C-L.",
    Year         = "1970",
    Title        = "{The Unit Proof and the Input Proof in Theorem Proving}",
    Journal      = "Journal of the ACM",
    Volume       = "17",
    Number       = "4",
    Pages        = "698-707",
    Comment      = "TPTPRef, resolution/linear systems"
}

@Book{CL73,
    Author       = "Chang, C-L. and Lee, R.C-T.",
    Year         = "1973",
    Title        = "{Symbolic Logic and Mechanical Theorem Proving}",
    Publisher    = "Academic Press",
    Comment      = "TPTPRef, general reasoning"
}

@Article{CE+14,
    Author       = "Chaudhri, V. and Elenius, D. and Goldenkranz, A. and Gong,
                    A. and Martone, M. and Webb, W. and Yorke-Smith, N.",
    Year         = "2014",
    Title        = "{Comparative Analysis of Knowledge Representation and
                    Reasoning Requirements Across a Range of Life Sciences
                    Textbooks}",
    Journal      = "Journal of Biomedical Semantics",
    Volume       = "5",
    Number       = "51",
    Comment      = "TPTPRef"
}

@Article{CC+13,
    Author       = "Chaudri, V. and Cheng, B. and Overholtzer, A. and
                    Roschelle, J. and Spaulding, A. and Clark, P. and Greaves,
                    M. and Gunning, D.",
    Year         = "2013",
    Title        = "{Inquire Biology: A Textbook that Answers Questions}",
    Journal      = "AI Magazine",
    Volume       = "34",
    Number       = "3",
    Comment      = "TPTPRef"
}

@InProceedings{CDI13,
    Author       = "Chaudri, V. and Dinesh, N. and Inclezan, D.",
    Year         = "2013",
    Title        = "{Three Lessons in Creating a Knowledge Base to Enable
                    Explanation, Reasoning and Dialog}",
    Editor       = "Klenk, M. and Laird, J.",
    BookTitle    = "{Proceedings of the 2nd Annual Conference on Advances in
                    Cognitive Systems}",
    Place        = "Baltimore, USA",
    Pages        = "187-203",
    Comment      = "TPTPRef"
}

@Book{Che80,
    Author       = "Chellas, B.F.",
    Year         = "1980",
    Title        = "{Modal Logic}",
    Publisher    = "Cambridge University Press",
    Comment      = "TPTPRef"
}

@InProceedings{CP94,
    Author       = "Chu, H. and Plaisted, D.",
    Year         = "1994",
    Title        = "{Semantically Guided First-order Theorem Proving using
                    Hyper-linking}",
    Editor       = "Bundy, A.",
    BookTitle    = "{Proceedings of the 12th International Conference on
                    Automated Deduction}",
    Place        = "Nancy, France",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "814",
    Pages        = "192-206",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRefForResults"
}

@Book{Chu56,
    Author       = "Church, A.",
    Year         = "1956",
    Title        = "{Introduction to Mathematical Logic I}",
    Publisher    = "Princeton University Press",
    Comment      = "TPTPRef"
}

@InProceedings{CHM02,
    Author       = "Claessen, K. and H{\"a}hnle, R. and M{\aa}rtensson, J.",
    Year         = "2002",
    Title        = "{Verification of Hardware Systems with First-Order Logic}",
    Editor       = "Sutcliffe, G. and Pelletier, J. and Suttner, C.",
    BookTitle    = "{Proceedings of the CADE-18 Workshop - Problem and Problem
                    Sets for ATP}",
    Place        = "Copenhagen, Denmark",
    Series       = "Department of Computer Science, University of Copenhagen,
                    Technical Report",
    Number       = "02/10",
    Comment      = "TPTPRef"
}

@InProceedings{CL09,
    Author       = "Claessen, K. and Lilliestrom, A.",
    Year         = "2009",
    Title        = "{Automated Inference of Finite Unsatisfiability}",
    Editor       = "Schmidt, R.",
    BookTitle    = "{Proceedings of the 22nd International Conference on
                    Automated Deduction}",
    Place        = "Montreal Canada",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "5663",
    Pages        = "388-403",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@InProceedings{CS18,
    Author       = "Claessen, K. and Smallbone, N.",
    Year         = "2018",
    Title        = "{Efficient Encodings of First-Order Horn Formulas in
                    Equational Logic}",
    Editor       = "Galmiche, D. and Schulz, S. and Sebastiani, R.",
    BookTitle    = "{Proceedings of the 9th International Joint Conference on
                    Automated Reasoning}",
    Place        = "Oxford, United Kingdom",
    Series       = "Lecture Notes in Computer Science",
    Number       = "10900",
    Pages        = "388-404",
    Comment      = "TPTPRef"
}

@InProceedings{Coh00,
    Author       = "Cohen, E.",
    Year         = "2000",
    Title        = "{Separation and Reduction}",
    Editor       = "Backhouse, R. and Oliveira, J.",
    BookTitle    = "{Proceedings of the 5th International Conference on the
                    Mathematics of Program Construction}",
    Place        = "Ponte de Lima, Portugal",
    Series       = "Lecture Notes in Computer Science",
    Number       = "1837",
    Pages        = "45-59",
    Comment      = "TPTPRef"
}

@Book{CB+89,
    Author       = "Comaromi, J.P. and Beall, J. and Matthews, W.E. and New,
                    G.R.",
    Year         = "1989",
    Title        = "{Dewey Decimal Classification and Relative Index}",
    Edition      = "20",
    Publisher    = "Forest Press",
    Comment      = "TPTPRef"
}

@Book{Con71,
    Author       = "Conway, J.",
    Year         = "1971",
    Title        = "{Regular Algebra and Finite Machines}",
    Publisher    = "Chapman and Hall",
    Comment      = "TPTPRef"
}

@Article{CR79,
    Author       = "Cook, S. and Reckhow, R.",
    Year         = "1979",
    Title        = "{The Relative Efficiency of Propositional Proof Systems}",
    Journal      = "Journal of Symbolic Logic",
    Volume       = "44",
    Pages        = "36-50",
    Comment      = "TPTPRef"
}

@InProceedings{CF+10,
    Author       = "Cramer, M. and Fisseni, B. and Koepke, P. and
                    K{\"u}hlwein, D. and Schr{\"o}der, B. and Veldman, J.",
    Year         = "2010",
    Title        = "{The Naproche Project: Controlled Natural Language Proof
                    Checking of Mathematical Texts}",
    Editor       = "Fuchs, N.",
    BookTitle    = "{Proceedings of the Workshop on Controlled Natural
                    Languages}",
    Place        = "Marettimo Island, Italy",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "5972",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Article{CDK10,
    Author       = "Cs{\"o}rg{\"o}, P. and Dr{\'a}pal, A. and Kinyon, M.",
    Year         = "2010",
    Title        = "{Buchsteiner Loops}",
    Journal      = "International Journal of Algebra and Computation",
    Volume       = "19",
    Number       = "8",
    Pages        = "1049-1088",
    Comment      = "TPTPRef"
}

@Book{CF58,
    Author       = "Curry, H.B. and Feys, R.",
    Year         = "1958",
    Title        = "{Combinatory Logic I}",
    Publisher    = "North Holland, Amsterdam",
    Comment      = "TPTPRef"
}

@Book{CHS72,
    Author       = "Curry, H.B. and Hindley, J.R. and Seldin, J.P.",
    Year         = "1972",
    Title        = "{Combinatory Logic II}",
    Publisher    = "North Holland, Amsterdam",
    Comment      = "TPTPRef"
}

@Article{Dar90,
    Author       = "Darmochwa{\l}, A.",
    Year         = "1990",
    Title        = "{Compact Spaces}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "1",
    Number       = "2",
    Pages        = "383-386",
    Comment      = "TPTPRef"
}

@Article{Dar90,
    Author       = "Darmochwa{\l}, A.",
    Year         = "1989",
    Title        = "{Finite Sets}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "1",
    Number       = "1",
    Pages        = "165-167",
    Comment      = "TPTPRef"
}

@InProceedings{dSP08,
    Author       = "de Melo, G. and Suchanek, F. and Pease, A.",
    Year         = "2008",
    Title        = "{Integrating YAGO into the Suggested Upper Merged
                    Ontology}",
    Editor       = "Chung, S.",
    BookTitle    = "{Proceedings of the 20th IEEE International Conference on
                    Tools with Artificial Intelligence}",
    Place        = "Dayton, USA",
    Pages        = "190-193",
    Publisher    = "IEEE Computer Society",
    Comment      = "TPTPRef"
}

@Unpublished{deN-Bliksem-URL,
    Author       = "de Nivelle, H.",
    Year         = "",
    Title        = "{Bliksem Resolution Prover}",
    Note         = "http://www.ii.uni.wroc.pl/~nivelle/software/bliksem",
    Comment      = "TPTPRef"
}

@Article{deN11,
    Author       = "de Nivelle, H.",
    Year         = "2011",
    Title        = "{Classical Logic with Partial Functions}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "47",
    Number       = "4",
    Pages        = "399-425",
    Comment      = "TPTPRefForResults"
}

@InProceedings{deN10,
    Author       = "de Nivelle, H.",
    Year         = "2010",
    Title        = "{Classical Logic with Partial Functions}",
    Editor       = "Giesl, J. and Haehnle, R.",
    BookTitle    = "{Proceedings of the 5th International Joint Conference on
                    Automated Reasoning}",
    Place        = "Edinburgh, United Kingdom",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "6173",
    Pages        = "203-217",
    Comment      = "TPTPRef"
}

@InProceedings{dNP05,
    Author       = "de Nivelle, H. and Piskac, R.",
    Year         = "2005",
    Title        = "{Verification of an Off-Line Checker for Priority Queues}",
    Editor       = "Aichernig, B. and Beckert, B.",
    BookTitle    = "{Proceedings of the 3rd IEEE International Conference on
                    Software Engineering and Formal Methods}",
    Place        = "Los Alamitos, USA",
    Pages        = "210-219",
    Comment      = "TPTPRef"
}

@InProceedings{DeC79,
    Author       = "DeChampeaux, D.",
    Year         = "1979",
    Title        = "{Sub-problem Finder and Instance Checker: Two Co-operating
                    Preprocessors for Theorem Provers}",
    BookTitle    = "{Proceedings of the 6th International Joint Conference on
                    Artificial Intelligence}",
    Pages        = "191-196",
    Publisher    = "Morgan Kaufmann",
    Comment      = "TPTPRef"
}

@Article{DeC72,
    Author       = "DeChampeaux, D.",
    Year         = "1972",
    Title        = "{Sub-problem Finder and Instance Checker: Two Co-operating
                    Preprocessors for Theorem Provers}",
    Journal      = "Journal of the ACM",
    Volume       = "33",
    Pages        = "633-657",
    Comment      = "TPTPRef"
}

@InProceedings{DKS08,
    Author       = "Delaune, S. and Kremer, S. and Steel, G.",
    Year         = "2008",
    Title        = "{Formal Analysis of PKCS#11}",
    Editor       = "Sabelfeld, A.",
    BookTitle    = "{Proceedings of the 21st IEEE Computer Security Foundations
                    Symposium}",
    Place        = "Pittsburg, USA",
    Pages        = "331-344",
    Publisher    = "IEEE Press",
    Comment      = "TPTPRef"
}

@MastersThesis{Del10,
    Author       = "Dellis, N.",
    Year         = "2010",
    Title        = "{Using Controlled Natural Language for World Knowledge
                    Reasoning}",
    School       = "University of Miami",
    Address      = "Miami, USA",
    Comment      = "TPTPRef"
}

@InProceedings{DFS04-IJCAR,
    Author       = "Denney, E. and Fischer, B. and Schumann, J.",
    Year         = "2004",
    Title        = "{Using Automated Theorem Provers to Certify Auto-generated
                    Aerospace Software}",
    Editor       = "Rusinowitch, M. and Basin, D.",
    BookTitle    = "{Proceedings of the 2nd International Joint Conference on
                    Automated Reasoning}",
    Place        = "Cork, Ireland",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "3097",
    Pages        = "198-212",
    Comment      = "TPTPRef,TPTPCite"
}

@InProceedings{DB02,
    Author       = "Dennis, L. and Bundy, A.",
    Year         = "2002",
    Title        = "{A Comparison of two Proof Critics: Power vs. Robustness}",
    Editor       = "Carreno, V. and Munoz, C. and Tahar, S.",
    BookTitle    = "{Proceedings of the 15th International Conference on
                    Theorem Proving in Higher Order Logics}",
    Place        = "Hampton, USA",
    Series       = "Lecture Notes in Computer Science",
    Number       = "2410",
    Pages        = "182-198",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Article{DKS97-JAR-18,
    Author       = "Denzinger, J. and Kronenburg, M. and Schulz, S.",
    Year         = "1997",
    Title        = "{DISCOUNT: A Distributed and Learning Equational Prover}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "18",
    Number       = "2",
    Pages        = "189-198",
    Comment      = "TPTPRefForResults"
}

@InProceedings{DS96-CADE-13,
    Author       = "Denzinger, J. and Schulz, S.",
    Year         = "1996",
    Title        = "{Learning Domain Knowledge to Improve Theorem Proving}",
    Editor       = "McRobbie, M. and Slaney, J.K.",
    BookTitle    = "{Proceedings of the 13th International Conference on
                    Automated Deduction}",
    Place        = "New Brunswick, USA",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "1104",
    Pages        = "62-76",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRefForResults,TPTPCite"
}

@Article{DS96-JSC,
    Author       = "Denzinger, J. and Schulz, S.",
    Year         = "1996",
    Title        = "{Recording and Analysing Knowledge-Based Distributed
                    Deduction Processes}",
    Journal      = "Journal of Symbolic Computation",
    Volume       = "21",
    Pages        = "523-541",
    Comment      = "TPTPRefForResults"
}

@Article{DMS06,
    Author       = "Desharnais, J. and M{\"o}ller, B. and Struth, G.",
    Year         = "2006",
    Title        = "{Kleene Algebra with Domain}",
    Journal      = "ACM Transactions on Computational Logic",
    Volume       = "7",
    Number       = "4",
    Pages        = "798-833",
    Comment      = "TPTPRef"
}

@InProceedings{DMS04,
    Author       = "Desharnais, J. and M{\"o}ller, B. and Struth, G.",
    Year         = "2004",
    Title        = "{Termination in Modal Kleene Algebra}",
    Editor       = "L{\'e}vy, J. and Mayr, E. and Mitchell, J.",
    BookTitle    = "{Proceedings of the 18th World Computer Congress, 3rd
                    International Conference on Theoretical Computer
                    Science}",
    Place        = "Toulouse, France",
    Pages        = "647-660",
    Publisher    = "Kluwer",
    Comment      = "TPTPRef"
}

@InProceedings{DS08,
    Author       = "Desharnais, J. and Struth, G.",
    Year         = "2008",
    Title        = "{Modal Semirings Revisited}",
    Editor       = "Audebaud, P. and Paulin-Mohring, C.",
    BookTitle    = "{Proceedings of the 9th International Conference on the
                    Mathematics of Program Construction}",
    Place        = "Marseille, France",
    Series       = "Lecture Notes in Computer Science",
    Number       = "5133",
    Pages        = "360-387",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Article{DBW97,
    Author       = "Doornbos, H. and Backhouse, R. and van der Woude, J.",
    Year         = "1997",
    Title        = "{A Calculational Approach to Mathematical Induction}",
    Journal      = "Theoretical Computer Science",
    Volume       = "179",
    Pages        = "103-135",
    Comment      = "TPTPRef"
}

@InProceedings{DHK95,
    Author       = "Dowek, G. and Hardin, T. and Kirchner, C.",
    Year         = "1995",
    Title        = "{Higher-order Unification via Explicit Substitutions}",
    Editor       = "Kozen, D.",
    BookTitle    = "{Proceedings of the 10th Annual IEEE Symposium on Logic in
                    Computer Science}",
    Place        = "San Diego, USA",
    Pages        = "366-374",
    Publisher    = "IEEE Computer Society Press",
    Comment      = "TPTPRef"
}

@TechReport{Dra93,
    Author       = "Draeger, J.",
    Year         = "1993",
    Title        = "{Anwendung des Theorembeweisers SETHEO auf angeordnete
                    K{\"o}rper}",
    Number       = "FKI-186-93",
    Institution  = "Technische Universit{\"a}t M{\"u}nchen",
    Address      = "M{\"u}nchen, Germany",
    Comment      = "TPTPRef"
}

@Book{DG79,
    Author       = "Dreben, B. and Goldfarb, W.",
    Year         = "1979",
    Title        = "{Decision Problem: Solvable Classes of Quantificational
                    Formulas}",
    Pages        = "120",
    Publisher    = "Addison-Wesley",
    Comment      = "TPTPRef"
}

@Unpublished{DdM06,
    Author       = "Dutertre, B. and de Moura, L.",
    Year         = "2006",
    Title        = "{The YICES SMT Solver}",
    Note         = "http://yices.csl.sri.com/tool-paper.pdf",
    Comment      = "TPTPRef"
}

@InProceedings{EH+16,
    Author       = "Ebner, G. and Hetzl, S. and Reis, G. and Riener, M. and
                    Wolfsteiner, S. and Zivota, S.",
    Year         = "2016",
    Title        = "{System Description: GAPT 2.0}",
    Editor       = "Olivetti, N. and Tiwari, A.",
    BookTitle    = "{Proceedings of the 8th International Joint Conference on
                    Automated Reasoning}",
    Place        = "Coimbra, Portugal",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "9706",
    Pages        = "293-301",
    Comment      = "TPTPRef"
}

@Article{EI+08,
    Author       = "Eiter, T. and Iannis, G. and Lukasiewicz, T. and
                    Schindlauer, R. and Tompits, H.",
    Year         = "2008",
    Title        = "{Combining Answer Set Programming with Description Logics
                    for the Semantic Web}",
    Journal      = "Artificial Intelligence",
    Volume       = "172",
    Number       = "12-13",
    Pages        = "1495-1539",
    Comment      = "TPTPRefForResults"
}

@Article{Ern02,
    Author       = "Ernst, Z.",
    Year         = "2002",
    Title        = "{Completions from TV-> to H->}",
    Journal      = "Bulletin of the Section of Logic",
    Comment      = "TPTPRef"
}

@InProceedings{EF+02,
    Author       = "Ernst, Z. and Fitelson, B. and Harris, K. and McCune, W.
                    and Padmanabhan, R. and Veroff, R. and Wos, L.",
    Year         = "2002",
    Title        = "{More First-order Test Problems in Math and Logic}",
    Editor       = "Sutcliffe, G. and Pelletier, J. and Suttner, C.",
    BookTitle    = "{Proceedings of the CADE-18 Workshop - Problem and Problem
                    Sets for ATP}",
    Place        = "Copenhagen, Denmark",
    Series       = "Department of Computer Science, University of Copenhagen,
                    Technical Report",
    Number       = "02/10",
    Comment      = "TPTPRef"
}

@Article{EF+01,
    Author       = "Ernst, Z. and Fitelson, B. and Harris, K. and Wos, L.",
    Year         = "2001",
    Title        = "{A Concise Axiomatization of RM->}",
    Journal      = "Bulletin of the Section of Logic",
    Volume       = "30",
    Number       = "4",
    Pages        = "191-194",
    Comment      = "TPTPRef"
}

@InProceedings{EHK99,
    Author       = "Eschenbach, C. and Habel, C. and Kulik, L.",
    Year         = "1999",
    Title        = "{Representing Simple Trajectories as Oriented Curves}",
    Editor       = "Russell I. and Kumar, A.",
    BookTitle    = "{Proceedings of the 12th International FLAIRS Conference}",
    Place        = "Orlando, USA",
    Pages        = "431-436",
    Publisher    = "AAAI Press",
    Comment      = "TPTPRef"
}

@InProceedings{FH+98,
    Author       = "Farinas del Cerro, L. and Herzig, A. and Longin, D. and
                    Rifi, O.",
    Year         = "1998",
    Title        = "{Belief Reconstruction in Cooperative Dialogues}",
    Editor       = "Giunchiglia, F.",
    BookTitle    = "{Proceedings of the 8th International Conference on
                    Artificial Intelligence: Methodology, SYstems, and
                    Applications}",
    Place        = "Sozopol, Bulgaria",
    Series       = "Lecture Notes in Computer Science",
    Number       = "1480",
    Pages        = "254-266",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Book{Fel98,
    Author       = "Fellbaum, C.",
    Year         = "1998",
    Title        = "{WordNet: An Electronic Lexical Database}",
    Publisher    = "MIT Press",
    Comment      = "TPTPRef"
}

@Book{FL+93,
    Author       = "Ferm{\"u}ller, C. and Leitsch, A. and Tammet, T. and
                    Zamov, N.",
    Year         = "1993",
    Title        = "{Resolution Methods for the Decision Problem}",
    Series       = "Lecture Notes in Computer Science",
    Number       = "679",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Book{Fey50,
    Author       = "Feys, R.",
    Year         = "1950",
    Title        = "{Les systemes formalises de modalites aristoteliciennes}",
    Comment      = "TPTPRef"
}

@Article{FH01,
    Author       = "Fitelson, B. and Harris, K.",
    Year         = "2001",
    Title        = "{Distributivity in LN0 and other Sentential Logics}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "27",
    Number       = "2",
    Pages        = "141-156",
    Comment      = "TPTPRef"
}

@Article{FW01,
    Author       = "Fitelson, B. and Wos, L.",
    Year         = "2001",
    Title        = "{Missing Proofs Found}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "27",
    Number       = "2",
    Pages        = "201-225",
    Comment      = "TPTPRef"
}

@Article{FZ07,
    Author       = "Fitelson, B. and Zalta, E.",
    Year         = "2007",
    Title        = "{Steps Toward a Computational Metaphysics}",
    Journal      = "Journal of Philosophical Logic",
    Volume       = "36",
    Number       = "2",
    Pages        = "227-247",
    Comment      = "TPTPRef"
}

@InCollection{Fit07,
    Author       = "Fitting, M.",
    Year         = "2007",
    Title        = "{Modal Proof Theory}",
    Editor       = "Blackburn, P. and van Benthem, J. and Wolther, F.",
    BookTitle    = "{Handbook of Modal Logic}",
    Pages        = "86-135",
    Publisher    = "Elsevier",
    Comment      = "TPTPRef"
}

@InCollection{Fit00,
    Author       = "Fitting, M.",
    Year         = "2000",
    Title        = "{Higher-Order Modal Logic - A Sketch}",
    Editor       = "Caferra, R. and Salzer, G.",
    BookTitle    = "{Automated Deduction in Classical and Non-Classical
                    Logics}",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "1761",
    Pages        = "23-38",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Book{FM98,
    Author       = "Fitting, M. and Mendelsohn, R.",
    Year         = "1998",
    Title        = "{First-Order Modal Logic}",
    Publisher    = "Kluwer",
    Comment      = "TPTPRef"
}

@Article{FL+74,
    Author       = "Fleisig, S. and Loveland, D.W. and Smiley, A.K. and
                    Yarmush D.L.",
    Year         = "1974",
    Title        = "{An Implementation of the Model Elimination Proof
                    Procedure}",
    Journal      = "Journal of the ACM",
    Volume       = "21",
    Number       = "1",
    Pages        = "124-139",
    Comment      = "TPTPRef, linear systems"
}

@Article{FRT84,
    Author       = "Font, J.M. and Rodriguez, A.J. and Torrens, A.",
    Year         = "1984",
    Title        = "{Wajsberg Algebras}",
    Journal      = "Stochastica",
    Volume       = "8",
    Number       = "1",
    Pages        = "5-31",
    Comment      = "TPTPRef"
}

@InProceedings{FMW11,
    Author       = "Fontaine, P. and Merz, S. and Woltzenlogel Paleo, B.",
    Year         = "2011",
    Title        = "{Compression of Propositional Resolution Proofs via Partial
                    Regularization}",
    Editor       = "Bj{\o}rner, N. and Sofronie-Stokkermans, V.",
    BookTitle    = "{Proceedings of the 23rd International Conference on
                    Automated Deduction}",
    Place        = "Wroclaw, Poland",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "6803",
    Pages        = "237-251",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Book{For94,
    Author       = "Forbes, G.",
    Year         = "1994",
    Title        = "{Modern Logic. A Text in Elementary Symbolic Logic}",
    Publisher    = "Oxford University Press",
    Comment      = "TPTPRef"
}

@Article{Fri63,
    Author       = "Friedman, J.",
    Year         = "1963",
    Title        = "{A Semi-Decision Procedure for the Functional Calculus}",
    Journal      = "Journal of the ACM",
    Volume       = "10",
    Number       = "1",
    Pages        = "1-24",
    Comment      = "TPTPRef,sample problems"
}

@Article{Fri04,
    Author       = "Friedrich, S.",
    Year         = "2004",
    Title        = "{Lazy Lists II}",
    Journal      = "Archive of Formal Proofs",
    Note         = "http://isa-afp.org/entries/Lazy-Lists-II.shtml",
    Comment      = "TPTPRef"
}

@TechReport{Fuc94,
    Author       = "Fuchs, M.",
    Year         = "1994",
    Title        = "{The Application of Goal-Orientated Heuristics for Proving
                    Equational Theorems via the Unfailing Knuth-Bendix
                    Completion Procedure. A case study: lattice ordered
                    groups}",
    Number       = "SEKI-Report SR-94-02",
    Institution  = "Universit{\"a}t Kaiserslautern",
    Address      = "Kaiserslautern, Germany",
    Comment      = "TPTPRef"
}

@InProceedings{FKK08,
    Author       = "Fuchs, N. and Kaljurand, K. and Kuhn, T.",
    Year         = "2008",
    Title        = "{Attempto Controlled English for Knowledge
                    Representation}",
    Editor       = "Baroglio, C. and Bonatti, P. and Maluszynski, J. and
                    Marchiori, M. and Polleres, A. and Schaffert, S.",
    BookTitle    = "{Proceedings of Reasoning Web: 4th International Summer
                    School}",
    Place        = "Venice, Italy",
    Series       = "Lecture Notes in Computer Science",
    Number       = "5224",
    Pages        = "104-124",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@InProceedings{FH+92,
    Author       = "Fujita, M. and Hasegawa, R. and Koshimura, M. and Fujita,
                    H.",
    Year         = "1992",
    Title        = "{Model Generation Theorem Provers on a Parallel Inference
                    Machine}",
    BookTitle    = "{Proceedings of the International Conference on Fifth
                    Generation Computer Systems}",
    Pages        = "357-375",
    Comment      = "TPTPRef"
}

@InProceedings{FSB93,
    Author       = "Fujita, M. and Slaney, J.K. and Bennett, F.",
    Year         = "1993",
    Title        = "{Automatic Generation of Some Results in Finite Algebra}",
    Editor       = "Bajcsy, R.",
    BookTitle    = "{Proceedings of the 13th International Joint Conference on
                    Artificial Intelligence}",
    Place        = "Chambery, France",
    Pages        = "52-57",
    Publisher    = "Morgan Kaufmann",
    Comment      = "TPTPRef"
}

@InProceedings{FG+08,
    Author       = "Furbach, U. and Gl{\"o}ckner, I. and Helbig, H. and
                    Pelzer, B.",
    Year         = "2008",
    Title        = "{LogAnswer - A Deduction-Based Question Answering System}",
    Editor       = "Baumgartner, P. and Armando, A. and Dowek, G.",
    BookTitle    = "{Proceedings of the 4th International Joint Conference on
                    Automated Reasoning}",
    Place        = "Sydney, Australia",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "5195",
    Pages        = "139-146",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Article{Gan96-JFM,
    Author       = "Ganczarski, J.",
    Year         = "1996",
    Title        = "{On the Lattice of Subgroups of a Group}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "5",
    Number       = "3",
    Pages        = "309-312",
    Comment      = "TPTPRef,LATSUBGR"
}

@InProceedings{Gar08,
    Author       = "Garg, D.",
    Year         = "2008",
    Title        = "{Principal-Centric Reasoning in Constructive Authorization
                    Logic}",
    BookTitle    = "{Proceedings of the LICS 2008 Workshop on Intuitionistic
                    Modal Logics and Applications}",
    Place        = "Pittsburg, USA",
    Comment      = "TPTPRef"
}

@InProceedings{GA08,
    Author       = "Garg, D. and Abadi, M.",
    Year         = "2008",
    Title        = "{A Modal Deconstruction of Access Control Logics}",
    Editor       = "Amadio, R.",
    BookTitle    = "{Proceedings of the 11th International Conference on the
                    Foundations of Software Science and Computational
                    Structures}",
    Place        = "Budapest, Hungary",
    Series       = "Lecture Notes in Computer Science",
    Number       = "4962",
    Pages        = "216-230",
    Comment      = "TPTPRef"
}

@InProceedings{GK15,
    Author       = "Gauthier, T. and Kaliszyk, C.",
    Year         = "2015",
    Title        = "{Premise Selection and External Provers for HOL4}",
    Editor       = "Leroy, X. and Tiu, A.",
    BookTitle    = "{Proceedings of the 4th ACM SIGPLAN Conference on Certified
                    Programs and Proofs}",
    Place        = "Mumbai, India",
    Pages        = "49-57",
    Publisher    = "ACM Press",
    Comment      = "TPTPRef"
}

@TechReport{GF92,
    Author       = "Genesereth, M.R. and Fikes, R.E.",
    Year         = "1992",
    Title        = "{Knowledge Interchange Format, Version 3.0 Reference
                    Manual}",
    Number       = "Logic-92-1",
    Institution  = "Computer Science Department, Stanford University",
    Comment      = "TPTPRef"
}

@Book{Gir00,
    Author       = "Girle, R.A.",
    Year         = "2000",
    Title        = "{Modal Logics and Philosophy}",
    Publisher    = "Acumen Publishers",
    Comment      = "TPTPRef"
}

@Article{GO86,
    Author       = "Glickfield, B. and Overbeek, R.",
    Year         = "1986",
    Title        = "{A Foray into Combinatory Logic}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "2",
    Number       = "4",
    Pages        = "419-431",
    Comment      = "TPTPRef"
}

@InProceedings{Glo07,
    Author       = "Gl{\"o}ckner, I.",
    Year         = "2007",
    Title        = "{University of Hagen at CLEF 2007: Answer Validation
                    Exercise}",
    Editor       = "Nardi, .A. and Peters, C.",
    BookTitle    = "{Working Notes for the CLEF 2007 Workshop}",
    Place        = "Budapest, Hungary",
    Comment      = "TPTPRef"
}

@InCollection{Gol06,
    Author       = "Goldblatt, R.",
    Year         = "2006",
    Title        = "{Mathematical Modal Logic: A View of its Evolution}",
    Editor       = "Gabbay, D. and Woods, J.",
    BookTitle    = "{Logic and the Modalities in the Twentieth Century}",
    Series       = "Handbook of the History of Logic",
    Number       = "7",
    Pages        = "1-98",
    Publisher    = "Elsevier",
    Comment      = "TPTPRef"
}

@Book{Gol92,
    Author       = "Goldblatt, R.",
    Year         = "1992",
    Title        = "{Logics of Time and Computation}",
    Series       = "Center for the Study of Language and Information - Lecture
                    Notes",
    Publisher    = "The University of Chicago Press",
    Comment      = "TPTPRef"
}

@TechReport{Gol93,
    Author       = "Goller, C.",
    Year         = "1993",
    Title        = "{Anwendung des Theorembeweisers SETHEO auf die Theorie der
                    Halbgruppen und Gruppen}",
    Number       = "FKI-174-93",
    Institution  = "Technische Universit{\"a}t M{\"u}nchen",
    Address      = "M{\"u}nchen, Germany",
    Comment      = "TPTPRef"
}

@Book{GW+03,
    Author       = "Gow, J. and Walsh, T. and Colton, S. and Sorge, V.",
    Year         = "2003",
    Title        = "{Proceedings of the Workshop on Challenges and Novel
                    Applications for Automated Reasoning, 19th International
                    Conference on Automated Reasoning}",
    Place        = "Miami, USA",
    Comment      = "TPTPRef"
}

@Article{GM97,
    Author       = "Grabowski, A. and Milewski, R.",
    Year         = "1997",
    Title        = "{Boolean Posets, Posets under Inclusion and Products of
                    Relational Structures}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "6",
    Number       = "1",
    Pages        = "117-121",
    Comment      = "TPTPRef"
}

@InProceedings{GE+15,
    Author       = "Grewe, S. and Erdweg, S. and Wittman, P. and Mezini, M.",
    Year         = "2015",
    Title        = "{Type Systems for the Masses: Deriving Soundness Proofs and
                    Efficient Checkers}",
    Editor       = "Murphy, G.",
    BookTitle    = "{Proceedings of Onward!}",
    Place        = "Pittsburg, USA",
    Publisher    = "ACM Press",
    Comment      = "TPTPRef"
}

@Article{GO+69,
    Author       = "Guard, J.R. and Oglesby, F.C. and Bennett, J.H. and Settle
                    L.G.",
    Year         = "1969",
    Title        = "{Semi-Automated Mathematics}",
    Journal      = "Journal of the ACM",
    Volume       = "16",
    Number       = "1",
    Pages        = "49-62",
    Comment      = "TPTPRef"
}

@InCollection{Goe69,
    Author       = "G{\"o}del, K.",
    Year         = "1969",
    Title        = "{An Interpretation of the Intuitionistic Sentential
                    Logic}",
    Editor       = "Hintikka, J.",
    BookTitle    = "{The Philosophy of Mathematics}",
    Pages        = "128-129",
    Publisher    = "Oxford University Press",
    Comment      = "TPTPRef"
}

@InCollection{Goe33,
    Author       = "G{\"o}del, K.",
    Year         = "1933",
    Title        = "{An Interpretation of the Intuitionistic Propositional
                    Calculus}",
    Editor       = "Feferman, S. and Dawson, J. and Kleene, S. and Moore, G.
                    and Solovay, R. and van Heijenoort, J.",
    BookTitle    = "{Collected Works: Publications 1929-1936}",
    Publisher    = "Oxford University Press",
    Comment      = "TPTPRef"
}

@Book{Hac66,
    Author       = "Hackstaff, L.",
    Year         = "1966",
    Title        = "{Systems of Formal Logic}",
    Publisher    = "Reidel Publishing",
    Comment      = "TPTPRef"
}

@Unpublished{Hal-Logic-URL,
    Author       = "Halleck, J.",
    Year         = "",
    Title        = "{John Halleck's Logic Systems}",
    Note         = "http://www.cc.utah.edu/~nahaj/logic/structures/systems/",
    Comment      = "TPTPRef"
}

@Article{Han98,
    Author       = "Hannan, M.T.",
    Year         = "1998",
    Title        = "{Rethinking Age Dependence in Organizational Mortality:
                    Logical Formalizations}",
    Journal      = "American Journal of Sociology",
    Volume       = "104",
    Pages        = "126-164",
    Comment      = "TPTPRef"
}

@Book{Har69,
    Author       = "Harary, F.",
    Year         = "1969",
    Title        = "{Graph Theory}",
    Publisher    = "Addison-Wesley",
    Comment      = "TPTPRef"
}

@Book{HW92,
    Author       = "Hardy, G.H. and Wright, E.M.",
    Year         = "1992",
    Title        = "{An Introduction to the Theory of Numbers}",
    Edition      = "5",
    Publisher    = "Oxford UP",
    Comment      = "TPTPRef"
}

@Book{Hay93,
    Author       = "Hayes, J.P.",
    Year         = "1993",
    Title        = "{Introduction to Digital Logic Circuit Design}",
    Publisher    = "Addison Wesley",
    Comment      = "TPTPRef"
}

@Article{He01-JAR,
    Author       = "He, L.",
    Year         = "2001",
    Title        = "{I-SATCHMO: An Improvement of SATCHMO}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "27",
    Number       = "3",
    Pages        = "313-322",
    Comment      = "TPTPCite,TPTPRef"
}

@Article{HC+98,
    Author       = "He, L. and Chao, Y. and Shimajiri, Y. and Seki, H. and
                    Itoh, H.",
    Year         = "1998",
    Title        = "{A-SATCHMORE: SATCHMORE with Availability Checking}",
    Journal      = "New Generation Computing",
    Volume       = "16",
    Pages        = "55-74",
    Comment      = "TPTPRef"
}

@Book{Hea56,
    Author       = "Heath, T.",
    Year         = "1956",
    Title        = "{The Thirteen Books of Euclid's Elements}",
    Publisher    = "Dover Publications",
    Comment      = "TPTPRef"
}

@Article{HK+94,
    Author       = "Heinsohn, J. and Kudenko, D. and Nebel, B. and Profitlich,
                    H-J.",
    Year         = "1994",
    Title        = "{An Empirical Analysis of Terminological Representation
                    Systems}",
    Journal      = "Artificial Intelligence",
    Volume       = "68",
    Number       = "2",
    Pages        = "367-397",
    Comment      = "TPTPRef"
}

@Article{Hen50,
    Author       = "Henkin, L.",
    Year         = "1950",
    Title        = "{Completeness in the Theory of Types}",
    Journal      = "Journal of Symbolic Logic",
    Volume       = "15",
    Number       = "2",
    Pages        = "81-91",
    Comment      = "TPTPRef"
}

@Book{HMT71,
    Author       = "Henkin, L. and Monk, J. and Tarski, A.",
    Year         = "1971",
    Title        = "{Cylindrical Algebras}",
    Volume       = "Part 1",
    Publisher    = "North-Holland",
    Comment      = "TPTPRef"
}

@Article{HN52,
    Author       = "Higman, G. and Neumann, B.H.",
    Year         = "1952",
    Title        = "{Groups as Groupoids with One Law}",
    Journal      = "Publicationes Mathematicae Debrecen",
    Volume       = "2",
    Pages        = "215-227",
    Comment      = "TPTPRef"
}

@Book{HB34,
    Author       = "Hilbert, D. and Bernays, P.",
    Year         = "1934",
    Title        = "{Grundlagen der Mathematick}",
    Publisher    = "Julius Springer Verlag",
    Comment      = "TPTPRef"
}

@InProceedings{HBF96,
    Author       = "Hillenbrand, T. and Buch, A. and Fettig, R.",
    Year         = "1996",
    Title        = "{On Gaining Efficiency in Completion-Based Theorem
                    Proving}",
    Editor       = "Ganzinger, H.",
    BookTitle    = "{Proceedings of the 7th International Conference on
                    Rewriting Techniques and Applications}",
    Place        = "New Brunswick, USA",
    Series       = "Lecture Notes in Computer Science",
    Number       = "1103",
    Pages        = "432-435",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRefForResults"
}

@Article{HB+97,
    Author       = "Hillenbrand, T. and Buch, A. and Vogt, R. and L{\"o}chner,
                    B.",
    Year         = "1997",
    Title        = "{Waldmeister: High Performance Equational Deduction}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "18",
    Number       = "2",
    Pages        = "265-270",
    Comment      = "TPTPRefForResults"
}

@InProceedings{HJL99,
    Author       = "Hillenbrand, T. and Jaeger, A. and L{\"o}chner, B.",
    Year         = "1999",
    Title        = "{Waldmeister - Improvements in Performance and Ease of
                    Use}",
    Editor       = "Ganzinger, H.",
    BookTitle    = "{Proceedings of the 16th International Conference on
                    Automated Deduction}",
    Place        = "Trento, Italy",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "1632",
    Pages        = "232-236",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRefForResults,TPTPCite"
}

@InProceedings{Hoe94,
    Author       = "Hoepman, J-H.",
    Year         = "1994",
    Title        = "{Uniform Deterministic Self-Stabilizing Ring-Orientation on
                    Odd-Length Rings}",
    Editor       = "Tel, G. and Vitanyi, P.",
    BookTitle    = "{Proceedings of the 8th International Workshop on
                    Distributed Algorithms}",
    Place        = "Terschelling, The Netherlands",
    Series       = "Lecture Notes in Computer Science",
    Number       = "857",
    Pages        = "265-279",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@TechReport{Hoe09-Thesis,
    Author       = "Hoeschele, M.",
    Year         = "2009",
    Title        = "{Towards a Semi-Automatic Higher-Order Tableau Prover}",
    Number       = "Bachelor's Thesis",
    Institution  = "Saarland University",
    Address      = "Saarbruecken, Germany",
    Comment      = "TPTPRef"
}

@InProceedings{HC96-DISCO,
    Author       = "Homann, K. and Calmet, J.",
    Year         = "1996",
    Title        = "{Structures for Symbolic Mathematical Reasoning and
                    Computation}",
    Editor       = "Calmet, J. and Limongelli, C.",
    BookTitle    = "{Proceedings of the International Symposium on the Design
                    and Implementation of Symbolic Computation Systems}",
    Place        = "Karlsruhe, Germany",
    Series       = "Lecture Notes in Computer Science",
    Number       = "1128",
    Pages        = "216-227",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRefForResults"
}

@InProceedings{HLB05,
    Author       = "Hommersom, A. and Lucas, P. and van Bommel, P.",
    Year         = "2005",
    Title        = "{Automated Theorem Proving for Quality-checking Medical
                    Guidelines}",
    Editor       = "Sutcliffe, G. and Fischer, B. and Schulz, S.",
    BookTitle    = "{Proceedings of the Workshop on Empirically Successful
                    Classical Automated Reasoning, 20th International
                    Conference on Automated Deduction}",
    Place        = "Tallinn, Estonia",
    Comment      = "TPTPRef"
}

@Book{How72,
    Author       = "Howson, A.G.",
    Year         = "1972",
    Title        = "{A Handbook of Terms used in Algebra and Analysis}",
    Publisher    = "Cambrige University Press",
    Comment      = "TPTPRef"
}

@Article{Hua96,
    Author       = "Huang G.",
    Year         = "1996",
    Title        = "{Using OTTER and Prolog to Solve TopSpin}",
    Journal      = "AAR Newsletter",
    Volume       = "33",
    Pages        = "3-4",
    Comment      = "TPTPRef"
}

@Article{HM98,
    Author       = "Huang, G. and Myers, D.",
    Year         = "1998",
    Title        = "{Subgoal Strategies for Solving Board Puzzles}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "20",
    Number       = "3",
    Pages        = "215-253",
    Comment      = "TPTPRef"
}

@Book{HC96,
    Author       = "Hughes, G. and Cresswell, M.",
    Year         = "1996",
    Title        = "{A New Introduction to Modal Logic}",
    Publisher    = "Methuen and Co",
    Comment      = "TPTPRef"
}

@InProceedings{HS97-IJCAI,
    Author       = "Hustadt, U. and Schmidt, R.A.",
    Year         = "1997",
    Title        = "{On Evaluating Decision Procedures for Modal Logics}",
    Editor       = "Pollack M.E.",
    BookTitle    = "{Proceedings of the 15th International Joint Conference on
                    Artificial Intelligence}",
    Place        = "Nagoya, Japan",
    Pages        = "202-207",
    Publisher    = "Morgan Kaufmann",
    Comment      = "TPTPRef"
}

@TechReport{HBG94,
    Author       = "H{\"a}hnle, R. and Beckert, B. and Gerberding, S.",
    Year         = "1994",
    Title        = "{The Many-Valued Tableau-Based Theorem Prover 3TAP}",
    Number       = "TR 30/94",
    Institution  = "Fakult{\"a}t f{\"u}r Informatik, Univers{\"a}t
                    Karlsruhe",
    Address      = "Karlsruhe, Germany",
    Comment      = "TPTPRef"
}

@TechReport{HKW96,
    Author       = "H{\"a}hnle, R. and Kerber, M. and Weidenbach, C.",
    Year         = "1996",
    Title        = "{Common Syntax of the DFG-Schwerpunktprogramm Deduction}",
    Number       = "TR 10/96",
    Institution  = "Fakult{\"a}t f{\"u}r Informatik, Univers{\"a}t
                    Karlsruhe",
    Address      = "Karlsruhe, Germany",
    Comment      = "TPTPRef,TPTPCite"
}

@InProceedings{HS08,
    Author       = "H{\"o}fner, P. and Struth, G.",
    Year         = "2008",
    Title        = "{On Automating the Calculus of Relations}",
    Editor       = "Baumgartner, P. and Armando, A. and Dowek, G.",
    BookTitle    = "{Proceedings of the 4th International Joint Conference on
                    Automated Reasoning}",
    Place        = "Sydney, Australia",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "5195",
    Pages        = "50-66",
    Comment      = "TPTPRef"
}

@InProceedings{HS07,
    Author       = "H{\"o}fner, P. and Struth, G.",
    Year         = "2007",
    Title        = "{Automated Reasoning in Kleene Algebra}",
    Editor       = "Pfenning, F.",
    BookTitle    = "{Proceedings of the 21st International Conference on
                    Automated Deduction}",
    Place        = "Bremen, Germany",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "4603",
    Pages        = "279-294",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Article{HSS09,
    Author       = "H{\"o}fner, P. and Struth, G. and Sutcliffe, G.",
    Year         = "2009",
    Title        = "{Automated Verification of Refinement Laws}",
    Journal      = "Annals of Mathematics and Artificial Intelligence",
    Volume       = "55",
    Number       = "1",
    Pages        = "35-62",
    Comment      = "TPTPRef"
}

@InCollection{ICO92,
    Author       = "ICOT",
    Year         = "1992",
    Title        = "{Model Generation Theorem Prover, MGTP}",
    BookTitle    = "{FGCS'92 - International Conference on Fifth Generation
                    Computer Systems, Demonstrations}",
    Pages        = "63-74",
    Comment      = "TPTPRef"
}

@InProceedings{Iwa97,
    Author       = "Iwanuma, K.",
    Year         = "1997",
    Title        = "{Lemma Matching for a PTTP-based Top-down Theorem Prover}",
    Editor       = "McCune, W.W.",
    BookTitle    = "{Proceedings of the 14th International Conference on
                    Automated Deduction}",
    Place        = "Townsville, Australia",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "1249",
    Pages        = "146-160",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRefForResults,TPTPCite"
}

@Article{Jec95,
    Author       = "Jech, T.",
    Year         = "1995",
    Title        = "{Otter Experiments in a System of Combinatory Logic}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "14",
    Number       = "3",
    Pages        = "413-426",
    Comment      = "TPTPRef"
}

@Article{Jec93,
    Author       = "Jech, T.",
    Year         = "1993",
    Title        = "{LD-Algebras}",
    Journal      = "Association for Automated Reasoning Newsletter",
    Volume       = "22",
    Pages        = "9-12",
    Comment      = "TPTPRef"
}

@Article{JW+99,
    Author       = "Joiner, T. and Walker, R. and Rudd, M. and Jobes, D.",
    Year         = "1999",
    Title        = "{Scientizing and Routinizing the Assessment of Suicidality
                    in Outpatient Practice}",
    Journal      = "Professional Psychology: Research and Practice",
    Volume       = "30",
    Number       = "5",
    Pages        = "447-453",
    Comment      = "TPTPRef"
}

@Book{Jon04,
    Author       = "Jones, L.",
    Year         = "2004",
    Title        = "{The Encyclopedia of Religion}",
    Publisher    = "Macmillan",
    Comment      = "TPTPRef"
}

@Unpublished{Jon93-Email,
    Author       = "Jones, R.",
    Year         = "1993",
    Title        = "{Little Problem, Solved by Otter}",
    Series       = "HOL mailing list",
    Number       = "http://lal.cs.byu.edu/lal/holdoc/info-hol/15xx/1572.html",
    Comment      = "TPTPRef"
}

@Article{JT51,
    Author       = "J{\'o}nsson, B. and Tarski, A.",
    Year         = "1951",
    Title        = "{Boolean Algebras with Operators, Part I}",
    Journal      = "American Journal of Mathematics",
    Volume       = "73",
    Pages        = "891-939",
    Comment      = "TPTPRef"
}

@Book{KM64,
    Author       = "Kalish, D. and Montague, R.",
    Year         = "1964",
    Title        = "{Logic: Techniques of Formal Reasoning}",
    Publisher    = "World, Harcourt and Brace",
    Comment      = "TPTPRef"
}

@Article{Kar96-JFM,
    Author       = "Karno, Z.",
    Year         = "1996",
    Title        = "{Maximal Kolmogorov Subspaces of a Topological Space as
                    Stone Retracts of the Ambient Space}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "5",
    Number       = "1",
    Pages        = "125-130",
    Comment      = "TPTPRef"
}

@Article{Kar93,
    Author       = "Karno, Z.",
    Year         = "1993",
    Title        = "{Maximal Discrete Subspaces of Almost Discrete Topological
                    Spaces}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "4",
    Number       = "1",
    Pages        = "125-135",
    Comment      = "TPTPRef"
}

@Article{Kar92,
    Author       = "Karno, Z.",
    Year         = "1992",
    Title        = "{Continuity of Mappings over the Union of Subspaces}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "3",
    Number       = "1",
    Pages        = "1-16",
    Comment      = "TPTPRef"
}

@InProceedings{KS96,
    Author       = "Kautz, H. and Selman, B.",
    Year         = "1996",
    Title        = "{Pushing the Envelope: Planning, Propositional Logic, and
                    Stochastic Search}",
    Editor       = "Clancey, W. and Weld, D.",
    BookTitle    = "{Proceedings of the 13th National Conference on Artificial
                    Intelligence}",
    Place        = "Portland, USA",
    Pages        = "1194-1201",
    Comment      = "TPTPRef"
}

@InProceedings{KS92,
    Author       = "Kautz, H. and Selman, B.",
    Year         = "1992",
    Title        = "{Planning as Satisfiability}",
    Editor       = "Neumann, B.",
    BookTitle    = "{Proceedings of the 10th European Conference on Artificial
                    Intelligence}",
    Place        = "Vienna, Austria",
    Comment      = "TPTPRef"
}

@Book{Kel55,
    Author       = "Kelley, J.L.",
    Year         = "1955",
    Title        = "{General Topology}",
    Publisher    = "D. Van Nostrand",
    Comment      = "TPTPRef"
}

@Article{KKP07,
    Author       = "Kepka, T. and Kunen, K. and Phillips, J.D.",
    Year         = "2007",
    Title        = "{The Structure of F-Quasigroups}",
    Journal      = "Journal of Algebra",
    Volume       = "317",
    Pages        = "435-461",
    Comment      = "TPTPRef"
}

@Article{KK06,
    Author       = "Kinyon, M. and Kunen, K.",
    Year         = "2006",
    Title        = "{Power-associative, Conjugacy Closed Loops}",
    Journal      = "Journal of Algebra",
    Volume       = "304",
    Number       = "12",
    Pages        = "679-711",
    Comment      = "TPTPRef"
}

@Article{KK04,
    Author       = "Kinyon, M. and Kunen, K.",
    Year         = "2004",
    Title        = "{The Structure of Extra Loops}",
    Journal      = "Quasigroups Related Systems",
    Volume       = "12",
    Pages        = "39-60",
    Comment      = "TPTPRef"
}

@Article{KKP04,
    Author       = "Kinyon, M. and Kunen, K. and Phillips, J.D.",
    Year         = "2004",
    Title        = "{Diassociativity in Conjugacy Closed Loops}",
    Journal      = "Communications in Algebra",
    Volume       = "32",
    Pages        = "767-786",
    Comment      = "TPTPRef"
}

@Article{KKP02a,
    Author       = "Kinyon, M. and Kunen, K. and Phillips, J.D.",
    Year         = "2002",
    Title        = "{Every Diassociative A-loop is Moufang}",
    Journal      = "Proceedings of the American Mathematical Society",
    Volume       = "17",
    Number       = "130",
    Pages        = "619-624",
    Comment      = "TPTPRef"
}

@Article{KKP02b,
    Author       = "Kinyon, M. and Kunen, K. and Phillips, J.D.",
    Year         = "2002",
    Title        = "{A Generalization of Moufang and Steiner Loops}",
    Journal      = "Algebra Universalis",
    Volume       = "48",
    Pages        = "81-101",
    Comment      = "TPTPRef"
}

@Article{KP05,
    Author       = "Kinyon, M. and Phillips, J.D.",
    Year         = "2005",
    Title        = "{Rectangular Quasigroups and Rectangular Loops}",
    Journal      = "Computers and Mathematics with Applications",
    Volume       = "49",
    Number       = "11-12",
    Pages        = "1679-1685",
    Comment      = "TPTPRef"
}

@Article{KP04-a,
    Author       = "Kinyon, M. and Phillips, J.D.",
    Year         = "2004",
    Title        = "{Commutants of Bol Loops of Odd Order}",
    Journal      = "Proceedings of the American Mathematical Society",
    Volume       = "132",
    Pages        = "617-619",
    Comment      = "TPTPRef"
}

@Article{KP04-b,
    Author       = "Kinyon, M. and Phillips, J.D.",
    Year         = "2004",
    Title        = "{Axioms for Trimedial Quasigroups}",
    Journal      = "Commentationes Mathematicae Universitatis Carolinae",
    Volume       = "45",
    Pages        = "287-294",
    Comment      = "TPTPRef"
}

@Article{KP02,
    Author       = "Kinyon, M. and Phillips, J.D.",
    Year         = "2002",
    Title        = "{A Note on Trimedial Quasigroups}",
    Journal      = "Quasigroups and Related Systems",
    Volume       = "9",
    Pages        = "65-66",
    Comment      = "TPTPRef"
}

@Article{KPV08,
    Author       = "Kinyon, M. and Phillips, J.D. and Vojtechovsky, P.",
    Year         = "2008",
    Title        = "{When is the Commutant of a Bol Loop a Subloop?}",
    Journal      = "Transactions of the American Mathematical Society",
    Volume       = "360",
    Number       = "5",
    Pages        = "2393-2408",
    Comment      = "TPTPRef"
}

@Article{KPV07,
    Author       = "Kinyon, M. and Phillips, J.D. and Vojtechovsky, P.",
    Year         = "2007",
    Title        = "{C-loops: Extensions and Constructions}",
    Journal      = "Journal of Algebra and its Applications",
    Volume       = "6",
    Number       = "1",
    Pages        = "1-20",
    Comment      = "TPTPRef"
}

@Article{Kis97,
    Author       = "Kisielewicz, A.",
    Year         = "1997",
    Title        = "{Austin Identities}",
    Journal      = "Algebra Universalis",
    Volume       = "38",
    Number       = "3",
    Pages        = "324-328",
    Comment      = "TPTPRef"
}

@Unpublished{Koh-OMDOC-URL,
    Author       = "Kohlhase, M.",
    Year         = "",
    Title        = "{OMDoc: A Standard for Open Mathematical Documents}",
    Note         = "https://trac.omdoc.org/OMDoc",
    Comment      = "TPTPRef"
}

@Article{Kol67,
    Author       = "Kolodner, I.",
    Year         = "1967",
    Title        = "{A Simple Proof of the Schroder-Bernstein Theorem}",
    Journal      = "The American Mathematical Monthly",
    Volume       = "74",
    Number       = "8",
    Pages        = "995-996",
    Comment      = "TPTPRef"
}

@Article{Kor96-JFM,
    Author       = "Kornilowicz, A.",
    Year         = "1996",
    Title        = "{On the Group of Inner Automorphisms}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "5",
    Number       = "1",
    Pages        = "43-45",
    Comment      = "TPTPRef,AUTGROUP"
}

@Article{Kor97,
    Author       = "Korni{\l}owicz, A.",
    Year         = "1997",
    Title        = "{On the Topological Properties of Meet-Continuous
                    Lattices}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "6",
    Number       = "2",
    Pages        = "269-277",
    Comment      = "TPTPRef"
}

@InProceedings{KUH05,
    Author       = "Koshimura, M. and Umeda, M. and Hasegawa, R.",
    Year         = "2005",
    Title        = "{Abstract Model Generation of Preprocessing Clause Sets}",
    Editor       = "Baader, F. and Voronkov, A.",
    BookTitle    = "{Proceedings of the 11th International Conference on Logic
                    for Programming, Artificial Intelligence, and Reasoning}",
    Place        = "Montevideo, Uruguay",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "3452",
    Pages        = "67-78",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef,TPTPData"
}

@Article{Kos97,
    Author       = "Kossey, I.",
    Year         = "1997",
    Title        = "{A Note on the Completeness of Higher Order Resolution}",
    Journal      = "Publicationes Mathematicae Debrecen",
    Volume       = "51",
    Number       = "1-2",
    Comment      = "TPTPRef"
}

@InProceedings{KK+16,
    Author       = "Kotelnikov, E. and Kovacs, L. and Reger, G. and Voronkov,
                    A.",
    Year         = "2016",
    Title        = "{The Vampire and the FOOL}",
    Editor       = "Avigad, J. and Chlipala, A.",
    BookTitle    = "{Proceedings of the 5th ACM SIGPLAN Conference on Certified
                    Programs and Proofs}",
    Place        = "St Petersburg, USA",
    Pages        = "37-48",
    Publisher    = "ACM",
    Comment      = "TPTPRef"
}

@Book{KA+06,
    Author       = "Kotler, P. and Armstrong, G. and Brown, L. and Adam, S.",
    Year         = "2006",
    Title        = "{Marketing}",
    Publisher    = "Pearson Education",
    Comment      = "TPTPRef"
}

@InProceedings{KV09,
    Author       = "Kovacs, L. and Voronkov, A.",
    Year         = "2009",
    Title        = "{Interpolation and Symbol Elimination}",
    Editor       = "Schmidt, R.",
    BookTitle    = "{Proceedings of the 22nd International Conference on
                    Automated Deduction}",
    Place        = "Montreal Canada",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "5663",
    Pages        = "199-213",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Article{Koz00,
    Author       = "Kozen, D.",
    Year         = "2000",
    Title        = "{On Hoare Logic and Kleene Algebra with Tests}",
    Journal      = "ACM Transactions on Computational Logic",
    Volume       = "1",
    Number       = "1",
    Pages        = "60-76",
    Comment      = "TPTPRef"
}

@Article{Koz97,
    Author       = "Kozen, D.",
    Year         = "1997",
    Title        = "{Kleene Algebra with Tests}",
    Journal      = "ACM Transactions on Programming Language Systems",
    Volume       = "19",
    Number       = "3",
    Pages        = "427-443",
    Comment      = "TPTPRef"
}

@Article{Koz94,
    Author       = "Kozen, D.",
    Year         = "1994",
    Title        = "{A Completeness Theorem for Kleene Algebras and the Algebra
                    of Regular Events}",
    Journal      = "Information and Computation",
    Volume       = "110",
    Number       = "2",
    Pages        = "366-390",
    Comment      = "TPTPRef"
}

@InProceedings{Kuh08,
    Author       = "Kuhn, T.",
    Year         = "2008",
    Title        = "{AceWiki: Collaborative Ontology Management in Controlled
                    Natural Language}",
    Editor       = "Lange, C. and Schaffert, S. and Skaf-Molli, H. and
                    V{\"o}lkel, M.",
    BookTitle    = "{Proceedings of the 3rd Semangtic Wiki Workshop}",
    Place        = "Tenerife, Spain",
    Series       = "CEUR Workshop Proceedings",
    Number       = "360",
    Pages        = "94-99",
    Comment      = "TPTPRef"
}

@TechReport{KE99,
    Author       = "Kulik, L. and Eschenbach, C.",
    Year         = "1999",
    Title        = "{A Geometry of Oriented Curves}",
    Number       = "Report from the project: Axiomatics of Spatial Concepts",
    Institution  = "Department for Informatics, University of Hamburg",
    Address      = "Hamburg, USA",
    Comment      = "TPTPRef"
}

@Article{KNR07,
    Author       = "Kuncak, V. and Hguyen, H. and Rinard, M.",
    Year         = "2007",
    Title        = "{Deciding Boolean Algebra with Presburger Arithmetic}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "36",
    Number       = "3",
    Pages        = "213-239",
    Comment      = "TPTPCite,TPTPRef"
}

@InProceedings{KR07,
    Author       = "Kuncak, V. and Rinard, M.",
    Year         = "2007",
    Title        = "{Towards Efficient Satisfiability Checking for Boolean
                    Algebra with Presburger Arithmetic}",
    Editor       = "Pfenning, F.",
    BookTitle    = "{Proceedings of the 21st International Conference on
                    Automated Deduction}",
    Place        = "Bremen, Germany",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "4603",
    Pages        = "215-230",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef,TPTPData"
}

@Article{Kun00,
    Author       = "Kunen, K.",
    Year         = "2000",
    Title        = "{The Structure of Conjugacy Closed Loops}",
    Journal      = "Transactions of the American Mathematical Society",
    Volume       = "352",
    Number       = "6",
    Pages        = "2889-2911",
    Comment      = "TPTPRef"
}

@Article{Kun98,
    Author       = "Kunen, K.",
    Year         = "1998",
    Title        = "{Alternative Loop Rings}",
    Journal      = "Communications of Algebra",
    Volume       = "26",
    Number       = "2",
    Pages        = "557-564",
    Comment      = "TPTPRef"
}

@Article{Kun96a,
    Author       = "Kunen, K.",
    Year         = "1996",
    Title        = "{Moufang Quasigroups}",
    Journal      = "Journal of Algebra",
    Volume       = "183",
    Number       = "1",
    Pages        = "231-234",
    Comment      = "TPTPRef"
}

@Article{Kun96b,
    Author       = "Kunen, K.",
    Year         = "1996",
    Title        = "{Quasigroups, Loops, and Associative Laws}",
    Journal      = "Journal of Algebra",
    Volume       = "185",
    Number       = "1",
    Pages        = "194-204",
    Comment      = "TPTPRef"
}

@Article{Kun92,
    Author       = "Kunen, K.",
    Year         = "1992",
    Title        = "{Single Axioms for Groups}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "9",
    Number       = "3",
    Pages        = "291-308",
    Comment      = "TPTPRef"
}

@Book{Kur56,
    Author       = "Kurosh, A.G.",
    Year         = "1956",
    Title        = "{The Theory of Groups}",
    Volume       = "1",
    Pages        = "99-100",
    Publisher    = "Chelsea",
    Comment      = "TPTPRef"
}

@InProceedings{KC+10,
    Author       = "K{\"u}lwein, D. and Cramer, M. and Koepke, P. and
                    Schr{\"o}der, B.",
    Year         = "2010",
    Title        = "{Premise Selection in the Naproche System}",
    Editor       = "Giesl, J. and Haehnle, R.",
    BookTitle    = "{Proceedings of the 5th International Joint Conference on
                    Automated Reasoning}",
    Place        = "Edinburgh, United Kingdom",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "6173",
    Pages        = "434-440",
    Comment      = "TPTPRef"
}

@Article{Lam09,
    Author       = "Lammich, P.",
    Year         = "2009",
    Title        = "{Collections Framework}",
    Journal      = "Archive of Formal Proofs",
    Note         = "http://isa-afp.org/entries/Collections.shtml",
    Comment      = "TPTPRef"
}

@Book{Lan30,
    Author       = "Landau, E.",
    Year         = "1930",
    Title        = "{Grundlagen der Analysis}",
    Publisher    = "Akademische Verlagsgesellschaft M.B.H",
    Comment      = "TPTPRef"
}

@TechReport{LS74,
    Author       = "Lawrence, J.D. and Starkey, J.D.",
    Year         = "1974",
    Title        = "{Experimental Tests of Resolution Based Theorem-proving
                    Strategies.}",
    Institution  = "Computer Science Department, Washington State
                    University",
    Address      = "Pullman, USA",
    Comment      = "TPTPRef"
}

@InCollection{Leb83,
    Author       = "Leblanc, H.",
    Year         = "1983",
    Title        = "{Alternatives to Standard First-Order Semantics}",
    Editor       = "Gabbay, D. and Guenther, F.",
    BookTitle    = "{Handbook of Philosophical Logic}",
    Chapter      = "I.3",
    Volume       = "I",
    Pages        = "189-274",
    Publisher    = "D. Reidel",
    Comment      = "TPTPRef"
}

@PhDThesis{Lee90,
    Author       = "Lee, S-J.",
    Year         = "1990",
    Title        = "{CLIN: An Automated Reasoning System Using Clause
                    Linking}",
    School       = "University of North-Carolina at Chapel Hill",
    Address      = "Chapel Hill, USA",
    Comment      = "TPTPRefForResults"
}

@Article{LP92,
    Author       = "Lee, S-J. and Plaisted, D.A.",
    Year         = "1992",
    Title        = "{Eliminating Duplication with the Hyper-Linking Strategy}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "9",
    Number       = "1",
    Pages        = "25-42",
    Comment      = "TPTPRefForResults,TPTPRef"
}

@Article{Lei06,
    Author       = "Leiss, H.",
    Year         = "2006",
    Title        = "{Kleene Modules and Linear Languages}",
    Journal      = "Journal of Logic and Algebraic Programming",
    Volume       = "66",
    Number       = "2",
    Pages        = "185-194",
    Comment      = "TPTPRef"
}

@Article{Let97,
    Author       = "Letz, R.",
    Year         = "1997",
    Title        = "{LINUS: A Link Instantiation Prover with Unit Support}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "18",
    Number       = "2",
    Pages        = "205-210",
    Comment      = "TPTPRefForResults,TPTPCite"
}

@Article{LMG94,
    Author       = "Letz, R. and Mayr, K. and Goller, C.",
    Year         = "1994",
    Title        = "{Controlled Integration of the Cut Rule into Connection
                    Tableau Calculi}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "13",
    Number       = "3",
    Pages        = "297-337",
    Comment      = "TPTPCite,TPTPRef,TPTPData"
}

@Article{LS+92,
    Author       = "Letz, R. and Schumann, J. and Bayerl, S. and Bibel, W.",
    Year         = "1992",
    Title        = "{SETHEO: A High-Performance Theorem Prover}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "8",
    Number       = "2",
    Pages        = "183-212",
    Comment      = "TPTPRefForResults,TPTPRef, linear systems"
}

@Article{Li98,
    Author       = "Li, D.",
    Year         = "1998",
    Title        = "{A Shorter and Intuitive Axiom to Replace the Third Axiom
                    of Compatibility of Equality with Apartness and
                    Convergence}",
    Journal      = "AAR Newsletter",
    Volume       = "39",
    Comment      = "TPTPRef"
}

@Article{Li97,
    Author       = "Li, D.",
    Year         = "1997",
    Title        = "{Replacing the Axioms for Connecting Lines and Intersection
                    Points by Two Single Axioms}",
    Journal      = "AAR Newsletter",
    Volume       = "37",
    Comment      = "TPTPRef"
}

@Article{Li94,
    Author       = "Li, D.",
    Year         = "1994",
    Title        = "{The Formulation of the Halting Problem Is Not Suitable for
                    Describing the Halting Problem}",
    Journal      = "AAR Newsletter",
    Volume       = "27",
    Pages        = "1-7",
    Comment      = "TPTPRef"
}

@Article{Lif89,
    Author       = "Lifschitz, V.",
    Year         = "1989",
    Title        = "{What is the Inverse Method?}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "5",
    Number       = "1",
    Pages        = "1-24",
    Comment      = "TPTPRef, general reasoning"
}

@Book{Liu85,
    Author       = "Liu, C.L.",
    Year         = "1985",
    Title        = "{Elements of Discrete Mathematics}",
    Publisher    = "McGraw-Hill",
    Comment      = "TPTPRef"
}

@Article{Loc10,
    Author       = "Lochbihler, A.",
    Year         = "2010",
    Title        = "{Coinductive}",
    Journal      = "Archive of Formal Proofs",
    Note         = "http://isa-afp.org/entries/Coinductive.shtml",
    Comment      = "TPTPRef"
}

@Book{LH+01,
    Author       = "Longmore, J.M. and Hope, R.A. and Longmore, M. and
                    Wilkinson, I. and Torok, E.",
    Year         = "2001",
    Title        = "{Oxford Handbook of Clinical Medicine}",
    Publisher    = "Oxford University Press",
    Comment      = "TPTPRef"
}

@Book{Lou06,
    Author       = "Loux, M.",
    Year         = "2006",
    Title        = "{Metaphysics: A Contemporary Introduction}",
    Publisher    = "Routledge",
    Comment      = "TPTPRef"
}

@Article{Lov69-MI,
    Author       = "Loveland, D.W.",
    Year         = "1969",
    Title        = "{Theorem-provers Combining Model Elimination and
                    Resolution}",
    Journal      = "Machine Intelligence",
    Volume       = "4",
    Pages        = "73-86",
    Comment      = "TPTPRef, linear systems"
}

@Article{Lov68,
    Author       = "Loveland, D.W.",
    Year         = "1968",
    Title        = "{Mechanical Theorem Proving by Model Elimination}",
    Journal      = "Journal of the ACM",
    Volume       = "15",
    Number       = "2",
    Pages        = "236-251",
    Comment      = "TPTPRef, linear systems"
}

@Article{Luc68,
    Author       = "Luckham, D.",
    Year         = "1968",
    Title        = "{Some Tree-paring Strategies for Theorem Proving}",
    Journal      = "Machine Intelligence",
    Volume       = "3",
    Pages        = "95-112",
    Comment      = "TPTPRef, general reasoning/resolution/semantics"
}

@Article{LM93,
    Author       = "Lusk, E.L. and McCune, W.W.",
    Year         = "1993",
    Title        = "{Uniform Strategies: The CADE-11 Theorem Proving Contest}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "11",
    Number       = "3",
    Pages        = "317-331",
    Comment      = "TPTPRef"
}

@InProceedings{LM92,
    Author       = "Lusk, E.L. and McCune, W.W.",
    Year         = "1992",
    Title        = "{Experiments with ROO, a Parallel Automated Deduction
                    System}",
    Editor       = "Fronhofer, B. and Wrightson, G.",
    BookTitle    = "{Parallelization in Inference Systems}",
    Volume       = "590",
    Pages        = "139-162",
    Comment      = "TPTPRef, parallel deduction"
}

@Article{LO85-JAR-1-103,
    Author       = "Lusk, E.L. and Overbeek, R.",
    Year         = "1985",
    Title        = "{Non-Horn Problems}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "1",
    Number       = "1",
    Pages        = "103-114",
    Comment      = "TPTPRef"
}

@Article{LO85-JAR-1-209,
    Author       = "Lusk, E.L. and Overbeek, R.",
    Year         = "1985",
    Title        = "{Reasoning about Equality}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "1",
    Number       = "2",
    Pages        = "209-228",
    Comment      = "TPTPRef"
}

@InProceedings{LW92,
    Author       = "Lusk, E.L. and Wos, L.",
    Year         = "1992",
    Title        = "{Benchmark Problems in Which Equality Plays the Major
                    Role}",
    Editor       = "Kapur D.",
    BookTitle    = "{Proceedings of the 11th International Conference on
                    Automated Deduction}",
    Place        = "Saratoga Springs, USA",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "607",
    Pages        = "781-785",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@TechReport{LW91,
    Author       = "Lusk, E.L. and Wos, L.",
    Year         = "1991",
    Title        = "{Benchmark Problems in Which Equality Plays the Major
                    Role}",
    Number       = "MCS-P275-1191",
    Institution  = "Mathematics and Computer Science Division, Argonne
                    National Laboratory",
    Address      = "Argonne, USA",
    Comment      = "TPTPRef"
}

@Article{LPV06,
    Author       = "Lyaletski, A. and Paskevich, A. and Verchinine, K.",
    Year         = "2006",
    Title        = "{SAD as a Mathematical Assistant - How should we go from
                    Here to There?}",
    Editor       = "Benzm{\"u}ller, C.",
    BookTitle    = "{Towards Computer Aided Mathematics}",
    Journal      = "Journal of Applied Logic",
    Volume       = "4",
    Number       = "4",
    Pages        = "560-591",
    Comment      = "TPTPRef"
}

@Book{Mac71,
    Author       = "MacLane, S.",
    Year         = "1971",
    Title        = "{Categories for the Working Mathematician}",
    Publisher    = "Springer Verlag",
    Comment      = "TPTPRef"
}

@Book{Mad06,
    Author       = "Maddux, R.",
    Year         = "2006",
    Title        = "{Relation Algebras}",
    Series       = "Studies in Logic and the Foundations of Mathematics",
    Number       = "150",
    Publisher    = "Elsevier",
    Comment      = "TPTPRef"
}

@Article{Mad95,
    Author       = "Maddux, R.",
    Year         = "1995",
    Title        = "{Relation-Algebraic Semantics}",
    Journal      = "Theoretical Computer Science",
    Volume       = "160",
    Number       = "1-2",
    Pages        = "1-85",
    Comment      = "TPTPRef"
}

@Article{MB85,
    Author       = "Manes, E. and Benson, D.",
    Year         = "1985",
    Title        = "{The Inverse Semigroup of a Sum-ordered Semiring}",
    Journal      = "Semigroup Forum",
    Volume       = "31",
    Pages        = "129-152",
    Comment      = "TPTPRef"
}

@TechReport{MP90,
    Author       = "Manna, Z. and Pnueli, A.",
    Year         = "1990",
    Title        = "{Tools and Rules for the Practicing Verifier}",
    Number       = "CS-TR-90-1321",
    Institution  = "Department of Computer Science, Stanford University",
    Address      = "Stanford, USA",
    Comment      = "TPTPRef"
}

@InProceedings{MB88,
    Author       = "Manthey, R. and Bry, F.",
    Year         = "1988",
    Title        = "{SATCHMO: A Theorem Prover Implemented in Prolog}",
    Editor       = "Lusk, E. and Overbeek, R.",
    BookTitle    = "{Proceedings of the 9th International Conference on
                    Automated Deduction}",
    Place        = "Argonne, USA",
    Series       = "Lecture Notes in Computer Science",
    Number       = "310",
    Pages        = "415-434",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Article{Mar97-JFM,
    Author       = "Marasik, A.",
    Year         = "1997",
    Title        = "{Algebraic Operation on Subsets of Many Sorted Sets}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "6",
    Number       = "3",
    Pages        = "397-401",
    Comment      = "TPTPRef,CLOSURE3"
}

@InProceedings{MOS05,
    Author       = "Marcinkowski, J. and Otop, J. and Stelmaszek, G.",
    Year         = "2005",
    Title        = "{On a Semantic Subsumption Test}",
    Editor       = "Baader, F. and Voronkov, A.",
    BookTitle    = "{Proceedings of the 11th International Conference on Logic
                    for Programming, Artificial Intelligence, and Reasoning}",
    Place        = "Montevideo, Uruguay",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "3452",
    Pages        = "142-153",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef,TPTPData"
}

@InProceedings{MI+16,
    Author       = "Matsuzaki, T. and Iwane, H. and Kobayashi, M. and Zhan, Y.
                    and Fukasaku, R. and Kudo, J. and Anai, H. and Arai, N.",
    Year         = "2016",
    Title        = "{Race against the Teens - Benchmarking Mechanized Math on
                    Pre-university Problems}",
    Editor       = "Olivetti, N. and Tiwari, A.",
    BookTitle    = "{Proceedings of the 8th International Joint Conference on
                    Automated Reasoning}",
    Place        = "Coimbra, Portugal",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "9706",
    Pages        = "213-227",
    Comment      = "TPTPRef,TPTPCite"
}

@Misc{Mat90,
    Author       = "Matuszewski, R.",
    Year         = "1990",
    Title        = "{Formalized Mathematics}",
    Note         = "http://www.mizar.org/fm/",
    Comment      = "TPTPRef"
}

@InProceedings{McC59,
    Author       = "McCarthy, J.",
    Year         = "1959",
    Title        = "{Programs with Common Sense}",
    BookTitle    = "{Proceedings of the Teddington Conference on the
                    Mechanization of Thought}",
    Place        = "Teddington, United Kingdom",
    Pages        = "75-91",
    Publisher    = "Her Majesty's Stationery Office",
    Comment      = "TPTPRef"
}

@Article{McC05-AAR,
    Author       = "McCune, W.",
    Year         = "2005",
    Title        = "{Fascinating XCB Inference}",
    Journal      = "Association for Automated Reasoning Newsletter",
    Number       = "66",
    Comment      = "TPTPRef"
}

@Unpublished{McC-EQP-URL,
    Author       = "McCune, W.W.",
    Year         = "",
    Title        = "{EQP: Equational Prover}",
    Note         = "http://www.cs.unm.edu/~mccune/eqp/",
    Comment      = "TPTPRef"
}

@Unpublished{McC-Otter-URL,
    Author       = "McCune, W.W.",
    Year         = "",
    Title        = "{Otter: An Automated Deduction System}",
    Note         = "http://www.cs.unm.edu/~mccune/otter/",
    Comment      = "TPTPRef,TPTPCite"
}

@TechReport{McC03-MACE4-TR,
    Author       = "McCune, W.W.",
    Year         = "2003",
    Title        = "{Mace4 Reference Manual and Guide}",
    Number       = "ANL/MCS-TM-264",
    Institution  = "Argonne National Laboratory",
    Address      = "Argonne, USA",
    Comment      = "TPTPRef,"
}

@Article{McC98,
    Author       = "McCune, W.W.",
    Year         = "1998",
    Title        = "{Automatic Proofs and Counterexamples for some Ortholattice
                    Identities}",
    Journal      = "Information Processing Letters",
    Volume       = "65",
    Comment      = "TPTPRef"
}

@Article{McC95,
    Author       = "McCune, W.W.",
    Year         = "1995",
    Title        = "{Four Challenge Problems in Equational Logic}",
    Journal      = "AAR Newsletter",
    Volume       = "28",
    Pages        = "9-10",
    Comment      = "TPTPRef"
}

@TechReport{McC94-TR-ANL-94-6,
    Author       = "McCune, W.W.",
    Year         = "1994",
    Title        = "{Otter 3.0 Reference Manual and Guide}",
    Number       = "ANL-94/6",
    Institution  = "Argonne National Laboratory",
    Address      = "Argonne, USA",
    Comment      = "TPTPRefForResults,TPTPRef"
}

@Article{McC93,
    Author       = "McCune, W.W.",
    Year         = "1993",
    Title        = "{Single Axioms for Groups and Abelian Groups with Various
                    Operations}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "10",
    Number       = "1",
    Pages        = "1-13",
    Comment      = "TPTPRef"
}

@Article{McC92,
    Author       = "McCune, W.W.",
    Year         = "1992",
    Title        = "{Automated Discovery of New Axiomatisations of the Left
                    Group and Right Group Calculi}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "9",
    Number       = "1",
    Pages        = "1-24",
    Comment      = "TPTPRef"
}

@InProceedings{McC88,
    Author       = "McCune, W.W.",
    Year         = "1988",
    Title        = "{Challenge Equality Problems in Lattice Theory}",
    BookTitle    = "{Proceedings of the 9th International Conference on
                    Automated Deduction}",
    Place        = "Argonne, USA",
    Pages        = "704-709",
    Publisher    = "Springer",
    Comment      = "TPTPRef"
}

@Article{ML92,
    Author       = "McCune, W.W. and Lusk, E.",
    Year         = "1992",
    Title        = "{A Challenging Theorem of Levi}",
    Journal      = "AAR Newsletter",
    Volume       = "21",
    Pages        = "8",
    Comment      = "TPTPRef"
}

@Book{MP96,
    Author       = "McCune, W.W. and Padmanabhan, R.",
    Year         = "1996",
    Title        = "{Automated Deduction in Equational Logic and Cubic
                    Curves}",
    Series       = "Lecture Notes in Artificial Intelligence",
    Volume       = "1095",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Unpublished{MRV-URL,
    Author       = "McCune, W.W. and Rose, M. and Veroff, R.",
    Year         = "",
    Title        = "{Sheffer Stroke Bases for Ortholattices}",
    Note         = "http://www.cs.unm.edu/~mccune/papers/olsax/",
    Comment      = "TPTPRef"
}

@Article{MV+02,
    Author       = "McCune, W.W. and Veroff, R. and Fitelson, B. and Harris,
                    K. and Feist, A. and Wos, L.",
    Year         = "2002",
    Title        = "{Short Single Axioms for Boolean Algebra}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "29",
    Number       = "1",
    Pages        = "1-16",
    Comment      = "TPTPRef"
}

@InProceedings{MW92-CADE-11,
    Author       = "McCune, W.W. and Wos, L.",
    Year         = "1992",
    Title        = "{Experiments in Automated Deduction with Condensed
                    Detachment}",
    Editor       = "Kapur D.",
    BookTitle    = "{Proceedings of the 11th International Conference on
                    Automated Deduction}",
    Place        = "Saratoga Springs, USA",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "607",
    Pages        = "209-223",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Article{MW88,
    Author       = "McCune, W.W. and Wos, L.",
    Year         = "1988",
    Title        = "{Some Fixed Point Problems in Combinatory Logic}",
    Journal      = "AAR Newsletter",
    Volume       = "10",
    Pages        = "7-8",
    Comment      = "TPTPRef"
}

@Article{MW87,
    Author       = "McCune, W.W. and Wos, L.",
    Year         = "1987",
    Title        = "{A Case Study in Automated Theorem Proving: Finding Sages
                    in Combinatory Logic}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "3",
    Number       = "1",
    Pages        = "91-107",
    Comment      = "TPTPRef"
}

@Article{MT48,
    Author       = "McKinsey, J. and Tarski, A.",
    Year         = "1948",
    Title        = "{Some Theorems about the Sentential Calculi of Lewis and
                    Heyting}",
    Journal      = "Journal of Symbolic Logic",
    Volume       = "13",
    Number       = "1",
    Pages        = "1-15",
    Comment      = "TPTPRef"
}

@Article{Meg00,
    Author       = "Megill, N. and Pavicic, M.",
    Year         = "2000",
    Title        = "{Equations and State and Lattice Properties that hold in
                    Infinite Dimensional Hilber Space}",
    Journal      = "International Journal of Theoretical Physics",
    Volume       = "39",
    Pages        = "2337-2379",
    Comment      = "TPTPRef"
}

@Article{Mer53,
    Author       = "Meredith, C.A.",
    Year         = "1953",
    Title        = "{Single Axioms for the Systems (C,N), (C,0), and (A,N) of
                    the Two-valued Propositional Calculus}",
    Journal      = "Journal of Computing Systems",
    Volume       = "1",
    Pages        = "155-164",
    Comment      = "TPTPRef"
}

@Article{MP68,
    Author       = "Meredith, C.A. and Prior, A.N.",
    Year         = "1968",
    Title        = "{Equational Logic}",
    Journal      = "Notre Dame Journal of Formal Logic",
    Volume       = "9",
    Pages        = "212-226",
    Comment      = "TPTPRef"
}

@Article{MRS72,
    Author       = "Michie, D. and Ross, R. and Shannan, G.J.",
    Year         = "1972",
    Title        = "{G-deduction}",
    Journal      = "Machine Intelligence",
    Volume       = "7",
    Pages        = "141-165",
    Comment      = "TPTPRef, resolution/sample problems"
}

@InCollection{MS02,
    Author       = "Miller, R. and Shanahan, M.",
    Year         = "2002",
    Title        = "{Some Alternative Formulations of the Event Calculus}",
    Editor       = "Kakas, A.C. and Sadri, F.",
    BookTitle    = "{Computational Logic: Logic Programming and Beyond}",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "2407",
    Pages        = "452-490",
    Publisher    = "McGraw-Hill",
    Comment      = "TPTPRef"
}

@Book{Mit67,
    Author       = "Mitchell, B.",
    Year         = "1967",
    Title        = "{Theory of Categories}",
    Series       = "Pure and Applied Mathematics",
    Volume       = "17",
    Publisher    = "Academic Press",
    Comment      = "TPTPRef"
}

@Article{Mon55,
    Author       = "Montague, R.",
    Year         = "1955",
    Title        = "{On the Paradox of Grounded Classes}",
    Journal      = "Journal of Symbolic Logic",
    Volume       = "20",
    Pages        = "140",
    Comment      = "TPTPRef"
}

@Article{Mor84,
    Author       = "Morgan, C.",
    Year         = "1984",
    Title        = "{Logic Problems}",
    Journal      = "AAR Newsletter",
    Volume       = "3",
    Pages        = "5-5",
    Comment      = "TPTPRef"
}

@InProceedings{Mue04,
    Author       = "Mueller, E.",
    Year         = "2004",
    Title        = "{A Tool for Satisfiability-based Commonsense Reasoning in
                    the Event Calculus}",
    Editor       = "Barr, V. and Markov, Z.",
    BookTitle    = "{Proceedings of the 17th International FLAIRS Conference}",
    Place        = "Miami, USA",
    Pages        = "147-152",
    Publisher    = "AAAI Press",
    Comment      = "TPTPRef"
}

@InProceedings{MS05,
    Author       = "Mueller, E. and Sutcliffe, G.",
    Year         = "2005",
    Title        = "{Reasoning in the Event Calculus using First-Order
                    Automated Theorem Proving}",
    Editor       = "Russell, I. and Markov, Z.",
    BookTitle    = "{Proceedings of the 18th International FLAIRS Conference}",
    Place        = "Clearwater Beach, USA",
    Pages        = "840-841",
    Publisher    = "AAAI Press",
    Comment      = "TPTPRef"
}

@InProceedings{MS05-IWIL,
    Author       = "Mueller, E. and Sutcliffe, G.",
    Year         = "2005",
    Title        = "{Discrete Event Calculus Deduction using First-Order
                    Automated Theorem Proving}",
    Editor       = "Konev, B. and Schulz, S.",
    BookTitle    = "{Proceedings of the 5th International Workshop on the
                    Implementation of Logics}",
    Place        = "Montevideo, Uruguay",
    Pages        = "43-56",
    Comment      = "TPTPRef"
}

@Book{Mun75,
    Author       = "Munkres, J.R.",
    Year         = "1975",
    Title        = "{Topology: A First Course}",
    Publisher    = "Prentice-Hall",
    Comment      = "TPTPRef"
}

@InProceedings{Mol04,
    Author       = "M{\"o}ller, B.",
    Year         = "2004",
    Title        = "{Lazy Kleene Algebra}",
    Editor       = "Kozen, D.",
    BookTitle    = "{Proceedings of the 7th International Conference on the
                    Mathematics of Program Construction}",
    Place        = "Stirling, United Kindom",
    Series       = "Lecture Notes in Computer Science",
    Number       = "3125",
    Pages        = "252-273",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Article{MS06,
    Author       = "M{\"o}ller, B. and Struth, G.",
    Year         = "2006",
    Title        = "{Algebras of Modal Operators and Partial Correctness}",
    Journal      = "Theoretical Computer Science",
    Volume       = "351",
    Number       = "2",
    Pages        = "221-239",
    Comment      = "TPTPRef"
}

@Book{NGS99,
    Author       = "National Geographic Society",
    Year         = "1999",
    Title        = "{National Geographic Desk Reference}",
    Publisher    = "National Geographic Society",
    Comment      = "TPTPRef"
}

@InProceedings{Nel08,
    Author       = "Nelson, S.",
    Year         = "2008",
    Title        = "{MeSH 2008-2009, Development and Future Plans}",
    BookTitle    = "{Presentation at the Web Conference of the National Network
                    of Libraries of Medicine, Southeastern Atlantic Region}",
    Place        = "Bethesda, USA",
    Comment      = "TPTPRef"
}

@Manual{Neu94,
    Author       = "Neugebauer, G.",
    Year         = "1994",
    Title        = "{XTPTP-An X Window Interface for the TPTP Library}",
    Edition      = "1.0",
    Organization = "IMN, HTWK Leipzig",
    Address      = "Leipzig, Germany",
    Comment      = "TPTPRef"
}

@Article{Neu86,
    Author       = "Neumann, B.H.",
    Year         = "1986",
    Title        = "{Yet Another Single Law for Groups}",
    Journal      = "Illinois Journal of Mathematics",
    Volume       = "30",
    Number       = "2",
    Pages        = "295-300",
    Comment      = "TPTPRef"
}

@Article{Neu81,
    Author       = "Neumann, B.H.",
    Year         = "1981",
    Title        = "{Another Single Law for Groups}",
    Journal      = "Bulletin of the Australian Maths Society",
    Volume       = "23",
    Pages        = "81-102",
    Comment      = "TPTPRef"
}

@Article{Neu25,
    Author       = "Neumann, J. von",
    Year         = "1925",
    Title        = "{Eine Axiomatisierung der Mengenlehre}",
    Journal      = "Journal f{\"u}r die reine und angewandte Mathematik",
    Volume       = "154",
    Pages        = "219-240",
    Comment      = "TPTPRef"
}

@InCollection{NSS63,
    Author       = "Newell, A. and Shaw, J.C. and Simon, H.A.",
    Year         = "1963",
    Title        = "{Empirical Explorations with the Logic Theory Machine: A
                    Case Study in Heuristics}",
    Editor       = "Feigenbaum, E.A. and Feldman, J.",
    BookTitle    = "{Computers and Thought}",
    Pages        = "109-133",
    Publisher    = "McGraw-Hill",
    Comment      = "TPTPRef, general AI/sample problems"
}

@Book{NS72,
    Author       = "Newell, A. and Simon, H.",
    Year         = "1972",
    Title        = "{Human Problem Solving}",
    Publisher    = "Prentice-Hall",
    Comment      = "TPTPRef"
}

@InProceedings{NRV97,
    Author       = "Nieuwenhuis, R. and Rivero, J.M. and Vallejo, M.A.",
    Year         = "1997",
    Title        = "{Dedam: A Kernel of Data Structures and Algorithms for
                    Automated Deduction with Equality Clauses}",
    Editor       = "McCune, W.W.",
    BookTitle    = "{Proceedings of the 14th International Conference on
                    Automated Deduction}",
    Place        = "Townsville, Australia",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "1249",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@InProceedings{NP01,
    Author       = "Niles, I. and Pease, A.",
    Year         = "2001",
    Title        = "{Towards A Standard Upper Ontology}",
    Editor       = "Welty, C. and Smith, B.",
    BookTitle    = "{Proceedings of the 2nd International Conference on Formal
                    Ontology in Information Systems}",
    Place        = "Ogunquit, USA",
    Pages        = "2-9",
    Comment      = "TPTPRef"
}

@Article{Nip14,
    Author       = "Nipkow, T.",
    Year         = "2014",
    Title        = "{Amortized Complexity Verified}",
    Journal      = "Archive of Formal Proofs",
    Note         = "http://isa-afp.org/entries/Amortized_Complexity.shtml",
    Comment      = "TPTPRef"
}

@Article{Nip09,
    Author       = "Nipkow, T.",
    Year         = "2009",
    Title        = "{Social Choice Theory in HOL: Arrow and
                    Gibbard-Satterthwaite}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "43",
    Number       = "3",
    Pages        = "289-304",
    Comment      = "TPTPRef"
}

@InProceedings{Nip08,
    Author       = "Nipkow, T.",
    Year         = "2008",
    Title        = "{Linear Quantifier Elimination}",
    Editor       = "Baumgartner, P. and Armando, A. and Dowek, G.",
    BookTitle    = "{Proceedings of the 4th International Joint Conference on
                    Automated Reasoning}",
    Place        = "Sydney, Australia",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "5195",
    Pages        = "18-33",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@InProceedings{NRW98,
    Author       = "Nonnengart, A. and Rock, G. and Weidenbach, C.",
    Year         = "1998",
    Title        = "{On Generating Small Clause Normal Forms}",
    Editor       = "Kirchner, C. and Kirchner, H.",
    BookTitle    = "{Proceedings of the 15th International Conference on
                    Automated Deduction}",
    Place        = "Lindau, Germany",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "1421",
    Pages        = "397-411",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRefForResults,TPTPCite"
}

@Article{ORo89,
    Author       = "O'Rourke, P.",
    Year         = "1989",
    Title        = "{LT Revisited: Explanation-Based Learning and the Logic of
                    Principia Mathematica}",
    Journal      = "Machine Learning",
    Volume       = "4",
    Pages        = "117-159",
    Comment      = "TPTPRef, general reasoning"
}

@Article{Ohl85,
    Author       = "Ohlbach, H.J.",
    Year         = "1985",
    Title        = "{Predicate Logic Hacker Tricks}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "1",
    Number       = "4",
    Pages        = "435-440",
    Comment      = "TPTPRef"
}

@TechReport{OS95,
    Author       = "Ohlbach, H.J. and Schmidt, R.A.",
    Year         = "1995",
    Title        = "{Functional Translation and Second-Order Frame Properties
                    of Modal Logics}",
    Number       = "MPI-I-95-2-002",
    Institution  = "Max-Planck-Institut f{\"u}r Informatik",
    Address      = "Saarbr{\"u}cken, Germany",
    Comment      = "TPTPRef"
}

@Article{OS85,
    Author       = "Ohlbach, H.J. and Schmidt-Schauss M.",
    Year         = "1985",
    Title        = "{The Lion and the Unicorn}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "1",
    Number       = "3",
    Pages        = "327-332",
    Comment      = "TPTPRef"
}

@Article{OZ11,
    Author       = "Oppenheimer, P. and Zalta, E.",
    Year         = "2011",
    Title        = "{A Computationally-Discovered Simplification of the
                    Ontological Argument}",
    Journal      = "Australasian Journal of Philosophy",
    Volume       = "89",
    Number       = "2",
    Pages        = "333-349",
    Comment      = "TPTPRef"
}

@Article{OS08,
    Author       = "Ortner, V. and Schirmer, N.",
    Year         = "2008",
    Title        = "{BDD Normalisation}",
    Journal      = "Archive of Formal Proofs",
    Note         = "http://isa-afp.org/entries/BDD.shtml",
    Comment      = "TPTPRef"
}

@Unpublished{OTTER,
    Author       = "Otter",
    Title        = "{The problem collection distributed with the Otter ATP
                    system [McC90]}",
    Comment      = "TPTPRef"
}

@Article{Ove93,
    Author       = "Overbeek, R.",
    Year         = "1993",
    Title        = "{The CADE-11 Competitions: A Personal View}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "11",
    Number       = "3",
    Pages        = "315-316",
    Comment      = "TPTPRef"
}

@Unpublished{Ove90,
    Author       = "Overbeek, R.",
    Year         = "1990",
    Title        = "{ATP competition announced at CADE-10}",
    Comment      = "TPTPRef"
}

@Article{OMW76,
    Author       = "Overbeek, R. and McCharen, J. and Wos, L.",
    Year         = "1976",
    Title        = "{Complexity and Related Enhancements for Automated
                    Theorem-Proving Programs}",
    Journal      = "Computers and Mathematics with Applications",
    Volume       = "2",
    Pages        = "1-16",
    Comment      = "TPTPRef, general reasoning"
}

@Article{Pad91,
    Author       = "Padlewska, B.",
    Year         = "1991",
    Title        = "{Locally Connected Spaces}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "2",
    Number       = "1",
    Pages        = "93-96",
    Comment      = "TPTPRef"
}

@Article{Pad90,
    Author       = "Padlewska, B.",
    Year         = "1990",
    Title        = "{Families of Sets}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "1",
    Number       = "1",
    Pages        = "147-152",
    Comment      = "TPTPRef"
}

@Article{PD90,
    Author       = "Padlewska, B. and Darmochwa{\l}, A.",
    Year         = "1990",
    Title        = "{Topological Spaces and Continuous Functions}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "1",
    Number       = "1",
    Pages        = "223-230",
    Comment      = "TPTPRef"
}

@Article{PMV05,
    Author       = "Padmanabhan, R. and McCune, B. and Veroff, R.",
    Year         = "2005",
    Title        = "{Levi's Commutator Theorems for Cancellative Semigroups}",
    Journal      = "Semigroup Forum",
    Volume       = "71",
    Pages        = "152-157",
    Comment      = "TPTPRef"
}

@Article{PP00,
    Author       = "Padmanabhan, R. and Penner, P.",
    Year         = "2000",
    Title        = "{A Hyperbase for Binary Lattice Hyperidentities}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "24",
    Number       = "3",
    Pages        = "365-370",
    Comment      = "TPTPRef"
}

@Unpublished{PP95,
    Author       = "Paramasivam, M. and Plaisted, D.",
    Year         = "1995",
    Title        = "{Automated Deduction Techniques for Classification in
                    Concept Languages}",
    Comment      = "TPTPRef"
}

@InProceedings{PV+07,
    Author       = "Paskevich, A. and Verchinine, K. and Lyaletski, A. and
                    Anisimov, A.",
    Year         = "2007",
    Title        = "{Reasoning Inside a Formula and Ontological Correctness of
                    a Formal Mathematical Text}",
    Editor       = "Kauers, M. and Kerber, M. and Miner, R. and Windsteiger,
                    W.",
    BookTitle    = "{Calculemus/MKM 2007 - Work in Progress}",
    Number       = "RISC-Linz Report Series, 07-06",
    Pages        = "77-91",
    Institution  = "University of Linz",
    Address      = "Linz, Austria",
    Comment      = "TPTPRef"
}

@Book{Pau96,
    Author       = "Paulson, L.",
    Year         = "1996",
    Title        = "{ML for the Working Programmer}",
    Publisher    = "Cambridge University Press",
    Comment      = "TPTPRef"
}

@Book{Pea11,
    Author       = "Pease, A.",
    Year         = "2011",
    Title        = "{Ontology: A Practical Guide}",
    Publisher    = "Articulate Software Press",
    Comment      = "TPTPCite,TPTPRef"
}

@InProceedings{PS07-ESARLT,
    Author       = "Pease, A. and Sutcliffe, G.",
    Year         = "2007",
    Title        = "{First Order Reasoning on a Large Ontology}",
    Editor       = "Urban, J. and Sutcliffe, G. and Schulz, S.",
    BookTitle    = "{Proceedings of the CADE-21 Workshop on Empirically
                    Successful Automated Reasoning in Large Theories}",
    Place        = "Bremen, German",
    Series       = "CEUR Workshop Proceedings",
    Number       = "257",
    Pages        = "61-70",
    Comment      = "TPTPRef"
}

@Article{PB+94-ASR,
    Author       = "Peli, G. and Bruggeman, J. and Masuch, M. and O Nuallain,
                    B.",
    Year         = "1994",
    Title        = "{A Logical Approach to Formalizing Organizational Ecology:
                    Formalizing the Inertia-Fragment in First-Order Logic}",
    Journal      = "American Sociological Review",
    Volume       = "59",
    Number       = "2",
    Comment      = "TPTPRef"
}

@TechReport{PB+92-TR,
    Author       = "Peli, G. and Bruggeman, J. and Masuch, M. and O Nuallain,
                    B.",
    Year         = "1992",
    Title        = "{A Logical Approach to Formalizing Organizational Ecology:
                    Formalizing the Inertia-Fragment in First-Order Logic}",
    Number       = "CCSOM Preprint 92-74",
    Institution  = "Department of Statistics and Methodology, University of
                    Amsterdam",
    Comment      = "TPTPRef"
}

@InProceedings{PM94,
    Author       = "Peli, G. and Masuch, M.",
    Year         = "1994",
    Title        = "{The Logic of Propogation Strategies: Axiomatizing a
                    Fragment of Organization Ecology in First-Order Logic}",
    Editor       = "Moore, D.P.",
    BookTitle    = "{Academy Of Management: Best Papers Proceedings 1994}",
    Pages        = "218-222",
    Comment      = "TPTPRef"
}

@TechReport{PM93-TR-100,
    Author       = "Peli, G. and Masuch, M.",
    Year         = "1993",
    Title        = "{The Logic of Propogation Strategies: Axiomatizing a
                    Fragment of Organizational Ecology in First-Order Logic}",
    Number       = "CCSOM Report 93-100",
    Institution  = "Department of Statistics and Methodology, University of
                    Amsterdam",
    Comment      = "TPTPRef"
}

@Article{Pel88,
    Author       = "Pelletier, F.J.",
    Year         = "1988",
    Title        = "{Errata}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "4",
    Number       = "2",
    Pages        = "235-236",
    Comment      = "TPTPRef"
}

@TechReport{Pel87,
    Author       = "Pelletier, F.J.",
    Year         = "1987",
    Title        = "{Further Developments in THINKER, and Automated Theorem
                    Prover}",
    Number       = "TR-ARP-16/87",
    Institution  = "Automated Reasoning Project, Australian National
                    University",
    Address      = "Canberra, Australia",
    Comment      = "TPTPRef"
}

@Article{Pel86-JAR,
    Author       = "Pelletier, F.J.",
    Year         = "1986",
    Title        = "{Seventy-five Problems for Testing Automatic Theorem
                    Provers}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "2",
    Number       = "2",
    Pages        = "191-216",
    Comment      = "TPTPRef"
}

@TechReport{Pel82,
    Author       = "Pelletier, F.J.",
    Year         = "1982",
    Title        = "{Completely Non-clausal, Completely Heuristically Driven
                    Automatic Theorem Proving}",
    Number       = "TR82-7",
    Institution  = "Department of Computer Science, Edmonton, Alberta",
    Comment      = "TPTPRef"
}

@Article{PR86,
    Author       = "Pelletier, F.J. and Rudnicki, P.",
    Year         = "1986",
    Title        = "{Non-Obviousness}",
    Journal      = "Association for Automated Reasoning Newsletter",
    Number       = "6",
    Pages        = "4-5",
    Comment      = "TPTPRef"
}

@InProceedings{PSH17,
    Author       = "Pelletier, F.J. and Sutcliffe, G. and Hazen, A.P.",
    Year         = "2017",
    Title        = "{Automated Reasoning for the Dialetheic Logic RM3}",
    Editor       = "Rus, V. and Markov, Z.",
    BookTitle    = "{Proceedings of the 30th International FLAIRS Conference}",
    Place        = "Marco Island, USA",
    Pages        = "110-115",
    Comment      = "TPTPRef"
}

@Article{Pel98-JLC,
    Author       = "Peltier, N.",
    Year         = "1998",
    Title        = "{A New Method for Automated Finite Model Building
                    Exploiting Failures and Symmetries}",
    Journal      = "Journal of Logic and Computation",
    Volume       = "8",
    Number       = "4",
    Pages        = "511-543",
    Comment      = "TPTPData,TPTPRef,TPTPCite"
}

@InProceedings{PW07,
    Author       = "Pelzer, B. and Wernhard, C.",
    Year         = "2007",
    Title        = "{System Description: E-KRHyper}",
    Editor       = "Pfenning, F.",
    BookTitle    = "{Proceedings of the 21st International Conference on
                    Automated Deduction}",
    Place        = "Bremen, Germany",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "4603",
    Pages        = "508-513",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Article{PS81,
    Author       = "Peterson, G. and Stickel, M.E.",
    Year         = "1981",
    Title        = "{Complete Sets of Reductions for Some Equational
                    Theories}",
    Journal      = "Journal of the ACM",
    Volume       = "28",
    Number       = "8",
    Pages        = "233-264",
    Comment      = "TPTPRef"
}

@InProceedings{Pfe88,
    Author       = "Pfenning, F.",
    Year         = "1988",
    Title        = "{Single Axioms in the Implicational Propositional
                    Calculus}",
    Editor       = "Lusk, E. and Overbeek, R.",
    BookTitle    = "{Proceedings of the 9th International Conference on
                    Automated Deduction}",
    Place        = "Argonne, USA",
    Series       = "Lecture Notes in Computer Science",
    Number       = "310",
    Pages        = "710 - 713",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Article{Phi06,
    Author       = "Phillips, J.D.",
    Year         = "2006",
    Title        = "{A Short Basis for the Variety of WIP PACC-loops}",
    Journal      = "Quasigroups and Related Systems",
    Volume       = "14",
    Pages        = "73-80",
    Comment      = "TPTPRef"
}

@Article{Phi06-SF,
    Author       = "Phillips, J.D.",
    Year         = "2006",
    Title        = "{Short Equational Bases for Two Varieties of Groupoids
                    Associated with Involuted Restrictive Bisemigroups of
                    Binary Relations}",
    Journal      = "Semigroup Forum",
    Volume       = "73",
    Number       = "2",
    Pages        = "308-312",
    Comment      = "TPTPRef"
}

@InProceedings{PS08,
    Author       = "Phillips, J.D. and Stanovsky, D.",
    Year         = "2008",
    Title        = "{Automated Theorem Proving in Loop Theory}",
    Editor       = "Sutcliffe, G. and Colton, S. and Schulz, S.",
    BookTitle    = "{Proceedings of the CICM Workshop on Empirically Successful
                    Automated Reasoning in Mathematics}",
    Place        = "Birmingham, United Kingdom",
    Series       = "CEUR Workshop Proceedings",
    Number       = "378",
    Pages        = "42-53",
    Comment      = "TPTPRef"
}

@InCollection{PS08-LPARShort,
    Author       = "Phillips, J.D. and Stanovsky, D.",
    Year         = "2008",
    Title        = "{Using Automated Theorem Provers in Nonassociative
                    Algebra}",
    Editor       = "Cervesato, I. and Veith, H. and Voronkov, A.",
    BookTitle    = "{Short Papers of the 15th International Conference on Logic
                    for Programming, Artificial Intelligence, and Reasoning}",
    Place        = "Doha, Qatar",
    Publisher    = "Cool Press",
    Comment      = "TPTPRef"
}

@Article{PV08,
    Author       = "Phillips, J.D. and Vojtechovsky, P.",
    Year         = "2008",
    Title        = "{A Scoop from Groups: New Equational Foundations for
                    Loops}",
    Journal      = "Commentationes Mathematicae Universitatis Carolinae",
    Volume       = "49",
    Number       = "2",
    Pages        = "279-290",
    Comment      = "TPTPRef"
}

@Article{PV06,
    Author       = "Phillips, J.D. and Vojtechovsky, P.",
    Year         = "2006",
    Title        = "{C-loops: an Introduction}",
    Journal      = "Publicationes Mathematicae Debrecen",
    Volume       = "68",
    Number       = "1-2",
    Pages        = "115-137",
    Comment      = "TPTPRef"
}

@Article{PV05-a,
    Author       = "Phillips, J.D. and Vojtechovsky, P.",
    Year         = "2005",
    Title        = "{The Varieties of Quasigroups of Bol-Moufang Type: An
                    Equational Reasoning Approach}",
    Journal      = "Journal of Algebra",
    Volume       = "293",
    Pages        = "17-33",
    Comment      = "TPTPRef"
}

@Article{PV05-b,
    Author       = "Phillips, J.D. and Vojtechovsky, P.",
    Year         = "2005",
    Title        = "{The Varieties of Loops of Bol-Moufang Type}",
    Journal      = "Algebra Universalis",
    Volume       = "54",
    Number       = "3",
    Pages        = "259-271",
    Comment      = "TPTPRef"
}

@Book{Pie02,
    Author       = "Pierce, B.",
    Year         = "2002",
    Title        = "{Programming Languages}",
    Publisher    = "MIT Press",
    Comment      = "TPTPRef"
}

@InProceedings{Pla94-CADE-12,
    Author       = "Plaisted, D.A.",
    Year         = "1994",
    Title        = "{The Search Efficiency of Theorem Proving Strategies}",
    Editor       = "Bundy, A.",
    BookTitle    = "{Proceedings of the 12th International Conference on
                    Automated Deduction}",
    Place        = "Nancy, France",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "814",
    Pages        = "57-71",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Article{Pla88,
    Author       = "Plaisted, D.A.",
    Year         = "1988",
    Title        = "{Non-Horn Clause Logic Programming Without
                    Contrapositives}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "4",
    Number       = "3",
    Pages        = "287-325",
    Comment      = "TPTPRef, resolution/semantics"
}

@Article{Pla82,
    Author       = "Plaisted, D.A.",
    Year         = "1982",
    Title        = "{A Simplified Problem Reduction Format}",
    Journal      = "Artificial Intelligence",
    Volume       = "18",
    Pages        = "227-261",
    Comment      = "TPTPRef, resolution/semantics"
}

@Article{Pla81,
    Author       = "Plaisted, D.A.",
    Year         = "1981",
    Title        = "{Theorem Proving with Abstraction}",
    Journal      = "Artificial Intelligence",
    Volume       = "16",
    Pages        = "47-108",
    Comment      = "TPTPRef, semantics"
}

@Article{Pol90,
    Author       = "Pollock, J.L.",
    Year         = "1990",
    Title        = "{Interest Driven Suppositional Reasoning}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "6",
    Number       = "4",
    Pages        = "419-461",
    Comment      = "TPTPRef,FOF"
}

@Book{Pop95,
    Author       = "Popkorn, S.",
    Year         = "1995",
    Title        = "{First Steps in Modal Logic}",
    Publisher    = "Cambridge University Press",
    Comment      = "TPTPRef"
}

@Unpublished{Pop70,
    Author       = "Popplestone, R.J.",
    Year         = "1970",
    Title        = "{Freddy, Things and Sets}",
    Comment      = "TPTPRef, See MRS72"
}

@Unpublished{Pra93-Email,
    Author       = "Prasetya, W.",
    Year         = "1993",
    Title        = "{How to get FAUST?}",
    Series       = "HOL mailing list",
    Number       = "http://lal.cs.byu.edu/lal/holdoc/info-hol/15xx/1515.html",
    Comment      = "TPTPRef"
}

@InProceedings{PW06,
    Author       = "Prevosto, V. and Waldmann, U.",
    Year         = "2006",
    Title        = "{SPASS+T}",
    Editor       = "Sutcliffe, G. and Schmidt, R. and Schulz, S.",
    BookTitle    = "{Proceedings of the FLoC'06 Workshop on Empirically
                    Successful Computerized Reasoning, 3rd International Joint
                    Conference on Automated Reasoning}",
    Place        = "Seattle, USA",
    Series       = "CEUR Workshop Proceedings",
    Number       = "192",
    Pages        = "19-33",
    Comment      = "TPTPRef"
}

@InProceedings{PGS06,
    Author       = "Puzis, Y. and Gao, Y. and Sutcliffe, G.",
    Year         = "2006",
    Title        = "{Automated Generation of Interesting Theorems}",
    Editor       = "Sutcliffe, G. and Goebel, R.",
    BookTitle    = "{Proceedings of the 19th International FLAIRS Conference}",
    Place        = "Melbourne Beach, USA",
    Pages        = "49-54",
    Publisher    = "AAAI Press",
    Comment      = "TPTPRef"
}

@Book{Qua92-Book,
    Author       = "Quaife, A.",
    Year         = "1992",
    Title        = "{Automated Development of Fundamental Mathematical
                    Theories}",
    Publisher    = "Kluwer Academic Publishers",
    Comment      = "TPTPRef"
}

@Article{Qua92-JAR,
    Author       = "Quaife, A.",
    Year         = "1992",
    Title        = "{Automated Deduction in von Neumann-Bernays-Godel Set
                    Theory}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "8",
    Number       = "1",
    Pages        = "91-147",
    Comment      = "TPTPRef"
}

@Unpublished{Qua92-Problems,
    Author       = "Quaife, A.",
    Year         = "1992",
    Title        = "{Problems based on NBG Set Theory}",
    Comment      = "TPTPRef, Emailed to G. Sutcliffe"
}

@Article{Qua90,
    Author       = "Quaife, A.",
    Year         = "1990",
    Title        = "{Andrews' Challenge Problem Revisited}",
    Journal      = "AAR Newsletter",
    Volume       = "15",
    Pages        = "3-7",
    Comment      = "TPTPRef"
}

@Article{Qua89,
    Author       = "Quaife, A.",
    Year         = "1989",
    Title        = "{Automated Development of Tarski's Geometry}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "5",
    Number       = "1",
    Pages        = "97-118",
    Comment      = "TPTPRef"
}

@Book{Qui82,
    Author       = "Quine, W.V.",
    Year         = "1982",
    Title        = "{Methods of Logic}",
    Pages        = "183",
    Publisher    = "Harvard University Press",
    Comment      = "TPTPRef"
}

@Book{Qui69,
    Author       = "Quine, W.V.",
    Year         = "1969",
    Title        = "{Set Theory and its Logic}",
    Publisher    = "Harvard University Press",
    Comment      = "TPTPRef"
}

@InProceedings{Rab06,
    Author       = "Rabe, F.",
    Year         = "2006",
    Title        = "{Towards Determining the Subset Relation between
                    Propositional Modal Logics}",
    Editor       = "Sutcliffe, G. and Schmidt, R. and Schulz, S.",
    BookTitle    = "{Proceedings of the FLoC'06 Workshop on Empirically
                    Successful Computerized Reasoning, 3rd International Joint
                    Conference on Automated Reasoning}",
    Place        = "Seattle, USA",
    Series       = "CEUR Workshop Proceedings",
    Number       = "192",
    Comment      = "TPTPRef"
}

@Article{Rad06,
    Author       = "Radziszowski, S.",
    Year         = "2006",
    Title        = "{Small Ramsey Numbers}",
    Journal      = "Journal of Combinatorics",
    Series       = "Dynamic Surveys",
    Number       = "DS1",
    Comment      = "TPTPRef"
}

@InProceedings{RRG05,
    Author       = "Ramachandran, D. and Reagan P. and Goolsbey, K.",
    Year         = "2005",
    Title        = "{First-orderized ResearchCyc: Expressiveness and Efficiency
                    in a Common Sense Knowledge Base}",
    Editor       = "Shvaiko P.",
    BookTitle    = "{Proceedings of the Workshop on Contexts and Ontologies:
                    Theory, Practice and Applications}",
    Place        = "Pittsburgh, USA",
    Comment      = "TPTPRef"
}

@InProceedings{RCC92,
    Author       = "Randell, D. and Cui, Z. and Cohn, A.",
    Year         = "1992",
    Title        = "{A Spatial Logic Based on Regions and Connection}",
    Editor       = "Nebel, B. and Swartout, W.",
    BookTitle    = "{Proceedings of the 3rd International Conference on the
                    Principles of Knowledge Representation and Reasoning}",
    Place        = "Cambridge, USA",
    Pages        = "165-176",
    Publisher    = "Morgan-Kaufmann",
    Comment      = "TPTPRef"
}

@Article{ROK07,
    Author       = "Raths, T. and Otten, J. and Kreitz, C.",
    Year         = "2007",
    Title        = "{The ILTP Problem Library for Intuitionistic Logic -
                    Release v1.1}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "38",
    Number       = "1-2",
    Pages        = "261-271",
    Comment      = "TPTPRef"
}

@Unpublished{RS+-URL,
    Author       = "Reagan Smith, P. and Sutcliffe, G. and Goolsbey, K. and
                    Kahlert, R.C.",
    Year         = "",
    Title        = "{The Cyc TPTP Challenge Problem Set}",
    Note         = "http://www.opencyc.org/doc/tptp_challenge_problem_set",
    Comment      = "TPTPRef"
}

@TechReport{RR+72,
    Author       = "Reboh, R. and Raphael, B. and Yates, R.A. and Kling, R.E.
                    and Velarde, C.",
    Year         = "1972",
    Title        = "{Study of automatic theorem proving programs}",
    Number       = "Technical Note 72",
    Institution  = "Artificial Intelligence Center, SRI International",
    Address      = "Menlo Park, CA",
    Comment      = "TPTPRef"
}

@InProceedings{RD+04,
    Author       = "Rector, A. and Drummond, N. and Horridge, M. and Rogers,
                    J. and Knublauch, H. and Stevens, R. and Wang, H. and
                    Wroe, C.",
    Year         = "2004",
    Title        = "{OWL Pizzas: Practical Experience of Teaching OWL-DL:
                    Common Errors & Common Patterns}",
    Editor       = "Motta, E. and Shadbolt, N. and Stutt, A. and Gibbins,
                    N.",
    BookTitle    = "{Proceedings of the 14th International Conference on
                    Engineering Knowledge in the Age of the Semantic Web}",
    Place        = "Whittlebury Hall, United Kingdom",
    Series       = "Lecture Notes in Computer Science",
    Number       = "3257",
    Pages        = "63-81",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Book{RU+13,
    Author       = "Reece, J. and Urry, L. and Cain, M. and Wasserman, S. and
                    Minorsky, P. and Jackson, R.",
    Year         = "2013",
    Title        = "{Campbell Biology}",
    Publisher    = "Benjamin-Cummings",
    Comment      = "TPTPRef"
}

@Book{Rei01,
    Author       = "Reiter, R.",
    Year         = "2001",
    Title        = "{Knowledge in Action: Logical Foundations for Specifying
                    and Implementing Dynamical Systems}",
    Publisher    = "MIT Press",
    Comment      = "TPTPRef"
}

@Article{Rei92,
    Author       = "Reiter, R.",
    Year         = "1992",
    Title        = "{What Should a Database Know?}",
    Journal      = "Journal of Logic Programming",
    Volume       = "14",
    Number       = "1-2",
    Pages        = "127-153",
    Comment      = "TPTPRef"
}

@Article{Ret05-JFM,
    Author       = "Retel, K.",
    Year         = "2005",
    Title        = "{Properties of First and Second Order Cutting of Binary
                    Relations}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "13",
    Number       = "3",
    Pages        = "361-365",
    Comment      = "TPTPRef,RELSET_2"
}

@Article{Rob63,
    Author       = "Robinson, J.A.",
    Year         = "1963",
    Title        = "{Theorem Proving on the Computer}",
    Journal      = "Jounal of the ACM",
    Volume       = "10",
    Number       = "2",
    Pages        = "163-174",
    Comment      = "TPTPRef/general reasoning"
}

@TechReport{RR98,
    Author       = "Rodrigues, O. and Russo, A.",
    Year         = "1998",
    Title        = "{A Translation Method for Belnap Logic}",
    Number       = "DoC 98/7",
    Institution  = "Imperial College London",
    Comment      = "TPTPRef"
}

@Article{RG04-JFM,
    Author       = "Romanowicz, K. and Grabowski, A.",
    Year         = "2004",
    Title        = "{The Operation of Addition of Relational Structures}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "12",
    Number       = "3",
    Pages        = "335-339",
    Comment      = "TPTPRef,LATSUM_1"
}

@Article{RW01,
    Author       = "Rose, M. and Wilkinson, K.",
    Year         = "2001",
    Title        = "{Application of Model Search to Lattice Theory}",
    Journal      = "Association for Automated Reasoning Newsletter",
    Volume       = "52",
    Comment      = "TPTPRef"
}

@Book{Ros90,
    Author       = "Ross, K.A.",
    Year         = "1990",
    Title        = "{Elementary Analysis: The Theory of Calculus}",
    Edition      = "2nd",
    Publisher    = "Springer",
    Comment      = "TPTPRef"
}

@Article{RR93,
    Author       = "Rubin, A. and Rubin, J.",
    Year         = "1993",
    Title        = "{Weak Forms of the Axiom of Choice and the Generalized
                    Continuum Hypothesis}",
    Journal      = "Mathematical Logic Quarterly",
    Volume       = "39",
    Number       = "1",
    Pages        = "7-22",
    Comment      = "TPTPRef"
}

@Article{Rud98-JFM,
    Author       = "Rudnicki, P.",
    Year         = "1998",
    Title        = "{Representation Theorem for Free Continuous Lattices}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "7",
    Number       = "2",
    Pages        = "185-188",
    Comment      = "TPTPRef,WAYBEL22"
}

@Book{Rus85,
    Author       = "Russell, B.",
    Year         = "1985",
    Title        = "{The Philosophy of Logical Atomism}",
    Publisher    = "Open Court",
    Comment      = "TPTPRef"
}

@Book{RW10,
    Author       = "Russell, B. and Whitehead, A.",
    Year         = "1910",
    Title        = "{Principia Mathmatica}",
    Publisher    = "Cambridge University Press",
    Comment      = "TPTPRef"
}

@Book{RN95,
    Author       = "Russell, S.J. and Norvig, P.",
    Year         = "1995",
    Title        = "{Artificial Intelligence: a modern approach}",
    Publisher    = "Prentice-Hall",
    Comment      = "TPTPRef,general AI"
}

@InProceedings{RN11,
    Author       = "Rybalchenko, A. and Navarro Perez, J.",
    Year         = "2011",
    Title        = "{Separation Logic + Superposition Calculus = Heap Theorem
                    Prover}",
    Editor       = "Cervesato, I. and Veith, H. and Voronkov, A.",
    BookTitle    = "{Proceedings of the 32nd ACM SIGPLAN conference on
                    Programming Language Design and Implementation}",
    Pages        = "To appear",
    Publisher    = "ACM Press",
    Comment      = "TPTPRef"
}

@InProceedings{Sah06,
    Author       = "Sahami, M.",
    Year         = "2006",
    Title        = "{Mining the Web to Determine Similarity Between Words,
                    Objects, and Communities}",
    Editor       = "Sutcliffe, G. and Goebel, R.",
    BookTitle    = "{Proceedings of the 19th International FLAIRS Conference}",
    Place        = "Melbourne Beach, USA",
    Pages        = "14-19",
    Publisher    = "AAAI Press",
    Comment      = "TPTPRef"
}

@Book{Sch99,
    Author       = "Schey, J.",
    Year         = "1999",
    Title        = "{Introduction to Manufacturing Processes}",
    Publisher    = "McGraw-Hill",
    Comment      = "TPTPRef"
}

@Book{SS93,
    Author       = "Schmidt, G. and Str{\"}ohlein, T.",
    Year         = "1993",
    Title        = "{Relations and Graphs: Discrete Mathematics for Computer
                    Scientists}",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@MastersThesis{Sch95,
    Author       = "Schulz, S.",
    Year         = "1995",
    Title        = "{Explanation Based Learning for Distributed Equational
                    Deduction}",
    School       = "Universit{\"a}t Kaiserslautern",
    Comment      = "TPTPRef"
}

@InProceedings{SB05-IWIL,
    Author       = "Schulz, S. and Bonacina, M.P.",
    Year         = "2005",
    Title        = "{On Handling Distinct Objects in the Superposition
                    Calculus}",
    Editor       = "Konev, B. and Schulz, S.",
    BookTitle    = "{Proceedings of the 5th International Workshop on the
                    Implementation of Logics}",
    Place        = "Montevideo, Uruguay",
    Pages        = "66-77",
    Comment      = "TPTPRef"
}

@Book{SST83,
    Author       = "Schwabbauser, W. and Szmielew, W. and Tarski, A.",
    Year         = "1983",
    Title        = "{Metamathematische Methoden in der Geometrie}",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Article{Sch01-JFM,
    Author       = "Schwarzweller, C.",
    Year         = "2001",
    Title        = "{A Characterization of Concept Lattices. Dual Concept
                    Lattices}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "9",
    Number       = "1",
    Pages        = "55-59",
    Comment      = "TPTPRef,CONLAT_2"
}

@InProceedings{Sco79,
    Author       = "Scott, D.",
    Year         = "1979",
    Title        = "{Identity and Existence in Intuitionist Logic}",
    Editor       = "Fournam M.P.",
    BookTitle    = "{Durham Proceedings Applications of Sheaves}",
    Pages        = "660-696",
    Publisher    = "Lecture Notes in Mathematics Volume 753, Springer",
    Comment      = "TPTPRef"
}

@Article{Seg73,
    Author       = "Segerberg, K.",
    Year         = "1973",
    Title        = "{Two-Dimensional Modal Logic}",
    Journal      = "Journal of Philosophical Logic",
    Volume       = "2",
    Number       = "1",
    Pages        = "77-96",
    Comment      = "TPTPRef"
}

@Article{SE94,
    Author       = "Segre, A. and Elkan, C.",
    Year         = "1994",
    Title        = "{A High-Performance Explanation-Based Learning Algorithm}",
    Journal      = "Artificial Intelligence",
    Volume       = "69",
    Number       = "NEED",
    Pages        = "1-50",
    Comment      = "TPTPRef"
}

@InProceedings{SLB12,
    Author       = "Seidl, M. and Lonsing, F. and Biere, A.",
    Year         = "2012",
    Title        = "{Tool for Generating EPR Formulas from QBF}",
    Editor       = "Fontaine, P. and Schmidt, R. and Schulz, S.",
    BookTitle    = "{Proceedings of the 3rd Workshop on Practical Aspects of
                    Automated Reasoning, 6th International Joint Conference on
                    Automated Reasoning}",
    Place        = "Manchester, England",
    Pages        = "139-148",
    Comment      = "TPTPRef"
}

@Unpublished{SETHE,
    Author       = "SETHEO",
    Title        = "{AR Research Group, Technische Universit{\"a}t M{\"u}nchen,
                    Problem Library}",
    Note         = "No longer available",
    Comment      = "TPTPRef"
}

@Book{Sha97,
    Author       = "Shanahan, M.",
    Year         = "1997",
    Title        = "{Solving the Frame Problem}",
    Publisher    = "MIT Press",
    Comment      = "TPTPRef"
}

@MastersThesis{She06,
    Author       = "Shen, W.",
    Year         = "2006",
    Title        = "{Automated Proofs of Equivalence of Modal Logic Systems}",
    School       = "Department of Computer Science, University of Miami",
    Address      = "Miami, USA",
    Comment      = "TPTPRef,TPTPCite"
}

@Article{Sho76,
    Author       = "Shostak, R.E.",
    Year         = "1976",
    Title        = "{Refutation Graphs}",
    Journal      = "Artificial Intelligence",
    Volume       = "7",
    Pages        = "51-64",
    Comment      = "TPTPRef, linear systems"
}

@Book{Sid09,
    Author       = "Sider, T.",
    Year         = "2009",
    Title        = "{Logic for Philosophy}",
    Publisher    = "Oxford University Press",
    Comment      = "TPTPRef"
}

@InCollection{SB+03,
    Author       = "Siekman, J. and Benzm{\"u}ller, C. and Fiedler, A. and
                    Meier A. and Normann, I. and Pollet, M.",
    Year         = "2003",
    Title        = "{Proof Development with Omega: The Irrationality of
                    Root2}",
    Editor       = "Kamareddine, F.",
    BookTitle    = "{Thirty Five Years of Automating Mathematics}",
    Series       = "Kluwer Applied Logic Series",
    Number       = "28",
    Pages        = "271-314",
    Publisher    = "Kluwer Academic Publishers",
    Comment      = "TPTPRef"
}

@Article{SRM73,
    Author       = "Siklossy, L. and Rich, A. and Marinov, V.",
    Year         = "1973",
    Title        = "{Breadth First Search: Some Surprising Results}",
    Journal      = "Artificial Intelligence",
    Volume       = "4",
    Pages        = "1-27",
    Comment      = "TPTPRef"
}

@Article{Sko01-JFM,
    Author       = "Skorulski, B.",
    Year         = "2001",
    Title        = "{The Tichonov Theorem}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "9",
    Number       = "2",
    Pages        = "373-376",
    Comment      = "TPTPRef,YELLOW17"
}

@Article{Sla67,
    Author       = "Slagle, J.R.",
    Year         = "1967",
    Title        = "{Automatic Theorem Proving with Renamable and Semantic
                    Resolution}",
    Journal      = "Journal of the ACM",
    Volume       = "14",
    Number       = "4",
    Pages        = "687-697",
    Comment      = "TPTPRef, resolution/semantics"
}

@Article{Sla02-JAR,
    Author       = "Slaney, J.K.",
    Year         = "2002",
    Title        = "{More Proofs of an Axiom of \Lukasiewicz}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "29",
    Number       = "1",
    Pages        = "59-66",
    Comment      = "TPTPRef"
}

@InProceedings{Sla93,
    Author       = "Slaney, J.K.",
    Year         = "1993",
    Title        = "{SCOTT: A Model-Guided Theorem Prover}",
    Editor       = "Bajcsy, R.",
    BookTitle    = "{Proceedings of the 13th International Conference on
                    Artificial Intelligence}",
    Place        = "Chambery, France",
    Pages        = "109-114",
    Publisher    = "Morgan-Kaufmann",
    Comment      = "TPTPRefForResults, semantics"
}

@TechReport{Sla92,
    Author       = "Slaney, J.K.",
    Year         = "1992",
    Title        = "{FINDER (Finite Domain Enumerator): Notes and Guide}",
    Number       = "TR-ARP-1/92",
    Institution  = "Automated Reasoning Project, Australian National
                    University",
    Address      = "Canberra, Australia",
    Comment      = "TPTPRef"
}

@Article{SFS95,
    Author       = "Slaney, J.K. and Fujita, M. and Stickel, M.E.",
    Year         = "1995",
    Title        = "{Automated Reasoning and Exhaustive Search: Quasigroup
                    Existence Problems}",
    Journal      = "Computers and Mathematics with Applications",
    Volume       = "29",
    Number       = "2",
    Pages        = "115-132",
    Comment      = "TPTPRef"
}

@InProceedings{SH97,
    Author       = "Slaney, J.K. and Hodgson, K.",
    Year         = "1997",
    Title        = "{Extending SCOTT to use Multiple Models}",
    Editor       = "Pollack M.E.",
    BookTitle    = "{Proceedings of the 15th International Joint Conference on
                    Artificial Intelligence}",
    Place        = "Nagoya, Japan",
    Pages        = "???-???",
    Publisher    = "Morgan Kaufmann",
    Comment      = "TPTPRefForResults"
}

@InProceedings{SLM94,
    Author       = "Slaney, J.K. and Lusk, E. and McCune, W.W.",
    Year         = "1994",
    Title        = "{SCOTT: Semantically Constrained Otter, System
                    Description}",
    Editor       = "Bundy, A.",
    BookTitle    = "{Proceedings of the 12th International Conference on
                    Automated Deduction}",
    Place        = "Nancy, France",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "814",
    Pages        = "764-768",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRefForResults"
}

@Book{Smi07,
    Author       = "Smith, P.",
    Year         = "2007",
    Title        = "{An Introduction to Goedel's Theorems}",
    Publisher    = "Cambridge University Press",
    Comment      = "TPTPRef"
}

@Book{Smu87,
    Author       = "Smullyan, R.M.",
    Year         = "1987",
    Title        = "{Forever Undecided - A Puzzle Guide to Godel}",
    Publisher    = "Knopf",
    Comment      = "TPTPRef"
}

@Book{Smu78,
    Author       = "Smullyan, R.M.",
    Year         = "1978",
    Title        = "{What is the Name of This Book? The Riddle of Dracula and
                    Other Logical Puzzles}",
    Publisher    = "Prentice-Hall",
    Comment      = "TPTPRef"
}

@Book{Smu85,
    Author       = "Smullyan, R.M.",
    Year         = "1978",
    Title        = "{To Mock a Mocking Bird and Other Logic Puzzles}",
    Publisher    = "Knopf",
    Comment      = "TPTPRef"
}

@Book{Smu68,
    Author       = "Smullyan, R.M.",
    Year         = "1968",
    Title        = "{First-Order Logic}",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Article{Sob52,
    Author       = "Soboci{\'n}ski, B.",
    Year         = "1952",
    Title        = "{Axiomatization of a Partial System of Three-valued
                    Calculus of Propositions`}",
    Journal      = "Journal of Computing Systems",
    Volume       = "1",
    Pages        = "23-55",
    Comment      = "TPTPRef"
}

@Article{Soc92,
    Author       = "Socher-Ambrosius, R.",
    Year         = "1992",
    Title        = "{How to Avoid the Derivation of Redundant Clauses in
                    Reasoning Systems`}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "9",
    Number       = "1",
    Pages        = "77-97",
    Comment      = "TPTPRef"
}

@Unpublished{SPRFN,
    Author       = "SPRFN",
    Title        = "{The problem collection distributed with the SPRFN ATP
                    system}",
    Comment      = "TPTPRef"
}

@Article{Sta08,
    Author       = "Stanovsky, D.",
    Year         = "2008",
    Title        = "{Distributive Groupoids are Symmetric-by-medial: An
                    Elementary Proof}",
    Journal      = "Commentationes Mathematicae Universitatis Carolinae",
    Volume       = "49",
    Number       = "4",
    Pages        = "541-546",
    Comment      = "TPTPRef"
}

@InProceedings{Ste05,
    Author       = "Steel, G.",
    Year         = "2005",
    Title        = "{Deduction with XOR Constraints in Security API
                    Modelling}",
    Editor       = "Nieuwenhuis, R.",
    BookTitle    = "{Proceedings of the 20th International Conference on
                    Automated Deduction}",
    Place        = "Tallinn, Estonia",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "3632",
    Pages        = "322-336",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Book{SS86,
    Author       = "Sterling, L. and Shapiro, E.",
    Year         = "1986",
    Title        = "{The Art of Prolog}",
    Publisher    = "MIT Press",
    Comment      = "TPTPRef"
}

@Unpublished{Ste92-Note,
    Author       = "Stevens, R.L.",
    Year         = "1992",
    Title        = "{Unpublished Note}",
    Comment      = "TPTPRef"
}

@InProceedings{Ste88,
    Author       = "Stevens, R.L.",
    Year         = "1988",
    Title        = "{Challenge Problems from Nonassociative Rings for Theorem
                    Provers}",
    Editor       = "Lusk, E. and Overbeek, R.",
    BookTitle    = "{Proceedings of the 9th International Conference on
                    Automated Deduction}",
    Place        = "Argonne, USA",
    Series       = "Lecture Notes in Computer Science",
    Number       = "310",
    Pages        = "730-734",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Article{Ste87,
    Author       = "Stevens, R.L.",
    Year         = "1987",
    Title        = "{Some Experiments in Nonassociative Ring Theory with an
                    Automated Theorem Prover}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "3",
    Number       = "2",
    Pages        = "211-221",
    Comment      = "TPTPRef"
}

@Article{Sti94-JAR,
    Author       = "Stickel, M.E.",
    Year         = "1994",
    Title        = "{Upside-Down Meta-Interpretation of the Model Elimination
                    Theorem-Proving Procedure for Deduction and Abduction}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "13",
    Number       = "2",
    Pages        = "189-210",
    Comment      = "TPTPRef"
}

@Article{Sti86-JAR,
    Author       = "Stickel, M.E.",
    Year         = "1986",
    Title        = "{Schubert's Steamroller Problem: Formulations and
                    Solutions}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "2",
    Number       = "1",
    Pages        = "89-101",
    Comment      = "TPTPRef, general reasoning"
}

@Article{Sti84-NGC,
    Author       = "Stickel, M.E.",
    Year         = "1984",
    Title        = "{A Prolog Technology Theorem Prover}",
    Journal      = "New Generation Computing",
    Volume       = "2",
    Number       = "4",
    Pages        = "371-383",
    Comment      = "TPTPRef"
}

@TechReport{Sto97,
    Author       = "Stoller, S.",
    Year         = "1997",
    Title        = "{Leader Election in Distributed Systems with Crash
                    Failures}",
    Number       = "TR481",
    Institution  = "Department of Computer Science, Indiana University",
    Address      = "Bloomington, USA",
    Comment      = "TPTPRef"
}

@Article{Sto00,
    Author       = "Stone, M.",
    Year         = "2000",
    Title        = "{Towards a Computational Account of Knowledge, Action and
                    Inference in Instructions}",
    Journal      = "Journal of Language and Computation",
    Volume       = "1",
    Pages        = "231-246",
    Comment      = "TPTPRef"
}

@InProceedings{Sto98,
    Author       = "Stone, M.",
    Year         = "1998",
    Title        = "{Abductive Planning with Sensing}",
    Editor       = "Mostow, J. and Rich, C.",
    BookTitle    = "{Proceedings of the 15th Conference on Artificial
                    Intelligence}",
    Place        = "Madison, USA",
    Pages        = "631-636",
    Publisher    = "AAAI Press",
    Comment      = "TPTPRef"
}

@InProceedings{Str08,
    Author       = "Struth, G.",
    Year         = "2008",
    Title        = "{Modal Tools for Separation and Refinement}",
    Editor       = "Boiten, E. and Derrick, J. and Schellhorn, G.",
    BookTitle    = "{Proceedings of the 13th BAC-FACS Refinement Workshop}",
    Place        = "Turku, Finland",
    Series       = "Electronic Notes in Theoretical Computer Science",
    Number       = "214",
    Pages        = "81-101",
    Publisher    = "Elsevier",
    Comment      = "TPTPRef"
}

@InProceedings{Str07,
    Author       = "Struth, G.",
    Year         = "2007",
    Title        = "{Reasoning Automatically about Termination and
                    Refinement}",
    Editor       = "Ranise, S.",
    BookTitle    = "{Proceedings of the 6th International Workshop on
                    First-Order Theorem Proving}",
    Place        = "Liverpool, United Kingdom",
    Pages        = "36-51",
    Comment      = "TPTPRef"
}

@Article{Str06,
    Author       = "Struth, G.",
    Year         = "2006",
    Title        = "{Abstract Abstract Reduction}",
    Journal      = "Journal of Logic and Algebraic Programming",
    Volume       = "66",
    Number       = "2",
    Pages        = "239-270",
    Comment      = "TPTPRef"
}

@InProceedings{SKW07,
    Author       = "Suchanek, F. and Kasneci, G. and Weikum, G.",
    Year         = "2007",
    Title        = "{YAGO: A Core of Semantic Knowledge}",
    Editor       = "Patel-Schneider, P. and Shenoy, P.",
    BookTitle    = "{Proceedings of the 16th International World Wide Web
                    Conference}",
    Place        = "Banff, Canada",
    Pages        = "697-706",
    Comment      = "TPTPRef"
}

@TechReport{Sus73,
    Author       = "Sussman, G.J.",
    Year         = "1973",
    Title        = "{A Computational Model of Skill Acquisition}",
    Number       = "297",
    Institution  = "MIT Artificial Intelligence Laboratory",
    Comment      = "TPTPRef"
}

@Article{Sut17,
    Author       = "Sutcliffe, G.",
    Year         = "2017",
    Title        = "{The TPTP Problem Library and Associated Infrastructure.
                    From CNF to TH0, TPTP v6.4.0}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "59",
    Number       = "4",
    Pages        = "483-502",
    Comment      = "TPTPRef"
}

@Article{Sut09,
    Author       = "Sutcliffe, G.",
    Year         = "2009",
    Title        = "{The TPTP Problem Library and Associated Infrastructure.
                    The FOF and CNF Parts, v3.5.0}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "43",
    Number       = "4",
    Pages        = "337-362",
    Comment      = "TPTPRef"
}

@InProceedings{Sut08-KEAPPA,
    Author       = "Sutcliffe, G.",
    Year         = "2008",
    Title        = "{The SZS Ontologies for Automated Reasoning Software}",
    Editor       = "Sutcliffe, G. and Rudnicki, P. and Schmidt, R. and Konev,
                    B. and Schulz, S.",
    BookTitle    = "{Proceedings of the LPAR Workshops: Knowledge Exchange:
                    Automated Provers and Proof Assistants, and The 7th
                    International Workshop on the Implementation of Logics}",
    Place        = "Doha, Qatar",
    Series       = "CEUR Workshop Proceedings",
    Number       = "418",
    Pages        = "38-49",
    Comment      = "TPTPRef"
}

@InProceedings{SGC03,
    Author       = "Sutcliffe, G. and Gao, Y. and Colton, S.",
    Year         = "2003",
    Title        = "{A Grand Challenge of Theorem Discovery}",
    Editor       = "Gow, J. and Walsh, T. and Colton, S. and Sorge, V.",
    BookTitle    = "{Proceedings of the Workshop on Challenges and Novel
                    Applications for Automated Reasoning, 19th International
                    Conference on Automated Reasoning}",
    Place        = "Miami, USA",
    Pages        = "1-11",
    Comment      = "TPTPRef"
}

@Article{SM96,
    Author       = "Sutcliffe, G. and Melville, S.",
    Year         = "1996",
    Title        = "{The Practice of Clausification in Automatic Theorem
                    Proving}",
    Journal      = "South African Computer Journal",
    Volume       = "18",
    Pages        = "57-68",
    Comment      = "TPTPRef,TPTPCite"
}

@InProceedings{SPH18,
    Author       = "Sutcliffe, G. and Pelletier, F.J. and Hazen, A.P.",
    Year         = "2018",
    Title        = "{Making Belnap's "Useful Four-Valued Logic" Useful}",
    Editor       = "Brawner, K. and Rus, V.",
    BookTitle    = "{Proceedings of the 31st International FLAIRS Conference}",
    Place        = "Melbourne, USA",
    Pages        = "116-121",
    Comment      = "TPTPRef"
}

@InProceedings{SP07,
    Author       = "Sutcliffe, G. and Puzis, Y.",
    Year         = "2007",
    Title        = "{SRASS - a Semantic Relevance Axiom Selection System}",
    Editor       = "Pfenning, F.",
    BookTitle    = "{Proceedings of the 21st International Conference on
                    Automated Deduction}",
    Place        = "Bremen, Germany",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "4603",
    Pages        = "295-310",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef,TPTPData"
}

@InProceedings{SS+10,
    Author       = "Sutcliffe, G. and Suda, M. and Teyssandier, A. and Dellis,
                    N. and de Melo, G.",
    Year         = "2010",
    Title        = "{Progress Towards Effective Automated Reasoning with World
                    Knowledge}",
    Editor       = "Murray, C. and Guesgen, H.",
    BookTitle    = "{Proceedings of the 23rd International FLAIRS Conference}",
    Place        = "Daytona Beach, USA",
    Pages        = "110-115",
    Publisher    = "AAAI Press",
    Comment      = "TPTPRef"
}

@Article{SS98-JAR,
    Author       = "Sutcliffe, G. and Suttner, C.B.",
    Year         = "1998",
    Title        = "{The TPTP Problem Library: CNF Release v1.2.1}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "21",
    Number       = "2",
    Pages        = "177-203",
    Comment      = "TPTPRef,SystemOnTPTP,TPTPCite"
}

@InProceedings{SYT09,
    Author       = "Sutcliffe, G. and Yerikalapudi, A. and Trac, S.",
    Year         = "2009",
    Title        = "{Multiple Answer Extraction for Question Answering with
                    Automated Theorem Proving Systems}",
    Editor       = "Guesgen, H. and Lane, C.",
    BookTitle    = "{Proceedings of the 22nd International FLAIRS Conference}",
    Place        = "Sanibel Island, USA",
    Pages        = "105-110",
    Publisher    = "AAAI Press",
    Comment      = "TPTPRef"
}

@InProceedings{SZS03,
    Author       = "Sutcliffe, G. and Zimmer, J. and Schulz, S.",
    Year         = "2003",
    Title        = "{Communication Formalisms for Automated Theorem Proving
                    Tools}",
    Editor       = "Sorge, V. and Colton, S. and Fisher, M. and Gow, J.",
    BookTitle    = "{Proceedings of the Workshop on Agents and Automated
                    Reasoning, 18th International Joint Conference on
                    Artificial Intelligence}",
    Place        = "Acapulco, Mexico",
    Pages        = "52-57",
    Comment      = "TPTPRef"
}

@PhDThesis{Sut95-Thesis,
    Author       = "Suttner, C.B.",
    Year         = "1995",
    Title        = "{Parallelization of Search-based Systems by Static
                    Partitioning with Slackness}",
    School       = "Institut f{\"u}r Informatik, Technische Universit{\"a}t
                    M{\"u}nchen",
    Address      = "Munich, Germany",
    Note         = "and Dissertationen zur k{\"u}nstlichen Intelligenz 101,
                    Springer-Verlag",
    Comment      = "TPTPRefForResults,TPTPCite,TPTPData"
}

@TechReport{Sve08,
    Author       = "Svensson, H.",
    Year         = "2008",
    Title        = "{A Semi-Automatic Correctness Proof Procedure applied to
                    Stoller's Leader Election Algorithm}",
    Number       = "Technical Report 2008:7",
    Institution  = "Computer Science and Engineering, Chalmers University of
                    Technology",
    Address      = "Goteborg, Sweden",
    Comment      = "TPTPRef"
}

@InProceedings{Tar59,
    Author       = "Tarski, A.",
    Year         = "1959",
    Title        = "{What is Elementary Geometry?}",
    Editor       = "Henkin, L.",
    BookTitle    = "{Proceedings of an International Symposium. The axiomatic
                    method with special reference to geometry and physics}",
    Comment      = "TPTPRef"
}

@Book{Tar51,
    Author       = "Tarski, A.",
    Year         = "1951",
    Title        = "{A Decision Method for Elementary Algebra and Geometry}",
    Edition      = "2ed",
    Publisher    = "University of California Press",
    Comment      = "TPTPRef"
}

@Article{Tar41,
    Author       = "Tarski, A.",
    Year         = "1941",
    Title        = "{On the Calculus of Relations}",
    Journal      = "Journal of Symbolic Logic",
    Volume       = "6",
    Number       = "3",
    Pages        = "73-89",
    Comment      = "TPTPRef"
}

@Article{Tar38,
    Author       = "Tarski, A.",
    Year         = "1938",
    Title        = "{Ein Beitrag zur Axiomatik der Abelschen Gruppe n}",
    Journal      = "Fundamenta Mathematicae",
    Volume       = "30",
    Pages        = "253-256",
    Comment      = "TPTPRef"
}

@Article{Tar38-68-89,
    Author       = "Tarski, A.",
    Year         = "1938",
    Title        = "{{\"U}ber unerreichbare Kardinalzahlen}",
    Journal      = "Fundamenta Mathematicae",
    Volume       = "30",
    Pages        = "68-89",
    Comment      = "TPTPRef"
}

@Book{TE99,
    Author       = "Teichmann, J. and Evans, K.",
    Year         = "1999",
    Title        = "{Philosophy: A Beginner's Guide}",
    Publisher    = "Blackwell",
    Comment      = "TPTPRef"
}

@Book{Ter03,
    Author       = "Terese",
    Year         = "2003",
    Title        = "{Term Rewriting Systems}",
    Series       = "Cambridge Tracts in Theoretical Computer Science",
    Number       = "55",
    Publisher    = "Cambridge University Press",
    Comment      = "TPTPRef"
}

@Book{TS00,
    Author       = "Troelstra, A. and Schwichtenberg, H.",
    Year         = "2000",
    Title        = "{Basic Proof Theory}",
    Series       = "Cambridge Tracts in Theoretical Computer Science",
    Volume       = "43",
    Publisher    = "Cambridge University Press",
    Comment      = "TPTPRef"
}

@Article{Try97,
    Author       = "Trybulec, A.",
    Year         = "1997",
    Title        = "{Moore-Smith Convergence}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "6",
    Number       = "2",
    Pages        = "213-225",
    Comment      = "TPTPRef"
}

@Article{Try92-JFM,
    Author       = "Trybulec, A.",
    Year         = "1992",
    Title        = "{Some Isomorphisms Between Functor Categories}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "3",
    Number       = "1",
    Pages        = "33-40",
    Comment      = "TPTPRef,ISOCAT_2"
}

@Article{Try90-JFM-ES,
    Author       = "Trybulec, A.",
    Year         = "1990",
    Title        = "{Enumerated Sets}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "1",
    Number       = "1",
    Pages        = "25-34",
    Comment      = "TPTPRef"
}

@Article{Try90-JFM-TGST,
    Author       = "Trybulec, A.",
    Year         = "1990",
    Title        = "{Tarski Grothendieck Set Theory}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "1",
    Number       = "1",
    Pages        = "9-11",
    Comment      = "TPTPRef"
}

@Article{Try90-JMF-TPCP,
    Author       = "Trybulec, A.",
    Year         = "1990",
    Title        = "{Tuples, Projections and Cartesian Products}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "1",
    Number       = "1",
    Pages        = "97-105",
    Comment      = "TPTPRef"
}

@Article{TD90,
    Author       = "Trybulec, A. and Darmochwal, A.",
    Year         = "1990",
    Title        = "{Boolean Domains}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "1",
    Number       = "1",
    Pages        = "187-190",
    Comment      = "TPTPRef"
}

@Article{TS89,
    Author       = "Trybulec, A. and Swieczkowska, H.",
    Year         = "1989",
    Title        = "{Boolean Properties of Sets}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "1",
    Number       = "1",
    Pages        = "17-23",
    Comment      = "TPTPRef"
}

@Article{TB90,
    Author       = "Trybulec, W. and Bancerek, G.",
    Year         = "1990",
    Title        = "{Kuratowski - Zorn Lemma}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "1",
    Number       = "2",
    Pages        = "387-393",
    Comment      = "TPTPRef"
}

@Article{Try90-JFM-PS,
    Author       = "Trybulec, Z.",
    Year         = "1990",
    Title        = "{Properties of Subsets}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "1",
    Number       = "1",
    Pages        = "67-71",
    Comment      = "TPTPRef"
}

@InProceedings{TR+04,
    Author       = "Tsarkov, D. and Riazanov, A. and Bechhofer, S. and
                    Horrocks, I.",
    Year         = "2004",
    Title        = "{Using Vampire to Reason with OWL}",
    Editor       = "McIlraith, S. and Plexousakis, D. and van Harmelen, F.",
    BookTitle    = "{Proceedings of the 3rd International Semantic Web
                    Conference}",
    Place        = "Hiroshima, Japan",
    Series       = "Lecture Notes in Computer Science",
    Number       = "3298",
    Pages        = "471-485",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef,TPTPCite"
}

@InProceedings{Tse83,
    Author       = "Tseitin, G.S.",
    Year         = "1983",
    Title        = "{On the Complexity of Derivations in Propositional
                    Calculus}",
    Editor       = "Siekmann, J. and Wrightson, G.",
    BookTitle    = "{The Automation of Reasoning}",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Article{Urb06,
    Author       = "Urban, J.",
    Year         = "2006",
    Title        = "{MPTP 0.2: Design, Implementation, and Initial
                    Experiments}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "37",
    Number       = "1-2",
    Pages        = "21-43",
    Comment      = "TPTPCite,TPTPRef"
}

@Article{URS13,
    Author       = "Urban, J. and Rudnicki, P. and Sutcliffe, G.",
    Year         = "2013",
    Title        = "{ATP and Presentation Service for Mizar Formalizations}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "50",
    Number       = "2",
    Pages        = "229-241",
    Comment      = "TPTPRef"
}

@Article{Urq87,
    Author       = "Urquhart, A.",
    Year         = "1987",
    Title        = "{Hard Problems for Resolution}",
    Journal      = "Journal of the ACM",
    Volume       = "34",
    Number       = "1",
    Pages        = "209-219",
    Comment      = "TPTPRef"
}

@PhDThesis{vBJ79,
    Author       = "van Benthem Jutting, L.S.",
    Year         = "1979",
    Title        = "{Checking Landau's "Grundlagen" in the AUTOMATH System}",
    Series       = "Math. Centre Tracts",
    Number       = "83",
    School       = "Eindhoven University",
    Address      = "Eindhoven, The Netherlands",
    Comment      = "TPTPRef"
}

@InProceedings{VLP07,
    Author       = "Verchinine, K. and Lyaletski, A. and Paskevich, A.",
    Year         = "2007",
    Title        = "{System for Automated Deduction (SAD): A Tool for Proof
                    Verification}",
    Editor       = "Pfenning, F.",
    BookTitle    = "{Proceedings of the 21st International Conference on
                    Automated Deduction}",
    Place        = "Bremen, Germany",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "4603",
    Pages        = "398-403",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef,TPTPCite"
}

@InProceedings{VL+08,
    Author       = "Verchinine, K. and Lyaletski, A. and Paskevich, A. and
                    Anisimov, A.",
    Year         = "2008",
    Title        = "{On Correctness of Mathematical Texts from a Logical and
                    Practical Point of View}",
    Editor       = "Autexier, S. and Campbell, J. and Rubio, J. and Sorge, V.
                    and Suzuki, M. and Wiedijk, F.",
    BookTitle    = "{Proceedings of the Conferences on Intelligent Computer
                    Mathematics}",
    Place        = "Birmingham, United Kingdon",
    Series       = "Lecture Notes in Computer Science",
    Number       = "5144",
    Pages        = "583-598",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Article{Ver01,
    Author       = "Veroff, R.",
    Year         = "2001",
    Title        = "{A Strategy for Proving Theorems in Many-Valued Logic}",
    Journal      = "AAR Newsletter",
    Volume       = "53",
    Comment      = "TPTPRef"
}

@Article{Ver94,
    Author       = "Veroff, R.",
    Year         = "1994",
    Title        = "{Problem Set}",
    Journal      = "AAR Newsletter",
    Volume       = "24",
    Pages        = "8",
    Comment      = "TPTPRef"
}

@Unpublished{VM-URL,
    Author       = "Veroff, R. and McCune, W.",
    Year         = "",
    Title        = "{First-order Proof of a Median Algebra Problem}",
    Note         = "http://www.cs.unm.edu/~veroff/MEDIAN_ALGEBRA/",
    Comment      = "TPTPRef"
}

@InCollection{vON99,
    Author       = "von Oheimb, D. and Nipkow, T.",
    Year         = "1999",
    Title        = "{Machine-Checking the Java Specification: Proving
                    Type-Safety}",
    Editor       = "Alves-Foss, J.",
    BookTitle    = "{Formal Syntax and Semantics of Java}",
    Series       = "Lecture Notes in Computer Science",
    Pages        = "119-156",
    Comment      = "TPTPRef"
}

@Article{vPl98,
    Author       = "von Plato, J.",
    Year         = "1998",
    Title        = "{A Constructive Theory of Ordered Affine Geometry}",
    Journal      = "Indagationes Mathematicae",
    Volume       = "9",
    Pages        = "549-562",
    Comment      = "TPTPRef"
}

@Article{vPl95,
    Author       = "von Plato, J.",
    Year         = "1995",
    Title        = "{The Axioms of Constructive Geometry}",
    Journal      = "Annals of Pure and Applied Logic",
    Volume       = "76",
    Number       = "2",
    Pages        = "169-200",
    Comment      = "TPTPRef"
}

@InProceedings{vW02,
    Author       = "von Wright, J.",
    Year         = "2002",
    Title        = "{From Kleene Algebra to Refinement Algebra}",
    Editor       = "Boiten, E. and M{\"o}ller, B.",
    BookTitle    = "{Proceedings of the 6th International Conference on the
                    Mathematics of Program Construction}",
    Place        = "Dagstuhl, Germany",
    Series       = "Lecture Notes in Computer Science",
    Number       = "2386",
    Pages        = "233-262",
    Comment      = "TPTPRef"
}

@Article{Wal93-JFM,
    Author       = "Walijewski, J.",
    Year         = "1993",
    Title        = "{Representation Theorem for Boolean Algebras}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "4",
    Number       = "1",
    Pages        = "45-50",
    Comment      = "TPTPRef,LOPCLSET"
}

@TechReport{Wal94,
    Author       = "Walsh, T.",
    Year         = "1994",
    Title        = "{The Binomial Theorem}",
    Number       = "Blue Book Note 903",
    Institution  = "University of Edinburgh, Mathematical Reasoning Group",
    Address      = "Edinburgh, United Kingdom",
    Comment      = "TPTPRef"
}

@TechReport{Wal93,
    Author       = "Walsh, T.",
    Year         = "1993",
    Title        = "{The Arithmetic/Geometric Mean Theorem}",
    Number       = "Blue Book Note 828",
    Institution  = "University of Edinburgh, Mathematical Reasoning Group",
    Address      = "Edinburgh, United Kingdom",
    Comment      = "TPTPRef"
}

@InCollection{Wal94,
    Author       = "Walther, C.",
    Year         = "1994",
    Title        = "{Mathematical Induction}",
    Editor       = "Gabbay, D. and Hogger, C. and Robinson, J.",
    BookTitle    = "{Handbook of Logic in Artificial Intelligence and Logic
                    Programming}",
    Volume       = "2",
    Pages        = "127-228",
    Publisher    = "Oxford University Press",
    Comment      = "TPTPRef"
}

@InProceedings{Wal83,
    Author       = "Walther, C.",
    Year         = "1983",
    Title        = "{A Many-Sorted Calculus Based on Resolution and
                    Paramodulation}",
    Editor       = "Bundy A.",
    BookTitle    = "{Proceedings of the 8th International Joint Conference on
                    Artificial Intelligence}",
    Place        = "Karlsruhe, Germany",
    Pages        = "882-891",
    Comment      = "TPTPRef"
}

@InProceedings{Wan65,
    Author       = "Wang, H.",
    Year         = "1965",
    Title        = "{Formalization and Automatic Theorem-Proving}",
    Editor       = "Kalenich W.A.",
    BookTitle    = "{Proceedings of the IFIP Congress}",
    Place        = "NEED",
    Pages        = "51-58",
    Publisher    = "Spartan Books",
    Comment      = "TPTPRef"
}

@InProceedings{Wan85,
    Author       = "Wang, T-C.",
    Year         = "1985",
    Title        = "{Designing Examples for Semantically Guided Hierarchical
                    Deduction}",
    Editor       = "Joshi A.",
    BookTitle    = "{Proceedings of the 9th International Joint Conference on
                    Artificial Intelligence}",
    Place        = "Los Angeles, USA",
    Pages        = "1201-1207",
    Comment      = "TPTPRef, semantics"
}

@Article{WB87,
    Author       = "Wang, T-C. and Bledsoe, W.W.",
    Year         = "1987",
    Title        = "{Hierarchical Deduction}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "3",
    Number       = "1",
    Pages        = "35-77",
    Comment      = "TPTPRef, general reasoning/semantics"
}

@Book{Wei94,
    Author       = "Weibel, C.",
    Year         = "1994",
    Title        = "{An Introduction to Homological Algebra}",
    Publisher    = "Cambridge University Press",
    Comment      = "TPTPRef"
}

@InCollection{Wei01,
    Author       = "Weidenbach, C.",
    Year         = "2001",
    Title        = "{Combining Superposition, Sorts and Splitting}",
    Editor       = "Robinson, A. and Voronkov, A.",
    BookTitle    = "{Handbook of Automated Reasoning}",
    Pages        = "1965-2011",
    Publisher    = "Elsevier Science",
    Comment      = "TPTPCite,TPTPRefForResults"
}

@InProceedings{Wei93,
    Author       = "Weidenbach, C.",
    Year         = "1993",
    Title        = "{Extending the Resolution Method with Sorts}",
    Editor       = "Bajcsy, R.",
    BookTitle    = "{Proceedings of the 13th International Joint Conference on
                    Artificial Intelligence}",
    Place        = "Chambery, France",
    Pages        = "60-65",
    Publisher    = "Morgan Kaufmann",
    Comment      = "TPTPRef"
}

@InProceedings{WGR96,
    Author       = "Weidenbach, C. and Gaede, B. and Rock, G.",
    Year         = "1996",
    Title        = "{SPASS and FLOTTER}",
    Editor       = "McRobbie, M. and Slaney, J.K.",
    BookTitle    = "{Proceedings of the 13th International Conference on
                    Automated Deduction}",
    Place        = "New Brunswick, USA",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "1104",
    Pages        = "141-145",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Book{WR27,
    Author       = "Whitehead, A.N. and Russell, B.",
    Year         = "1927",
    Title        = "{Principia Mathematica}",
    Edition      = "2",
    Volume       = "1",
    Publisher    = "Cambridge United Press",
    Comment      = "TPTPRef"
}

@Book{Whi61,
    Author       = "Whitesitt, J.E.",
    Year         = "1961",
    Title        = "{Boolean Algebra and Its Applications}",
    Publisher    = "Addison-Wesley",
    Comment      = "TPTPRef, Chapter 2"
}

@Article{WM89,
    Author       = "Wick, C. and McCune, W.W.",
    Year         = "1989",
    Title        = "{Automated Reasoning about Elementary Point-Set Topology}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "5",
    Pages        = "239 - 255",
    Comment      = "TPTPRef"
}

@Book{WS+06,
    Author       = "Willis, N. and Sloane, P. and MacHale, D. and Dispezio, M.
                    and Smith, K. and Gardner, M. and Sole, T. and Marshall,
                    R.",
    Year         = "2006",
    Title        = "{The World's Biggest Book of Brainteasers & Logic
                    Puzzles}",
    Editor       = "Kimble, B.",
    Publisher    = "Sterling Publishing",
    Comment      = "TPTPRef"
}

@TechReport{WL89,
    Author       = "Wilson, D.S. and Loveland, D.W.",
    Year         = "1989",
    Title        = "{Incorporating Relevancy Testing in SATCHMO}",
    Number       = "CS-1989-24",
    Institution  = "Department of Computer Science, Duke University",
    Address      = "Durham, USA",
    Comment      = "TPTPRef, general reasoning"
}

@Article{WM76,
    Author       = "Wilson, G.A. and Minker, J.",
    Year         = "1976",
    Title        = "{Resolution, Refinements, and Search Strategies: A
                    Comparative Study}",
    Journal      = "IEEE Transactions on Computers",
    Volume       = "C-25",
    Number       = "8",
    Pages        = "782-801",
    Comment      = "TPTPRef"
}

@Article{Win90,
    Author       = "Winker, S.",
    Year         = "1990",
    Title        = "{Robbins Algebra: Conditions that make a Near-Boolean
                    Algebra Boolean}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "6",
    Number       = "4",
    Pages        = "465-489",
    Comment      = "TPTPRef"
}

@Article{Win82,
    Author       = "Winker, S.",
    Year         = "1982",
    Title        = "{Generation and Verification of Finite Models and
                    Counterexamples Using an Automated Theorem Prover
                    Answering Two Open Questions}",
    Journal      = "Journal of the ACM",
    Volume       = "29",
    Number       = "2",
    Pages        = "273-284",
    Comment      = "TPTPRef, semantics"
}

@Article{Woj97-JFM,
    Author       = "Wojciechowski, M.",
    Year         = "1997",
    Title        = "{Yoneda Embedding}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "6",
    Number       = "3",
    Pages        = "377-379",
    Comment      = "TPTPRef,YONEDA_1"
}

@Article{WW83,
    Author       = "Wojciechowski, W.S. and Wojcik, A.S.",
    Year         = "1983",
    Title        = "{Automated Design of Multi-valued Logic Circuits by
                    Automated Theorem Proving Techniques}",
    Journal      = "IEEE Transactions on Computers",
    Volume       = "C-32",
    Number       = "8",
    Pages        = "785-798",
    Comment      = "TPTPRef"
}

@InProceedings{Woj83,
    Author       = "Wojcik, A.S.",
    Year         = "1983",
    Title        = "{Formal Design Verification of Digital Systems}",
    BookTitle    = "{Proceedings of the 20th Design Automation Conference}",
    Comment      = "TPTPRef"
}

@Book{Wol02,
    Author       = "Wolfram, S.",
    Year         = "2002",
    Title        = "{A New Kind of Science}",
    Publisher    = "Wolfram Media",
    Comment      = "TPTPRef"
}

@Article{Wor90-JFM-RDS,
    Author       = "Woronowicz, E.",
    Year         = "1990",
    Title        = "{Relations Defined on Sets}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "1",
    Number       = "1",
    Pages        = "181-186",
    Comment      = "TPTPRef"
}

@Article{Wos10,
    Author       = "Wos, L.",
    Year         = "2010",
    Title        = "{Deriving a Complex Formula from Simple Axioms}",
    Journal      = "AAR Newsletter",
    Volume       = "088-2010-06",
    Comment      = "TPTPRef"
}

@Article{Wos98,
    Author       = "Wos, L.",
    Year         = "1998",
    Title        = "{Automating the Search for Elegant Proofs}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "21",
    Number       = "2",
    Pages        = "135-175",
    Comment      = "TPTPRef"
}

@Book{Wos96,
    Author       = "Wos, L.",
    Year         = "1996",
    Title        = "{The Automation of Reasoning: An Experimenter's Notebook
                    with OTTER Tutorial}",
    Publisher    = "Academic Press",
    Comment      = "TPTPRef, general reasoning"
}

@Article{Wos96-JAR-17-1,
    Author       = "Wos, L.",
    Year         = "1996",
    Title        = "{The Power of Combining Resonance with Heat}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "17",
    Number       = "1",
    Pages        = "23-81",
    Comment      = "TPTPRef"
}

@Article{Wos96-JAR-17-2,
    Author       = "Wos, L.",
    Year         = "1996",
    Title        = "{OTTER and the Moufang Identity Problem}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "17",
    Number       = "2",
    Pages        = "215-257",
    Comment      = "TPTPRef"
}

@Article{Wos95,
    Author       = "Wos, L.",
    Year         = "1995",
    Title        = "{Searching for Circles of Pure Proofs}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "15",
    Number       = "3",
    Pages        = "279-315",
    Comment      = "TPTPRef"
}

@Article{Wos94-AAR-26,
    Author       = "Wos, L.",
    Year         = "1994",
    Title        = "{Challenge in Group Theory}",
    Journal      = "AAR Newsletter",
    Volume       = "26",
    Pages        = "3-5",
    Comment      = "TPTPRef"
}

@Article{Wos94-AAR-27,
    Author       = "Wos, L.",
    Year         = "1994",
    Title        = "{Two Challenge Problems}",
    Journal      = "AAR Newsletter",
    Volume       = "27",
    Pages        = "9",
    Comment      = "TPTPRef"
}

@Article{Wos93,
    Author       = "Wos, L.",
    Year         = "1993",
    Title        = "{The Kernel Strategy and Its Use for the Study of
                    Combinatory Logic}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "10",
    Number       = "3",
    Pages        = "287-344",
    Comment      = "TPTPRef, general reasoning"
}

@Article{Wos92-AAR,
    Author       = "Wos, L.",
    Year         = "1992",
    Title        = "{An Opportunity to Test Your Skills, and the Power of Your
                    Automated Reasoning Program}",
    Journal      = "AAR Newsletter",
    Volume       = "21",
    Pages        = "10-11",
    Comment      = "TPTPRef"
}

@Article{Wos89,
    Author       = "Wos, L.",
    Year         = "1989",
    Title        = "{A Challenge Problem and a Recent Workshop}",
    Journal      = "AAR Newsletter",
    Volume       = "13",
    Pages        = "2-8",
    Comment      = "TPTPRef"
}

@Book{Wos88,
    Author       = "Wos, L.",
    Year         = "1988",
    Title        = "{Automated Reasoning - 33 Basic Research Problems}",
    Publisher    = "Prentice-Hall",
    Comment      = "TPTPRef, general reasoning"
}

@TechReport{Wos65,
    Author       = "Wos, L.",
    Year         = "1965",
    Title        = "{Unpublished Note}",
    Number       = "NEED",
    Institution  = "Argonne National Laboratory",
    Address      = "Argonne, USA",
    Comment      = "TPTPRef"
}

@InProceedings{WM88-CADE-9,
    Author       = "Wos, L. and McCune, W.W.",
    Year         = "1988",
    Title        = "{Challenge Problems Focusing on Equality and Combinatory
                    Logic: Evaluating Automated Theorem-Proving Programs}",
    Editor       = "Lusk, E. and Overbeek, R.",
    BookTitle    = "{Proceedings of the 9th International Conference on
                    Automated Deduction}",
    Place        = "Argonne, USA",
    Series       = "Lecture Notes in Computer Science",
    Number       = "310",
    Pages        = "714-729",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@TechReport{WM88-TR,
    Author       = "Wos, L. and McCune, W.W.",
    Year         = "1988",
    Title        = "{Searching for a Fixed Point Combinators by Using Automated
                    Theorem Proving: A Preliminary Report}",
    Number       = "ANL-88-10",
    Institution  = "Argonne National Laboratory",
    Address      = "Argonne, USA",
    Comment      = "TPTPRef"
}

@Book{WO+92,
    Author       = "Wos, L. and Overbeek, R. and Lusk E.L. and Boyle, J.",
    Year         = "1992",
    Title        = "{Automated Reasoning: Introduction and Applications}",
    Edition      = "2nd",
    Publisher    = "McGraw-Hill",
    Comment      = "TPTPRef"
}

@Book{WO+84,
    Author       = "Wos, L. and Overbeek, R. and Lusk E.L. and Boyle, J.",
    Year         = "1984",
    Title        = "{Automated Reasoning: Introduction and Applications}",
    Publisher    = "Prentice-Hall",
    Comment      = "TPTPRef, general reasoning"
}

@Article{WUF02,
    Author       = "Wos, L. and Ulrich, D. and Fitelson, B.",
    Year         = "2002",
    Title        = "{Vanquishing the XCB Question: The Methodological Discovery
                    of the last Shortest Single Axiom for the Equivalential
                    Calculus}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "29",
    Number       = "2",
    Pages        = "107-124",
    Comment      = "TPTPRef"
}

@InProceedings{WW+90,
    Author       = "Wos, L. and Winker, S. and McCune, W.W. and Overbeek, R.
                    and Lusk E.L. and Stevens, R.",
    Year         = "1990",
    Title        = "{Automated Reasoning Contributes to Mathemetics and
                    Logic}",
    Editor       = "Stickel, M.E.",
    BookTitle    = "{Proceedings of the 10th International Conference on
                    Automated Deduction}",
    Place        = "Kaiserslautern, Germany",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "449",
    Pages        = "485-499",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Article{WW+83,
    Author       = "Wos, L. and Winker, S. and Veroff, R. and Smith, B. and
                    Henschen, L.",
    Year         = "1983",
    Title        = "{Questions Concerning Possible Shortest Single Axioms in
                    Equivalential Calculus: An Application of Automated
                    Theorem Proving to infinite Domains}",
    Journal      = "Notre Dame Journal of Formnal Logic",
    Volume       = "24",
    Number       = "2",
    Pages        = "205-223",
    Comment      = "TPTPRef"
}

@Article{MOW76,
    Author       = "Wos, L.A. and Overbeek, R.A. and McCharen, J.D.",
    Year         = "1976",
    Title        = "{Problems and Experiments for and with Automated
                    Theorem-Proving Programs}",
    Journal      = "IEEE Transactions on Computers",
    Volume       = "C-25",
    Number       = "8",
    Pages        = "773-782",
    Comment      = "TPTPRef"
}

@Article{WL01,
    Author       = "Wu, C.H. and Lee, S.J.",
    Year         = "2001",
    Title        = "{Parallelization of a Hyper-Linking-Based Theorem Prover}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "26",
    Number       = "1",
    Pages        = "67-106",
    Comment      = "TPTPRef"
}

@Article{WD90,
    Author       = "Wysocki, M. and Darmochwa{\l}, A.",
    Year         = "1990",
    Title        = "{Subsets of Topological Spaces}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "1",
    Number       = "1",
    Pages        = "231-237",
    Comment      = "TPTPRef"
}

@Book{Zem73,
    Author       = "Zeman, J.",
    Year         = "1973",
    Title        = "{Modal Logic, the Lewis-Modal Systems}",
    Publisher    = "Oxford University Press",
    Comment      = "TPTPRef"
}

@Article{Zha93,
    Author       = "Zhang, H.",
    Year         = "1993",
    Title        = "{Automated Proofs of Equality Problems in Overbeek's
                    Competition}",
    Journal      = "Journal of Automated Reasoning",
    Volume       = "11",
    Number       = "3",
    Pages        = "333-351",
    Comment      = "TPTPRef"
}

@InProceedings{ZH92,
    Author       = "Zhang, H. and Hua, X.",
    Year         = "1992",
    Title        = "{Proving the Chinese Remainder Theorem by the Cover Set
                    Induction}",
    Editor       = "Kapur D.",
    BookTitle    = "{Proceedings of the 11th International Conference on
                    Automated Deduction}",
    Place        = "Saratoga Springs, USA",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "607",
    Pages        = "431-445",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@InProceedings{ZKK88,
    Author       = "Zhang, H. and Kapur, D. and Krishnamoorthy,M.",
    Year         = "1988",
    Title        = "{A Mechanizable Induction Principle for Equational
                    Specifications}",
    Editor       = "Lusk, E. and Overbeek, R.",
    BookTitle    = "{Proceedings of the 9th International Conference on
                    Automated Deduction}",
    Place        = "Argonne, USA",
    Series       = "Lecture Notes in Computer Science",
    Number       = "310",
    Pages        = "152-181",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@InProceedings{Zha05,
    Author       = "Zhang, J.",
    Year         = "2005",
    Title        = "{Computer Search for Counterexamples to Wilkie's
                    Identity}",
    Editor       = "Nieuwenhuis, R.",
    BookTitle    = "{Proceedings of the 20th International Conference on
                    Automated Deduction}",
    Place        = "Tallinn, Estonia",
    Series       = "Lecture Notes in Artificial Intelligence",
    Number       = "3632",
    Pages        = "441-451",
    Publisher    = "Springer-Verlag",
    Comment      = "TPTPRef"
}

@Article{Zha00,
    Author       = "Zhang, J.",
    Year         = "2000",
    Title        = "{Test Problem and Perl Scripts for Finite Model
                    Searching}",
    Journal      = "Association for Automated Reasoning Newsletter",
    Number       = "47",
    Comment      = "TPTPRef"
}

@Article{Zha98,
    Author       = "Zhang, J.",
    Year         = "1998",
    Title        = "{Showing the Independence of An Axiom for Temporal
                    Intervals by Model Generation}",
    Journal      = "AAR Newsletter",
    Volume       = "40",
    Comment      = "TPTPRef"
}

@Article{Zha94,
    Author       = "Zhang, J.",
    Year         = "1994",
    Title        = "{Solution to Another Open Question in Combinatory Logic}",
    Journal      = "AAR Newsletter",
    Volume       = "25",
    Pages        = "8-10",
    Comment      = "TPTPRef"
}

@Article{Zha92,
    Author       = "Zhang, J.",
    Year         = "1992",
    Title        = "{Solution to an Open Question in Combinatory Logic}",
    Journal      = "AAR Newsletter",
    Volume       = "21",
    Pages        = "12",
    Comment      = "TPTPRef"
}

@MastersThesis{Zha08,
    Author       = "Zhang, X.",
    Year         = "2008",
    Title        = "{Using LEO-II to Prove Properties of an Explicit
                    Substitution M-set Model}",
    School       = "Saarland University",
    Address      = "Saarbruecken, Germany",
    Comment      = "TPTPRef"
}

@InProceedings{ZS05,
    Author       = "Zhang, Y. and Sutcliffe, G.",
    Year         = "2005",
    Title        = "{Lemma Management Techniques for Automated Theorem
                    Proving}",
    Editor       = "Konev, B. and Schulz, S.",
    BookTitle    = "{Proceedings of the 5th International Workshop on the
                    Implementation of Logics}",
    Place        = "Montevideo, Uruguay",
    Pages        = "87-94",
    Comment      = "TPTPRef"
}

@Article{Zuk90,
    Author       = "Zukowski, S.",
    Year         = "1990",
    Title        = "{Introduction to Lattice Theory}",
    Journal      = "Journal of Formalized Mathematics",
    Volume       = "1",
    Number       = "1",
    Pages        = "215-222",
    Comment      = "TPTPRef"
}

@Book{Luk63,
    Author       = "{\L}ukasiewicz, J.",
    Year         = "1963",
    Title        = "{Elements of Mathematical Logic}",
    Publisher    = "Pergamon Press",
    Comment      = "TPTPRef, English translation of the second Edition (1958)
                    of Elementy logiki matematycznej, PWN, Warsaw."
}

@InProceedings{Luk48,
    Author       = "{\L}ukasiewicz, J.",
    Year         = "1948",
    Title        = "{The Shortest Axiom of the Implicational Calculus of
                    Propositions}",
    BookTitle    = "{Proceedings of the Royal Irish Academy 52(3)}",
    Pages        = "25-33",
    Comment      = "TPTPRef"
}