1.1 --- a/contrib/SystemOnTPTP/vampire	Wed Jan 21 15:22:51 2009 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,60 +0,0 @@
     1.4 -#!/usr/bin/env perl
     1.5 -#
     1.6 -# Vampire Wrapper for SystemOnTPTP
     1.7 -# Author: Fabian Immler, TU Muenchen
     1.8 -#
     1.9 -# - querys a Vampire theorem prover on SystemOnTPTP
    1.10 -#   (http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP)
    1.11 -# - behaves like a local Vampire
    1.12 -# => can be used for Isabelle when Vampire is not available (e.g. on a Mac)
    1.13 -#
    1.14 -
    1.15 -use warnings;
    1.16 -use strict;
    1.17 -
    1.18 -use Getopt::Std;
    1.19 -use HTTP::Request::Common;
    1.20 -use LWP::UserAgent;
    1.21 -
    1.22 -# address of proof-server
    1.23 -my $SystemOnTPTPFormReplyURL = "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
    1.24 -
    1.25 -#name of prover and its executable on the server, e.g.
    1.26 -# Vampire---9.0
    1.27 -# jumpirefix
    1.28 -my $prover = "Vampire---9.0";
    1.29 -my $command = "jumpirefix";
    1.30 -
    1.31 -# pass arguments
    1.32 -my $options = "";
    1.33 -while(scalar(@ARGV)>1){
    1.34 -	$options.=" ".shift(@ARGV);
    1.35 -}
    1.36 -# last argument is problemfile to be uploaded
    1.37 -my $problem = [shift(@ARGV)];
    1.38 -
    1.39 -# fill in form
    1.40 -my %URLParameters = (
    1.41 -    "NoHTML" => 1,
    1.42 -    "QuietFlag" => "-q01",
    1.43 -    "SubmitButton" => "RunSelectedSystems",
    1.44 -    "ProblemSource" => "UPLOAD",
    1.45 -    "UPLOADProblem" => $problem,
    1.46 -    "System___$prover" => "$prover",
    1.47 -    "Format___$prover" => "tptp",
    1.48 -    "Command___$prover" => "$command $options %s"
    1.49 -);
    1.50 -
    1.51 -# Query Server
    1.52 -my $Agent = LWP::UserAgent->new;
    1.53 -my $Request = POST($SystemOnTPTPFormReplyURL,
    1.54 -	Content_Type => 'form-data',Content => \%URLParameters);
    1.55 -my $Response = $Agent->request($Request);
    1.56 -    
    1.57 -#catch errors, let isabelle/watcher know
    1.58 -if($Response->is_success){
    1.59 -	print $Response->content;
    1.60 -} else {
    1.61 -	print $Response->message;
    1.62 -	print "\nCANNOT PROVE\n";
    1.63 -}

     2.1 --- a/etc/settings	Wed Jan 21 15:22:51 2009 +0100
     2.2 +++ b/etc/settings	Wed Jan 21 15:26:02 2009 +0100
     2.3 @@ -242,7 +242,6 @@
     2.4    "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" \
     2.5    "$ISABELLE_HOME/../vampire/$ML_PLATFORM" \
     2.6    "/usr/local/Vampire" \
     2.7 -  "$ISABELLE_HOME/contrib/SystemOnTPTP" \
     2.8    "")
     2.9  SPASS_HOME=$(choosefrom \
    2.10    "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" \