diff -r 174568533593 -r 3b80d6082131 src/HOL/Tools/ATP_Manager/scripts/remote_atp
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP_Manager/scripts/remote_atp	Wed Jul 28 18:32:54 2010 +0200
@@ -0,0 +1,142 @@
+#!/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",
+    "ForceSystem" => "-force",
+    );
+
+#----Get format and transform options if specified
+my %Options;
+getopts("hwxs:t:c:",\%Options);
+
+#----Usage
+sub usage() {
+  print("Usage: remote_atp [<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|Theorem).*\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 "sledgehammer_proof_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);
+}
+