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; Thu, 2 Dec 1993 14:00:24 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA14282;
          Thu, 2 Dec 1993 06:50:37 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA14278;
          Thu, 2 Dec 1993 06:50:26 -0700
Received: from infix.cs.ruu.nl by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA09795; Thu, 2 Dec 93 05:47:36 -0800
Received: by relay.cs.ruu.nl id AA19926 (5.67a/IDA-1.5 
          for info-hol@ted.cs.uidaho.edu); Thu, 2 Dec 1993 14:47:33 +0100
From: Wishnu Prasetya <wishnu@cs.ruu.nl>
Message-Id: <199312021347.AA19926@relay.cs.ruu.nl>
Subject: can FAUST prove this?
To: info-hol@cs.uidaho.edu (hol mailing list)
Date: Thu, 2 Dec 1993 14:47:33 +0100 (MET)
X-Mailer: ELM [version 2.4 PL23]
Mime-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Content-Length: 226

Hi,

I have a question again about FAUST.

Can it solve the the following:

"(!s:*. q s ==> r s) /\ ~r s /\ (!s. ~r s /\ ~q s ==> p t \/ q t) 
  ==> 
  p t \/ r t"

Thanks in advance,

-Wishnu-

PS: Does FAUST run for HOL 88?