use Vampire's clausifier with iProver, now that E's is no longer supported

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Mon Jul 19 10:37:48 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Mon Jul 19 10:38:14 2021 +0200
@@ -319,8 +319,8 @@
 val iprover_config : atp_config =
   {exec = (["IPROVER_HOME"], ["iproveropt", "iprover"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ =>
-     ["--clausifier \"$E_HOME\"/eprover " ^
-      "--clausifier_options \"--tstp-format --silent --cnf\" " ^
+     ["--clausifier \"$VAMPIRE_HOME\"/vampire " ^
+      "--clausifier_options \"--mode clausify\" " ^
       "--time_out_real " ^ string_of_real (Time.toReal timeout) ^ " " ^ File.bash_path problem],
    proof_delims = tstp_proof_delims,
    known_failures =