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

