diff -r 5ef633275b15 -r 96f9e6402403 lib/scripts/SystemOnTPTP
--- a/lib/scripts/SystemOnTPTP	Mon Aug 10 08:37:37 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,141 +0,0 @@
-#!/usr/bin/env perl
-#
-# Wrapper for custom remote provers on SystemOnTPTP
-# Author: Fabian Immler, TU Muenchen
-#
-
-use warnings;
-use strict;
-use Getopt::Std;
-use HTTP::Request::Common;
-use LWP;
-
-my $SystemOnTPTPFormReplyURL =
-  "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
-
-# default parameters
-my %URLParameters = (
-    "NoHTML" => 1,
-    "QuietFlag" => "-q01",
-    "SubmitButton" => "RunSelectedSystems",
-    "ProblemSource" => "UPLOAD",
-    );
-
-#----Get format and transform options if specified
-my %Options;
-getopts("hwxs:t:c:",\%Options);
-
-#----Usage
-sub usage() {
-  print("Usage: remote [<options>] <File name>\n");
-  print("    <options> are ...\n");
-  print("    -h            - print this help\n");
-  print("    -w            - list available ATP systems\n");
-  print("    -x            - use X2TPTP to convert output of prover\n");
-  print("    -s<system>    - specified system to use\n");
-  print("    -t<timelimit> - CPU time limit for system\n");
-  print("    -c<command>   - custom command for system\n");
-  print("    <File name>   - TPTP problem file\n");
-  exit(0);
-}
-if (exists($Options{'h'})) {
-  usage();
-}
-
-#----What systems flag
-if (exists($Options{'w'})) {
-    $URLParameters{"SubmitButton"} = "ListSystems";
-    delete($URLParameters{"ProblemSource"});
-}
-
-#----X2TPTP
-if (exists($Options{'x'})) {
-    $URLParameters{"X2TPTP"} = "-S";
-}
-
-#----Selected system
-my $System;
-if (exists($Options{'s'})) {
-    $System = $Options{'s'};
-} else {
-    # use Vampire as default
-    $System = "Vampire---9.0";
-}
-$URLParameters{"System___$System"} = $System;
-
-#----Time limit
-if (exists($Options{'t'})) {
-    $URLParameters{"TimeLimit___$System"} = $Options{'t'};
-}
-#----Custom command
-if (exists($Options{'c'})) {
-    $URLParameters{"Command___$System"} = $Options{'c'};
-}
-
-#----Get single file name
-if (exists($URLParameters{"ProblemSource"})) {
-    if (scalar(@ARGV) >= 1) {
-        $URLParameters{"UPLOADProblem"} = [shift(@ARGV)];
-    } else {
-      print("Missing problem file\n");
-      usage();
-      die;
-    }
-}
-
-# Query Server
-my $Agent = LWP::UserAgent->new;
-if (exists($Options{'t'})) {
-  # give server more time to respond
-  $Agent->timeout($Options{'t'} + 10);
-}
-my $Request = POST($SystemOnTPTPFormReplyURL,
-	Content_Type => 'form-data',Content => \%URLParameters);
-my $Response = $Agent->request($Request);
-
-#catch errors / failure
-if(!$Response->is_success) {
-  print "HTTP-Error: " . $Response->message . "\n";
-  exit(-1);
-} elsif (exists($Options{'w'})) {
-  print $Response->content;
-  exit (0);
-} elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
-  print "Specified System $1 does not exist\n";
-  exit(-1);
-} elsif (exists($Options{'x'}) &&
-  $Response->content =~
-    /%\s*Result\s*:\s*Unsatisfiable.*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/ &&
-  $Response->content !~ /ERROR: Could not form TPTP format derivation/ )
-{
-  # converted output: extract proof
-  my @lines = split( /\n/, $Response->content);
-  my $extract = "";
-  foreach my $line (@lines){
-      #ignore comments
-      if ($line !~ /^%/ && !($line eq "")) {
-          $extract .= "$line";
-      }
-  }
-  # insert newlines after ').'
-  $extract =~ s/\s//g;
-  $extract =~ s/\)\.cnf/\)\.\ncnf/g;
-
-  print "========== ~~/lib/scripts/SystemOnTPTP extracted proof: ==========\n";
-  # orientation for res_reconstruct.ML
-  print "# SZS output start CNFRefutation.\n";
-  print "$extract\n";
-  print "# SZS output end CNFRefutation.\n";
-  # can be useful for debugging; Isabelle ignores this
-  print "============== original response from SystemOnTPTP: ==============\n";
-  print $Response->content;
-  exit(0);
-} elsif (!exists($Options{'x'})) {
-  # pass output directly to Isabelle
-  print $Response->content;
-  exit(0);
-}else {
-  print "Remote-script could not extract proof:\n".$Response->content;
-  exit(-1);
-}
-