contrib/SystemOnTPTP/remote

--- a/contrib/SystemOnTPTP/remote	Sun Jan 11 21:50:05 2009 +0100
+++ b/contrib/SystemOnTPTP/remote	Mon Jan 12 16:16:05 2009 +0100
@@ -3,14 +3,18 @@
 # Wrapper for custom remote provers on SystemOnTPTP
 # Author: Fabian Immler, TU Muenchen
 #
-# Similar to the vampire wrapper, but compatible provers can be passed in the
-# command line, with %s for the problemfile e.g. 
+# Usage: ./remote prover timelimit problemfile
+# 
+# where prover should be the name of the System from http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP
+# tested and working with the standard settings: 
 #
-# ./remote Vampire---9.0 jumpirefix --output_syntax tptp --mode casc -t 3600 %s
-# ./remote Vampire---10.0 drakosha.pl 60 %s
-# ./remote SPASS---3.01 SPASS -Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof %s
-# ./remote Metis---2.1 metis --show proof --show saturation %s
-# ./remote SNARK---20080805r005 run-snark %s
+# ./remote Vampire---9.0 timelimit file
+# ./remote SPASS---3.01 timelimit file
+# ./remote Metis---2.1 timelimit file
+# ./remote SNARK---20080805r005 timelimit file
+# ./remote Otter---3.3 timelimit file
+# ./remote SOS---2.0 timelimit file
+# ./remote EP---1.0 timelimit file
 
 use warnings;
 use strict;
@@ -22,19 +26,12 @@
 # address of proof-server
 my $SystemOnTPTPFormReplyURL = "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply";
 
-if(scalar(@ARGV) < 2) {
-    print "prover and command missing";
+if(scalar(@ARGV) != 3) {
+    print "usage: ";
     exit -1;
 }
 my $prover = shift(@ARGV);
-my $command = shift(@ARGV);
-
-# pass arguments
-my $options = "";
-while(scalar(@ARGV)>1){
-	$options.=" ".shift(@ARGV);
-}
-# last argument is problemfile to be uploaded
+my $timelimit = shift(@ARGV);
 my $problem = [shift(@ARGV)];
 
 # fill in form
@@ -46,8 +43,7 @@
     "ProblemSource" => "UPLOAD",
     "UPLOADProblem" => $problem,
     "System___$prover" => "$prover",
-    "Format___$prover" => "tptp",
-    "Command___$prover" => "$command $options %s"
+    "TimeLimit___$prover" => "$timelimit",
 );
 
 # Query Server
@@ -89,6 +85,7 @@
     print "# SZS output end CNFRefutation.\n";
 } else {
 	print "HTTP-Request: " . $Response->message;
+	print "\nResponse: " . $Response->content;
 	print "\nCANNOT PROVE: \n";
   print $Response->content;
 }