better handling of skolemization for Isar reconstruction in Sledgehammer for veriT

--- a/src/HOL/SMT.thy	Tue Oct 27 16:59:44 2020 +0000
+++ b/src/HOL/SMT.thy	Wed Oct 28 08:41:07 2020 +0100
@@ -250,7 +250,8 @@
   by auto
 
 lemma verit_and_pos:
-  \<open>(a \<Longrightarrow> \<not>b \<or> A) \<Longrightarrow> \<not>(a \<and> b) \<or> A\<close>
+  \<open>(a \<Longrightarrow> \<not>(b \<and> c) \<or> A) \<Longrightarrow> \<not>(a \<and> b \<and> c) \<or> A\<close>
+  \<open>(a \<Longrightarrow> b \<Longrightarrow> A) \<Longrightarrow> \<not>(a \<and> b) \<or> A\<close>
   \<open>(a \<Longrightarrow> A) \<Longrightarrow> \<not>a \<or> A\<close>
   \<open>(\<not>a \<Longrightarrow> A) \<Longrightarrow> a \<or> A\<close>
   by blast+
@@ -276,9 +277,10 @@
   by auto
 
 lemma verit_and_neg:
-  \<open>B \<or> B' \<Longrightarrow> (A \<and> B) \<or> \<not>A \<or> B'\<close>
-  \<open>B \<or> B' \<Longrightarrow> (\<not>A \<and> B) \<or> A \<or> B'\<close>
-  by auto
+  \<open>(a \<Longrightarrow> \<not>b \<or> A) \<Longrightarrow> \<not>(a \<and> b) \<or> A\<close>
+  \<open>(a \<Longrightarrow> A) \<Longrightarrow> \<not>a \<or> A\<close>
+  \<open>(\<not>a \<Longrightarrow> A) \<Longrightarrow> a \<or> A\<close>
+  by blast+
 
 lemma verit_forall_inst:
   \<open>A \<longleftrightarrow> B \<Longrightarrow> \<not>A \<or> B\<close>

--- a/src/HOL/SMT_Examples/SMT_Tests_Verit.thy	Tue Oct 27 16:59:44 2020 +0000
+++ b/src/HOL/SMT_Examples/SMT_Tests_Verit.thy	Wed Oct 28 08:41:07 2020 +0100
@@ -127,10 +127,13 @@
   "(\<exists>x. P x) \<or> R \<longleftrightarrow> (\<exists>x. P x \<or> R)"
   "\<exists>x. P x \<longrightarrow> P a \<and> P b"
   "(\<exists>x. Q \<longrightarrow> P x) \<longleftrightarrow> (Q \<longrightarrow> (\<exists>x. P x))"
-  supply[[smt_trace]]
   by smt+
 
 lemma
+  "(P False \<or> P True) \<or> \<not> P False"
+  by smt
+
+lemma
   "(\<not> (\<exists>x. P x)) \<longleftrightarrow> (\<forall>x. \<not> P x)"
   "(\<exists>x. P x \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P x) \<longrightarrow> Q"
   "(\<forall>x y. R x y = x) \<longrightarrow> (\<exists>y. R x y) = R x c"

--- a/src/HOL/Tools/SMT/smt_replay_arith.ML	Tue Oct 27 16:59:44 2020 +0000
+++ b/src/HOL/Tools/SMT/smt_replay_arith.ML	Wed Oct 28 08:41:07 2020 +0100
@@ -109,7 +109,7 @@
   |> Simplifier.full_simp_tac
 
 fun la_farkas args ctxt =
-  REPEAT' (resolve_tac ctxt @{thms verit_and_pos(2,3)})
+  REPEAT' (resolve_tac ctxt @{thms verit_and_pos(3,4)})
   THEN' TRY' (resolve_tac ctxt @{thms ccontr})
   THEN' TRY' (rewrite_only_thms ctxt @{thms linorder_class.not_less linorder_class.not_le not_not})
   THEN' (Subgoal.FOCUS (fn focus => la_farkas_tac focus args) ctxt)

--- a/src/HOL/Tools/SMT/verit_proof.ML	Tue Oct 27 16:59:44 2020 +0000
+++ b/src/HOL/Tools/SMT/verit_proof.ML	Wed Oct 28 08:41:07 2020 +0100
@@ -46,9 +46,15 @@
   val veriT_def : string
   val subproof_rule : string
   val local_input_rule : string
