src/HOL/Tools/ATP/scripts/remote_atp

     "ForceSystem" => "-force",
     );
 
 #----Get format and transform options if specified
 my %Options;
-getopts("hws:t:c:",\%Options);
+getopts("hws:t:c:q:",\%Options);
 
 #----Usage
 sub usage() {
   print("Usage: remote_atp [<options>] <file_name>\n");
   print("Options:\n");
   print("    -h              print this help\n");
   print("    -w              list available ATPs\n");
   print("    -s<system>      ATP to use\n");
   print("    -t<time_limit>  CPU time limit for ATP\n");
   print("    -c<command>     custom ATP invocation command\n");
+  print("    -q<num>         quietness level (0 = most verbose, 3 = least verbose)\n");
   print("    <file_name>     TPTP problem file\n");
   exit(0);
 }
 if (exists($Options{'h'})) {
   usage();

     $URLParameters{"TimeLimit___$System"} = $Options{'t'};
 }
 #----Custom command
 if (exists($Options{'c'})) {
     $URLParameters{"Command___$System"} = $Options{'c'};
+}
+#----Quietness
+if (exists($Options{'q'})) {
+    $URLParameters{"QuietFlag"} = "-q" . $Options{'q'};
 }
 
 #----Get single file name
 if (exists($URLParameters{"ProblemSource"})) {
     if (scalar(@ARGV) >= 1) {