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