# HG changeset patch
# User blanchet
# Date 1335533077 -7200
# Node ID c17cc138064278c1dae37b7d9d34477874fb380b
# Parent  2e1636e45770a19c55719988a0c93f2621f5e380
smaller batches, to play safe

diff -r 2e1636e45770 -r c17cc1380642 src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Fri Apr 27 15:24:37 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML	Fri Apr 27 15:24:37 2012 +0200
@@ -71,7 +71,7 @@
        ("box", "false"),
        ("sat_solver", "smart"),
        ("max_threads", "1"),
-       ("batch_size", "10"),
+       ("batch_size", "5"),
        ("falsify", if null conjs then "false" else "true"),
        ("verbose", "true"),
        ("debug", if debug then "true" else "false"),