--- a/contrib/SystemOnTPTP/vampire Wed Jan 21 15:22:51 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-#!/usr/bin/env perl
-#
-# Vampire Wrapper for SystemOnTPTP
-# Author: Fabian Immler, TU Muenchen
-#
-# - querys a Vampire theorem prover on SystemOnTPTP
-# (http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP)
-# - behaves like a local Vampire
-# => can be used for Isabelle when Vampire is not available (e.g. on a Mac)
-#
-
-use warnings;
-use strict;
-
-use Getopt::Std;
-use HTTP::Request::Common;
-use LWP::UserAgent;
-
-# address of proof-server
-my $SystemOnTPTPFormReplyURL = "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
-
-#name of prover and its executable on the server, e.g.
-# Vampire---9.0
-# jumpirefix
-my $prover = "Vampire---9.0";
-my $command = "jumpirefix";
-
-# pass arguments
-my $options = "";
-while(scalar(@ARGV)>1){
- $options.=" ".shift(@ARGV);
-}
-# last argument is problemfile to be uploaded
-my $problem = [shift(@ARGV)];
-
-# fill in form
-my %URLParameters = (
- "NoHTML" => 1,
- "QuietFlag" => "-q01",
- "SubmitButton" => "RunSelectedSystems",
- "ProblemSource" => "UPLOAD",
- "UPLOADProblem" => $problem,
- "System___$prover" => "$prover",
- "Format___$prover" => "tptp",
- "Command___$prover" => "$command $options %s"
-);
-
-# Query Server
-my $Agent = LWP::UserAgent->new;
-my $Request = POST($SystemOnTPTPFormReplyURL,
- Content_Type => 'form-data',Content => \%URLParameters);
-my $Response = $Agent->request($Request);
-
-#catch errors, let isabelle/watcher know
-if($Response->is_success){
- print $Response->content;
-} else {
- print $Response->message;
- print "\nCANNOT PROVE\n";
-}
--- a/etc/settings Wed Jan 21 15:22:51 2009 +0100
+++ b/etc/settings Wed Jan 21 15:26:02 2009 +0100
@@ -242,7 +242,6 @@
"$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" \
"$ISABELLE_HOME/../vampire/$ML_PLATFORM" \
"/usr/local/Vampire" \
- "$ISABELLE_HOME/contrib/SystemOnTPTP" \
"")
SPASS_HOME=$(choosefrom \
"$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" \