# HG changeset patch
# User blanchet
# Date 1587649542 -7200
# Node ID e771b8157fc74c15dd1fda4b87a25d47acde9019
# Parent  936718dede803bc363654b654da742a125ba147f
tweaked Vampire's options + tuning

diff -r 936718dede80 -r e771b8157fc7 src/HOL/ATP.thy
--- a/src/HOL/ATP.thy	Thu Apr 23 13:49:46 2020 +0200
+++ b/src/HOL/ATP.thy	Thu Apr 23 15:45:42 2020 +0200
@@ -137,6 +137,5 @@
 ML_file \<open>Tools/monomorph.ML\<close>
 ML_file \<open>Tools/ATP/atp_problem_generate.ML\<close>
 ML_file \<open>Tools/ATP/atp_proof_reconstruct.ML\<close>
-ML_file \<open>Tools/ATP/atp_systems.ML\<close>
 
 end
diff -r 936718dede80 -r e771b8157fc7 src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Thu Apr 23 13:49:46 2020 +0200
+++ b/src/HOL/Sledgehammer.thy	Thu Apr 23 15:45:42 2020 +0200
@@ -16,6 +16,7 @@
 lemma size_ne_size_imp_ne: "size x \<noteq> size y \<Longrightarrow> x \<noteq> y"
   by (erule contrapos_nn) (rule arg_cong)
 
+ML_file \<open>Tools/ATP/atp_systems.ML\<close>
 ML_file \<open>Tools/Sledgehammer/async_manager_legacy.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_util.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_fact.ML\<close>
diff -r 936718dede80 -r e771b8157fc7 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Apr 23 13:49:46 2020 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Apr 23 15:45:42 2020 +0200
@@ -453,7 +453,7 @@
       (InternalError, "Please report this error")] @
       known_perl_failures,
    prem_role = Conjecture,
-   best_slices = fn ctxt =>
+   best_slices = fn _ =>
      (* FUDGE *)
      [(0.1667, (((150, meshN), DFG Monomorphic, "mono_native", combsN, true), "")),
       (0.1667, (((500, meshN), DFG Monomorphic, "mono_native", liftingN, true), spass_H2SOS)),
@@ -499,7 +499,7 @@
 val vampire_basic_options = "--proof tptp --output_axiom_names on $VAMPIRE_EXTRA_OPTIONS"
 
 val vampire_full_proof_options =
-  " --forced_options equality_proxy=off:general_splitting=off:inequality_splitting=0:naming=0"
+  " --proof_extra free --forced_options avatar=off:equality_proxy=off:general_splitting=off:inequality_splitting=0:naming=0"
 
 val remote_vampire_command =
   "vampire " ^ vampire_basic_options ^ " " ^ vampire_full_proof_options ^ " -t %d %s"