diff -uNr eqp-09e.orig/LICENSE eqp-09e/LICENSE --- eqp-09e.orig/LICENSE 1969-12-31 16:00:00.000000000 -0800 +++ eqp-09e/LICENSE 2017-03-19 18:35:59.791340069 -0700 @@ -0,0 +1,138 @@ +The EQP source distribution (a compressed tar file) did not include any +information that explicitly stated the terms of the software license. + +It was not possible to contact the author of EQP, William McCune, as he +sadly passed away in May 2011. The development of EQP was while he was +affiliated with the Argonne National Laboratory, so they were contacted +with the hope of providing clarification of the license terms. + +The emails received in response to a request for clarification are +included below. Also included is the text of the web pages that hosted +the EQP source distribution that the emails referred us to. The intended +license is presumed to be Public Domain. + + +Date: Thu, 25 Oct 2012 11:18:10 -0500 +Message-Id: <9223F4CF-6479-4988-8055-D06DAD2ADF43@mcs.anl.gov> +From: Gail Pieper +To: jcp@eskimo.com +Cc: Larry Wos , Gail Pieper +Subject: OTTER and EQP +X-Mailer: Apple Mail (2.1257) + +Dear John, +Larry asked me to look into the situation about OTTER and EQP. +Here is what our lawyers responded. +Gail Pieper + +The Otter software (by Bill Otter) was never reported to Legal for an +official meeting and is not in our reported software database. +I looked on the ANL website and found an ANL +website, http://www.mcs.anl.gov/research/projects/AR/otter/#copyright where +Otter is discussed. The webpage has a copyright notice, attached below, +indicating that Otter (at least this Version 3.3) is publically +available. Although it does say on this website that this version is +obsolete and maintained elsewhere. +I hope this helps you. + +Paul Betten, Ph.D. +Technology Development and Commercialization Division, Bldg 201 +Argonne National Laboratory +9700 S. Cass Avenue +Argonne, IL 60564 +Tel: (630) 252-4962 fax-5230 +e-mail: betten@anl.gov + ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ + +Otter and MACE Legal Page + +-------------------------------------------------------------------------------- +November 21, 2001. +-------------------------------------------------------------------------------- +This information refers to the Otter and MACE automated deduction +software, created at Argonne National Laboratory. + +Copyrights +The University of Chicago has declined to assert its copyrights in this +software. It may be used by the public without restriction and is +available here by download. + +License +This material resulted from work developed under a U.S. Government +contract and is subject to the following license: the Government is +granted for itself and the public a paid-up, nonexclusive, irrevocable +worldwide license in this material to reproduce, prepare derivative works, +distribute copies to the public, and perform publicly and display +publicly. + +Disclaimer +NEITHER THE UNITED STATES GOVERNMENT NOR ANY AGENCY THEREOF, NOR ANY OF +THEIR EMPLOYEES OR OFFICERS, MAKES ANY WARRANTY, EXPRESS OR IMPLIED, OR +ASSUMES ANY LEGAL LIABILITY OR RESPONSIBILITY FOR THE ACCURACY, +COMPLETENESS, OR USEFULNESS OF ANY INFORMATION, APPARATUS, PRODUCT, OR +PROCESS DISCLOSED, OR REPRESENTS THAT ITS USE WOULD NOT INFRINGE PRIVATELY +OWNED RIGHTS. + +Date: Mon, 29 Oct 2012 10:03:34 -0500 +Message-Id: <992AF342-1C2D-4E0F-BA6F-4CEF26AE39A5@mcs.anl.gov> +From: Gail Pieper +To: "John C. Peterson" +Subject: Re: OTTER and EQP +X-Mailer: Apple Mail (2.1257) + +John, +Have you looked at the websites +http://www.mcs.anl.gov/research/projects/AR/eqp/ and +http://www.cs.unm.edu/~mccune/eqp/ ? +If those are not enough, please let me know and I will contact +Paul Betten again. +Gail + +On Oct 29, 2012, at 2:01 AM, John C. Peterson wrote: +> On Thu, Oct 25, 2012 at 11:18:10AM -0500, Gail Pieper wrote: +>> Dear John, +>> Larry asked me to look into the situation about OTTER and EQP. +>> Here is what our lawyers responded. > Gail Pieper +> +> Hi Gail, +> +> Thanks so much for taking time out to look into these copyright, +> licensing issues for me. I'm volunteering my own time to try and get +> Bill McCune's software packaged so it can be distributed with Fedora +> Linux. +> +> I'm not certain, but I suspect the page you referred me to about +> OTTER may satisfy the Fedora Legal team regarding the issues they +> had. (I haven't heard back from them yet). +> +> I still have a question regarding Bill's EQP software. Should I contact +> Paul Betten (named below) or would it be better to work through you? +> +> Best Regards, John +> +>> Paul Betten, Ph.D. +>> Technology Development and Commercialization Division, Bldg 201 +>> Argonne National Laboratory +>> 9700 S. Cass Avenue +>> Argonne, IL 60564 +>> Tel: (630) 252-4962 fax-5230 +>> e-mail: betten@anl.gov +> +> -- +> John C. Peterson, KD6EKQ +> mailto:jcp@eskimo.com +> San Diego, CA U.S.A +> + +The quoted text below appears on both of the EQP web sites (as of 17 Dec, 2011): +http://www.mcs.anl.gov/research/projects/AR/eqp/ +http://www.cs.unm.edu/~mccune/eqp/ + +"EQP is not as stable and polished as our main production theorem prover +Otter. But it has obtained several interesting results, and we have +decided to make it available (including the source code) to everyone, +with no restrictions (and of course no warranty). EQP's documentation +is not good, but if you already know Otter, you might not have great +difficulty in learning to use EQP." +