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 <pieper@mcs.anl.gov>

+To: jcp@eskimo.com

+Cc: Larry Wos <wos@mcs.anl.gov>, Gail Pieper <pieper@mcs.anl.gov>

+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 <pieper@mcs.anl.gov>

+To: "John C. Peterson" <jcp@eskimo.com>

+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."

+