Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 28 Feb 1995 06:31:29 +0000
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA076912161;
          Mon, 27 Feb 1995 23:16:01 -0700
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with ESMTP (1.37.109.15/16.2) id AA076882159;
          Mon, 27 Feb 1995 23:15:59 -0700
Received: from APL.FOX.CS.CMU.EDU (APL.FOX.CS.CMU.EDU [128.2.198.58]) 
          by dworshak.cs.uidaho.edu (8.6.9/1.0) with SMTP id WAA19598 
          for <info-hol@cs.uidaho.edu>; Mon, 27 Feb 1995 22:14:54 -0800
From: terra@APL.FOX.CS.CMU.EDU
Message-Id: <199502280614.WAA19598@dworshak.cs.uidaho.edu>
To: info-hol@cs.uidaho.edu
Subject: Need real-world Hol-90 proofs running for 5-60 minutes
Date: Tue, 28 Feb 95 1:14:05 EST
Source-Info: Sender is really terra@APL.FOX.CS.CMU.EDU


Hi!

For benchmark purposes I need real-world[tm] examples of Hol-90
(release 7, if possible) that run for some time.  I was
thinking of something like 5-60 minutes.

I know I could take one of the libraries (e.g., the integer
library), but I'm not sure that would be representative.

TIA,

Morten Welinder