# HG changeset patch
# User blanchet
# Date 1660807751 -7200
# Node ID 77cbf472fcc9e2b0c3c977590b2e6c9bfdaa2e47
# Parent  5f7d22354a658c9eae34b651fec5a27ca2c7448a
reintroduced SPASS to the mix

diff -r 5f7d22354a65 -r 77cbf472fcc9 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Aug 17 18:20:10 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Aug 18 09:29:11 2022 +0200
@@ -301,11 +301,12 @@
 
 val default_slice_schedule =
   (* FUDGE (loosely inspired by Seventeen evaluation) *)
-  [cvc4N, zipperpositionN, vampireN, veritN, zipperpositionN, eN, cvc4N,
+  [cvc4N, zipperpositionN, vampireN, veritN, spassN, zipperpositionN, eN, cvc4N,
    zipperpositionN, cvc4N, zipperpositionN, vampireN, cvc4N, cvc4N, vampireN,
-   cvc4N, iproverN, zipperpositionN, vampireN, zipperpositionN, vampireN,
-   zipperpositionN, z3N, zipperpositionN, vampireN, iproverN, zipperpositionN,
-   vampireN, cvc4N, zipperpositionN, z3N, z3N, cvc4N, cvc4N, zipperpositionN]
+   cvc4N, iproverN, zipperpositionN, spassN, vampireN, zipperpositionN,
+   vampireN, zipperpositionN, z3N, zipperpositionN, vampireN, iproverN, spassN,
+   zipperpositionN, vampireN, cvc4N, zipperpositionN, z3N, z3N, cvc4N, cvc4N,
+   zipperpositionN]
 
 fun schedule_of_provers provers num_slices =
   let