+  val not_not_rule : string
+  val contract_rule : string
+  val ite_intro_rule : string
+  val eq_congruent_rule : string
+  val eq_congruent_pred_rule : string
+  val skolemization_steps : string list
 
-  val is_skolemisation: string -> bool
-  val is_skolemisation_step: veriT_replay_node -> bool
+  val is_skolemization: string -> bool
+  val is_skolemization_step: veriT_replay_node -> bool
 
   val number_of_steps: veriT_replay_node list -> int
 
@@ -187,12 +193,10 @@
   rule: string,
   prems: string list,
   proof_ctxt: term list,
-  concl: term,
-  bounds: string list}
+  concl: term}
 
-fun mk_node id rule prems proof_ctxt concl bounds =
-  VeriT_Node {id = id, rule = rule, prems = prems, proof_ctxt = proof_ctxt, concl = concl,
-    bounds = bounds}
+fun mk_node id rule prems proof_ctxt concl =
+  VeriT_Node {id = id, rule = rule, prems = prems, proof_ctxt = proof_ctxt, concl = concl}
 
 datatype veriT_replay_node = VeriT_Replay_Node of {
   id: string,
@@ -226,18 +230,26 @@
 val step_prefix = ".c"
 val input_rule = "input"
 val la_generic_rule = "la_generic"
-val normalized_input_rule = "__normalized_input" (* arbitrary *)
-val rewrite_rule = "__rewrite" (* arbitrary *)
+val normalized_input_rule = "__normalized_input" (*arbitrary*)
+val rewrite_rule = "__rewrite" (*arbitrary*)
 val subproof_rule = "subproof"
-val local_input_rule = "__local_input" (* arbitrary *)
+val local_input_rule = "__local_input" (*arbitrary*)
 val simp_arith_rule = "simp_arith"
 val veriT_def = "__skolem_definition" (*arbitrary*)
+val not_not_rule = "not_not"
+val contract_rule = "contraction"
+val eq_congruent_pred_rule = "eq_congruent_pred"
+val eq_congruent_rule = "eq_congruent"
+val ite_intro_rule = "ite_intro"
+val default_skolem_rule = "sko_forall" (*arbitrary, but must be one of the skolems*)
 
-val is_skolemisation = member (op =) ["sko_forall", "sko_ex"]
-val keep_app_symbols = member (op =) ["eq_congruent_pred", "eq_congruent", "ite_intro"]
-val keep_raw_lifting = member (op =) ["eq_congruent_pred", "eq_congruent", "ite_intro"]
+val skolemization_steps = ["sko_forall", "sko_ex"]
+val is_skolemization = member (op =) skolemization_steps
+val keep_app_symbols = member (op =) [eq_congruent_pred_rule, eq_congruent_rule, ite_intro_rule]
+val keep_raw_lifting = member (op =) [eq_congruent_pred_rule, eq_congruent_rule, ite_intro_rule]
+val is_SH_trivial = member (op =) [not_not_rule, contract_rule]
 
-fun is_skolemisation_step (VeriT_Replay_Node {id, ...}) = is_skolemisation id
+fun is_skolemization_step (VeriT_Replay_Node {id, ...}) = is_skolemization id
 
 (* Even the veriT developers do not know if the following rule can still appear in proofs: *)
 val veriT_deep_skolemize_rule = "deep_skolemize"
@@ -534,7 +546,7 @@
      (if f a then apfst (curry op :: a) else apsnd (curry op :: a)) (filter_split f xs)
 
 fun collect_skolem_defs (Raw_VeriT_Node {rule, subproof = subproof, args, ...}) =
-  (if is_skolemisation rule then map (fn id => id ^ veriT_def) (skolems_introduced_by_rule args) else []) @
+  (if is_skolemization rule then map (fn id => id ^ veriT_def) (skolems_introduced_by_rule args) else []) @
   flat (map collect_skolem_defs subproof)
 
 (*The postprocessing does:
@@ -606,7 +618,7 @@
       val alpha_conversion = rule = "bind" andalso is_alpha_renaming concl
 
       val can_remove_subproof =
-        compress andalso (is_skolemisation rule orelse alpha_conversion)
+        compress andalso (is_skolemization rule orelse alpha_conversion)
       val (fixed_subproof : veriT_replay_node list, _) =
          fold_map postprocess (if can_remove_subproof then [] else subproof)
            (subproof_cx, subproof_rew)
@@ -646,9 +658,9 @@
       val bound_t = bounds
         |> map (fn s => (s, the (find_type_in_formula concl s)))
 
-      val skolem_defs = (if is_skolemisation rule
+      val skolem_defs = (if is_skolemization rule
          then map (fn id => id ^ veriT_def) (skolems_introduced_by_rule args) else [])
-      val skolems_of_subproof = (if is_skolemisation rule
+      val skolems_of_subproof = (if is_skolemization rule
          then flat (map collect_skolem_defs subproof) else [])
       val fixed_prems =
         prems @ (if is_assm_repetition id rule then [id] else []) @
@@ -675,33 +687,130 @@
 
 val linearize_proof =
   let
+    fun map_node_concl f (VeriT_Node {id, rule, prems, proof_ctxt, concl}) =
+       mk_node id rule prems proof_ctxt (f concl)
     fun linearize (VeriT_Replay_Node {id = id, rule = rule, args = _, prems = prems,
         proof_ctxt = proof_ctxt, concl = concl, bounds = bounds, insts = _, declarations = _,
-        subproof = (_, _, _, subproof)}) =
+        subproof = (bounds', assms, inputs, subproof)}) =
       let
+        val bounds = distinct (op =) bounds
+        val bounds' = distinct (op =) bounds'
         fun mk_prop_of_term concl =
           concl |> fastype_of concl = \<^typ>\<open>bool\<close> ? curry (op $) \<^term>\<open>Trueprop\<close>
         fun remove_assumption_id assumption_id prems =
           filter_out (curry (op =) assumption_id) prems
+        fun add_assumption assumption concl =
+          \<^const>\<open>Pure.imp\<close> $ mk_prop_of_term assumption $ mk_prop_of_term concl
         fun inline_assumption assumption assumption_id
-            (VeriT_Node {id, rule, prems, proof_ctxt, concl, bounds}) =
+            (VeriT_Node {id, rule, prems, proof_ctxt, concl}) =
           mk_node id rule (remove_assumption_id assumption_id prems) proof_ctxt
-            (\<^const>\<open>Pure.imp\<close> $ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds
+            (add_assumption assumption concl)
         fun find_input_steps_and_inline [] = []
           | find_input_steps_and_inline
-              (VeriT_Node {id = id', rule, prems, concl, bounds, ...} :: steps) =
+              (VeriT_Node {id = id', rule, prems, concl, ...} :: steps) =
             if rule = input_rule then
               find_input_steps_and_inline (map (inline_assumption concl id') steps)
             else
-              mk_node (id') rule prems [] concl bounds :: find_input_steps_and_inline steps
+              mk_node (id') rule prems [] concl :: find_input_steps_and_inline steps
 
-        val subproof = flat (map linearize subproof)
-        val subproof' = find_input_steps_and_inline subproof
+        fun free_bounds bounds (concl) =
+          fold (fn (var, typ) => fn t => Logic.all (Free (var, typ)) t) bounds concl
+        val subproof = subproof
+          |> flat o map linearize
+          |> map (map_node_concl (fold add_assumption (assms @ inputs)))
+          |> map (map_node_concl (free_bounds (bounds @ bounds')))
+          |> find_input_steps_and_inline
+        val concl = free_bounds bounds concl
       in
-        subproof' @ [mk_node id rule prems proof_ctxt concl (map fst bounds)]
+        subproof @ [mk_node id rule prems proof_ctxt concl]
       end
   in linearize end
 
+fun rule_of (VeriT_Replay_Node {rule,...}) = rule
+fun subproof_of (VeriT_Replay_Node {subproof = (_, _, _, subproof),...}) = subproof
+
+
+(* Massage Skolems for Sledgehammer.
+
+We have to make sure that there is an "arrow" in the graph for skolemization steps.
+
+
+A. The normal easy case
+
+This function detects the steps of the form
+  P \<longleftrightarrow> Q :skolemization
+  Q       :resolution with P
+and replace them by
+  Q       :skolemization
+Throwing away the step "P \<longleftrightarrow> Q" completely. This throws away a lot of information, but it does not
+matter too much for Sledgehammer.
+
+
+B. Skolems in subproofs
+Supporting this is more or less hopeless as long as the Isar reconstruction of Sledgehammer
+does not support more features like definitions. veriT is able to generate proofs with skolemization
+happening in subproofs inside the formula. 
+  (assume "A \<or> P"
+   ...
+   P \<longleftrightarrow> Q :skolemization in the subproof
+   ...)
+  hence A \<or> P \<longrightarrow> A \<or> Q :lemma
+  ...
+  R :something with some rule
+and replace them by
+  R :skolemization with some rule
+Without any subproof
+*)
+fun remove_skolem_definitions_proof steps =
+  let
+    fun replace_equivalent_by_imp (judgement $ ((Const(\<^const_name>\<open>HOL.eq\<close>, typ) $ arg1) $ arg2)) =
+       judgement $ ((Const(\<^const_name>\<open>HOL.implies\<close>, typ) $ arg1) $ arg2)
+     | replace_equivalent_by_imp a = a (*This case is probably wrong*)
+    fun remove_skolem_definitions (VeriT_Replay_Node {id = id, rule = rule, args = args,
+         prems = prems,
+        proof_ctxt = proof_ctxt, concl = concl, bounds = bounds, insts = insts,
+        declarations = declarations,
+        subproof = (vars, assms', extra_assms', subproof)}) (prems_to_remove, skolems) =
+    let
+      val prems = prems
+        |> filter_out (member (op =) prems_to_remove)
+      val trivial_step = is_SH_trivial rule
+      fun has_skolem_substep st NONE = if is_skolemization (rule_of st) then SOME (rule_of st)
+             else fold has_skolem_substep (subproof_of st) NONE
+        | has_skolem_substep _ a = a
+      val promote_to_skolem = exists (fn t => member (op =) skolems t) prems
+      val promote_from_assms = fold has_skolem_substep subproof NONE <> NONE
+      val promote_step = promote_to_skolem orelse promote_from_assms
+      val skolem_step_to_skip = is_skolemization rule orelse 
+        (promote_from_assms andalso length prems > 1)
+      val is_skolem = is_skolemization rule orelse promote_step
+      val prems = prems
+        |> filter_out (fn t => member (op =) skolems t)
+        |> is_skolem ? filter_out (String.isPrefix id)
+      val rule = (if promote_step then default_skolem_rule else rule)
+      val subproof = subproof
+        |> (is_skolem ? K []) (*subproofs of skolemization steps are useless for SH*)
+        |> map (fst o (fn st => remove_skolem_definitions st (prems_to_remove, skolems)))
+             (*no new definitions in subproofs*)
+        |> flat
+      val concl = concl
+        |> is_skolem ? replace_equivalent_by_imp
+      val step = (if skolem_step_to_skip orelse rule = veriT_def orelse trivial_step then []
+        else mk_replay_node id rule args prems proof_ctxt concl bounds insts declarations
+            (vars, assms', extra_assms', subproof)
+          |> single)
+      val defs = (if rule = veriT_def orelse trivial_step then id :: prems_to_remove
+         else prems_to_remove)
+      val skolems = (if skolem_step_to_skip then id :: skolems else skolems)
+    in
+      (step, (defs, skolems))
+    end
+  in
+    fold_map remove_skolem_definitions steps ([], [])
+    |> fst
+    |> flat
+  end
+
 local
   fun import_proof_and_post_process typs funs lines ctxt =
     let
@@ -719,7 +828,7 @@
           let val (step, cx) = postprocess_proof compress ctxt step cx
           in (step, (cx, cx')) end
         in uncurry (fold_map postprocess) (preprocess compress step (cx, cx')) end
-       val step =
+      val step =
         (empty_context ctxt typs funs, [])
         |> fold_map process raw_steps
         |> (fn (steps, (cx, _)) => (flat steps, cx))
@@ -729,9 +838,11 @@
 fun parse typs funs lines ctxt =
   let
     val (u, env) = import_proof_and_post_process typs funs lines ctxt
-    val t = flat (map linearize_proof u)
-    fun node_to_step (VeriT_Node {id, rule, prems, concl, bounds, ...}) =
-      mk_step id rule prems [] concl bounds
+    val t = u
+       |> remove_skolem_definitions_proof
+       |> flat o (map linearize_proof)
+    fun node_to_step (VeriT_Node {id, rule, prems, concl, ...}) =
+      mk_step id rule prems [] concl []
   in
     (map node_to_step t, ctxt_of env)
   end

--- a/src/HOL/Tools/SMT/verit_replay.ML	Tue Oct 27 16:59:44 2020 +0000
+++ b/src/HOL/Tools/SMT/verit_replay.ML	Wed Oct 28 08:41:07 2020 +0100
@@ -131,7 +131,7 @@
        function is in proofs *)
     val nthms = prems
       |> map (apsnd export_thm) o map_filter (Symtab.lookup (if (null subproof) then proofs else proofs'))
-    val nthms' = (if Verit_Proof.is_skolemisation rule
+    val nthms' = (if Verit_Proof.is_skolemization rule
          then prems else [])
       |> map_filter (Symtab.lookup proofs)
     val args = map (Term.subst_free concl_tranformation o subst_only_free global_transformation) args

--- a/src/HOL/Tools/SMT/verit_replay_methods.ML	Tue Oct 27 16:59:44 2020 +0000
+++ b/src/HOL/Tools/SMT/verit_replay_methods.ML	Wed Oct 28 08:41:07 2020 +0100
@@ -94,7 +94,6 @@
   | verit_rule_of "or" = Or
   | verit_rule_of "not_or" = Not_Or
   | verit_rule_of "resolution" = Resolution
-  | verit_rule_of "eq_congruent" = Eq_Congruent
   | verit_rule_of "trans" = Trans
   | verit_rule_of "false" = False
   | verit_rule_of "ac_simp" = AC_Simp
@@ -120,7 +119,6 @@
   | verit_rule_of "ite_pos2" = ITE_Pos2
   | verit_rule_of "ite_neg1" = ITE_Neg1
   | verit_rule_of "ite_neg2" = ITE_Neg2
-  | verit_rule_of "ite_intro" = ITE_Intro
   | verit_rule_of "la_disequality" = LA_Disequality
   | verit_rule_of "lia_generic" = LIA_Generic
   | verit_rule_of "la_generic" = LA_Generic
@@ -132,7 +130,6 @@
   | verit_rule_of "qnt_rm_unused" = Qnt_Rm_Unused
   | verit_rule_of "onepoint" = Onepoint
   | verit_rule_of "qnt_join" = Qnt_Join
-  | verit_rule_of "eq_congruent_pred" = Eq_Congruent_Pred
   | verit_rule_of "subproof" = Subproof
   | verit_rule_of "bool_simplify" = Bool_Simplify
   | verit_rule_of "or_simplify" = Or_Simplify
@@ -148,14 +145,17 @@
   | verit_rule_of "prod_simplify" = Prod_Simplify
   | verit_rule_of "comp_simplify" = Comp_Simplify
   | verit_rule_of "qnt_simplify" = Qnt_Simplify
-  | verit_rule_of "not_not" = Not_Not
   | verit_rule_of "tautology" = Tautological_Clause
-  | verit_rule_of "contraction" = Duplicate_Literals
   | verit_rule_of "qnt_cnf" = Qnt_CNF
   | verit_rule_of r =
      if r = Verit_Proof.normalized_input_rule then Normalized_Input
      else if r = Verit_Proof.local_input_rule then Local_Input
      else if r = Verit_Proof.veriT_def then Definition
+     else if r = Verit_Proof.not_not_rule then Not_Not
+     else if r = Verit_Proof.contract_rule then Duplicate_Literals
+     else if r = Verit_Proof.ite_intro_rule then ITE_Intro
+     else if r = Verit_Proof.eq_congruent_rule then Eq_Congruent
+     else if r = Verit_Proof.eq_congruent_pred_rule then Eq_Congruent_Pred
      else (@{print} ("Unsupport rule", r); Unsupported)
 
 fun string_of_verit_rule Bind = "Bind"
@@ -231,9 +231,9 @@
   | string_of_verit_rule Prod_Simplify = "prod_simplify"
   | string_of_verit_rule Comp_Simplify = "comp_simplify"
   | string_of_verit_rule Qnt_Simplify = "qnt_simplify"
-  | string_of_verit_rule Not_Not = "not_not"
+  | string_of_verit_rule Not_Not = Verit_Proof.not_not_rule
   | string_of_verit_rule Tautological_Clause = "tautology"
-  | string_of_verit_rule Duplicate_Literals = "contraction"
+  | string_of_verit_rule Duplicate_Literals = Verit_Proof.contract_rule
   | string_of_verit_rule Qnt_CNF = "qnt_cnf"
   | string_of_verit_rule r = "Unknown rule: " ^ \<^make_string> r
 
@@ -586,9 +586,9 @@
           (case (prop_of thm1, prop_of thm2) of
             ((Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2),
              (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t3 $ t4)) =>
-            if t2 = t3 then thm1 RSN (1, thm2 RSN (2, @{thm trans}))
-            else if t2 = t4 then thm1 RSN ((1, ((thm2 RS sym)) RSN (2, @{thm trans})))
-            else if t1 = t4 then thm2 RSN (1, thm1 RSN (2, @{thm trans}))
+            if t2 aconv t3 then thm1 RSN (1, thm2 RSN (2, @{thm trans}))
+            else if t2 aconv t4 then thm1 RSN ((1, ((thm2 RS sym)) RSN (2, @{thm trans})))
+            else if t1 aconv t4 then thm2 RSN (1, thm1 RSN (2, @{thm trans}))
             else raise Fail "invalid trans theorem"
           | _ => trans_bool_thm OF [thm1, thm2])
       | combine_thms (thm1 :: thm2 :: thms) =
@@ -626,7 +626,7 @@
   fun or_pos_prove ctxt _ =
      K (unfold_tac ctxt @{thms de_Morgan_disj not_not})
      THEN' match_tac ctxt @{thms verit_and_pos}
-     THEN' K (unfold_tac ctxt @{thms de_Morgan_conj not_not})
+     THEN' K (unfold_tac ctxt @{thms de_Morgan_conj de_Morgan_disj not_not})
      THEN' TRY' (assume_tac ctxt)
 
   fun not_or_rule_prove ctxt prems =
@@ -642,7 +642,7 @@
      THEN' TRY' (assume_tac ctxt)
 
   fun and_neg_rule_prove ctxt _ =
-     match_tac ctxt @{thms verit_and_pos}
+     match_tac ctxt @{thms verit_and_neg}
      THEN' K (unfold_tac ctxt @{thms de_Morgan_conj not_not})
      THEN' TRY' (assume_tac ctxt)
 
@@ -986,7 +986,8 @@
 fun rewrite_or_simplify ctxt _ t =
   SMT_Replay_Methods.prove ctxt t (fn _ =>
    (chain_rewrite_two_step_with_ac_simps ctxt @{thms verit_or_simplify verit_or_simplify_1}
-    @{thms verit_or_simplify}))
+    @{thms verit_or_simplify})
+    THEN' TRY' (REPEAT' (match_tac ctxt @{thms verit_and_pos}) THEN' assume_tac ctxt))
 
 fun rewrite_not_simplify ctxt _ t =
   SMT_Replay_Methods.prove ctxt t (fn _ =>

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Oct 27 16:59:44 2020 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Oct 28 08:41:07 2020 +0100
@@ -54,15 +54,15 @@
 val vampire_skolemisation_rule = "skolemisation"
 val veriT_la_generic_rule = "la_generic"
 val veriT_simp_arith_rule = "simp_arith"
-val veriT_tmp_skolemize_rule = "tmp_skolemize"
+val veriT_skolemize_rules = Verit_Proof.skolemization_steps
 val z3_skolemize_rule = Z3_Proof.string_of_rule Z3_Proof.Skolemize
 val z3_th_lemma_rule_prefix = Z3_Proof.string_of_rule (Z3_Proof.Th_Lemma "")
 val zipperposition_cnf_rule = "cnf"
 
 val skolemize_rules =
   [e_definition_rule, e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule,
-   spass_skolemize_rule, vampire_skolemisation_rule, veriT_tmp_skolemize_rule, z3_skolemize_rule,
-   zipperposition_cnf_rule]
+   spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule,
+   zipperposition_cnf_rule] @ veriT_skolemize_rules
 
 fun is_ext_rule rule = (rule = leo2_extcnf_equal_neg_rule)
 val is_maybe_ext_rule = is_ext_rule orf String.isPrefix satallax_tab_rule_prefix