1.1 --- a/src/HOL/Tools/ATP_Manager/scripts/remote_atp	Wed Jul 28 18:32:54 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/scripts/remote_atp	Wed Jul 28 18:35:15 2010 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4  
     1.5  #----Get format and transform options if specified
     1.6  my %Options;
     1.7 -getopts("hwxs:t:c:",\%Options);
     1.8 +getopts("hws:t:c:",\%Options);
     1.9  
    1.10  #----Usage
    1.11  sub usage() {
    1.12 @@ -32,7 +32,6 @@
    1.13    print("    <options> are ...\n");
    1.14    print("    -h            - print this help\n");
    1.15    print("    -w            - list available ATP systems\n");
    1.16 -  print("    -x            - use X2TPTP to convert output of prover\n");
    1.17    print("    -s<system>    - specified system to use\n");
    1.18    print("    -t<timelimit> - CPU time limit for system\n");
    1.19    print("    -c<command>   - custom command for system\n");
    1.20 @@ -104,39 +103,7 @@
    1.21  } elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
    1.22    print "Specified System $1 does not exist\n";
    1.23    exit(-1);
    1.24 -} elsif (exists($Options{'x'}) &&
    1.25 -  $Response->content =~
    1.26 -    /%\s*Result\s*:\s*(Unsatisfiable|Theorem).*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/ &&
    1.27 -  $Response->content !~ /ERROR: Could not form TPTP format derivation/ )
    1.28 -{
    1.29 -  # converted output: extract proof
    1.30 -  my @lines = split( /\n/, $Response->content);
    1.31 -  my $extract = "";
    1.32 -  foreach my $line (@lines){
    1.33 -      #ignore comments
    1.34 -      if ($line !~ /^%/ && !($line eq "")) {
    1.35 -          $extract .= "$line";
    1.36 -      }
    1.37 -  }
    1.38 -  # insert newlines after ').'
    1.39 -  $extract =~ s/\s//g;
    1.40 -  $extract =~ s/\)\.cnf/\)\.\ncnf/g;
    1.41 -
    1.42 -  print "========== ~~/lib/scripts/SystemOnTPTP extracted proof: ==========\n";
    1.43 -  # orientation for "sledgehammer_proof_reconstruct.ML"
    1.44 -  print "# SZS output start CNFRefutation.\n";
    1.45 -  print "$extract\n";
    1.46 -  print "# SZS output end CNFRefutation.\n";
    1.47 -  # can be useful for debugging; Isabelle ignores this
    1.48 -  print "============== original response from SystemOnTPTP: ==============\n";
    1.49 +} else {
    1.50    print $Response->content;
    1.51    exit(0);
    1.52 -} elsif (!exists($Options{'x'})) {
    1.53 -  # pass output directly to Isabelle
    1.54 -  print $Response->content;
    1.55 -  exit(0);
    1.56 -}else {
    1.57 -  print "Remote script could not extract proof:\n".$Response->content;
    1.58 -  exit(-1);
    1.59  }
    1.60 -