src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML

   if is_prover_supported ctxt name andalso is_prover_installed ctxt name then SOME name
   else remotify_prover_if_supported_and_not_already_remote ctxt name
 
 (* The first ATP of the list is used by Auto Sledgehammer. *)
 fun default_provers_param_value mode ctxt =
-  [cvc4N] @
-  (if is_vampire_noncommercial_license_accepted () = SOME false then [] else [vampireN]) @
-  [z3N, eN, spassN, veritN]
+  [cvc4N, vampireN, z3N, eN, spassN, veritN]
   |> map_filter (remotify_prover_if_not_installed ctxt)
   (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *)
   |> take (Multithreading.max_threads () - (if mode = Try then 1 else 0))
   |> implode_param