# HG changeset patch
# User blanchet
# Date 1648805428 -7200
# Node ID 840256534f34b1cd03350249136bdfed7e74154a
# Parent  c2532adbfa3eb87a5a7c992989118c5e3d0e8ced
tuned slices to get the fifth Zipperposition slice in a typical run

diff -r c2532adbfa3e -r 840256534f34 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Apr 01 09:58:05 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Apr 01 11:30:28 2022 +0200
@@ -300,7 +300,7 @@
   (* FUDGE (inspired by Seventeen evaluation) *)
   [cvc4N, zipperpositionN, vampireN, veritN, eN, cvc4N, zipperpositionN, cvc4N, vampireN, cvc4N,
    cvc4N, vampireN, cvc4N, iproverN, zipperpositionN, vampireN, vampireN, zipperpositionN, z3N,
-   cvc4N, vampireN, iproverN, vampireN, zipperpositionN, z3N, z3N, cvc4N, cvc4N]
+   zipperpositionN, vampireN, iproverN, vampireN, cvc4N, z3N, z3N, cvc4N, cvc4N]
 
 fun schedule_of_provers provers num_slices =
   let