diff --git a/src/HOL/Library/Tools/smt_word.ML b/src/HOL/Library/Tools/smt_word.ML
--- a/src/HOL/Library/Tools/smt_word.ML
+++ b/src/HOL/Library/Tools/smt_word.ML
@@ -1,158 +1,167 @@
 (*  Title:      HOL/Word/Tools/smt_word.ML
     Author:     Sascha Boehme, TU Muenchen
 
 SMT setup for words.
 *)
 
 signature SMT_WORD =
 sig
   val add_word_shift': term * string -> Context.generic -> Context.generic
 end
 
 structure SMT_Word : SMT_WORD =
 struct
 
 open Word_Lib
 
 
 (* SMT-LIB logic *)
 
 (* "QF_AUFBV" is too restrictive for Isabelle's problems, which contain aritmetic and quantifiers.
    Better set the logic to "" and make at least Z3 happy. *)
 fun smtlib_logic ts =
   if exists (Term.exists_type (Term.exists_subtype is_wordT)) ts then SOME "" else NONE
 
 
 (* SMT-LIB builtins *)
 
 local
   val smtlibC = SMTLIB_Interface.smtlibC
 
   val wordT = \<^typ>\<open>'a::len word\<close>
 
   fun index1 s i = "(_ " ^ s ^ " " ^ string_of_int i ^ ")"
   fun index2 s i j = "(_ " ^ s ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^ ")"
 
   fun word_typ (Type (\<^type_name>\<open>word\<close>, [T])) =
       Option.map (rpair [] o index1 "BitVec") (try dest_binT T)
     | word_typ _ = NONE
 
+  (*CVC4 does not support "_bvk T" when k does not fit in the BV of size T, so remove the bits that
+   will be ignored according to the SMT-LIB*)
   fun word_num (Type (\<^type_name>\<open>word\<close>, [T])) k =
-        Option.map (index1 ("bv" ^ string_of_int k)) (try dest_binT T)
+        let
+          val size = try dest_binT T
+          fun max_int size = IntInf.pow (2, size)
+        in
+          (case size of
+            NONE => NONE
+          | SOME size => SOME (index1 ("bv" ^ string_of_int (Int.rem(k, max_int size))) size))
+        end
     | word_num _ _ = NONE
 
   fun if_fixed pred m n T ts =
     let val (Us, U) = Term.strip_type T
     in
       if pred (U, Us) then SOME (n, length Us, ts, Term.list_comb o pair (Const (m, T))) else NONE
     end
 
   fun if_fixed_all m = if_fixed (forall (can dest_wordT) o (op ::)) m
   fun if_fixed_args m = if_fixed (forall (can dest_wordT) o snd) m
 
   fun add_word_fun f (t, n) =
     let val (m, _) = Term.dest_Const t
     in SMT_Builtin.add_builtin_fun smtlibC (Term.dest_Const t, K (f m n)) end
 
   val mk_nat = HOLogic.mk_number \<^typ>\<open>nat\<close>
 
   fun mk_shift c [u, t] = Const c $ mk_nat (snd (HOLogic.dest_number u)) $ t
     | mk_shift c ts = raise TERM ("bad arguments", Const c :: ts)
 
   fun shift m n T ts =
     let val U = Term.domain_type (Term.range_type T)
     in
       (case (can dest_wordT U, try (snd o HOLogic.dest_number o hd) ts) of
         (true, SOME i) =>
           SOME (n, 2, [hd (tl ts), HOLogic.mk_number U i], mk_shift (m, T))
       | _ => NONE)   (* FIXME: also support non-numerical shifts *)
     end
 
   fun mk_shift' c [t, u] = Const c $ t $ mk_nat (snd (HOLogic.dest_number u))
     | mk_shift' c ts = raise TERM ("bad arguments", Const c :: ts)
 
   fun shift' m n T ts =
     let val U = Term.domain_type T
     in
       (case (can dest_wordT U, try (snd o HOLogic.dest_number o hd o tl) ts) of
         (true, SOME i) =>
           SOME (n, 2, [hd ts, HOLogic.mk_number U i], mk_shift' (m, T))
       | _ => NONE)   (* FIXME: also support non-numerical shifts *)
     end
 
   fun mk_extract c i ts = Term.list_comb (Const c, mk_nat i :: ts)
 
   fun extract m n T ts =
     let val U = Term.range_type (Term.range_type T)
     in
       (case (try (snd o HOLogic.dest_number o hd) ts, try dest_wordT U) of
         (SOME lb, SOME i) =>
           SOME (index2 n (i + lb - 1) lb, 1, tl ts, mk_extract (m, T) lb)
       | _ => NONE)
     end
 
   fun mk_extend c ts = Term.list_comb (Const c, ts)
 
   fun extend m n T ts =
     let val (U1, U2) = Term.dest_funT T
     in
       (case (try dest_wordT U1, try dest_wordT U2) of
         (SOME i, SOME j) =>
           if j-i >= 0 then SOME (index1 n (j-i), 1, ts, mk_extend (m, T))
           else NONE
       | _ => NONE)
     end
 
   fun mk_rotate c i ts = Term.list_comb (Const c, mk_nat i :: ts)
 
   fun rotate m n T ts =
     let val U = Term.domain_type (Term.range_type T)
     in
       (case (can dest_wordT U, try (snd o HOLogic.dest_number o hd) ts) of
         (true, SOME i) => SOME (index1 n i, 1, tl ts, mk_rotate (m, T) i)
       | _ => NONE)
     end
 in
 
 val setup_builtins =
   SMT_Builtin.add_builtin_typ smtlibC (wordT, word_typ, word_num) #>
   fold (add_word_fun if_fixed_all) [
     (\<^term>\<open>uminus :: 'a::len word \<Rightarrow> _\<close>, "bvneg"),
     (\<^term>\<open>plus :: 'a::len word \<Rightarrow> _\<close>, "bvadd"),
     (\<^term>\<open>minus :: 'a::len word \<Rightarrow> _\<close>, "bvsub"),
     (\<^term>\<open>times :: 'a::len word \<Rightarrow> _\<close>, "bvmul"),
     (\<^term>\<open>NOT :: 'a::len word \<Rightarrow> _\<close>, "bvnot"),
     (\<^term>\<open>(AND) :: 'a::len word \<Rightarrow> _\<close>, "bvand"),
     (\<^term>\<open>(OR) :: 'a::len word \<Rightarrow> _\<close>, "bvor"),
     (\<^term>\<open>(XOR) :: 'a::len word \<Rightarrow> _\<close>, "bvxor"),
     (\<^term>\<open>word_cat :: 'a::len word \<Rightarrow> _\<close>, "concat") ] #>
   fold (add_word_fun shift) [
     (\<^term>\<open>push_bit :: nat \<Rightarrow> 'a::len word \<Rightarrow> _ \<close>, "bvshl"),
     (\<^term>\<open>drop_bit :: nat \<Rightarrow> 'a::len word \<Rightarrow> _\<close>, "bvlshr"),
     (\<^term>\<open>signed_drop_bit :: nat \<Rightarrow> 'a::len word \<Rightarrow> _\<close>, "bvashr") ] #>
   add_word_fun extract
     (\<^term>\<open>slice :: _ \<Rightarrow> 'a::len word \<Rightarrow> _\<close>, "extract") #>
   fold (add_word_fun extend) [
     (\<^term>\<open>ucast :: 'a::len word \<Rightarrow> _\<close>, "zero_extend"),
     (\<^term>\<open>scast :: 'a::len word \<Rightarrow> _\<close>, "sign_extend") ] #>
   fold (add_word_fun rotate) [
     (\<^term>\<open>word_rotl\<close>, "rotate_left"),
     (\<^term>\<open>word_rotr\<close>, "rotate_right") ] #>
   fold (add_word_fun if_fixed_args) [
     (\<^term>\<open>less :: 'a::len word \<Rightarrow> _\<close>, "bvult"),
     (\<^term>\<open>less_eq :: 'a::len word \<Rightarrow> _\<close>, "bvule"),
     (\<^term>\<open>word_sless\<close>, "bvslt"),
     (\<^term>\<open>word_sle\<close>, "bvsle") ]
 
 val add_word_shift' = add_word_fun shift'
 
 end
 
 
 (* setup *)
 
 val _ = Theory.setup (Context.theory_map (
   SMTLIB_Interface.add_logic (20, smtlib_logic) #>
   setup_builtins))
 
 end;
diff --git a/src/HOL/SMT_Examples/SMT_Examples_Verit.thy b/src/HOL/SMT_Examples/SMT_Examples_Verit.thy
--- a/src/HOL/SMT_Examples/SMT_Examples_Verit.thy
+++ b/src/HOL/SMT_Examples/SMT_Examples_Verit.thy
@@ -1,741 +1,741 @@
 (*  Title:      HOL/SMT_Examples/SMT_Examples_Verit.thy
     Author:     Sascha Boehme, TU Muenchen
     Author:     Mathias Fleury, JKU
 
 Half of the examples come from the corresponding file for z3,
 the others come from the Isabelle distribution or the AFP.
 *)
 
 section \<open>Examples for the (smt (verit)) binding\<close>
 
 theory SMT_Examples_Verit
 imports Complex_Main
 begin
 
 external_file \<open>SMT_Examples_Verit.certs\<close>
  
 declare [[smt_certificates = "SMT_Examples_Verit.certs"]]
 declare [[smt_read_only_certificates = true]]
 
 
 section \<open>Propositional and first-order logic\<close>
 
 lemma "True" by (smt (verit))
 lemma "p \<or> \<not>p" by (smt (verit))
 lemma "(p \<and> True) = p" by (smt (verit))
 lemma "(p \<or> q) \<and> \<not>p \<Longrightarrow> q" by (smt (verit))
 lemma "(a \<and> b) \<or> (c \<and> d) \<Longrightarrow> (a \<and> b) \<or> (c \<and> d)" by (smt (verit))
 lemma "(p1 \<and> p2) \<or> p3 \<longrightarrow> (p1 \<longrightarrow> (p3 \<and> p2) \<or> (p1 \<and> p3)) \<or> p1" by (smt (verit))
 lemma "P = P = P = P = P = P = P = P = P = P" by (smt (verit))
 
 lemma
   assumes "a \<or> b \<or> c \<or> d"
       and "e \<or> f \<or> (a \<and> d)"
       and "\<not> (a \<or> (c \<and> ~c)) \<or> b"
       and "\<not> (b \<and> (x \<or> \<not> x)) \<or> c"
       and "\<not> (d \<or> False) \<or> c"
       and "\<not> (c \<or> (\<not> p \<and> (p \<or> (q \<and> \<not> q))))"
   shows False
   using assms by (smt (verit))
 
 axiomatization symm_f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
   symm_f: "symm_f x y = symm_f y x"
 
 lemma "a = a \<and> symm_f a b = symm_f b a"
   by (smt (verit) symm_f)
 
 (*
 Taken from ~~/src/HOL/ex/SAT_Examples.thy.
 Translated from TPTP problem library: PUZ015-2.006.dimacs
 *)
 lemma
   assumes "~x0"
   and "~x30"
   and "~x29"
   and "~x59"
   and "x1 \<or> x31 \<or> x0"
   and "x2 \<or> x32 \<or> x1"
   and "x3 \<or> x33 \<or> x2"
   and "x4 \<or> x34 \<or> x3"
   and "x35 \<or> x4"
   and "x5 \<or> x36 \<or> x30"
   and "x6 \<or> x37 \<or> x5 \<or> x31"
   and "x7 \<or> x38 \<or> x6 \<or> x32"
   and "x8 \<or> x39 \<or> x7 \<or> x33"
   and "x9 \<or> x40 \<or> x8 \<or> x34"
   and "x41 \<or> x9 \<or> x35"
   and "x10 \<or> x42 \<or> x36"
   and "x11 \<or> x43 \<or> x10 \<or> x37"
   and "x12 \<or> x44 \<or> x11 \<or> x38"
   and "x13 \<or> x45 \<or> x12 \<or> x39"
   and "x14 \<or> x46 \<or> x13 \<or> x40"
   and "x47 \<or> x14 \<or> x41"
   and "x15 \<or> x48 \<or> x42"
   and "x16 \<or> x49 \<or> x15 \<or> x43"
   and "x17 \<or> x50 \<or> x16 \<or> x44"
   and "x18 \<or> x51 \<or> x17 \<or> x45"
   and "x19 \<or> x52 \<or> x18 \<or> x46"
   and "x53 \<or> x19 \<or> x47"
   and "x20 \<or> x54 \<or> x48"
   and "x21 \<or> x55 \<or> x20 \<or> x49"
   and "x22 \<or> x56 \<or> x21 \<or> x50"
   and "x23 \<or> x57 \<or> x22 \<or> x51"
   and "x24 \<or> x58 \<or> x23 \<or> x52"
   and "x59 \<or> x24 \<or> x53"
   and "x25 \<or> x54"
   and "x26 \<or> x25 \<or> x55"
   and "x27 \<or> x26 \<or> x56"
   and "x28 \<or> x27 \<or> x57"
   and "x29 \<or> x28 \<or> x58"
   and "~x1 \<or> ~x31"
   and "~x1 \<or> ~x0"
   and "~x31 \<or> ~x0"
   and "~x2 \<or> ~x32"
   and "~x2 \<or> ~x1"
   and "~x32 \<or> ~x1"
   and "~x3 \<or> ~x33"
   and "~x3 \<or> ~x2"
   and "~x33 \<or> ~x2"
   and "~x4 \<or> ~x34"
   and "~x4 \<or> ~x3"
   and "~x34 \<or> ~x3"
   and "~x35 \<or> ~x4"
   and "~x5 \<or> ~x36"
   and "~x5 \<or> ~x30"
   and "~x36 \<or> ~x30"
   and "~x6 \<or> ~x37"
   and "~x6 \<or> ~x5"
   and "~x6 \<or> ~x31"
   and "~x37 \<or> ~x5"
   and "~x37 \<or> ~x31"
   and "~x5 \<or> ~x31"
   and "~x7 \<or> ~x38"
   and "~x7 \<or> ~x6"
   and "~x7 \<or> ~x32"
   and "~x38 \<or> ~x6"
   and "~x38 \<or> ~x32"
   and "~x6 \<or> ~x32"
   and "~x8 \<or> ~x39"
   and "~x8 \<or> ~x7"
   and "~x8 \<or> ~x33"
   and "~x39 \<or> ~x7"
   and "~x39 \<or> ~x33"
   and "~x7 \<or> ~x33"
   and "~x9 \<or> ~x40"
   and "~x9 \<or> ~x8"
   and "~x9 \<or> ~x34"
   and "~x40 \<or> ~x8"
   and "~x40 \<or> ~x34"
   and "~x8 \<or> ~x34"
   and "~x41 \<or> ~x9"
   and "~x41 \<or> ~x35"
   and "~x9 \<or> ~x35"
   and "~x10 \<or> ~x42"
   and "~x10 \<or> ~x36"
   and "~x42 \<or> ~x36"
   and "~x11 \<or> ~x43"
   and "~x11 \<or> ~x10"
   and "~x11 \<or> ~x37"
   and "~x43 \<or> ~x10"
   and "~x43 \<or> ~x37"
   and "~x10 \<or> ~x37"
   and "~x12 \<or> ~x44"
   and "~x12 \<or> ~x11"
   and "~x12 \<or> ~x38"
   and "~x44 \<or> ~x11"
   and "~x44 \<or> ~x38"
   and "~x11 \<or> ~x38"
   and "~x13 \<or> ~x45"
   and "~x13 \<or> ~x12"
   and "~x13 \<or> ~x39"
   and "~x45 \<or> ~x12"
   and "~x45 \<or> ~x39"
   and "~x12 \<or> ~x39"
   and "~x14 \<or> ~x46"
   and "~x14 \<or> ~x13"
   and "~x14 \<or> ~x40"
   and "~x46 \<or> ~x13"
   and "~x46 \<or> ~x40"
   and "~x13 \<or> ~x40"
   and "~x47 \<or> ~x14"
   and "~x47 \<or> ~x41"
   and "~x14 \<or> ~x41"
   and "~x15 \<or> ~x48"
   and "~x15 \<or> ~x42"
   and "~x48 \<or> ~x42"
   and "~x16 \<or> ~x49"
   and "~x16 \<or> ~x15"
   and "~x16 \<or> ~x43"
   and "~x49 \<or> ~x15"
   and "~x49 \<or> ~x43"
   and "~x15 \<or> ~x43"
   and "~x17 \<or> ~x50"
   and "~x17 \<or> ~x16"
   and "~x17 \<or> ~x44"
   and "~x50 \<or> ~x16"
   and "~x50 \<or> ~x44"
   and "~x16 \<or> ~x44"
   and "~x18 \<or> ~x51"
   and "~x18 \<or> ~x17"
   and "~x18 \<or> ~x45"
   and "~x51 \<or> ~x17"
   and "~x51 \<or> ~x45"
   and "~x17 \<or> ~x45"
   and "~x19 \<or> ~x52"
   and "~x19 \<or> ~x18"
   and "~x19 \<or> ~x46"
   and "~x52 \<or> ~x18"
   and "~x52 \<or> ~x46"
   and "~x18 \<or> ~x46"
   and "~x53 \<or> ~x19"
   and "~x53 \<or> ~x47"
   and "~x19 \<or> ~x47"
   and "~x20 \<or> ~x54"
   and "~x20 \<or> ~x48"
   and "~x54 \<or> ~x48"
   and "~x21 \<or> ~x55"
   and "~x21 \<or> ~x20"
   and "~x21 \<or> ~x49"
   and "~x55 \<or> ~x20"
   and "~x55 \<or> ~x49"
   and "~x20 \<or> ~x49"
   and "~x22 \<or> ~x56"
   and "~x22 \<or> ~x21"
   and "~x22 \<or> ~x50"
   and "~x56 \<or> ~x21"
   and "~x56 \<or> ~x50"
   and "~x21 \<or> ~x50"
   and "~x23 \<or> ~x57"
   and "~x23 \<or> ~x22"
   and "~x23 \<or> ~x51"
   and "~x57 \<or> ~x22"
   and "~x57 \<or> ~x51"
   and "~x22 \<or> ~x51"
   and "~x24 \<or> ~x58"
   and "~x24 \<or> ~x23"
   and "~x24 \<or> ~x52"
   and "~x58 \<or> ~x23"
   and "~x58 \<or> ~x52"
   and "~x23 \<or> ~x52"
   and "~x59 \<or> ~x24"
   and "~x59 \<or> ~x53"
   and "~x24 \<or> ~x53"
   and "~x25 \<or> ~x54"
   and "~x26 \<or> ~x25"
   and "~x26 \<or> ~x55"
   and "~x25 \<or> ~x55"
   and "~x27 \<or> ~x26"
   and "~x27 \<or> ~x56"
   and "~x26 \<or> ~x56"
   and "~x28 \<or> ~x27"
   and "~x28 \<or> ~x57"
   and "~x27 \<or> ~x57"
   and "~x29 \<or> ~x28"
   and "~x29 \<or> ~x58"
   and "~x28 \<or> ~x58"
 shows False
   using assms by (smt (verit))
 
 lemma "\<forall>x::int. P x \<longrightarrow> (\<forall>y::int. P x \<or> P y)"
   by (smt (verit))
 
 lemma
   assumes "(\<forall>x y. P x y = x)"
   shows "(\<exists>y. P x y) = P x c"
   using assms by (smt (verit))
 
 lemma
   assumes "(\<forall>x y. P x y = x)"
   and "(\<forall>x. \<exists>y. P x y) = (\<forall>x. P x c)"
   shows "(\<exists>y. P x y) = P x c"
   using assms by (smt (verit))
 
 lemma
   assumes "if P x then \<not>(\<exists>y. P y) else (\<forall>y. \<not>P y)"
   shows "P x \<longrightarrow> P y"
   using assms by (smt (verit))
 
 
 section \<open>Arithmetic\<close>
 
 subsection \<open>Linear arithmetic over integers and reals\<close>
 
 lemma "(3::int) = 3" by (smt (verit))
 lemma "(3::real) = 3" by (smt (verit))
 lemma "(3 :: int) + 1 = 4" by (smt (verit))
 lemma "x + (y + z) = y + (z + (x::int))" by (smt (verit))
 lemma "max (3::int) 8 > 5" by (smt (verit))
 lemma "\<bar>x :: real\<bar> + \<bar>y\<bar> \<ge> \<bar>x + y\<bar>" by (smt (verit))
 lemma "P ((2::int) < 3) = P True" supply[[smt_trace]] by (smt (verit))
 lemma "x + 3 \<ge> 4 \<or> x < (1::int)" by (smt (verit))
 
 lemma
   assumes "x \<ge> (3::int)" and "y = x + 4"
   shows "y - x > 0"
   using assms by (smt (verit))
 
 lemma "let x = (2 :: int) in x + x \<noteq> 5" by (smt (verit))
 
 lemma
   fixes x :: int
   assumes "3 * x + 7 * a < 4" and "3 < 2 * x"
   shows "a < 0"
   using assms by (smt (verit))
 
 lemma "(0 \<le> y + -1 * x \<or> \<not> 0 \<le> x \<or> 0 \<le> (x::int)) = (\<not> False)" by (smt (verit))
 
 lemma "
   (n < m \<and> m < n') \<or> (n < m \<and> m = n') \<or> (n < n' \<and> n' < m) \<or>
   (n = n' \<and> n' < m) \<or> (n = m \<and> m < n') \<or>
   (n' < m \<and> m < n) \<or> (n' < m \<and> m = n) \<or>
   (n' < n \<and> n < m) \<or> (n' = n \<and> n < m) \<or> (n' = m \<and> m < n) \<or>
   (m < n \<and> n < n') \<or> (m < n \<and> n' = n) \<or> (m < n' \<and> n' < n) \<or>
   (m = n \<and> n < n') \<or> (m = n' \<and> n' < n) \<or>
   (n' = m \<and> m = (n::int))"
   by (smt (verit))
 
 text\<open>
 The following example was taken from HOL/ex/PresburgerEx.thy, where it says:
 
   This following theorem proves that all solutions to the
   recurrence relation $x_{i+2} = |x_{i+1}| - x_i$ are periodic with
   period 9.  The example was brought to our attention by John
   Harrison. It does does not require Presburger arithmetic but merely
   quantifier-free linear arithmetic and holds for the rationals as well.
 
   Warning: it takes (in 2006) over 4.2 minutes!
 
 There, it is proved by "arith". (smt (verit)) is able to prove this within a fraction
 of one second. With proof reconstruction, it takes about 13 seconds on a Core2
 processor.
 \<close>
 
 lemma "\<lbrakk> x3 = \<bar>x2\<bar> - x1; x4 = \<bar>x3\<bar> - x2; x5 = \<bar>x4\<bar> - x3;
          x6 = \<bar>x5\<bar> - x4; x7 = \<bar>x6\<bar> - x5; x8 = \<bar>x7\<bar> - x6;
          x9 = \<bar>x8\<bar> - x7; x10 = \<bar>x9\<bar> - x8; x11 = \<bar>x10\<bar> - x9 \<rbrakk>
  \<Longrightarrow> x1 = x10 \<and> x2 = (x11::int)"
   supply [[smt_timeout=360]]
   by (smt (verit))
 
 
 lemma "let P = 2 * x + 1 > x + (x::real) in P \<or> False \<or> P" by (smt (verit))
 
 
 subsection \<open>Linear arithmetic with quantifiers\<close>
 
 lemma "~ (\<exists>x::int. False)" by (smt (verit))
 lemma "~ (\<exists>x::real. False)" by (smt (verit))
 
 
 lemma "\<forall>x y::int. (x = 0 \<and> y = 1) \<longrightarrow> x \<noteq> y" by (smt (verit))
 lemma "\<forall>x y::int. x < y \<longrightarrow> (2 * x + 1) < (2 * y)" by (smt (verit))
 lemma "\<forall>x y::int. x + y > 2 \<or> x + y = 2 \<or> x + y < 2" by (smt (verit))
 lemma "\<forall>x::int. if x > 0 then x + 1 > 0 else 1 > x" by (smt (verit))
 lemma "(if (\<forall>x::int. x < 0 \<or> x > 0) then -1 else 3) > (0::int)" by (smt (verit))
 lemma "\<exists>x::int. \<forall>x y. 0 < x \<and> 0 < y \<longrightarrow> (0::int) < x + y" by (smt (verit))
 lemma "\<exists>u::int. \<forall>(x::int) y::real. 0 < x \<and> 0 < y \<longrightarrow> -1 < x" by (smt (verit))
 lemma "\<forall>(a::int) b::int. 0 < b \<or> b < 1" by (smt (verit))
 
 subsection \<open>Linear arithmetic for natural numbers\<close>
 
 declare [[smt_nat_as_int]]
 
 lemma "2 * (x::nat) \<noteq> 1" by (smt (verit))
 
 lemma "a < 3 \<Longrightarrow> (7::nat) > 2 * a" by (smt (verit))
 
 lemma "let x = (1::nat) + y in x - y > 0 * x" by (smt (verit))
 
 lemma
   "let x = (1::nat) + y in
    let P = (if x > 0 then True else False) in
    False \<or> P = (x - 1 = y) \<or> (\<not>P \<longrightarrow> False)"
   by (smt (verit))
 
 lemma "int (nat \<bar>x::int\<bar>) = \<bar>x\<bar>" by (smt (verit) int_nat_eq)
 
 definition prime_nat :: "nat \<Rightarrow> bool" where
   "prime_nat p = (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
 
 lemma "prime_nat (4*m + 1) \<Longrightarrow> m \<ge> (1::nat)" by (smt (verit) prime_nat_def)
 
 lemma "2 * (x::nat) \<noteq> 1" 
   by (smt (verit))
 
 lemma \<open>2*(x :: int) \<noteq> 1\<close>
   by (smt (verit))
 
 declare [[smt_nat_as_int = false]]
 
 
 section \<open>Pairs\<close>
 
 lemma "fst (x, y) = a \<Longrightarrow> x = a"
   using fst_conv by (smt (verit))
 
 lemma "p1 = (x, y) \<and> p2 = (y, x) \<Longrightarrow> fst p1 = snd p2"
   using fst_conv snd_conv by (smt (verit))
 
 
 section \<open>Higher-order problems and recursion\<close>
 
 lemma "i \<noteq> i1 \<and> i \<noteq> i2 \<Longrightarrow> (f (i1 := v1, i2 := v2)) i = f i"
   using fun_upd_same fun_upd_apply by (smt (verit))
 
 lemma "(f g (x::'a::type) = (g x \<and> True)) \<or> (f g x = True) \<or> (g x = True)"
   by (smt (verit))
 
 lemma "id x = x \<and> id True = True"
   by (smt (verit) id_def)
 
 lemma "i \<noteq> i1 \<and> i \<noteq> i2 \<Longrightarrow> ((f (i1 := v1)) (i2 := v2)) i = f i"
   using fun_upd_same fun_upd_apply by (smt (verit))
 
 lemma
   "f (\<exists>x. g x) \<Longrightarrow> True"
   "f (\<forall>x. g x) \<Longrightarrow> True"
   by (smt (verit))+
 
 lemma True using let_rsp by (smt (verit))
 lemma "le = (\<le>) \<Longrightarrow> le (3::int) 42" by (smt (verit))
 lemma "map (\<lambda>i::int. i + 1) [0, 1] = [1, 2]" by (smt (verit) list.map)
 lemma "(\<forall>x. P x) \<or> \<not> All P" by (smt (verit))
 
 fun dec_10 :: "int \<Rightarrow> int" where
   "dec_10 n = (if n < 10 then n else dec_10 (n - 10))"
 
 lemma "dec_10 (4 * dec_10 4) = 6" by (smt (verit) dec_10.simps)
 
 context complete_lattice
 begin
 
 lemma
   assumes "Sup {a | i::bool. True} \<le> Sup {b | i::bool. True}"
   and "Sup {b | i::bool. True} \<le> Sup {a | i::bool. True}"
   shows "Sup {a | i::bool. True} \<le> Sup {a | i::bool. True}"
   using assms by (smt (verit) order_trans)
 
 end
 
 lemma
  "eq_set (List.coset xs) (set ys) = rhs"
     if "\<And>ys. subset' (List.coset xs) (set ys) = (let n = card (UNIV::'a set) in 0 < n \<and> card (set (xs @ ys)) = n)"
       and "\<And>uu A. (uu::'a) \<in> - A \<Longrightarrow> uu \<notin> A"
       and "\<And>uu. card (set (uu::'a list)) = length (remdups uu)"
       and "\<And>uu. finite (set (uu::'a list))"
       and "\<And>uu. (uu::'a) \<in> UNIV"
       and "(UNIV::'a set) \<noteq> {}"
       and "\<And>c A B P. \<lbrakk>(c::'a) \<in> A \<union> B; c \<in> A \<Longrightarrow> P; c \<in> B \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
       and "\<And>a b. (a::nat) + b = b + a"
       and "\<And>a b. ((a::nat) = a + b) = (b = 0)"
       and "card' (set xs) = length (remdups xs)"
       and "card' = (card :: 'a set \<Rightarrow> nat)"
       and "\<And>A B. \<lbrakk>finite (A::'a set); finite B\<rbrakk> \<Longrightarrow> card A + card B = card (A \<union> B) + card (A \<inter> B)"
       and "\<And>A. (card (A::'a set) = 0) = (A = {} \<or> infinite A)"
       and "\<And>A. \<lbrakk>finite (UNIV::'a set); card (A::'a set) = card (UNIV::'a set)\<rbrakk> \<Longrightarrow> A = UNIV"
       and "\<And>xs. - List.coset (xs::'a list) = set xs"
       and "\<And>xs. - set (xs::'a list) = List.coset xs"
       and "\<And>A B. (A \<inter> B = {}) = (\<forall>x. (x::'a) \<in> A \<longrightarrow> x \<notin> B)"
       and "eq_set = (=)"
       and "\<And>A. finite (A::'a set) \<Longrightarrow> finite (- A) = finite (UNIV::'a set)"
       and "rhs \<equiv> let n = card (UNIV::'a set) in if n = 0 then False else let xs' = remdups xs; ys' = remdups ys in length xs' + length ys' = n \<and> (\<forall>x\<in>set xs'. x \<notin> set ys') \<and> (\<forall>y\<in>set ys'. y \<notin> set xs')"
       and "\<And>xs ys. set ((xs::'a list) @ ys) = set xs \<union> set ys"
       and "\<And>A B. ((A::'a set) = B) = (A \<subseteq> B \<and> B \<subseteq> A)"
       and "\<And>xs. set (remdups (xs::'a list)) = set xs"
       and "subset' = (\<subseteq>)"
       and "\<And>A B. (\<And>x. (x::'a) \<in> A \<Longrightarrow> x \<in> B) \<Longrightarrow> A \<subseteq> B"
       and "\<And>A B. \<lbrakk>(A::'a set) \<subseteq> B; B \<subseteq> A\<rbrakk> \<Longrightarrow> A = B"
       and "\<And>A ys. (A \<subseteq> List.coset ys) = (\<forall>y\<in>set ys. (y::'a) \<notin> A)"
   using that by (smt (verit, default))
 
 notepad
 begin
   have "line_integral F {i, j} g = line_integral F {i} g + line_integral F {j} g"
     if \<open>(k, g) \<in> one_chain_typeI\<close>
       \<open>\<And>A b B. ({} = (A::(real \<times> real) set) \<inter> insert (b::real \<times> real) (B::(real \<times> real) set)) = (b \<notin> A \<and> {} = A \<inter> B)\<close>
       \<open>finite ({} :: (real \<times> real) set)\<close>
       \<open>\<And>a A. finite (A::(real \<times> real) set) \<Longrightarrow> finite (insert (a::real \<times> real) A)\<close>
       \<open>(i::real \<times> real) = (1::real, 0::real)\<close>
       \<open> \<And>a A. (a::real \<times> real) \<in> (A::(real \<times> real) set) \<Longrightarrow> insert a A = A\<close> \<open>j = (0, 1)\<close>
       \<open>\<And>x. (x::(real \<times> real) set) \<inter> {} = {}\<close>
       \<open>\<And>y x A. insert (x::real \<times> real) (insert (y::real \<times> real) (A::(real \<times> real) set)) =  insert y (insert x A)\<close>
       \<open>\<And>a A. insert (a::real \<times> real) (A::(real \<times> real) set) = {a} \<union> A\<close>
       \<open>\<And>F u basis2 basis1 \<gamma>. finite (u :: (real \<times> real) set) \<Longrightarrow>
     line_integral_exists F basis1 \<gamma> \<Longrightarrow>
     line_integral_exists F basis2 \<gamma> \<Longrightarrow>
     basis1 \<union> basis2 = u \<Longrightarrow>
     basis1 \<inter> basis2 = {} \<Longrightarrow>
     line_integral F u \<gamma> = line_integral F basis1 \<gamma> + line_integral F basis2 \<gamma>\<close>
       \<open>one_chain_line_integral F {i} one_chain_typeI =
     one_chain_line_integral F {i} one_chain_typeII \<and>
     (\<forall>(k, \<gamma>)\<in>one_chain_typeI. line_integral_exists F {i} \<gamma>) \<and>
     (\<forall>(k, \<gamma>)\<in>one_chain_typeII. line_integral_exists F {i} \<gamma>)\<close>
       \<open> one_chain_line_integral (F::real \<times> real \<Rightarrow> real \<times> real) {j::real \<times> real}
      (one_chain_typeII::(int \<times> (real \<Rightarrow> real \<times> real)) set) =
     one_chain_line_integral F {j} (one_chain_typeI::(int \<times> (real \<Rightarrow> real \<times> real)) set) \<and>
     (\<forall>(k::int, \<gamma>::real \<Rightarrow> real \<times> real)\<in>one_chain_typeII. line_integral_exists F {j} \<gamma>) \<and>
     (\<forall>(k::int, \<gamma>::real \<Rightarrow> real \<times> real)\<in>one_chain_typeI. line_integral_exists F {j} \<gamma>)\<close>
     for F i j g one_chain_typeI one_chain_typeII and
       line_integral :: \<open>(real \<times> real \<Rightarrow> real \<times> real) \<Rightarrow> (real \<times> real) set \<Rightarrow> (real \<Rightarrow> real \<times> real) \<Rightarrow> real\<close> and
       line_integral_exists :: \<open>(real \<times> real \<Rightarrow> real \<times> real) \<Rightarrow> (real \<times> real) set \<Rightarrow> (real \<Rightarrow> real \<times> real) \<Rightarrow> bool\<close> and
       one_chain_line_integral :: \<open>(real \<times> real \<Rightarrow> real \<times> real) \<Rightarrow> (real \<times> real) set \<Rightarrow> (int \<times> (real \<Rightarrow> real \<times> real)) set \<Rightarrow> real\<close> and
       k
     using prod.case_eq_if singleton_inject snd_conv
       that
     by (smt (verit))
 end
 
 
 lemma
   fixes x y z :: real
   assumes \<open>x + 2 * y > 0\<close> and
     \<open>x - 2 * y > 0\<close> and
     \<open>x < 0\<close>
   shows False
   using assms by (smt (verit))
 
 (*test for arith reconstruction*)
 lemma
   fixes d :: real
   assumes \<open>0 < d\<close>
    \<open>diamond_y \<equiv> \<lambda>t. d / 2 - \<bar>t\<bar>\<close>
    \<open>\<And>a b c :: real. (a / c < b / c) =
     ((0 < c \<longrightarrow> a < b) \<and> (c < 0 \<longrightarrow> b < a) \<and> c \<noteq> 0)\<close>
    \<open>\<And>a b c :: real. (a / c < b / c) =
     ((0 < c \<longrightarrow> a < b) \<and> (c < 0 \<longrightarrow> b < a) \<and> c \<noteq> 0)\<close>
    \<open>\<And>a b :: real. - a / b = - (a / b)\<close>
    \<open>\<And>a b :: real. - a * b = - (a * b)\<close>
    \<open>\<And>(x1 :: real) x2 y1 y2 :: real. ((x1, x2) = (y1, y2)) = (x1 = y1 \<and> x2 = y2)\<close>
  shows \<open>(\<lambda>y. (d / 2, (2 * y - 1) * diamond_y (d / 2))) \<noteq>
     (\<lambda>x. ((x - 1 / 2) * d, - diamond_y ((x - 1 / 2) * d))) \<Longrightarrow>
     (\<lambda>y. (- (d / 2), (2 * y - 1) * diamond_y (- (d / 2)))) =
     (\<lambda>x. ((x - 1 / 2) * d, diamond_y ((x - 1 / 2) * d))) \<Longrightarrow>
     False\<close>
   using assms
   by (smt (verit,del_insts))
 
 lemma
   fixes d :: real
   assumes \<open>0 < d\<close>
    \<open>diamond_y \<equiv> \<lambda>t. d / 2 - \<bar>t\<bar>\<close>
    \<open>\<And>a b c :: real. (a / c < b / c) =
     ((0 < c \<longrightarrow> a < b) \<and> (c < 0 \<longrightarrow> b < a) \<and> c \<noteq> 0)\<close>
    \<open>\<And>a b c :: real. (a / c < b / c) =
     ((0 < c \<longrightarrow> a < b) \<and> (c < 0 \<longrightarrow> b < a) \<and> c \<noteq> 0)\<close>
    \<open>\<And>a b :: real. - a / b = - (a / b)\<close>
    \<open>\<And>a b :: real. - a * b = - (a * b)\<close>
    \<open>\<And>(x1 :: real) x2 y1 y2 :: real. ((x1, x2) = (y1, y2)) = (x1 = y1 \<and> x2 = y2)\<close>
  shows \<open>(\<lambda>y. (d / 2, (2 * y - 1) * diamond_y (d / 2))) \<noteq>
     (\<lambda>x. ((x - 1 / 2) * d, - diamond_y ((x - 1 / 2) * d))) \<Longrightarrow>
     (\<lambda>y. (- (d / 2), (2 * y - 1) * diamond_y (- (d / 2)))) =
     (\<lambda>x. ((x - 1 / 2) * d, diamond_y ((x - 1 / 2) * d))) \<Longrightarrow>
     False\<close>
   using assms
   by (smt (verit,ccfv_threshold))
 
 (*qnt_rm_unused example*)
 lemma 
   assumes \<open>\<forall>z y x. P z y\<close>
     \<open>P z y \<Longrightarrow> False\<close>
   shows False
   using assms
   by (smt (verit))
 
 
 lemma
   "max (x::int) y \<ge> y"
   supply [[smt_trace]]
   by (smt (verit))+
 
 context
 begin
 abbreviation finite' :: "'a set \<Rightarrow> bool"
   where "finite' A \<equiv> finite A \<and> A \<noteq> {}"
 
 lemma
   fixes f :: "'b \<Rightarrow> 'c :: linorder"
   assumes
     \<open>\<forall>(S::'b::type set) f::'b::type \<Rightarrow> 'c::linorder. finite' S \<longrightarrow> arg_min_on f S \<in> S\<close>
     \<open>\<forall>(S::'a::type set) f::'a::type \<Rightarrow> 'c::linorder. finite' S \<longrightarrow> arg_min_on f S \<in> S\<close>
     \<open>\<forall>(S::'b::type set) (y::'b::type) f::'b::type \<Rightarrow> 'c::linorder.
        finite S \<and> S \<noteq> {} \<and> y \<in> S \<longrightarrow> f (arg_min_on f S) \<le> f y\<close>
     \<open>\<forall>(S::'a::type set) (y::'a::type) f::'a::type \<Rightarrow> 'c::linorder.
        finite S \<and> S \<noteq> {} \<and> y \<in> S \<longrightarrow> f (arg_min_on f S) \<le> f y\<close>
     \<open>\<forall>(f::'b::type \<Rightarrow> 'c::linorder) (g::'a::type \<Rightarrow> 'b::type) x::'a::type. (f \<circ> g) x = f (g x)\<close>
     \<open>\<forall>(F::'b::type set) h::'b::type \<Rightarrow> 'a::type. finite F \<longrightarrow> finite (h ` F)\<close>
     \<open>\<forall>(F::'b::type set) h::'b::type \<Rightarrow> 'b::type. finite F \<longrightarrow> finite (h ` F)\<close>
     \<open>\<forall>(F::'a::type set) h::'a::type \<Rightarrow> 'b::type. finite F \<longrightarrow> finite (h ` F)\<close>
     \<open>\<forall>(F::'a::type set) h::'a::type \<Rightarrow> 'a::type. finite F \<longrightarrow> finite (h ` F)\<close>
     \<open>\<forall>(b::'a::type) (f::'b::type \<Rightarrow> 'a::type) A::'b::type set.
        b \<in> f ` A \<and> (\<forall>x::'b::type. b = f x \<and> x \<in> A \<longrightarrow> False) \<longrightarrow> False\<close>
     \<open>\<forall>(b::'b::type) (f::'b::type \<Rightarrow> 'b::type) A::'b::type set.
        b \<in> f ` A \<and> (\<forall>x::'b::type. b = f x \<and> x \<in> A \<longrightarrow> False) \<longrightarrow> False\<close>
     \<open>\<forall>(b::'b::type) (f::'a::type \<Rightarrow> 'b::type) A::'a::type set.
        b \<in> f ` A \<and> (\<forall>x::'a::type. b = f x \<and> x \<in> A \<longrightarrow> False) \<longrightarrow> False\<close>
     \<open>\<forall>(b::'a::type) (f::'a::type \<Rightarrow> 'a::type) A::'a::type set.
        b \<in> f ` A \<and> (\<forall>x::'a::type. b = f x \<and> x \<in> A \<longrightarrow> False) \<longrightarrow> False\<close>
     \<open>\<forall>(b::'a::type) (f::'b::type \<Rightarrow> 'a::type) (x::'b::type) A::'b::type set. b = f x \<and> x \<in> A \<longrightarrow> b \<in> f ` A    \<close>
     \<open>\<forall>(b::'b::type) (f::'b::type \<Rightarrow> 'b::type) (x::'b::type) A::'b::type set. b = f x \<and> x \<in> A \<longrightarrow> b \<in> f ` A    \<close>
     \<open>\<forall>(b::'b::type) (f::'a::type \<Rightarrow> 'b::type) (x::'a::type) A::'a::type set. b = f x \<and> x \<in> A \<longrightarrow> b \<in> f ` A    \<close>
     \<open>\<forall>(b::'a::type) (f::'a::type \<Rightarrow> 'a::type) (x::'a::type) A::'a::type set. b = f x \<and> x \<in> A \<longrightarrow> b \<in> f ` A    \<close>
     \<open>\<forall>(f::'b::type \<Rightarrow> 'a::type) A::'b::type set. (f ` A = {}) = (A = {})  \<close>
     \<open>\<forall>(f::'b::type \<Rightarrow> 'b::type) A::'b::type set. (f ` A = {}) = (A = {})  \<close>
     \<open>\<forall>(f::'a::type \<Rightarrow> 'b::type) A::'a::type set. (f ` A = {}) = (A = {})  \<close>
     \<open>\<forall>(f::'a::type \<Rightarrow> 'a::type) A::'a::type set. (f ` A = {}) = (A = {})  \<close>
     \<open>\<forall>(f::'b::type \<Rightarrow> 'c::linorder) (A::'b::type set) (x::'b::type) y::'b::type.
        inj_on f A \<and> f x = f y \<and> x \<in> A \<and> y \<in> A \<longrightarrow> x = y\<close>
     \<open>\<forall>(x::'c::linorder) y::'c::linorder. (x < y) = (x \<le> y \<and> x \<noteq> y)\<close>
     \<open>inj_on (f::'b::type \<Rightarrow> 'c::linorder) ((g::'a::type \<Rightarrow> 'b::type) ` (B::'a::type set))\<close>
     \<open>finite (B::'a::type set)\<close>
     \<open>(B::'a::type set) \<noteq> {}\<close>
     \<open>arg_min_on ((f::'b::type \<Rightarrow> 'c::linorder) \<circ> (g::'a::type \<Rightarrow> 'b::type)) (B::'a::type set) \<in> B\<close>
     \<open>\<nexists>x::'a::type.
        x \<in> (B::'a::type set) \<and>
        ((f::'b::type \<Rightarrow> 'c::linorder) \<circ> (g::'a::type \<Rightarrow> 'b::type)) x < (f \<circ> g) (arg_min_on (f \<circ> g) B)\<close>
     \<open>\<forall>(f::'b::type \<Rightarrow> 'c::linorder) (P::'b::type \<Rightarrow> bool) a::'b::type.
        inj_on f (Collect P) \<and> P a \<and> (\<forall>y::'b::type. P y \<longrightarrow> f a \<le> f y) \<longrightarrow> arg_min f P = a\<close>
     \<open>\<forall>(S::'b::type set) f::'b::type \<Rightarrow> 'c::linorder. finite' S \<longrightarrow> arg_min_on f S \<in> S\<close>
     \<open>\<forall>(S::'a::type set) f::'a::type \<Rightarrow> 'c::linorder. finite' S \<longrightarrow> arg_min_on f S \<in> S\<close>
     \<open>\<forall>(S::'b::type set) (y::'b::type) f::'b::type \<Rightarrow> 'c::linorder.
        finite S \<and> S \<noteq> {} \<and> y \<in> S \<longrightarrow> f (arg_min_on f S) \<le> f y\<close>
     \<open>\<forall>(S::'a::type set) (y::'a::type) f::'a::type \<Rightarrow> 'c::linorder.
        finite S \<and> S \<noteq> {} \<and> y \<in> S \<longrightarrow> f (arg_min_on f S) \<le> f y\<close>
     \<open>\<forall>(f::'b::type \<Rightarrow> 'c::linorder) (g::'a::type \<Rightarrow> 'b::type) x::'a::type. (f \<circ> g) x = f (g x)\<close>
     \<open>\<forall>(F::'b::type set) h::'b::type \<Rightarrow> 'a::type. finite F \<longrightarrow> finite (h ` F)\<close>
     \<open>\<forall>(F::'b::type set) h::'b::type \<Rightarrow> 'b::type. finite F \<longrightarrow> finite (h ` F)\<close>
     \<open>\<forall>(F::'a::type set) h::'a::type \<Rightarrow> 'b::type. finite F \<longrightarrow> finite (h ` F)\<close>
     \<open>\<forall>(F::'a::type set) h::'a::type \<Rightarrow> 'a::type. finite F \<longrightarrow> finite (h ` F)\<close>
     \<open>\<forall>(b::'a::type) (f::'b::type \<Rightarrow> 'a::type) A::'b::type set.
        b \<in> f ` A \<and> (\<forall>x::'b::type. b = f x \<and> x \<in> A \<longrightarrow> False) \<longrightarrow> False\<close>
     \<open>\<forall>(b::'b::type) (f::'b::type \<Rightarrow> 'b::type) A::'b::type set.
        b \<in> f ` A \<and> (\<forall>x::'b::type. b = f x \<and> x \<in> A \<longrightarrow> False) \<longrightarrow> False\<close>
     \<open>\<forall>(b::'b::type) (f::'a::type \<Rightarrow> 'b::type) A::'a::type set.
        b \<in> f ` A \<and> (\<forall>x::'a::type. b = f x \<and> x \<in> A \<longrightarrow> False) \<longrightarrow> False\<close>
     \<open>\<forall>(b::'a::type) (f::'a::type \<Rightarrow> 'a::type) A::'a::type set.
        b \<in> f ` A \<and> (\<forall>x::'a::type. b = f x \<and> x \<in> A \<longrightarrow> False) \<longrightarrow> False\<close>
     \<open>\<forall>(b::'a::type) (f::'b::type \<Rightarrow> 'a::type) (x::'b::type) A::'b::type set. b = f x \<and> x \<in> A \<longrightarrow> b \<in> f ` A \<close>
     \<open>\<forall>(b::'b::type) (f::'b::type \<Rightarrow> 'b::type) (x::'b::type) A::'b::type set. b = f x \<and> x \<in> A \<longrightarrow> b \<in> f ` A \<close>
     \<open>\<forall>(b::'b::type) (f::'a::type \<Rightarrow> 'b::type) (x::'a::type) A::'a::type set. b = f x \<and> x \<in> A \<longrightarrow> b \<in> f ` A \<close>
     \<open>\<forall>(b::'a::type) (f::'a::type \<Rightarrow> 'a::type) (x::'a::type) A::'a::type set. b = f x \<and> x \<in> A \<longrightarrow> b \<in> f ` A \<close>
     \<open>\<forall>(f::'b::type \<Rightarrow> 'a::type) A::'b::type set. (f ` A = {}) = (A = {})      \<close>
     \<open>\<forall>(f::'b::type \<Rightarrow> 'b::type) A::'b::type set. (f ` A = {}) = (A = {})      \<close>
     \<open>\<forall>(f::'a::type \<Rightarrow> 'b::type) A::'a::type set. (f ` A = {}) = (A = {})      \<close>
     \<open>\<forall>(f::'a::type \<Rightarrow> 'a::type) A::'a::type set. (f ` A = {}) = (A = {})\<close>
     \<open>\<forall>(f::'b::type \<Rightarrow> 'c::linorder) (A::'b::type set) (x::'b::type) y::'b::type.
        inj_on f A \<and> f x = f y \<and> x \<in> A \<and> y \<in> A \<longrightarrow> x = y\<close>
     \<open>\<forall>(x::'c::linorder) y::'c::linorder. (x < y) = (x \<le> y \<and> x \<noteq> y)\<close>
     \<open>arg_min_on (f::'b::type \<Rightarrow> 'c::linorder) ((g::'a::type \<Rightarrow> 'b::type) ` (B::'a::type set)) \<noteq>
        g (arg_min_on (f \<circ> g) B) \<close>
    shows False
   using assms
   by (smt (verit))
 end
 
 
 experiment
 begin
 private datatype abort =
     Rtype_error
   | Rtimeout_error
 private datatype ('a) error_result =
   Rraise " 'a " \<comment> \<open>\<open> Should only be a value of type exn \<close>\<close>
   | Rabort " abort "
 
 private datatype( 'a, 'b) result =
     Rval " 'a "
     | Rerr " ('b) error_result "
 
 lemma
   fixes clock :: \<open>'astate \<Rightarrow> nat\<close> and
-fun_evaluate_match :: \<open>'astate \<Rightarrow> 'vsemv_env \<Rightarrow> _ \<Rightarrow> ('pat \<times> 'exp0) list \<Rightarrow> _ \<Rightarrow>
+    fun_evaluate_match :: \<open>'astate \<Rightarrow> 'vsemv_env \<Rightarrow> _ \<Rightarrow> ('pat \<times> 'exp0) list \<Rightarrow> _ \<Rightarrow>
       'astate*((('v)list),('v))result\<close>
   assumes
          " fix_clock (st::'astate) (fun_evaluate st (env::'vsemv_env) [e::'exp0]) =
        (st'::'astate, r::('v list, 'v) result)"
       " clock (fst (fun_evaluate (st::'astate) (env::'vsemv_env) [e::'exp0])) \<le> clock st"
        "\<forall>(b::nat) (a::nat) c::nat. b \<le> a \<and> c \<le> b \<longrightarrow> c \<le> a"
        "\<forall>(a::'astate) p::'astate \<times> ('v list, 'v) result. (a = fst p) = (\<exists>b::('v list, 'v) result. p = (a, b))"
        "\<forall>y::'v error_result. (\<forall>x1::'v. y = Rraise x1 \<longrightarrow> False) \<and> (\<forall>x2::abort. y = Rabort x2 \<longrightarrow> False) \<longrightarrow> False"
        "\<forall>(f1::'v \<Rightarrow> 'astate \<times> ('v list, 'v) result) (f2::abort \<Rightarrow> 'astate \<times> ('v list, 'v) result) x1::'v.
           (case Rraise x1 of Rraise (x::'v) \<Rightarrow> f1 x | Rabort (x::abort) \<Rightarrow> f2 x) = f1 x1"
       " \<forall>(f1::'v \<Rightarrow> 'astate \<times> ('v list, 'v) result) (f2::abort \<Rightarrow> 'astate \<times> ('v list, 'v) result) x2::abort.
           (case Rabort x2 of Rraise (x::'v) \<Rightarrow> f1 x | Rabort (x::abort) \<Rightarrow> f2 x) = f2 x2"
        "\<forall>(s1::'astate) (s2::'astate) (x::('v list, 'v) result) s::'astate.
           fix_clock s1 (s2, x) = (s, x) \<longrightarrow> clock s \<le> clock s2"
        "\<forall>(s::'astate) (s'::'astate) res::('v list, 'v) result.
           fix_clock s (s', res) =
           (update_clock (\<lambda>_::nat. if clock s' \<le> clock s then clock s' else clock s) s', res)"
        "\<forall>(x2::'v error_result) x1::'v.
           (r::('v list, 'v) result) = Rerr x2 \<and> x2 = Rraise x1 \<longrightarrow>
           clock (fst (fun_evaluate_match (st'::'astate) (env::'vsemv_env) x1 (pes::('pat \<times> 'exp0) list) x1))
           \<le> clock st'"
      shows "((r::('v list, 'v) result) = Rerr (x2::'v error_result) \<longrightarrow>
            clock
             (fst (case x2 of
                   Rraise (v2::'v) \<Rightarrow>
                     fun_evaluate_match (st'::'astate) (env::'vsemv_env) v2 (pes::('pat \<times> 'exp0) list) v2
                   | Rabort (abort::abort) \<Rightarrow> (st', Rerr (Rabort abort))))
            \<le> clock (st::'astate)) "
   using assms by (smt (verit))
 end
 
 
 context
   fixes piecewise_C1 :: "('real :: {one,zero,ord} \<Rightarrow> 'a :: {one,zero,ord}) \<Rightarrow> 'real set \<Rightarrow> bool"  and
      joinpaths :: "('real \<Rightarrow> 'a) \<Rightarrow> ('real \<Rightarrow> 'a) \<Rightarrow> 'real \<Rightarrow> 'a"
 begin
 notation piecewise_C1 (infixr "piecewise'_C1'_differentiable'_on" 50)
 notation joinpaths (infixr "+++" 75)
 
 lemma
    \<open>(\<And>v1. \<forall>v0. (rec_join v0 = v1 \<and>
                (v0 = [] \<and> (\<lambda>uu. 0) = v1 \<longrightarrow> False) \<and>
                (\<forall>v2. v0 = [v2] \<and> v1 = coeff_cube_to_path v2 \<longrightarrow> False) \<and>
                (\<forall>v2 v3 v4.
                    v0 = v2 # v3 # v4 \<and> v1 = coeff_cube_to_path v2 +++ rec_join (v3 # v4) \<longrightarrow> False) \<longrightarrow>
                False) =
               (rec_join v0 = rec_join v0 \<and>
                (v0 = [] \<and> (\<lambda>uu. 0) = rec_join v0 \<longrightarrow> False) \<and>
                (\<forall>v2. v0 = [v2] \<and> rec_join v0 = coeff_cube_to_path v2 \<longrightarrow> False) \<and>
                (\<forall>v2 v3 v4.
                    v0 = v2 # v3 # v4 \<and> rec_join v0 = coeff_cube_to_path v2 +++ rec_join (v3 # v4) \<longrightarrow>
                    False) \<longrightarrow>
                False)) \<Longrightarrow>
          (\<forall>v0 v1.
              rec_join v0 = v1 \<and>
              (v0 = [] \<and> (\<lambda>uu. 0) = v1 \<longrightarrow> False) \<and>
              (\<forall>v2. v0 = [v2] \<and> v1 = coeff_cube_to_path v2 \<longrightarrow> False) \<and>
              (\<forall>v2 v3 v4. v0 = v2 # v3 # v4 \<and> v1 = coeff_cube_to_path v2 +++ rec_join (v3 # v4) \<longrightarrow> False) \<longrightarrow>
              False) =
          (\<forall>v0. rec_join v0 = rec_join v0 \<and>
                (v0 = [] \<and> (\<lambda>uu. 0) = rec_join v0 \<longrightarrow> False) \<and>
                (\<forall>v2. v0 = [v2] \<and> rec_join v0 = coeff_cube_to_path v2 \<longrightarrow> False) \<and>
                (\<forall>v2 v3 v4.
                    v0 = v2 # v3 # v4 \<and> rec_join v0 = coeff_cube_to_path v2 +++ rec_join (v3 # v4) \<longrightarrow>
                    False) \<longrightarrow>
                False)\<close>
   by (smt (verit))
 
 end
 
 
 section \<open>Monomorphization examples\<close>
 
 definition Pred :: "'a \<Rightarrow> bool" where
   "Pred x = True"
 
 lemma poly_Pred: "Pred x \<and> (Pred [x] \<or> \<not> Pred [x])"
   by (simp add: Pred_def)
 
 lemma "Pred (1::int)"
   by (smt (verit) poly_Pred)
 
 axiomatization g :: "'a \<Rightarrow> nat"
 axiomatization where
   g1: "g (Some x) = g [x]" and
   g2: "g None = g []" and
   g3: "g xs = length xs"
 
 lemma "g (Some (3::int)) = g (Some True)" by (smt (verit) g1 g2 g3 list.size)
 
 end
\ No newline at end of file
diff --git a/src/HOL/SMT_Examples/SMT_Word_Examples.certs b/src/HOL/SMT_Examples/SMT_Word_Examples.certs
--- a/src/HOL/SMT_Examples/SMT_Word_Examples.certs
+++ b/src/HOL/SMT_Examples/SMT_Word_Examples.certs
@@ -1,747 +1,365 @@
-8e6fd56de8adc20c29f4bdb8c2c55e63988185a8 8 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x38 (monotonicity (rewrite (= (bvneg (_ bv5 4)) (_ bv11 4))) (= (= (_ bv11 4) (bvneg (_ bv5 4))) (= (_ bv11 4) (_ bv11 4))))))
-(let ((@x42 (trans @x38 (rewrite (= (= (_ bv11 4) (_ bv11 4)) true)) (= (= (_ bv11 4) (bvneg (_ bv5 4))) true))))
-(let ((@x49 (trans (monotonicity @x42 (= (not (= (_ bv11 4) (bvneg (_ bv5 4)))) (not true))) (rewrite (= (not true) false)) (= (not (= (_ bv11 4) (bvneg (_ bv5 4)))) false))))
-(mp (asserted (not (= (_ bv11 4) (bvneg (_ bv5 4))))) @x49 false))))))
-
-aa1cdd144e99278cb2bdb51d68a75ec8d25b433d 7 0
+152f808e76881b6ae41a49c63654f988bc675b52 7 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((@x35 (monotonicity (rewrite (= (= (_ bv11 4) (_ bv11 4)) true)) (= (not (= (_ bv11 4) (_ bv11 4))) (not true)))))
 (let ((@x39 (trans @x35 (rewrite (= (not true) false)) (= (not (= (_ bv11 4) (_ bv11 4))) false))))
 (mp (asserted (not (= (_ bv11 4) (_ bv11 4)))) @x39 false)))))
 
-a14afea8a52a1586ff44eff03b88f1717144d17a 7 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x38 (monotonicity (rewrite (= (bvult (_ bv23 8) (_ bv27 8)) true)) (= (not (bvult (_ bv23 8) (_ bv27 8))) (not true)))))
-(let ((@x42 (trans @x38 (rewrite (= (not true) false)) (= (not (bvult (_ bv23 8) (_ bv27 8))) false))))
-(mp (asserted (not (bvult (_ bv23 8) (_ bv27 8)))) @x42 false)))))
-
-282d94be68c87485ea9ec13e80f6f2a51b18f5bd 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x38 (monotonicity (rewrite (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5))) (= (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5)) (= (_ bv6 5) (_ bv6 5))))))
-(let ((@x42 (trans @x38 (rewrite (= (= (_ bv6 5) (_ bv6 5)) true)) (= (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5)) true))))
-(let ((@x45 (monotonicity @x42 (= (not (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5))) (not true)))))
-(let ((@x49 (trans @x45 (rewrite (= (not true) false)) (= (not (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5))) false))))
-(mp (asserted (not (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5)))) @x49 false)))))))
-
-4df99826f79b2c96079a4c58ea51a58b8cc6199c 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x38 (monotonicity (rewrite (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) (= (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)) (= (_ bv21 8) (_ bv21 8))))))
-(let ((@x42 (trans @x38 (rewrite (= (= (_ bv21 8) (_ bv21 8)) true)) (= (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)) true))))
-(let ((@x45 (monotonicity @x42 (= (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) (not true)))))
-(let ((@x49 (trans @x45 (rewrite (= (not true) false)) (= (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) false))))
-(mp (asserted (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)))) @x49 false)))))))
-
-45bf9e0a746f7dde46f8242e5851928c2671c7f2 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x43 (monotonicity (rewrite (= (bvsub (_ bv11 8) (_ bv27 8)) (_ bv240 8))) (rewrite (= (bvneg (_ bv16 8)) (_ bv240 8))) (= (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))) (= (_ bv240 8) (_ bv240 8))))))
-(let ((@x47 (trans @x43 (rewrite (= (= (_ bv240 8) (_ bv240 8)) true)) (= (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))) true))))
-(let ((@x50 (monotonicity @x47 (= (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8)))) (not true)))))
-(let ((@x54 (trans @x50 (rewrite (= (not true) false)) (= (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8)))) false))))
-(mp (asserted (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))))) @x54 false)))))))
-
-6dd848d7b26e0521039e21a5e2bafebc1fee8c9b 7 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x35 (monotonicity (rewrite (= (= (_ bv11 5) (_ bv11 5)) true)) (= (not (= (_ bv11 5) (_ bv11 5))) (not true)))))
-(let ((@x39 (trans @x35 (rewrite (= (not true) false)) (= (not (= (_ bv11 5) (_ bv11 5))) false))))
-(mp (asserted (not (= (_ bv11 5) (_ bv11 5)))) @x39 false)))))
-
-00a7ff287d9c23d984163ea8e0cac8ac61008afd 11 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x42 (monotonicity (rewrite (= (bvneg (_ bv40 7)) (_ bv88 7))) (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvadd (_ bv88 7) (_ bv1 7))))))
-(let ((@x47 (trans @x42 (rewrite (= (bvadd (_ bv88 7) (_ bv1 7)) (_ bv89 7))) (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (_ bv89 7)))))
-(let ((@x52 (monotonicity @x47 (rewrite (= (bvneg (_ bv39 7)) (_ bv89 7))) (= (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7))) (= (_ bv89 7) (_ bv89 7))))))
-(let ((@x56 (trans @x52 (rewrite (= (= (_ bv89 7) (_ bv89 7)) true)) (= (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7))) true))))
-(let ((@x59 (monotonicity @x56 (= (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7)))) (not true)))))
-(let ((@x63 (trans @x59 (rewrite (= (not true) false)) (= (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7)))) false))))
-(mp (asserted (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7))))) @x63 false)))))))))
-
-9673ca576ccae343db48aa68f876fd3a2515cc33 19 0
-unsat
-((set-logic <null>)
-(proof
-(let ((?x35 (bvadd b$ c$)))
-(let ((?x36 (bvadd ?x35 a$)))
-(let ((?x30 (bvmul (_ bv2 32) b$)))
-(let ((?x31 (bvadd a$ ?x30)))
-(let ((?x33 (bvadd ?x31 c$)))
-(let ((?x34 (bvsub ?x33 b$)))
-(let (($x37 (= ?x34 ?x36)))
-(let (($x38 (not $x37)))
-(let ((@x58 (rewrite (= (= (bvadd a$ b$ c$) (bvadd a$ b$ c$)) true))))
-(let ((@x48 (rewrite (= (bvsub (bvadd a$ ?x30 c$) b$) (bvadd a$ b$ c$)))))
-(let ((@x46 (monotonicity (rewrite (= ?x33 (bvadd a$ ?x30 c$))) (= ?x34 (bvsub (bvadd a$ ?x30 c$) b$)))))
-(let ((@x56 (monotonicity (trans @x46 @x48 (= ?x34 (bvadd a$ b$ c$))) (rewrite (= ?x36 (bvadd a$ b$ c$))) (= $x37 (= (bvadd a$ b$ c$) (bvadd a$ b$ c$))))))
-(let ((@x63 (monotonicity (trans @x56 @x58 (= $x37 true)) (= $x38 (not true)))))
-(let ((@x67 (trans @x63 (rewrite (= (not true) false)) (= $x38 false))))
-(mp (asserted $x38) @x67 false)))))))))))))))))
-
-b4600e6d14c88b633ac7bcc5b2e24af8539b0218 18 0
-unsat
-((set-logic <null>)
-(proof
-(let ((?x31 (bvmul (_ bv4 4) x$)))
-(let (($x32 (= ?x31 (_ bv4 4))))
-(let (($x43 (= (_ bv5 4) x$)))
-(let (($x56 (not (or (not $x43) (= (_ bv4 4) ?x31)))))
-(let ((@x48 (monotonicity (rewrite (= (= x$ (_ bv5 4)) $x43)) (= (not (= x$ (_ bv5 4))) (not $x43)))))
-(let ((@x55 (monotonicity @x48 (rewrite (= $x32 (= (_ bv4 4) ?x31))) (= (or (not (= x$ (_ bv5 4))) $x32) (or (not $x43) (= (_ bv4 4) ?x31))))))
-(let (($x34 (not (=> (= x$ (_ bv5 4)) $x32))))
-(let ((@x39 (rewrite (= (=> (= x$ (_ bv5 4)) $x32) (or (not (= x$ (_ bv5 4))) $x32)))))
-(let ((@x60 (trans (monotonicity @x39 (= $x34 (not (or (not (= x$ (_ bv5 4))) $x32)))) (monotonicity @x55 (= (not (or (not (= x$ (_ bv5 4))) $x32)) $x56)) (= $x34 $x56))))
-(let ((@x67 (monotonicity (not-or-elim (mp (asserted $x34) @x60 $x56) $x43) (= ?x31 (bvmul (_ bv4 4) (_ bv5 4))))))
-(let ((@x73 (monotonicity (trans @x67 (rewrite (= (bvmul (_ bv4 4) (_ bv5 4)) (_ bv4 4))) $x32) (= (= (_ bv4 4) ?x31) (= (_ bv4 4) (_ bv4 4))))))
-(let ((@x77 (trans @x73 (rewrite (= (= (_ bv4 4) (_ bv4 4)) true)) (= (= (_ bv4 4) ?x31) true))))
-(let ((@x84 (trans (monotonicity @x77 (= (not (= (_ bv4 4) ?x31)) (not true))) (rewrite (= (not true) false)) (= (not (= (_ bv4 4) ?x31)) false))))
-(mp (not-or-elim (mp (asserted $x34) @x60 $x56) (not (= (_ bv4 4) ?x31))) @x84 false))))))))))))))))
-
-d150015a66b6757a72346710966844993c0f3c27 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x37 (monotonicity (rewrite (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) (= (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)) (= (_ bv4 32) (_ bv4 32))))))
-(let ((@x41 (trans @x37 (rewrite (= (= (_ bv4 32) (_ bv4 32)) true)) (= (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)) true))))
-(let ((@x44 (monotonicity @x41 (= (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) (not true)))))
-(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) false))))
-(mp (asserted (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)))) @x48 false)))))))
-
-200e29aa9f19844d244c5c9755155eb956c5cf7c 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x37 (monotonicity (rewrite (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8))) (= (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8)) (= (_ bv7 8) (_ bv7 8))))))
-(let ((@x41 (trans @x37 (rewrite (= (= (_ bv7 8) (_ bv7 8)) true)) (= (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8)) true))))
-(let ((@x44 (monotonicity @x41 (= (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8))) (not true)))))
-(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8))) false))))
-(mp (asserted (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8)))) @x48 false)))))))
-
-d7cc0827eb340c29b0f489145022e4b3e3610818 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x37 (monotonicity (rewrite (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) (= (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)) (= (_ bv15 8) (_ bv15 8))))))
-(let ((@x41 (trans @x37 (rewrite (= (= (_ bv15 8) (_ bv15 8)) true)) (= (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)) true))))
-(let ((@x44 (monotonicity @x41 (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) (not true)))))
-(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) false))))
-(mp (asserted (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)))) @x48 false)))))))
-
-3838eb33edcd292c3a0ecbf1662b54af3940189f 8 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x36 (monotonicity (rewrite (= (bvnot (_ bv240 16)) (_ bv65295 16))) (= (= (bvnot (_ bv240 16)) (_ bv65295 16)) (= (_ bv65295 16) (_ bv65295 16))))))
-(let ((@x40 (trans @x36 (rewrite (= (= (_ bv65295 16) (_ bv65295 16)) true)) (= (= (bvnot (_ bv240 16)) (_ bv65295 16)) true))))
-(let ((@x47 (trans (monotonicity @x40 (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) (not true))) (rewrite (= (not true) false)) (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) false))))
-(mp (asserted (not (= (bvnot (_ bv240 16)) (_ bv65295 16)))) @x47 false))))))
-
-14431ccb33137348161eb6ca6cfb2e57942c3f9d 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x37 (monotonicity (rewrite (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) (= (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)) (= (_ bv2843 12) (_ bv2843 12))))))
-(let ((@x41 (trans @x37 (rewrite (= (= (_ bv2843 12) (_ bv2843 12)) true)) (= (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)) true))))
-(let ((@x44 (monotonicity @x41 (= (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) (not true)))))
-(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) false))))
-(mp (asserted (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)))) @x48 false)))))))
-
-880bee16a8f6469b14122277b92e87533ef6a071 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x37 (monotonicity (rewrite (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) (= (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)) (= (_ bv207 10) (_ bv207 10))))))
-(let ((@x41 (trans @x37 (rewrite (= (= (_ bv207 10) (_ bv207 10)) true)) (= (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)) true))))
-(let ((@x44 (monotonicity @x41 (= (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) (not true)))))
-(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) false))))
-(mp (asserted (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)))) @x48 false)))))))
-
-b48f55cefc567df166d8e9967c53372c30620183 8 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x36 (monotonicity (rewrite (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) (= (_ bv3 2) (_ bv3 2))))))
-(let ((@x40 (trans @x36 (rewrite (= (= (_ bv3 2) (_ bv3 2)) true)) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) true))))
-(let ((@x47 (trans (monotonicity @x40 (= (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) (not true))) (rewrite (= (not true) false)) (= (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) false))))
-(mp (asserted (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)))) @x47 false))))))
-
-446b3cb9d63aa1f488dc092ed3fb111d2ad50b4e 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x36 (monotonicity (rewrite (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10))) (= (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10)) (= (_ bv10 10) (_ bv10 10))))))
-(let ((@x40 (trans @x36 (rewrite (= (= (_ bv10 10) (_ bv10 10)) true)) (= (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10)) true))))
-(let ((@x43 (monotonicity @x40 (= (not (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10))) (not true)))))
-(let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10))) false))))
-(mp (asserted (not (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10)))) @x47 false)))))))
-
-956d8b6229140c8c4aa869ab0f3765697ab8ff25 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x36 (monotonicity (rewrite (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) (= (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)) (= (_ bv58 6) (_ bv58 6))))))
-(let ((@x40 (trans @x36 (rewrite (= (= (_ bv58 6) (_ bv58 6)) true)) (= (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)) true))))
-(let ((@x43 (monotonicity @x40 (= (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) (not true)))))
-(let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) false))))
-(mp (asserted (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)))) @x47 false)))))))
-
-24e98aaba1a95c03812c938201b3faa04d97c341 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x37 (monotonicity (rewrite (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) (= (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)) (= (_ bv76 8) (_ bv76 8))))))
-(let ((@x41 (trans @x37 (rewrite (= (= (_ bv76 8) (_ bv76 8)) true)) (= (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)) true))))
-(let ((@x44 (monotonicity @x41 (= (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) (not true)))))
-(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) false))))
-(mp (asserted (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)))) @x48 false)))))))
-
-c13d08f3c98afca39a5c9317ed8ca7b7d4e35b5a 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x37 (monotonicity (rewrite (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) (= (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)) (= (_ bv6 8) (_ bv6 8))))))
-(let ((@x41 (trans @x37 (rewrite (= (= (_ bv6 8) (_ bv6 8)) true)) (= (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)) true))))
-(let ((@x44 (monotonicity @x41 (= (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) (not true)))))
-(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) false))))
-(mp (asserted (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)))) @x48 false)))))))
-
-053f04ff749dbee44bfba8828181ab0a78473f75 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x37 (monotonicity (rewrite (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) (= (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)) (= (_ bv4 8) (_ bv4 8))))))
-(let ((@x41 (trans @x37 (rewrite (= (= (_ bv4 8) (_ bv4 8)) true)) (= (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)) true))))
-(let ((@x44 (monotonicity @x41 (= (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) (not true)))))
-(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) false))))
-(mp (asserted (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)))) @x48 false)))))))
-
-42de7906f9755bf3d790213172b0ec7fab46237c 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x36 (monotonicity (rewrite (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4))) (= (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4)) (= (_ bv9 4) (_ bv9 4))))))
-(let ((@x40 (trans @x36 (rewrite (= (= (_ bv9 4) (_ bv9 4)) true)) (= (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4)) true))))
-(let ((@x43 (monotonicity @x40 (= (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4))) (not true)))))
-(let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4))) false))))
-(mp (asserted (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4)))) @x47 false)))))))
-
-6b83b0b418738896f8c64ad12f5670cb5bf96e0f 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x36 (monotonicity (rewrite (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) (= (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)) (= (_ bv13 4) (_ bv13 4))))))
-(let ((@x40 (trans @x36 (rewrite (= (= (_ bv13 4) (_ bv13 4)) true)) (= (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)) true))))
-(let ((@x43 (monotonicity @x40 (= (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) (not true)))))
-(let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) false))))
-(mp (asserted (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)))) @x47 false)))))))
-
-5c4e275bed2d91897e820ccd6744b0a775a6e26e 17 0
-unsat
-((set-logic <null>)
-(proof
-(let ((?x31 (bvand x$ (_ bv255 16))))
-(let ((?x29 (bvand x$ (_ bv65280 16))))
-(let ((?x32 (bvor ?x29 ?x31)))
-(let (($x33 (= ?x32 x$)))
-(let (($x34 (not $x33)))
-(let ((@x59 (symm (commutativity (= (= x$ ?x32) $x33)) (= $x33 (= x$ ?x32)))))
-(let ((@x35 (asserted $x34)))
-(let ((@x63 (mp @x35 (monotonicity @x59 (= $x34 (not (= x$ ?x32)))) (not (= x$ ?x32)))))
-(let (($x52 (= x$ ?x32)))
-(let ((@x26 (true-axiom true)))
-(let (($x53 (or $x52 false false false false false false false false false false false false false false false false)))
-(let ((@x55 (unit-resolution ((_ th-lemma bv) $x53) @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 $x52)))
-(unit-resolution @x55 @x63 false)))))))))))))))
-
-1d4a0e2a4449a8adbcf5a134bf7f2b0ee940d954 51 0
-unsat
-((set-logic <null>)
-(proof
-(let ((?x31 (bvand w$ (_ bv255 16))))
-(let (($x32 (= ?x31 w$)))
-(let (($x64 (not $x32)))
-(let ((@x318 (symm (commutativity (= (= w$ ?x31) $x32)) (= $x32 (= w$ ?x31)))))
-(let (($x57 (not (or (bvule (_ bv256 16) w$) $x32))))
-(let ((@x49 (monotonicity (rewrite (= (bvult w$ (_ bv256 16)) (not (bvule (_ bv256 16) w$)))) (= (not (bvult w$ (_ bv256 16))) (not (not (bvule (_ bv256 16) w$)))))))
-(let ((@x53 (trans @x49 (rewrite (= (not (not (bvule (_ bv256 16) w$))) (bvule (_ bv256 16) w$))) (= (not (bvult w$ (_ bv256 16))) (bvule (_ bv256 16) w$)))))
-(let ((@x56 (monotonicity @x53 (= (or (not (bvult w$ (_ bv256 16))) $x32) (or (bvule (_ bv256 16) w$) $x32)))))
-(let ((@x59 (monotonicity @x56 (= (not (or (not (bvult w$ (_ bv256 16))) $x32)) $x57))))
-(let (($x34 (not (=> (bvult w$ (_ bv256 16)) $x32))))
-(let ((@x39 (rewrite (= (=> (bvult w$ (_ bv256 16)) $x32) (or (not (bvult w$ (_ bv256 16))) $x32)))))
-(let ((@x42 (monotonicity @x39 (= $x34 (not (or (not (bvult w$ (_ bv256 16))) $x32))))))
-(let ((@x65 (not-or-elim (mp (asserted $x34) (trans @x42 @x59 (= $x34 $x57)) $x57) $x64)))
-(let ((@x322 (mp @x65 (monotonicity @x318 (= $x64 (not (= w$ ?x31)))) (not (= w$ ?x31)))))
-(let (($x300 (= w$ ?x31)))
-(let (($x81 (= ((_ extract 15 15) w$) (_ bv1 1))))
-(let (($x264 (not $x81)))
-(let (($x74 (= ((_ extract 8 8) w$) (_ bv1 1))))
-(let (($x75 (= ((_ extract 9 9) w$) (_ bv1 1))))
-(let (($x82 (and $x75 $x74)))
-(let (($x83 (or $x75 $x74 $x82)))
-(let (($x76 (= ((_ extract 10 10) w$) (_ bv1 1))))
-(let (($x84 (and $x76 $x83)))
-(let (($x85 (or $x76 $x75 $x74 $x82 $x84)))
-(let (($x77 (= ((_ extract 11 11) w$) (_ bv1 1))))
-(let (($x86 (and $x77 $x85)))
-(let (($x87 (or $x77 $x76 $x75 $x74 $x82 $x84 $x86)))
-(let (($x78 (= ((_ extract 12 12) w$) (_ bv1 1))))
-(let (($x88 (and $x78 $x87)))
-(let (($x89 (or $x78 $x77 $x76 $x75 $x74 $x82 $x84 $x86 $x88)))
-(let (($x79 (= ((_ extract 13 13) w$) (_ bv1 1))))
-(let (($x90 (and $x79 $x89)))
-(let (($x91 (or $x79 $x78 $x77 $x76 $x75 $x74 $x82 $x84 $x86 $x88 $x90)))
-(let (($x80 (= ((_ extract 14 14) w$) (_ bv1 1))))
-(let (($x92 (and $x80 $x91)))
-(let (($x93 (or $x80 $x79 $x78 $x77 $x76 $x75 $x74 $x82 $x84 $x86 $x88 $x90 $x92)))
-(let (($x94 (and $x81 $x93)))
-(let (($x95 (or $x81 $x80 $x79 $x78 $x77 $x76 $x75 $x74 $x82 $x84 $x86 $x88 $x90 $x92 $x94)))
-(let (($x297 (not $x95)))
-(let (($x43 (bvule (_ bv256 16) w$)))
-(let (($x44 (not $x43)))
-(let ((@x63 (not-or-elim (mp (asserted $x34) (trans @x42 @x59 (= $x34 $x57)) $x57) $x44)))
-(let ((@x303 (unit-resolution ((_ th-lemma bv) (or $x43 $x297)) @x63 $x297)))
-(let ((@x26 (true-axiom true)))
-(let (($x312 (or $x300 false false false false false false false false $x74 $x75 $x76 $x77 $x78 $x79 $x80 $x81)))
-(let ((@x314 (unit-resolution ((_ th-lemma bv) $x312) @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 (unit-resolution (def-axiom (or $x95 (not $x74))) @x303 (not $x74)) (unit-resolution (def-axiom (or $x95 (not $x75))) @x303 (not $x75)) (unit-resolution (def-axiom (or $x95 (not $x76))) @x303 (not $x76)) (unit-resolution (def-axiom (or $x95 (not $x77))) @x303 (not $x77)) (unit-resolution (def-axiom (or $x95 (not $x78))) @x303 (not $x78)) (unit-resolution (def-axiom (or $x95 (not $x79))) @x303 (not $x79)) (unit-resolution (def-axiom (or $x95 (not $x80))) @x303 (not $x80)) (unit-resolution (def-axiom (or $x95 $x264)) @x303 $x264) $x300)))
-(unit-resolution @x314 @x322 false)))))))))))))))))))))))))))))))))))))))))))))))))
-
-115ab22c9945d493b971e69a38d9e608c5b40a71 29 0
-unsat
-((set-logic <null>)
-(proof
-(let ((?x28 (bv2int$ (_ bv0 2))))
-(let (($x183 (<= ?x28 0)))
-(let (($x184 (not $x183)))
-(let (($x175 (forall ((?v0 (_ BitVec 2)) )(! (let ((?x47 (bv2int$ ?v0)))
-(let (($x53 (<= ?x47 0)))
-(not $x53))) :pattern ( (bv2int$ ?v0) ) :qid k!9))
-))
-(let (($x57 (forall ((?v0 (_ BitVec 2)) )(! (let ((?x47 (bv2int$ ?v0)))
-(let (($x53 (<= ?x47 0)))
-(not $x53))) :qid k!9))
-))
-(let ((@x177 (refl (= (not (<= (bv2int$ ?0) 0)) (not (<= (bv2int$ ?0) 0))))))
-(let ((@x112 (refl (~ (not (<= (bv2int$ ?0) 0)) (not (<= (bv2int$ ?0) 0))))))
-(let (($x49 (forall ((?v0 (_ BitVec 2)) )(! (let ((?x47 (bv2int$ ?v0)))
-(< 0 ?x47)) :qid k!9))
-))
-(let ((@x56 (rewrite (= (< 0 (bv2int$ ?0)) (not (<= (bv2int$ ?0) 0))))))
-(let ((@x115 (mp~ (mp (asserted $x49) (quant-intro @x56 (= $x49 $x57)) $x57) (nnf-pos @x112 (~ $x57 $x57)) $x57)))
-(let ((@x180 (mp @x115 (quant-intro @x177 (= $x57 $x175)) $x175)))
-(let (($x187 (not $x175)))
-(let (($x188 (or $x187 $x184)))
-(let ((@x189 ((_ quant-inst (_ bv0 2)) $x188)))
-(let (($x29 (= ?x28 0)))
-(let ((@x30 (asserted $x29)))
-(unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x29) $x183)) @x30 (unit-resolution @x189 @x180 $x184) false)))))))))))))))))))
-
-d14e7b8f0d1858316e700b4eb09e7d03e57cf9c3 16 0
-unsat
-((set-logic <null>)
-(proof
-(let ((?x32 (p$ true)))
-(let (($x29 (bvule (_ bv0 4) a$)))
-(let (($x30 (ite $x29 true false)))
-(let ((?x31 (p$ $x30)))
-(let (($x33 (= ?x31 ?x32)))
-(let (($x34 (not $x33)))
-(let ((@x52 (monotonicity (monotonicity (rewrite (= $x29 true)) (= (p$ $x29) ?x32)) (= (= (p$ $x29) ?x32) (= ?x32 ?x32)))))
-(let ((@x56 (trans @x52 (rewrite (= (= ?x32 ?x32) true)) (= (= (p$ $x29) ?x32) true))))
-(let ((@x63 (trans (monotonicity @x56 (= (not (= (p$ $x29) ?x32)) (not true))) (rewrite (= (not true) false)) (= (not (= (p$ $x29) ?x32)) false))))
-(let ((@x43 (monotonicity (monotonicity (rewrite (= $x30 $x29)) (= ?x31 (p$ $x29))) (= $x33 (= (p$ $x29) ?x32)))))
-(let ((@x46 (monotonicity @x43 (= $x34 (not (= (p$ $x29) ?x32))))))
-(mp (asserted $x34) (trans @x46 @x63 (= $x34 false)) false))))))))))))))
-
-6182523304a5597432fa1bb8dd16e804ddd8d7ee 12 0
-unsat
-((set-logic <null>)
-(proof
-(let ((?x31 (p$ true)))
-(let (($x29 (bvule (_ bv0 4) a$)))
-(let ((?x30 (p$ $x29)))
-(let (($x32 (= ?x30 ?x31)))
-(let ((@x42 (monotonicity (monotonicity (rewrite (= $x29 true)) $x32) (= $x32 (= ?x31 ?x31)))))
-(let ((@x49 (monotonicity (trans @x42 (rewrite (= (= ?x31 ?x31) true)) (= $x32 true)) (= (not $x32) (not true)))))
-(let ((@x53 (trans @x49 (rewrite (= (not true) false)) (= (not $x32) false))))
-(mp (asserted (not $x32)) @x53 false))))))))))
-
-9f7a96d88c6326ad836384c37d13934828ff726d 8 0
+9fbec967ab26119b905e134e9f6da22a94ff68aa 8 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((@x38 (monotonicity (rewrite (= (bvneg (_ bv5 4)) (_ bv11 4))) (= (= (_ bv11 4) (bvneg (_ bv5 4))) (= (_ bv11 4) (_ bv11 4))))))
 (let ((@x42 (trans @x38 (rewrite (= (= (_ bv11 4) (_ bv11 4)) true)) (= (= (_ bv11 4) (bvneg (_ bv5 4))) true))))
 (let ((@x49 (trans (monotonicity @x42 (= (not (= (_ bv11 4) (bvneg (_ bv5 4)))) (not true))) (rewrite (= (not true) false)) (= (not (= (_ bv11 4) (bvneg (_ bv5 4)))) false))))
 (mp (asserted (not (= (_ bv11 4) (bvneg (_ bv5 4))))) @x49 false))))))
 
-6cad4ca9b92628993328e0c9cd5982fe4690567b 7 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x35 (monotonicity (rewrite (= (= (_ bv11 4) (_ bv11 4)) true)) (= (not (= (_ bv11 4) (_ bv11 4))) (not true)))))
-(let ((@x39 (trans @x35 (rewrite (= (not true) false)) (= (not (= (_ bv11 4) (_ bv11 4))) false))))
-(mp (asserted (not (= (_ bv11 4) (_ bv11 4)))) @x39 false)))))
-
 55b7bec34258b475381a754439390616488c924c 7 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((@x38 (monotonicity (rewrite (= (bvult (_ bv23 8) (_ bv27 8)) true)) (= (not (bvult (_ bv23 8) (_ bv27 8))) (not true)))))
 (let ((@x42 (trans @x38 (rewrite (= (not true) false)) (= (not (bvult (_ bv23 8) (_ bv27 8))) false))))
 (mp (asserted (not (bvult (_ bv23 8) (_ bv27 8)))) @x42 false)))))
 
 fa462c1327b4231dc12d6f379b9bb280ea17bfd3 9 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((@x38 (monotonicity (rewrite (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5))) (= (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5)) (= (_ bv6 5) (_ bv6 5))))))
 (let ((@x42 (trans @x38 (rewrite (= (= (_ bv6 5) (_ bv6 5)) true)) (= (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5)) true))))
 (let ((@x45 (monotonicity @x42 (= (not (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5))) (not true)))))
 (let ((@x49 (trans @x45 (rewrite (= (not true) false)) (= (not (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5))) false))))
 (mp (asserted (not (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5)))) @x49 false)))))))
 
 bf6c2eb2daf9373dd063355969e25afc57fc44fe 9 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((@x38 (monotonicity (rewrite (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) (= (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)) (= (_ bv21 8) (_ bv21 8))))))
 (let ((@x42 (trans @x38 (rewrite (= (= (_ bv21 8) (_ bv21 8)) true)) (= (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)) true))))
 (let ((@x45 (monotonicity @x42 (= (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) (not true)))))
 (let ((@x49 (trans @x45 (rewrite (= (not true) false)) (= (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) false))))
 (mp (asserted (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)))) @x49 false)))))))
 
 21dcbc62e4a0d275653bc7c57a948d4bf6975168 9 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((@x43 (monotonicity (rewrite (= (bvsub (_ bv11 8) (_ bv27 8)) (_ bv240 8))) (rewrite (= (bvneg (_ bv16 8)) (_ bv240 8))) (= (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))) (= (_ bv240 8) (_ bv240 8))))))
 (let ((@x47 (trans @x43 (rewrite (= (= (_ bv240 8) (_ bv240 8)) true)) (= (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))) true))))
 (let ((@x50 (monotonicity @x47 (= (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8)))) (not true)))))
 (let ((@x54 (trans @x50 (rewrite (= (not true) false)) (= (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8)))) false))))
 (mp (asserted (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))))) @x54 false)))))))
 
 6dd961e81bf75734a230f5a110b28edf98e90aaf 7 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((@x35 (monotonicity (rewrite (= (= (_ bv11 5) (_ bv11 5)) true)) (= (not (= (_ bv11 5) (_ bv11 5))) (not true)))))
 (let ((@x39 (trans @x35 (rewrite (= (not true) false)) (= (not (= (_ bv11 5) (_ bv11 5))) false))))
 (mp (asserted (not (= (_ bv11 5) (_ bv11 5)))) @x39 false)))))
 
 10d0fe43a5dca47373c59ffadf5d4a9049a8df88 11 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((@x42 (monotonicity (rewrite (= (bvneg (_ bv40 7)) (_ bv88 7))) (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvadd (_ bv88 7) (_ bv1 7))))))
 (let ((@x47 (trans @x42 (rewrite (= (bvadd (_ bv88 7) (_ bv1 7)) (_ bv89 7))) (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (_ bv89 7)))))
 (let ((@x52 (monotonicity @x47 (rewrite (= (bvneg (_ bv39 7)) (_ bv89 7))) (= (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7))) (= (_ bv89 7) (_ bv89 7))))))
 (let ((@x56 (trans @x52 (rewrite (= (= (_ bv89 7) (_ bv89 7)) true)) (= (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7))) true))))
 (let ((@x59 (monotonicity @x56 (= (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7)))) (not true)))))
 (let ((@x63 (trans @x59 (rewrite (= (not true) false)) (= (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7)))) false))))
 (mp (asserted (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7))))) @x63 false)))))))))
 
 de1bc26329091943d56ccf83cf9662c0b2001c97 19 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((?x35 (bvadd b$ c$)))
 (let ((?x36 (bvadd ?x35 a$)))
 (let ((?x30 (bvmul (_ bv2 32) b$)))
 (let ((?x31 (bvadd a$ ?x30)))
 (let ((?x33 (bvadd ?x31 c$)))
 (let ((?x34 (bvsub ?x33 b$)))
 (let (($x37 (= ?x34 ?x36)))
 (let (($x38 (not $x37)))
 (let ((@x58 (rewrite (= (= (bvadd a$ b$ c$) (bvadd a$ b$ c$)) true))))
 (let ((@x48 (rewrite (= (bvsub (bvadd a$ ?x30 c$) b$) (bvadd a$ b$ c$)))))
 (let ((@x46 (monotonicity (rewrite (= ?x33 (bvadd a$ ?x30 c$))) (= ?x34 (bvsub (bvadd a$ ?x30 c$) b$)))))
 (let ((@x56 (monotonicity (trans @x46 @x48 (= ?x34 (bvadd a$ b$ c$))) (rewrite (= ?x36 (bvadd a$ b$ c$))) (= $x37 (= (bvadd a$ b$ c$) (bvadd a$ b$ c$))))))
 (let ((@x63 (monotonicity (trans @x56 @x58 (= $x37 true)) (= $x38 (not true)))))
 (let ((@x67 (trans @x63 (rewrite (= (not true) false)) (= $x38 false))))
 (mp (asserted $x38) @x67 false)))))))))))))))))
 
 821acdf5acf235899fac29bcb5ad69c40cffe88f 18 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((?x31 (bvmul (_ bv4 4) x$)))
 (let (($x32 (= ?x31 (_ bv4 4))))
 (let (($x43 (= (_ bv5 4) x$)))
 (let (($x56 (not (or (not $x43) (= (_ bv4 4) ?x31)))))
 (let ((@x48 (monotonicity (rewrite (= (= x$ (_ bv5 4)) $x43)) (= (not (= x$ (_ bv5 4))) (not $x43)))))
 (let ((@x55 (monotonicity @x48 (rewrite (= $x32 (= (_ bv4 4) ?x31))) (= (or (not (= x$ (_ bv5 4))) $x32) (or (not $x43) (= (_ bv4 4) ?x31))))))
 (let (($x34 (not (=> (= x$ (_ bv5 4)) $x32))))
 (let ((@x39 (rewrite (= (=> (= x$ (_ bv5 4)) $x32) (or (not (= x$ (_ bv5 4))) $x32)))))
 (let ((@x60 (trans (monotonicity @x39 (= $x34 (not (or (not (= x$ (_ bv5 4))) $x32)))) (monotonicity @x55 (= (not (or (not (= x$ (_ bv5 4))) $x32)) $x56)) (= $x34 $x56))))
 (let ((@x67 (monotonicity (not-or-elim (mp (asserted $x34) @x60 $x56) $x43) (= ?x31 (bvmul (_ bv4 4) (_ bv5 4))))))
 (let ((@x73 (monotonicity (trans @x67 (rewrite (= (bvmul (_ bv4 4) (_ bv5 4)) (_ bv4 4))) $x32) (= (= (_ bv4 4) ?x31) (= (_ bv4 4) (_ bv4 4))))))
 (let ((@x77 (trans @x73 (rewrite (= (= (_ bv4 4) (_ bv4 4)) true)) (= (= (_ bv4 4) ?x31) true))))
 (let ((@x84 (trans (monotonicity @x77 (= (not (= (_ bv4 4) ?x31)) (not true))) (rewrite (= (not true) false)) (= (not (= (_ bv4 4) ?x31)) false))))
 (mp (not-or-elim (mp (asserted $x34) @x60 $x56) (not (= (_ bv4 4) ?x31))) @x84 false))))))))))))))))
 
 fb4d74278af64850ed8084451a8ff7a7075dbdfe 9 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((@x37 (monotonicity (rewrite (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) (= (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)) (= (_ bv4 32) (_ bv4 32))))))
 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv4 32) (_ bv4 32)) true)) (= (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)) true))))
 (let ((@x44 (monotonicity @x41 (= (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) (not true)))))
 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) false))))
 (mp (asserted (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)))) @x48 false)))))))
 
 5a9d6d65605763b3b0286a0d4717a93a4da85a34 9 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((@x37 (monotonicity (rewrite (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8))) (= (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8)) (= (_ bv7 8) (_ bv7 8))))))
 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv7 8) (_ bv7 8)) true)) (= (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8)) true))))
 (let ((@x44 (monotonicity @x41 (= (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8))) (not true)))))
 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8))) false))))
 (mp (asserted (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8)))) @x48 false)))))))
 
 71f993d99975ef37af8d8478a6f1c26548b6f4a7 9 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((@x37 (monotonicity (rewrite (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) (= (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)) (= (_ bv15 8) (_ bv15 8))))))
 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv15 8) (_ bv15 8)) true)) (= (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)) true))))
 (let ((@x44 (monotonicity @x41 (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) (not true)))))
 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) false))))
 (mp (asserted (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)))) @x48 false)))))))
 
 353b2591bd8c22d0df29b19faf56739aac7b9b6d 8 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((@x36 (monotonicity (rewrite (= (bvnot (_ bv240 16)) (_ bv65295 16))) (= (= (bvnot (_ bv240 16)) (_ bv65295 16)) (= (_ bv65295 16) (_ bv65295 16))))))
 (let ((@x40 (trans @x36 (rewrite (= (= (_ bv65295 16) (_ bv65295 16)) true)) (= (= (bvnot (_ bv240 16)) (_ bv65295 16)) true))))
 (let ((@x47 (trans (monotonicity @x40 (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) (not true))) (rewrite (= (not true) false)) (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) false))))
 (mp (asserted (not (= (bvnot (_ bv240 16)) (_ bv65295 16)))) @x47 false))))))
 
-f40271ef9e5c8b600036568090a9c30a30fba3c1 9 0
+88af7aeb0e9a24cb60cf70ebed32fe4a6b94a809 9 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((@x37 (monotonicity (rewrite (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) (= (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)) (= (_ bv2843 12) (_ bv2843 12))))))
 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv2843 12) (_ bv2843 12)) true)) (= (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)) true))))
 (let ((@x44 (monotonicity @x41 (= (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) (not true)))))
 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) false))))
 (mp (asserted (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)))) @x48 false)))))))
 
 98fd1bf6fea1dce9107b6a84cfa810d8ae0827ad 9 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((@x37 (monotonicity (rewrite (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) (= (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)) (= (_ bv207 10) (_ bv207 10))))))
 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv207 10) (_ bv207 10)) true)) (= (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)) true))))
 (let ((@x44 (monotonicity @x41 (= (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) (not true)))))
 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) false))))
 (mp (asserted (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)))) @x48 false)))))))
 
-f5796d75c7b1d8ea9a2c70c40ab57315660fbcf3 8 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x36 (monotonicity (rewrite (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) (= (_ bv3 2) (_ bv3 2))))))
-(let ((@x40 (trans @x36 (rewrite (= (= (_ bv3 2) (_ bv3 2)) true)) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) true))))
-(let ((@x47 (trans (monotonicity @x40 (= (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) (not true))) (rewrite (= (not true) false)) (= (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) false))))
-(mp (asserted (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)))) @x47 false))))))
-
 44630a6139544aa8cc936f2dcdd464d5967b2876 9 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((@x36 (monotonicity (rewrite (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10))) (= (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10)) (= (_ bv10 10) (_ bv10 10))))))
 (let ((@x40 (trans @x36 (rewrite (= (= (_ bv10 10) (_ bv10 10)) true)) (= (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10)) true))))
 (let ((@x43 (monotonicity @x40 (= (not (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10))) (not true)))))
 (let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10))) false))))
 (mp (asserted (not (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10)))) @x47 false)))))))
 
+36033c98ec9d88c28e82a4d5b423281f56a42859 8 0
+unsat
+((set-logic <null>)
+(proof
+(let ((@x36 (monotonicity (rewrite (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) (= (_ bv3 2) (_ bv3 2))))))
+(let ((@x40 (trans @x36 (rewrite (= (= (_ bv3 2) (_ bv3 2)) true)) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) true))))
+(let ((@x47 (trans (monotonicity @x40 (= (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) (not true))) (rewrite (= (not true) false)) (= (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) false))))
+(mp (asserted (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)))) @x47 false))))))
+
 2b91c33c03a89b80ac6fb984f384bd9814c2b51d 9 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((@x36 (monotonicity (rewrite (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) (= (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)) (= (_ bv58 6) (_ bv58 6))))))
 (let ((@x40 (trans @x36 (rewrite (= (= (_ bv58 6) (_ bv58 6)) true)) (= (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)) true))))
 (let ((@x43 (monotonicity @x40 (= (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) (not true)))))
 (let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) false))))
 (mp (asserted (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)))) @x47 false)))))))
 
 80e93d77c56b62b509cae750a834ba3c2a6545e3 9 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((@x37 (monotonicity (rewrite (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) (= (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)) (= (_ bv76 8) (_ bv76 8))))))
 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv76 8) (_ bv76 8)) true)) (= (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)) true))))
 (let ((@x44 (monotonicity @x41 (= (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) (not true)))))
 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) false))))
 (mp (asserted (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)))) @x48 false)))))))
 
 08e3a62c0a330f1ab742b05e694f723668925d10 9 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((@x37 (monotonicity (rewrite (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) (= (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)) (= (_ bv6 8) (_ bv6 8))))))
 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv6 8) (_ bv6 8)) true)) (= (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)) true))))
 (let ((@x44 (monotonicity @x41 (= (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) (not true)))))
 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) false))))
 (mp (asserted (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)))) @x48 false)))))))
 
+d1e9761fb935892f82a21268d39aac76f75ee282 9 0
+unsat
+((set-logic <null>)
+(proof
+(let ((@x37 (monotonicity (rewrite (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) (= (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)) (= (_ bv4 8) (_ bv4 8))))))
+(let ((@x41 (trans @x37 (rewrite (= (= (_ bv4 8) (_ bv4 8)) true)) (= (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)) true))))
+(let ((@x44 (monotonicity @x41 (= (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) (not true)))))
+(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) false))))
+(mp (asserted (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)))) @x48 false)))))))
+
 1b01af1c33961b4a329d46a526471313f71130ca 9 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((@x36 (monotonicity (rewrite (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4))) (= (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4)) (= (_ bv9 4) (_ bv9 4))))))
 (let ((@x40 (trans @x36 (rewrite (= (= (_ bv9 4) (_ bv9 4)) true)) (= (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4)) true))))
 (let ((@x43 (monotonicity @x40 (= (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4))) (not true)))))
 (let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4))) false))))
 (mp (asserted (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4)))) @x47 false)))))))
 
-d1e9761fb935892f82a21268d39aac76f75ee282 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x37 (monotonicity (rewrite (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) (= (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)) (= (_ bv4 8) (_ bv4 8))))))
-(let ((@x41 (trans @x37 (rewrite (= (= (_ bv4 8) (_ bv4 8)) true)) (= (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)) true))))
-(let ((@x44 (monotonicity @x41 (= (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) (not true)))))
-(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) false))))
-(mp (asserted (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)))) @x48 false)))))))
-
 a14e30a88e731b5e605d4726dbb1f583497ab894 9 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((@x36 (monotonicity (rewrite (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) (= (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)) (= (_ bv13 4) (_ bv13 4))))))
 (let ((@x40 (trans @x36 (rewrite (= (= (_ bv13 4) (_ bv13 4)) true)) (= (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)) true))))
 (let ((@x43 (monotonicity @x40 (= (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) (not true)))))
 (let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) false))))
 (mp (asserted (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)))) @x47 false)))))))
 
 08dd0af4f9cea470363f78957650260a900928c8 17 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((?x31 (bvand x$ (_ bv255 16))))
 (let ((?x29 (bvand x$ (_ bv65280 16))))
 (let ((?x32 (bvor ?x29 ?x31)))
 (let (($x33 (= ?x32 x$)))
 (let (($x34 (not $x33)))
 (let ((@x59 (symm (commutativity (= (= x$ ?x32) $x33)) (= $x33 (= x$ ?x32)))))
 (let ((@x35 (asserted $x34)))
 (let ((@x63 (mp @x35 (monotonicity @x59 (= $x34 (not (= x$ ?x32)))) (not (= x$ ?x32)))))
 (let (($x52 (= x$ ?x32)))
 (let ((@x26 (true-axiom true)))
 (let (($x53 (or $x52 false false false false false false false false false false false false false false false false)))
 (let ((@x55 (unit-resolution ((_ th-lemma bv) $x53) @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 $x52)))
 (unit-resolution @x55 @x63 false)))))))))))))))
 
 cffe711faa89f3f62e8e8e58173aaeb3cedc5d63 51 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((?x31 (bvand w$ (_ bv255 16))))
 (let (($x32 (= ?x31 w$)))
 (let (($x64 (not $x32)))
 (let ((@x318 (symm (commutativity (= (= w$ ?x31) $x32)) (= $x32 (= w$ ?x31)))))
 (let (($x57 (not (or (bvule (_ bv256 16) w$) $x32))))
 (let ((@x49 (monotonicity (rewrite (= (bvult w$ (_ bv256 16)) (not (bvule (_ bv256 16) w$)))) (= (not (bvult w$ (_ bv256 16))) (not (not (bvule (_ bv256 16) w$)))))))
 (let ((@x53 (trans @x49 (rewrite (= (not (not (bvule (_ bv256 16) w$))) (bvule (_ bv256 16) w$))) (= (not (bvult w$ (_ bv256 16))) (bvule (_ bv256 16) w$)))))
 (let ((@x56 (monotonicity @x53 (= (or (not (bvult w$ (_ bv256 16))) $x32) (or (bvule (_ bv256 16) w$) $x32)))))
 (let ((@x59 (monotonicity @x56 (= (not (or (not (bvult w$ (_ bv256 16))) $x32)) $x57))))
 (let (($x34 (not (=> (bvult w$ (_ bv256 16)) $x32))))
 (let ((@x39 (rewrite (= (=> (bvult w$ (_ bv256 16)) $x32) (or (not (bvult w$ (_ bv256 16))) $x32)))))
 (let ((@x42 (monotonicity @x39 (= $x34 (not (or (not (bvult w$ (_ bv256 16))) $x32))))))
 (let ((@x65 (not-or-elim (mp (asserted $x34) (trans @x42 @x59 (= $x34 $x57)) $x57) $x64)))
 (let ((@x322 (mp @x65 (monotonicity @x318 (= $x64 (not (= w$ ?x31)))) (not (= w$ ?x31)))))
 (let (($x300 (= w$ ?x31)))
 (let (($x81 (= ((_ extract 15 15) w$) (_ bv1 1))))
 (let (($x264 (not $x81)))
 (let (($x74 (= ((_ extract 8 8) w$) (_ bv1 1))))
 (let (($x75 (= ((_ extract 9 9) w$) (_ bv1 1))))
 (let (($x82 (and $x75 $x74)))
 (let (($x83 (or $x75 $x74 $x82)))
 (let (($x76 (= ((_ extract 10 10) w$) (_ bv1 1))))
 (let (($x84 (and $x76 $x83)))
 (let (($x85 (or $x76 $x75 $x74 $x82 $x84)))
 (let (($x77 (= ((_ extract 11 11) w$) (_ bv1 1))))
 (let (($x86 (and $x77 $x85)))
 (let (($x87 (or $x77 $x76 $x75 $x74 $x82 $x84 $x86)))
 (let (($x78 (= ((_ extract 12 12) w$) (_ bv1 1))))
 (let (($x88 (and $x78 $x87)))
 (let (($x89 (or $x78 $x77 $x76 $x75 $x74 $x82 $x84 $x86 $x88)))
 (let (($x79 (= ((_ extract 13 13) w$) (_ bv1 1))))
 (let (($x90 (and $x79 $x89)))
 (let (($x91 (or $x79 $x78 $x77 $x76 $x75 $x74 $x82 $x84 $x86 $x88 $x90)))
 (let (($x80 (= ((_ extract 14 14) w$) (_ bv1 1))))
 (let (($x92 (and $x80 $x91)))
 (let (($x93 (or $x80 $x79 $x78 $x77 $x76 $x75 $x74 $x82 $x84 $x86 $x88 $x90 $x92)))
 (let (($x94 (and $x81 $x93)))
 (let (($x95 (or $x81 $x80 $x79 $x78 $x77 $x76 $x75 $x74 $x82 $x84 $x86 $x88 $x90 $x92 $x94)))
 (let (($x297 (not $x95)))
 (let (($x43 (bvule (_ bv256 16) w$)))
 (let (($x44 (not $x43)))
 (let ((@x63 (not-or-elim (mp (asserted $x34) (trans @x42 @x59 (= $x34 $x57)) $x57) $x44)))
 (let ((@x303 (unit-resolution ((_ th-lemma bv) (or $x43 $x297)) @x63 $x297)))
 (let ((@x26 (true-axiom true)))
 (let (($x312 (or $x300 false false false false false false false false $x74 $x75 $x76 $x77 $x78 $x79 $x80 $x81)))
 (let ((@x314 (unit-resolution ((_ th-lemma bv) $x312) @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 (unit-resolution (def-axiom (or $x95 (not $x74))) @x303 (not $x74)) (unit-resolution (def-axiom (or $x95 (not $x75))) @x303 (not $x75)) (unit-resolution (def-axiom (or $x95 (not $x76))) @x303 (not $x76)) (unit-resolution (def-axiom (or $x95 (not $x77))) @x303 (not $x77)) (unit-resolution (def-axiom (or $x95 (not $x78))) @x303 (not $x78)) (unit-resolution (def-axiom (or $x95 (not $x79))) @x303 (not $x79)) (unit-resolution (def-axiom (or $x95 (not $x80))) @x303 (not $x80)) (unit-resolution (def-axiom (or $x95 $x264)) @x303 $x264) $x300)))
 (unit-resolution @x314 @x322 false)))))))))))))))))))))))))))))))))))))))))))))))))
 
 024e51ae2c856c79195e59dfbc39c68dcf8ab939 29 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((?x28 (bv2int$ (_ bv0 2))))
 (let (($x183 (<= ?x28 0)))
 (let (($x184 (not $x183)))
 (let (($x175 (forall ((?v0 (_ BitVec 2)) )(! (let ((?x47 (bv2int$ ?v0)))
 (let (($x53 (<= ?x47 0)))
 (not $x53))) :pattern ( (bv2int$ ?v0) ) :qid k!9))
 ))
 (let (($x57 (forall ((?v0 (_ BitVec 2)) )(! (let ((?x47 (bv2int$ ?v0)))
 (let (($x53 (<= ?x47 0)))
 (not $x53))) :qid k!9))
 ))
 (let ((@x177 (refl (= (not (<= (bv2int$ ?0) 0)) (not (<= (bv2int$ ?0) 0))))))
 (let ((@x112 (refl (~ (not (<= (bv2int$ ?0) 0)) (not (<= (bv2int$ ?0) 0))))))
 (let (($x49 (forall ((?v0 (_ BitVec 2)) )(! (let ((?x47 (bv2int$ ?v0)))
 (< 0 ?x47)) :qid k!9))
 ))
 (let ((@x56 (rewrite (= (< 0 (bv2int$ ?0)) (not (<= (bv2int$ ?0) 0))))))
 (let ((@x115 (mp~ (mp (asserted $x49) (quant-intro @x56 (= $x49 $x57)) $x57) (nnf-pos @x112 (~ $x57 $x57)) $x57)))
 (let ((@x180 (mp @x115 (quant-intro @x177 (= $x57 $x175)) $x175)))
 (let (($x187 (not $x175)))
 (let (($x188 (or $x187 $x184)))
 (let ((@x189 ((_ quant-inst (_ bv0 2)) $x188)))
 (let (($x29 (= ?x28 0)))
 (let ((@x30 (asserted $x29)))
 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x29) $x183)) @x30 (unit-resolution @x189 @x180 $x184) false)))))))))))))))))))
 
 20245d49b4c03da63c3124c5910beafc837f359a 12 0
 unsat
 ((set-logic <null>)
 (proof
 (let ((?x31 (p$ true)))
 (let (($x29 (bvule (_ bv0 4) a$)))
 (let ((?x30 (p$ $x29)))
 (let (($x32 (= ?x30 ?x31)))
 (let ((@x42 (monotonicity (monotonicity (rewrite (= $x29 true)) $x32) (= $x32 (= ?x31 ?x31)))))
 (let ((@x49 (monotonicity (trans @x42 (rewrite (= (= ?x31 ?x31) true)) (= $x32 true)) (= (not $x32) (not true)))))
 (let ((@x53 (trans @x49 (rewrite (= (not true) false)) (= (not $x32) false))))
 (mp (asserted (not $x32)) @x53 false))))))))))
 
diff --git a/src/HOL/Tools/SMT/smt_config.ML b/src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML
+++ b/src/HOL/Tools/SMT/smt_config.ML
@@ -1,287 +1,287 @@
 (*  Title:      HOL/Tools/SMT/smt_config.ML
     Author:     Sascha Boehme, TU Muenchen
 
 Configuration options and diagnostic tools for SMT.
 *)
 
 signature SMT_CONFIG =
 sig
   (*solver*)
   type solver_info = {
     name: string,
     class: Proof.context -> SMT_Util.class,
     avail: unit -> bool,
     options: Proof.context -> string list }
   val add_solver: solver_info -> Context.generic -> Context.generic
   val set_solver_options: string * string -> Context.generic -> Context.generic
   val is_available: Proof.context -> string -> bool
   val available_solvers_of: Proof.context -> string list
   val select_solver: string -> Context.generic -> Context.generic
   val solver_of: Proof.context -> string
   val solver_class_of: Proof.context -> SMT_Util.class
   val solver_options_of: Proof.context -> string list
 
   (*options*)
   val oracle: bool Config.T
   val timeout: real Config.T
   val reconstruction_step_timeout: real Config.T
   val random_seed: int Config.T
   val read_only_certificates: bool Config.T
   val verbose: bool Config.T
   val trace: bool Config.T
   val statistics: bool Config.T
   val monomorph_limit: int Config.T
   val monomorph_instances: int Config.T
   val explicit_application: int Config.T
   val higher_order: bool Config.T
   val nat_as_int: bool Config.T
   val infer_triggers: bool Config.T
   val debug_files: string Config.T
   val sat_solver: string Config.T
   val compress_verit_proofs: Proof.context -> bool
 
   (*tools*)
   val with_time_limit: Proof.context -> real Config.T -> ('a -> 'b) -> 'a -> 'b
   val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
 
   (*diagnostics*)
   val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
   val verbose_msg: Proof.context -> ('a -> string) -> 'a -> unit
   val statistics_msg: Proof.context -> ('a -> string) -> 'a -> unit
   val verit_msg: Proof.context -> (unit -> 'a) -> unit
   val verit_arith_msg: Proof.context -> (unit -> 'a) -> unit
   val spy_verit: Proof.context -> bool
   val spy_Z3: Proof.context -> bool
 
   (*certificates*)
   val select_certificates: string -> Context.generic -> Context.generic
   val certificates_of: Proof.context -> Cache_IO.cache option
 
   (*setup*)
   val print_setup: Proof.context -> unit
 end;
 
 structure SMT_Config: SMT_CONFIG =
 struct
 
 (* solver *)
 
 type solver_info = {
   name: string,
   class: Proof.context -> SMT_Util.class,
   avail: unit -> bool,
   options: Proof.context -> string list}
 
 type data = {
   solvers: (solver_info * string list) Symtab.table,
   solver: string option,
   certs: Cache_IO.cache option}
 
 fun mk_data solvers solver certs: data = {solvers=solvers, solver=solver, certs=certs}
 
 val empty_data = mk_data Symtab.empty NONE NONE
 
 fun solvers_of ({solvers, ...}: data) = solvers
 fun solver_of ({solver, ...}: data) = solver
 fun certs_of ({certs, ...}: data) = certs
 
 fun map_solvers f ({solvers, solver, certs}: data) = mk_data (f solvers) solver certs
 fun map_solver f ({solvers, solver, certs}: data) = mk_data solvers (f solver) certs
 fun put_certs c ({solvers, solver, ...}: data) = mk_data solvers solver c
 
 fun merge_data ({solvers=ss1,solver=s1,certs=c1}: data, {solvers=ss2,solver=s2,certs=c2}: data) =
   mk_data (Symtab.merge (K true) (ss1, ss2)) (merge_options (s1, s2)) (merge_options (c1, c2))
 
 structure Data = Generic_Data
 (
   type T = data
   val empty = empty_data
   val extend = I
   val merge = merge_data
 )
 
 fun set_solver_options (name, options) =
   let val opts = String.tokens (Symbol.is_ascii_blank o str) options
   in Data.map (map_solvers (Symtab.map_entry name (apsnd (K opts)))) end
 
 fun add_solver (info as {name, ...} : solver_info) context =
   if Symtab.defined (solvers_of (Data.get context)) name then
     error ("Solver already registered: " ^ quote name)
   else
     context
     |> Data.map (map_solvers (Symtab.update (name, (info, []))))
     |> Context.map_theory (Attrib.setup (Binding.name (name ^ "_options"))
         (Scan.lift (\<^keyword>\<open>=\<close> |-- Args.name) >>
           (Thm.declaration_attribute o K o set_solver_options o pair name))
         ("additional command line options for SMT solver " ^ quote name))
 
 fun all_solvers_of ctxt = Symtab.keys (solvers_of (Data.get (Context.Proof ctxt)))
 
 fun solver_name_of ctxt = solver_of (Data.get (Context.Proof ctxt))
 
 fun is_available ctxt name =
   (case Symtab.lookup (solvers_of (Data.get (Context.Proof ctxt))) name of
     SOME ({avail, ...}, _) => avail ()
   | NONE => false)
 
 fun available_solvers_of ctxt =
   filter (is_available ctxt) (all_solvers_of ctxt)
 
 fun warn_solver (Context.Proof ctxt) name =
       if Context_Position.is_visible ctxt then
         warning ("The SMT solver " ^ quote name ^ " is not installed")
       else ()
   | warn_solver _ _ = ()
 
 fun select_solver name context =
   let
     val ctxt = Context.proof_of context
     val upd = Data.map (map_solver (K (SOME name)))
   in
     if not (member (op =) (all_solvers_of ctxt) name) then
       error ("Trying to select unknown solver: " ^ quote name)
     else if not (is_available ctxt name) then
       (warn_solver context name; upd context)
     else upd context
   end
 
 fun no_solver_err () = error "No SMT solver selected"
 
 fun solver_of ctxt =
   (case solver_name_of ctxt of
     SOME name => name
   | NONE => no_solver_err ())
 
 fun solver_info_of default select ctxt =
   (case solver_name_of ctxt of
     NONE => default ()
   | SOME name => select (Symtab.lookup (solvers_of (Data.get (Context.Proof ctxt))) name))
 
 fun solver_class_of ctxt =
   let fun class_of ({class, ...}: solver_info, _) = class ctxt
   in solver_info_of no_solver_err (class_of o the) ctxt end
 
 fun solver_options_of ctxt =
   let
     fun all_options NONE = []
       | all_options (SOME ({options, ...} : solver_info, opts)) =
           opts @ options ctxt
   in solver_info_of (K []) all_options ctxt end
 
 val setup_solver =
   Attrib.setup \<^binding>\<open>smt_solver\<close>
     (Scan.lift (\<^keyword>\<open>=\<close> |-- Args.name) >>
       (Thm.declaration_attribute o K o select_solver))
     "SMT solver configuration"
 
 
 (* options *)
 
 val oracle = Attrib.setup_config_bool \<^binding>\<open>smt_oracle\<close> (K true)
 val timeout = Attrib.setup_config_real \<^binding>\<open>smt_timeout\<close> (K 1000000.0)
 val reconstruction_step_timeout = Attrib.setup_config_real \<^binding>\<open>smt_reconstruction_step_timeout\<close> (K 10.0)
 val random_seed = Attrib.setup_config_int \<^binding>\<open>smt_random_seed\<close> (K 1)
 val read_only_certificates = Attrib.setup_config_bool \<^binding>\<open>smt_read_only_certificates\<close> (K false)
 val verbose = Attrib.setup_config_bool \<^binding>\<open>smt_verbose\<close> (K true)
 val trace = Attrib.setup_config_bool \<^binding>\<open>smt_trace\<close> (K false)
 val trace_verit = Attrib.setup_config_bool \<^binding>\<open>smt_debug_verit\<close> (K false)
 val spy_verit_attr = Attrib.setup_config_bool \<^binding>\<open>smt_spy_verit\<close> (K false)
 val spy_z3 = Attrib.setup_config_bool \<^binding>\<open>smt_spy_z3\<close> (K false)
 val trace_arith_verit = Attrib.setup_config_bool \<^binding>\<open>smt_debug_arith_verit\<close> (K false)
-val trace_verit_compression = Attrib.setup_config_bool \<^binding>\<open>verit_compress_proofs\<close> (K false)
+val trace_verit_compression = Attrib.setup_config_bool \<^binding>\<open>verit_compress_proofs\<close> (K true)
 val statistics = Attrib.setup_config_bool \<^binding>\<open>smt_statistics\<close> (K false)
 val monomorph_limit = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_limit\<close> (K 10)
 val monomorph_instances = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_instances\<close> (K 500)
 val explicit_application = Attrib.setup_config_int \<^binding>\<open>smt_explicit_application\<close> (K 1)
 val higher_order = Attrib.setup_config_bool \<^binding>\<open>smt_higher_order\<close> (K false)
 val nat_as_int = Attrib.setup_config_bool \<^binding>\<open>smt_nat_as_int\<close> (K false)
 val infer_triggers = Attrib.setup_config_bool \<^binding>\<open>smt_infer_triggers\<close> (K false)
 val debug_files = Attrib.setup_config_string \<^binding>\<open>smt_debug_files\<close> (K "")
 val sat_solver = Attrib.setup_config_string \<^binding>\<open>smt_sat_solver\<close> (K "cdclite")
 
 
 (* diagnostics *)
 
 fun cond_trace flag f x = if flag then tracing ("SMT: " ^ f x) else ()
 
 fun verbose_msg ctxt = cond_trace (Config.get ctxt verbose)
 fun trace_msg ctxt = cond_trace (Config.get ctxt trace)
 fun statistics_msg ctxt = cond_trace (Config.get ctxt statistics)
 
 fun verit_msg ctxt (x : unit -> 'a) = if (Config.get ctxt trace_verit) then ignore(x ()) else ()
 fun verit_arith_msg ctxt (x : unit -> 'a) = if (Config.get ctxt trace_arith_verit) then ignore(x ()) else ()
 
 fun spy_verit ctxt  = Config.get ctxt spy_verit_attr
 fun spy_Z3 ctxt  = Config.get ctxt spy_z3
 fun compress_verit_proofs ctxt  = Config.get ctxt trace_verit_compression
 
 
 (* tools *)
 
 fun with_time_limit ctxt timeout_config f x =
   Timeout.apply (seconds (Config.get ctxt timeout_config)) f x
     handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out
 
 fun with_timeout ctxt = with_time_limit ctxt timeout
 
 
 (* certificates *)
 
 val certificates_of = certs_of o Data.get o Context.Proof
 
 val get_certificates_path = Option.map (Cache_IO.cache_path_of) o certificates_of
 
 fun select_certificates name context = context |> Data.map (put_certs (
   if name = "" then NONE
   else
     (Resources.master_directory (Context.theory_of context) + Path.explode name)
     |> SOME o Cache_IO.unsynchronized_init))
 
 val setup_certificates =
   Attrib.setup \<^binding>\<open>smt_certificates\<close>
     (Scan.lift (\<^keyword>\<open>=\<close> |-- Args.name) >>
       (Thm.declaration_attribute o K o select_certificates))
     "SMT certificates configuration"
 
 
 (* setup *)
 
 val _ = Theory.setup (
   setup_solver #>
   setup_certificates)
 
 fun print_setup ctxt =
   let
     fun string_of_bool b = if b then "true" else "false"
 
     val names = available_solvers_of ctxt
     val ns = if null names then ["(none)"] else sort_strings names
     val n = the_default "(none)" (solver_name_of ctxt)
     val opts = solver_options_of ctxt
 
     val t = string_of_real (Config.get ctxt timeout)
 
     val certs_filename =
       (case get_certificates_path ctxt of
         SOME path => Path.print path
       | NONE => "(disabled)")
   in
     Pretty.writeln (Pretty.big_list "SMT setup:" [
       Pretty.str ("Current SMT solver: " ^ n),
       Pretty.str ("Current SMT solver options: " ^ space_implode " " opts),
       Pretty.str_list "Available SMT solvers: "  "" ns,
       Pretty.str ("Current timeout: " ^ t ^ " seconds"),
       Pretty.str ("With proofs: " ^
         string_of_bool (not (Config.get ctxt oracle))),
       Pretty.str ("Certificates cache: " ^ certs_filename),
       Pretty.str ("Fixed certificates: " ^
         string_of_bool (Config.get ctxt read_only_certificates))])
   end
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>smt_status\<close>
     "show the available SMT solvers, the currently selected SMT solver, \
     \and the values of SMT configuration options"
     (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))
 
 end;
diff --git a/src/HOL/Tools/SMT/verit_proof.ML b/src/HOL/Tools/SMT/verit_proof.ML
--- a/src/HOL/Tools/SMT/verit_proof.ML
+++ b/src/HOL/Tools/SMT/verit_proof.ML
@@ -1,859 +1,898 @@
 (*  Title:      HOL/Tools/SMT/Verit_Proof.ML
     Author:     Mathias Fleury, ENS Rennes
     Author:     Sascha Boehme, TU Muenchen
 
 VeriT proofs: parsing and abstract syntax tree.
 *)
 
 signature VERIT_PROOF =
 sig
   (*proofs*)
   datatype veriT_step = VeriT_Step of {
     id: string,
     rule: string,
     prems: string list,
     proof_ctxt: term list,
     concl: term,
     fixes: string list}
 
   datatype veriT_replay_node = VeriT_Replay_Node of {
     id: string,
     rule: string,
     args: term list,
     prems: string list,
     proof_ctxt: term list,
     concl: term,
     bounds: (string * typ) list,
     declarations: (string * term) list,
     insts: term Symtab.table,
     subproof: (string * typ) list * term list * term list * veriT_replay_node list}
 
   (*proof parser*)
   val parse: typ Symtab.table -> term Symtab.table -> string list ->
     Proof.context -> veriT_step list * Proof.context
   val parse_replay: typ Symtab.table -> term Symtab.table -> string list ->
     Proof.context -> veriT_replay_node list * Proof.context
 
   val step_prefix : string
   val input_rule: string
   val keep_app_symbols: string -> bool
   val keep_raw_lifting: string -> bool
   val normalized_input_rule: string
   val la_generic_rule : string
   val rewrite_rule : string
   val simp_arith_rule : string
   val veriT_deep_skolemize_rule : string
   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 theory_resolution2_rule: string
+  val equiv_pos2_rule: string
+  val th_resolution_rule: string
 
   val is_skolemization: string -> bool
   val is_skolemization_step: veriT_replay_node -> bool
 
   val number_of_steps: veriT_replay_node list -> int
 
   (*Strategy related*)
   val veriT_strategy : string Config.T
   val veriT_current_strategy : Context.generic -> string list
   val all_veriT_stgies: Context.generic -> string list;
 
   val select_veriT_stgy: string -> Context.generic -> Context.generic;
   val valid_veriT_stgy: string -> Context.generic -> bool;
   val verit_add_stgy: string * string list -> Context.generic -> Context.generic
   val verit_rm_stgy: string -> Context.generic -> Context.generic
 
   (*Global tactic*)
   val verit_tac: Proof.context -> thm list -> int -> tactic
   val verit_tac_stgy: string -> Proof.context -> thm list -> int -> tactic
 end;
 
 structure Verit_Proof: VERIT_PROOF =
 struct
 
 open SMTLIB_Proof
 
 val veriT_strategy_default_name = "default"; (*FUDGE*)
 val veriT_strategy_del_insts_name = "del_insts"; (*FUDGE*)
 val veriT_strategy_rm_insts_name = "ccfv_SIG"; (*FUDGE*)
 val veriT_strategy_ccfv_insts_name = "ccfv_threshold"; (*FUDGE*)
 val veriT_strategy_best_name = "best"; (*FUDGE*)
 
 val veriT_strategy_best = ["--index-sorts", "--index-fresh-sorts", "--triggers-new",
   "--triggers-sel-rm-specific"];
 val veriT_strategy_del_insts = ["--index-sorts", "--index-fresh-sorts", "--ccfv-breadth",
   "--inst-deletion", "--index-SAT-triggers", "--inst-deletion-loops", "--inst-deletion-track-vars",
   "--inst-deletion", "--index-SAT-triggers"];
 val veriT_strategy_rm_insts = ["--index-SIG", "--triggers-new", "--triggers-sel-rm-specific"];
 val veriT_strategy_ccfv_insts = ["--index-sorts", "--index-fresh-sorts", "--triggers-new",
   "--triggers-sel-rm-specific", "--triggers-restrict-combine", "--inst-deletion",
   "--index-SAT-triggers", "--inst-deletion-loops", "--inst-deletion-track-vars", "--inst-deletion",
   "--index-SAT-triggers", "--inst-sorts-threshold=100000", "--ematch-exp=10000000",
   "--ccfv-index=100000", "--ccfv-index-full=1000"]
 
 val veriT_strategy_default = [];
 
 type verit_strategy = {default_strategy: string, strategies: (string * string list) list}
 fun mk_verit_strategy default_strategy strategies : verit_strategy = {default_strategy=default_strategy,strategies=strategies}
 
 val empty_data = mk_verit_strategy veriT_strategy_best_name
   [(veriT_strategy_default_name, veriT_strategy_default),
    (veriT_strategy_del_insts_name, veriT_strategy_del_insts),
    (veriT_strategy_rm_insts_name, veriT_strategy_rm_insts),
    (veriT_strategy_ccfv_insts_name, veriT_strategy_ccfv_insts),
    (veriT_strategy_best_name, veriT_strategy_best)]
 
 fun merge_data ({strategies=strategies1,...}:verit_strategy,
     {default_strategy,strategies=strategies2}:verit_strategy) : verit_strategy =
   mk_verit_strategy default_strategy (AList.merge (op =) (op =) (strategies1, strategies2))
 
 structure Data = Generic_Data
 (
   type T = verit_strategy
   val empty = empty_data
   val extend = I
   val merge = merge_data
 )
 
 fun veriT_current_strategy ctxt =
   let
     val {default_strategy,strategies} = (Data.get ctxt)
   in
     AList.lookup (op=) strategies default_strategy
    |> the
   end
 
 val veriT_strategy = Attrib.setup_config_string \<^binding>\<open>smt_verit_strategy\<close> (K veriT_strategy_best_name);
 
 fun valid_veriT_stgy stgy context =
   let
     val {strategies,...} = Data.get context
   in
     AList.defined (op =) strategies stgy
   end
 
 fun select_veriT_stgy stgy context =
   let
     val {strategies,...} = Data.get context
     val upd = Data.map (K (mk_verit_strategy stgy strategies))
   in
     if not (AList.defined (op =) strategies stgy) then
       error ("Trying to select unknown veriT strategy: " ^ quote stgy)
     else upd context
   end
 
 fun verit_add_stgy stgy context =
   let
     val {default_strategy,strategies} = Data.get context
   in
-    Data.map 
+    Data.map
       (K (mk_verit_strategy default_strategy (AList.update (op =) stgy strategies)))
       context
   end
 
 fun verit_rm_stgy stgy context =
   let
     val {default_strategy,strategies} = Data.get context
   in
-    Data.map 
+    Data.map
       (K (mk_verit_strategy default_strategy (AList.delete (op =) stgy strategies)))
       context
   end
 
 fun all_veriT_stgies context =
   let
     val {strategies,...} = Data.get context
    in
     map fst strategies
   end
 
 fun verit_tac ctxt = SMT_Solver.smt_tac (Context.proof_map (SMT_Config.select_solver "verit") ctxt)
 fun verit_tac_stgy stgy ctxt = verit_tac (Context.proof_of (select_veriT_stgy stgy (Context.Proof ctxt)))
 
 datatype raw_veriT_node = Raw_VeriT_Node of {
   id: string,
   rule: string,
   args: SMTLIB.tree,
   prems: string list,
   concl: SMTLIB.tree,
   declarations: (string * SMTLIB.tree) list,
   subproof: raw_veriT_node list}
 
 fun mk_raw_node id rule args prems declarations concl subproof =
   Raw_VeriT_Node {id = id, rule = rule, args = args, prems = prems, declarations = declarations,
     concl = concl, subproof = subproof}
 
 datatype veriT_node = VeriT_Node of {
   id: string,
   rule: string,
   prems: string list,
   proof_ctxt: term list,
   concl: term}
 
 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,
   rule: string,
   args: term list,
   prems: string list,
   proof_ctxt: term list,
   concl: term,
   bounds: (string * typ) list,
   insts: term Symtab.table,
   declarations: (string * term) list,
   subproof: (string * typ) list * term list * term list * veriT_replay_node list}
 
 fun mk_replay_node id rule args prems proof_ctxt concl bounds insts declarations subproof =
   VeriT_Replay_Node {id = id, rule = rule, args = args, prems = prems, proof_ctxt = proof_ctxt,
     concl = concl, bounds = bounds, insts = insts, declarations = declarations,
     subproof = subproof}
 
 datatype veriT_step = VeriT_Step of {
   id: string,
   rule: string,
   prems: string list,
   proof_ctxt: term list,
   concl: term,
   fixes: string list}
 
 fun mk_step id rule prems proof_ctxt concl fixes =
   VeriT_Step {id = id, rule = rule, prems = prems, proof_ctxt = proof_ctxt, concl = concl,
     fixes = fixes}
 
 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 subproof_rule = "subproof"
 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 theory_resolution2_rule = "__theory_resolution2" (*arbitrary*)
+val equiv_pos2_rule = "equiv_pos2"
+val th_resolution_rule = "th_resolution"
 
 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_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"
 
 fun number_of_steps [] = 0
   | number_of_steps ((VeriT_Replay_Node {subproof = (_, _, _, subproof), ...}) :: pf) =
       1 + number_of_steps subproof + number_of_steps pf
 
 (* proof parser *)
 
 fun node_of p cx =
   ([], cx)
   ||>> `(with_fresh_names (term_of p))
   |>> snd
 
 fun find_type_in_formula (Abs (v, T, u)) var_name =
     if String.isPrefix var_name v then SOME T else find_type_in_formula u var_name
   | find_type_in_formula (u $ v) var_name =
     (case find_type_in_formula u var_name of
       NONE => find_type_in_formula v var_name
     | some_T => some_T)
   | find_type_in_formula (Free(v, T)) var_name =
     if String.isPrefix var_name v then SOME T else NONE
   | find_type_in_formula _ _ = NONE
 
 fun synctactic_var_subst old_name new_name (u $ v) =
     (synctactic_var_subst old_name new_name u $ synctactic_var_subst old_name new_name v)
   | synctactic_var_subst old_name new_name (Abs (v, T, u)) =
     Abs (if String.isPrefix old_name v then new_name else v, T,
       synctactic_var_subst old_name new_name u)
   | synctactic_var_subst old_name new_name (Free (v, T)) =
      if String.isPrefix old_name v then Free (new_name, T) else Free (v, T)
   | synctactic_var_subst _ _ t = t
 
 fun synctatic_rew_in_lhs_subst old_name new_name (Const(\<^const_name>\<open>HOL.eq\<close>, T) $ t1 $ t2) =
      Const(\<^const_name>\<open>HOL.eq\<close>, T) $ synctactic_var_subst old_name new_name t1 $ t2
   | synctatic_rew_in_lhs_subst old_name new_name (Const(\<^const_name>\<open>Trueprop\<close>, T) $ t1) =
      Const(\<^const_name>\<open>Trueprop\<close>, T) $ (synctatic_rew_in_lhs_subst old_name new_name t1)
   | synctatic_rew_in_lhs_subst _ _ t = t
 
 fun add_bound_variables_to_ctxt concl =
   fold (update_binding o
     (fn s => (s, Term (Free (s, the_default dummyT (find_type_in_formula concl s))))))
 
 local
 
   fun remove_Sym (SMTLIB.Sym y) = y
     | remove_Sym y = (@{print} y; raise (Fail "failed to match"))
 
   fun extract_symbols bds =
     bds
     |> map (fn SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym x, SMTLIB.Sym y] => [[x, y]]
              | SMTLIB.S [SMTLIB.Key "=", SMTLIB.Sym x, SMTLIB.Sym y] => [[x, y]]
              | SMTLIB.S syms => map (single o remove_Sym) syms
              | SMTLIB.Sym x => [[x]]
              | t => raise (Fail ("match error " ^ @{make_string} t)))
     |> flat
 
   (* onepoint can bind a variable to another variable or to a constant *)
   fun extract_qnt_symbols cx bds =
     bds
     |> map (fn SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym x, SMTLIB.Sym y] =>
                 (case node_of (SMTLIB.Sym y) cx  of
                   ((_, []), _) => [[x]]
                 | _ => [[x, y]])
              | SMTLIB.S [SMTLIB.Key "=", SMTLIB.Sym x, SMTLIB.Sym y] =>
                 (case node_of (SMTLIB.Sym y) cx  of
                   ((_, []), _) => [[x]]
                 | _ => [[x, y]])
              | SMTLIB.S (SMTLIB.Sym "=" :: SMTLIB.Sym x :: _) => [[x]]
              | SMTLIB.S (SMTLIB.Key "=" :: SMTLIB.Sym x :: _) => [[x]]
              | SMTLIB.S syms => map (single o remove_Sym) syms
              | SMTLIB.Sym x => [[x]]
              | t => raise (Fail ("match error " ^ @{make_string} t)))
     |> flat
 
   fun extract_symbols_map bds =
     bds
     |> map (fn SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym x, _] => [[x]]
              | SMTLIB.S syms =>  map (single o remove_Sym) syms)
     |> flat
 in
 
 fun declared_csts _ "__skolem_definition" (SMTLIB.S [SMTLIB.Sym x, typ, _]) = [(x, typ)]
   | declared_csts _ _ _ = []
 
 fun skolems_introduced_by_rule (SMTLIB.S bds) =
    fold (fn (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym _, SMTLIB.Sym y]) => curry (op ::) y) bds []
 
 (*FIXME there is probably a way to use the information given by onepoint*)
 fun bound_vars_by_rule _ "bind" (SMTLIB.S bds) = extract_symbols bds
   | bound_vars_by_rule cx "onepoint" (SMTLIB.S bds) = extract_qnt_symbols cx bds
   | bound_vars_by_rule _ "sko_forall" (SMTLIB.S bds) = extract_symbols_map bds
   | bound_vars_by_rule _ "sko_ex" (SMTLIB.S bds) = extract_symbols_map bds
   | bound_vars_by_rule _ "__skolem_definition" (SMTLIB.S [SMTLIB.Sym x, _, _]) = [[x]]
   | bound_vars_by_rule _ _ _ = []
 
 (* VeriT adds "?" before some variables. *)
 fun remove_all_qm (SMTLIB.Sym v :: l) =
     SMTLIB.Sym (perhaps (try (unprefix "?")) v) :: remove_all_qm l
   | remove_all_qm (SMTLIB.S l :: l') = SMTLIB.S (remove_all_qm l) :: remove_all_qm l'
   | remove_all_qm (SMTLIB.Key v :: l) = SMTLIB.Key v :: remove_all_qm l
   | remove_all_qm (v :: l) = v :: remove_all_qm l
   | remove_all_qm [] = []
 
 fun remove_all_qm2 (SMTLIB.Sym v) = SMTLIB.Sym (perhaps (try (unprefix "?")) v)
   | remove_all_qm2 (SMTLIB.S l) = SMTLIB.S (remove_all_qm l)
   | remove_all_qm2 (SMTLIB.Key v) = SMTLIB.Key v
   | remove_all_qm2 v = v
 
 end
 
 datatype step_kind = ASSUME | ANCHOR | NO_STEP | NORMAL_STEP | SKOLEM
 
 fun parse_raw_proof_steps (limit : string option) (ls : SMTLIB.tree list) (cx : name_bindings) :
      (raw_veriT_node list * SMTLIB.tree list * name_bindings) =
   let
     fun rotate_pair (a, (b, c)) = ((a, b), c)
     fun step_kind [] = (NO_STEP, SMTLIB.S [], [])
       | step_kind ((p as SMTLIB.S (SMTLIB.Sym "anchor" :: _)) :: l) = (ANCHOR, p, l)
       | step_kind ((p as SMTLIB.S (SMTLIB.Sym "assume" :: _)) :: l) = (ASSUME, p, l)
       | step_kind ((p as SMTLIB.S (SMTLIB.Sym "step" :: _)) :: l) = (NORMAL_STEP, p, l)
       | step_kind ((p as SMTLIB.S (SMTLIB.Sym "define-fun" :: _)) :: l) = (SKOLEM, p, l)
     fun parse_skolem (SMTLIB.S [SMTLIB.Sym "define-fun", SMTLIB.Sym id,  _, typ,
            SMTLIB.S (SMTLIB.Sym "!" :: t :: [SMTLIB.Key _, SMTLIB.Sym name])]) cx =
          (*replace the name binding by the constant instead of the full term in order to reduce
            the size of the generated terms and therefore the reconstruction time*)
          let val (l, cx) = (fst oo SMTLIB_Proof.extract_and_update_name_bindings) t cx
             |> apsnd (SMTLIB_Proof.update_name_binding (name, SMTLIB.Sym id))
          in
            (mk_raw_node (id ^ veriT_def) veriT_def (SMTLIB.S [SMTLIB.Sym id, typ, l]) [] []
               (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym id, l]) [], cx)
          end
       | parse_skolem (SMTLIB.S [SMTLIB.Sym "define-fun", SMTLIB.Sym id,  _, typ, SMTLIB.S l]) cx =
          let val (l, cx) = (fst oo SMTLIB_Proof.extract_and_update_name_bindings) (SMTLIB.S l ) cx
          in
            (mk_raw_node (id ^ veriT_def) veriT_def (SMTLIB.S [SMTLIB.Sym id, typ, l]) [] []
               (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym id, l]) [], cx)
          end
       | parse_skolem t _ = raise Fail ("unrecognized VeriT proof " ^ \<^make_string> t)
     fun get_id_cx (SMTLIB.S ((SMTLIB.Sym _) :: (SMTLIB.Sym id) :: l), cx) = (id, (l, cx))
       | get_id_cx t = raise Fail ("unrecognized VeriT proof " ^ \<^make_string> t)
     fun get_id (SMTLIB.S ((SMTLIB.Sym _) :: (SMTLIB.Sym id) :: l)) = (id, l)
       | get_id t = raise Fail ("unrecognized VeriT proof " ^ \<^make_string> t)
     fun parse_source (SMTLIB.Key "premises" :: SMTLIB.S source ::l, cx) =
         (SOME (map (fn (SMTLIB.Sym id) => id) source), (l, cx))
       | parse_source (l, cx) = (NONE, (l, cx))
     fun parse_rule (SMTLIB.Key "rule" :: SMTLIB.Sym r :: l, cx) = (r, (l, cx))
       | parse_rule t = raise Fail ("unrecognized VeriT proof " ^ \<^make_string> t)
     fun parse_anchor_step (SMTLIB.S (SMTLIB.Sym "anchor" :: SMTLIB.Key "step" :: SMTLIB.Sym r :: l), cx) = (r, (l, cx))
       | parse_anchor_step t = raise Fail ("unrecognized VeriT proof " ^ \<^make_string> t)
     fun parse_args (SMTLIB.Key "args" :: args :: l, cx) =
           let val ((args, cx), _) = SMTLIB_Proof.extract_and_update_name_bindings args cx
           in (args, (l, cx)) end
       | parse_args (l, cx) = (SMTLIB.S [], (l, cx))
     fun parse_and_clausify_conclusion (SMTLIB.S (SMTLIB.Sym "cl" :: []) :: l, cx) =
           (SMTLIB.Sym "false", (l, cx))
       | parse_and_clausify_conclusion (SMTLIB.S (SMTLIB.Sym "cl" :: concl) :: l, cx) =
           let val (concl, cx) = fold_map (fst oo SMTLIB_Proof.extract_and_update_name_bindings) concl cx
           in (SMTLIB.S (SMTLIB.Sym "or" :: concl), (l, cx)) end
       | parse_and_clausify_conclusion t = raise Fail ("unrecognized VeriT proof " ^ \<^make_string> t)
     val parse_normal_step =
         get_id_cx
         ##> parse_and_clausify_conclusion
         #> rotate_pair
         ##> parse_rule
         #> rotate_pair
         ##> parse_source
         #> rotate_pair
         ##> parse_args
         #> rotate_pair
 
     fun to_raw_node subproof ((((id, concl), rule), prems), args) =
         mk_raw_node id rule args (the_default [] prems) [] concl subproof
     fun at_discharge NONE _ = false
       | at_discharge (SOME id) p = p |> get_id |> fst |> (fn id2 => id = id2)
   in
     case step_kind ls of
         (NO_STEP, _, _) => ([],[], cx)
       | (NORMAL_STEP, p, l) =>
           if at_discharge limit p then ([], ls, cx) else
             let
               val (s, (_, cx)) =  (p, cx)
                 |> parse_normal_step
                 ||> (fn i => i)
                 |>>  (to_raw_node [])
               val (rp, rl, cx) = parse_raw_proof_steps limit l cx
           in (s :: rp, rl, cx) end
       | (ASSUME, p, l) =>
           let
             val (id, t :: []) = p
               |> get_id
             val ((t, cx), _) = SMTLIB_Proof.extract_and_update_name_bindings t cx
             val s = mk_raw_node id input_rule (SMTLIB.S []) [] [] t []
             val (rp, rl, cx) = parse_raw_proof_steps limit l cx
           in (s :: rp, rl, cx) end
       | (ANCHOR, p, l) =>
           let
             val (anchor_id, (anchor_args, (_, cx))) = (p, cx) |> (parse_anchor_step ##> parse_args)
             val (subproof, discharge_step :: remaining_proof, cx) = parse_raw_proof_steps (SOME anchor_id) l cx
             val (curss, (_, cx)) = parse_normal_step (discharge_step, cx)
             val s = to_raw_node subproof (fst curss, anchor_args)
             val (rp, rl, cx) = parse_raw_proof_steps limit remaining_proof cx
           in (s :: rp, rl, cx) end
       | (SKOLEM, p, l) =>
           let
             val (s, cx) = parse_skolem p cx
             val (rp, rl, cx) = parse_raw_proof_steps limit l cx
           in (s :: rp, rl, cx) end
   end
 
 fun proof_ctxt_of_rule "bind" t = t
   | proof_ctxt_of_rule "sko_forall" t = t
   | proof_ctxt_of_rule "sko_ex" t = t
   | proof_ctxt_of_rule "let" t = t
   | proof_ctxt_of_rule "onepoint" t = t
   | proof_ctxt_of_rule _ _ = []
 
 fun args_of_rule "bind" t = t
   | args_of_rule "la_generic" t = t
   | args_of_rule "lia_generic" t = t
   | args_of_rule _ _ = []
 
 fun insts_of_forall_inst "forall_inst" t = map (fn SMTLIB.S [_, SMTLIB.Sym x, a] => (x, a)) t
   | insts_of_forall_inst _ _ = []
 
 fun id_of_last_step prems =
   if null prems then []
   else
     let val VeriT_Replay_Node {id, ...} = List.last prems in [id] end
 
 fun extract_assumptions_from_subproof subproof =
   let fun extract_assumptions_from_subproof (VeriT_Replay_Node {rule, concl, ...}) assms =
     if rule = local_input_rule then concl :: assms else assms
   in
     fold extract_assumptions_from_subproof subproof []
   end
 
 fun normalized_rule_name id rule =
   (case (rule = input_rule, can (unprefix SMTLIB_Interface.assert_prefix) id) of
     (true, true) => normalized_input_rule
   | (true, _) => local_input_rule
   | _ => rule)
 
 fun is_assm_repetition id rule =
   rule = input_rule andalso can (unprefix SMTLIB_Interface.assert_prefix) id
 
 fun extract_skolem ([SMTLIB.Sym var, typ, choice]) = (var, typ, choice)
   | extract_skolem t = raise Fail ("fail to parse type" ^ @{make_string} t)
 
 (* The preprocessing takes care of:
      1. unfolding the shared terms
      2. extract the declarations of skolems to make sure that there are not unfolded
 *)
 fun preprocess compress step =
   let
     fun expand_assms cs =
       map (fn t => case AList.lookup (op =) cs t of NONE => t | SOME a => a)
     fun expand_lonely_arguments (args as SMTLIB.S [SMTLIB.Sym "=", _, _]) = [args]
       | expand_lonely_arguments (SMTLIB.S S) = map (fn x => SMTLIB.S [SMTLIB.Sym "=", x, x]) S
       | expand_lonely_arguments (x as SMTLIB.Sym _) = [SMTLIB.S [SMTLIB.Sym "=", x, x]]
       | expand_lonely_arguments t = [t]
 
     fun preprocess (Raw_VeriT_Node {id, rule, args, prems, concl, subproof, ...}) (cx, remap_assms)  =
       let
         val stripped_args = args
           |> (fn SMTLIB.S args => args)
           |> map
               (fn SMTLIB.S [SMTLIB.Key "=", x, y] => SMTLIB.S [SMTLIB.Sym "=", x, y]
               | x => x)
           |> (rule = "bind" orelse rule = "onepoint") ? flat o (map expand_lonely_arguments)
           |> `(if rule = veriT_def then single o extract_skolem else K [])
           ||> SMTLIB.S
 
         val (subproof, (cx, _)) = fold_map preprocess subproof (cx, remap_assms) |> apfst flat
         val (skolem_names, stripped_args) = stripped_args
         val remap_assms = (if rule = "or" then (id, hd prems) :: remap_assms else remap_assms)
         (* declare variables in the context *)
         val declarations =
            if rule = veriT_def
            then skolem_names |> map (fn (name, _, choice) => (name, choice))
            else []
       in
         if compress andalso rule = "or"
         then ([], (cx, remap_assms))
         else ([Raw_VeriT_Node {id = id, rule = rule, args = stripped_args,
            prems = expand_assms remap_assms prems, declarations = declarations, concl = concl, subproof = subproof}],
           (cx, remap_assms))
       end
   in preprocess step end
 
 fun filter_split _ [] = ([], [])
   | filter_split f (a :: xs) =
      (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_skolemization rule then map (fn id => id ^ veriT_def) (skolems_introduced_by_rule args) else []) @
   flat (map collect_skolem_defs subproof)
 
 (*The postprocessing does:
   1. translate the terms to Isabelle syntax, taking care of free variables
   2. remove the ambiguity in the proof terms:
        x \<leadsto> y |- x = x
     means y = x. To remove ambiguity, we use the fact that y is a free variable and replace the term
     by:
       xy \<leadsto> y |- xy = x.
     This is now does not have an ambiguity and we can safely move the "xy \<leadsto> y" to the proof
     assumptions.
 *)
 fun postprocess_proof compress ctxt step cx =
   let
     fun postprocess (Raw_VeriT_Node {id, rule, args, prems, declarations, concl, subproof}) (cx, rew) =
     let
       val _ = (SMT_Config.verit_msg ctxt) (fn () => @{print} ("id =", id, "concl =", concl))
 
       val globally_bound_vars = declared_csts cx rule args
       val cx = fold (update_binding o (fn (s, typ) => (s, Term (Free (s, type_of cx typ)))))
            globally_bound_vars cx
 
       (*find rebound variables specific to the LHS of the equivalence symbol*)
       val bound_vars = bound_vars_by_rule cx rule args
 
       val rhs_vars = fold (fn [t', t] => t <> t' ? (curry (op ::) t) | _ => fn x => x) bound_vars []
       fun not_already_bound cx t = SMTLIB_Proof.lookup_binding cx t = None andalso
           not (member (op =) rhs_vars t)
       val (shadowing_vars, rebound_lhs_vars) = bound_vars
         |> filter_split (fn [t, _] => not_already_bound cx t | _ => true)
         |>> map (single o hd)
         |>> (fn vars => vars @ map (fn [_, t] => [t] | _ => []) bound_vars)
         |>> flat
       val subproof_rew = fold (fn [t, t'] => curry (op ::) (t, t ^ t'))
         rebound_lhs_vars rew
       val subproof_rewriter = fold (fn (t, t') => synctatic_rew_in_lhs_subst t t')
          subproof_rew
 
       val ((concl, bounds), cx') = node_of concl cx
 
       val extra_lhs_vars = map (fn [a,b] => (a, a^b)) rebound_lhs_vars
 
       (* postprocess conclusion *)
       val concl = SMTLIB_Isar.unskolemize_names ctxt (subproof_rewriter concl)
 
       val _ = (SMT_Config.verit_msg ctxt) (fn () => \<^print> ("id =", id, "concl =", concl))
       val _ = (SMT_Config.verit_msg ctxt) (fn () => \<^print> ("id =", id, "cx' =", cx',
         "bound_vars =", bound_vars))
 
       val bound_tvars =
         map (fn s => (s, the (find_type_in_formula concl s)))
          (shadowing_vars @ map snd extra_lhs_vars)
       val subproof_cx =
          add_bound_variables_to_ctxt concl (shadowing_vars @ map snd extra_lhs_vars) cx
 
       fun could_unify (Bound i, Bound j) = i = j
         | could_unify (Var v, Var v') = v = v'
         | could_unify (Free v, Free v') = v = v'
         | could_unify (Const (v, ty), Const (v', ty')) = v = v' andalso ty = ty'
         | could_unify (Abs (_, ty, bdy), Abs (_, ty', bdy')) = ty = ty' andalso could_unify (bdy, bdy')
         | could_unify (u $ v, u' $ v') = could_unify (u, u') andalso could_unify (v, v')
         | could_unify _ = false
       fun is_alpha_renaming t =
           t
           |> HOLogic.dest_Trueprop
           |> HOLogic.dest_eq
           |> could_unify
         handle TERM _ => false
       val alpha_conversion = rule = "bind" andalso is_alpha_renaming concl
 
       val can_remove_subproof =
         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)
 
       val unsk_and_rewrite = SMTLIB_Isar.unskolemize_names ctxt o subproof_rewriter
 
       (* postprocess assms *)
       val stripped_args = args |> (fn SMTLIB.S S => S)
       val sanitized_args = proof_ctxt_of_rule rule stripped_args
 
       val arg_cx =
         subproof_cx
         |> add_bound_variables_to_ctxt concl (shadowing_vars @ map fst extra_lhs_vars)
       val (termified_args, _) = fold_map node_of sanitized_args arg_cx |> apfst (map fst)
       val normalized_args = map unsk_and_rewrite termified_args
 
       val subproof_assms = proof_ctxt_of_rule rule normalized_args
 
       (* postprocess arguments *)
       val rule_args = args_of_rule rule stripped_args
       val (termified_args, _) = fold_map term_of rule_args subproof_cx
       val normalized_args = map unsk_and_rewrite termified_args
       val rule_args = map subproof_rewriter normalized_args
 
       val raw_insts = insts_of_forall_inst rule stripped_args
       fun termify_term (x, t) cx = let val (t, cx) = term_of t cx in ((x, t), cx) end
       val (termified_args, _) = fold_map termify_term raw_insts subproof_cx
       val insts = Symtab.empty
         |> fold (fn (x, t) => fn insts => Symtab.update_new (x, t) insts) termified_args
         |> Symtab.map (K unsk_and_rewrite)
 
       (* declarations *)
       val (declarations, _) = fold_map termify_term declarations cx
         |> apfst (map (apsnd unsk_and_rewrite))
 
       (* fix step *)
       val bound_t = bounds
         |> map (fn s => (s, the (find_type_in_formula concl s)))
 
       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_skolemization rule
          then flat (map collect_skolem_defs subproof) else [])
       val fixed_prems =
         prems @ (if is_assm_repetition id rule then [id] else []) @
         skolem_defs @ skolems_of_subproof @ (id_of_last_step fixed_subproof)
 
       (* fix subproof *)
       val normalized_rule = normalized_rule_name id rule
         |> (if compress andalso alpha_conversion then K "refl" else I)
 
       val extra_assms2 =
         (if rule = subproof_rule then extract_assumptions_from_subproof fixed_subproof else [])
 
       val step = mk_replay_node id normalized_rule rule_args fixed_prems subproof_assms concl
         bound_t insts declarations (bound_tvars, subproof_assms, extra_assms2, fixed_subproof)
 
     in
        (step, (cx', rew))
     end
   in
     postprocess step (cx, [])
     |> (fn (step, (cx, _)) => (step, cx))
-   end
+  end
+
+fun combine_proof_steps ((step1 : veriT_replay_node) :: step2 :: steps) =
+      let
+        val (VeriT_Replay_Node {id = id1, rule = rule1, args = args1, prems = prems1,
+            proof_ctxt = proof_ctxt1, concl = concl1, bounds = bounds1, insts = insts1,
+            declarations = declarations1,
+            subproof = (bound_sub1, assms_sub1, assms_extra1, subproof1)}) = step1
+        val (VeriT_Replay_Node {id = id2, rule = rule2, args = args2, prems = prems2,
+            proof_ctxt = proof_ctxt2, concl = concl2, bounds = bounds2, insts = insts2,
+            declarations = declarations2,
+            subproof = (bound_sub2, assms_sub2, assms_extra2, subproof2)}) = step2
+        val goals1 =
+          (case concl1 of
+            _ $ (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ _ $
+                  (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ (Const (\<^const_name>\<open>HOL.Not\<close>, _) $a) $ b)) => [a,b]
+          | _ => [])
+        val goal2 = (case concl2 of _ $ a => a)
+      in
+        if rule1 = equiv_pos2_rule andalso rule2 = th_resolution_rule andalso member (op =) prems2 id1
+          andalso member (op =) goals1 goal2
+        then
+          mk_replay_node id2 theory_resolution2_rule args2 (filter_out (curry (op =) id1) prems2)
+            proof_ctxt2 concl2 bounds2 insts2 declarations2
+            (bound_sub2, assms_sub2, assms_extra2, combine_proof_steps subproof2) ::
+          combine_proof_steps steps
+        else
+          mk_replay_node id1 rule1 args1 prems1
+            proof_ctxt1 concl1 bounds1 insts1 declarations1
+            (bound_sub1, assms_sub1, assms_extra1, combine_proof_steps subproof1) ::
+          combine_proof_steps (step2 :: steps)
+      end
+  | combine_proof_steps steps = steps
 
 
 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 = (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}) =
           mk_node id rule (remove_assumption_id assumption_id prems) proof_ctxt
             (add_assumption assumption concl)
         fun find_input_steps_and_inline [] = []
           | find_input_steps_and_inline
               (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 :: find_input_steps_and_inline steps
 
         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]
       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. 
+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 
+      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
       val compress = SMT_Config.compress_verit_proofs ctxt
       val smtlib_lines_without_qm =
         lines
         |> map single
         |> map SMTLIB.parse
         |> map remove_all_qm2
-      val (raw_steps, _, _) = 
+      val (raw_steps, _, _) =
         parse_raw_proof_steps NONE smtlib_lines_without_qm SMTLIB_Proof.empty_name_binding
-      
+
       fun process step (cx, cx') =
         let fun postprocess step (cx, cx') =
           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 =
         (empty_context ctxt typs funs, [])
         |> fold_map process raw_steps
         |> (fn (steps, (cx, _)) => (flat steps, cx))
+        |> compress? apfst combine_proof_steps
     in step end
 in
 
 fun parse typs funs lines ctxt =
   let
     val (u, env) = import_proof_and_post_process typs funs lines ctxt
     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
 
 fun parse_replay typs funs lines ctxt =
   let
     val (u, env) = import_proof_and_post_process typs funs lines ctxt
     val _ = (SMT_Config.verit_msg ctxt) (fn () => \<^print> u)
   in
     (u, ctxt_of env)
   end
 end
 
 end;
diff --git a/src/HOL/Tools/SMT/verit_replay_methods.ML b/src/HOL/Tools/SMT/verit_replay_methods.ML
--- a/src/HOL/Tools/SMT/verit_replay_methods.ML
+++ b/src/HOL/Tools/SMT/verit_replay_methods.ML
@@ -1,1180 +1,1192 @@
 (*  Title:      HOL/Tools/SMT/verit_replay_methods.ML
     Author:     Mathias Fleury, MPII, JKU
 
 Proof method for replaying veriT proofs.
 *)
 
 signature VERIT_REPLAY_METHODS =
 sig
   (*methods for verit proof rules*)
   val method_for: string -> Proof.context -> thm list -> term list -> term Symtab.table ->
      (string * term) list -> term -> thm
 
   val requires_subproof_assms : string list -> string -> bool
   val requires_local_input: string list -> string -> bool
   val eq_congruent_pred: Proof.context -> 'a -> term -> thm
   val discharge: Proof.context -> thm list -> term -> thm
 end;
 
 
 structure Verit_Replay_Methods: VERIT_REPLAY_METHODS =
 struct
 
 (*Some general comments on the proof format:
   1. Double negations are not always removed. This means for example that the equivalence rules
      cannot assume that the double negations have already been removed. Therefore, we match the
      term, instantiate the theorem, then use simp (to remove double negations), and finally use
      assumption.
   2. The reconstruction for rule forall_inst is buggy and tends to be very fragile, because the rule
      is doing much more that is supposed to do. Moreover types can make trivial goals (for the
      boolean structure) impossible to prove.
   3. Duplicate literals are sometimes removed, mostly by the SAT solver.
 
   Rules unsupported on purpose:
     * Distinct_Elim, XOR, let (we don't need them).
     * deep_skolemize (because it is not clear if verit still generates using it).
 *)
 
 datatype verit_rule =
    False | True |
 
    (*input: a repeated (normalized) assumption of  assumption of in a subproof*)
    Normalized_Input | Local_Input |
    (*Subproof:*)
    Subproof |
    (*Conjunction:*)
    And | Not_And | And_Pos | And_Neg |
    (*Disjunction""*)
    Or | Or_Pos | Not_Or | Or_Neg |
    (*Disjunction:*)
    Implies | Implies_Neg1 | Implies_Neg2 | Implies_Pos | Not_Implies1 | Not_Implies2 |
    (*Equivalence:*)
    Equiv_neg1 | Equiv_pos1 | Equiv_pos2 | Equiv_neg2 | Not_Equiv1 | Not_Equiv2 | Equiv1 | Equiv2 |
    (*If-then-else:*)
    ITE_Pos1 | ITE_Pos2 | ITE_Neg1 | ITE_Neg2 | Not_ITE1 | Not_ITE2 | ITE_Intro | ITE1 | ITE2 |
    (*Equality:*)
    Eq_Congruent | Eq_Reflexive | Eq_Transitive | Eq_Congruent_Pred | Trans |  Refl |  Cong |
    (*Arithmetics:*)
    LA_Disequality | LA_Generic | LA_Tautology |  LIA_Generic | LA_Totality | LA_RW_Eq |
    NLA_Generic |
    (*Quantifiers:*)
    Forall_Inst | Qnt_Rm_Unused | Qnt_Join | Onepoint | Bind | Skolem_Forall | Skolem_Ex |
    (*Resolution:*)
    Theory_Resolution | Resolution |
    (*Temporary rules, that the verit developpers want to remove:*)
    AC_Simp |
    Bfun_Elim |
    Qnt_CNF |
    (*Used to introduce skolem constants*)
    Definition |
    (*Former cong rules*)
    Bool_Simplify | Or_Simplify | Not_Simplify | And_Simplify | Equiv_Simplify |
    Implies_Simplify | Connective_Def | Minus_Simplify | Comp_Simplify |
    Eq_Simplify | ITE_Simplify | Sum_Simplify | Prod_Simplify |
    Qnt_Simplify | Not_Not | Tautological_Clause | Duplicate_Literals |
    (*Unsupported rule*)
-   Unsupported
+   Unsupported |
+   (*For compression*)
+   Theory_Resolution2
 
 
 fun verit_rule_of "bind" = Bind
   | verit_rule_of "cong" = Cong
   | verit_rule_of "refl" = Refl
   | verit_rule_of "equiv1" = Equiv1
   | verit_rule_of "equiv2" = Equiv2
   | verit_rule_of "equiv_pos1" = Equiv_pos1
-  | verit_rule_of "equiv_pos2" = Equiv_pos2
+   (*Equiv_pos2 covered below*)
   | verit_rule_of "equiv_neg1" = Equiv_neg1
   | verit_rule_of "equiv_neg2" = Equiv_neg2
   | verit_rule_of "sko_forall" = Skolem_Forall
   | verit_rule_of "sko_ex" = Skolem_Ex
   | verit_rule_of "eq_reflexive" = Eq_Reflexive
-  | verit_rule_of "th_resolution" = Theory_Resolution
   | verit_rule_of "forall_inst" = Forall_Inst
   | verit_rule_of "implies_pos" = Implies_Pos
   | verit_rule_of "or" = Or
   | verit_rule_of "not_or" = Not_Or
   | verit_rule_of "resolution" = Resolution
   | verit_rule_of "trans" = Trans
   | verit_rule_of "false" = False
   | verit_rule_of "ac_simp" = AC_Simp
   | verit_rule_of "and" = And
   | verit_rule_of "not_and" = Not_And
   | verit_rule_of "and_pos" = And_Pos
   | verit_rule_of "and_neg" = And_Neg
   | verit_rule_of "or_pos" = Or_Pos
   | verit_rule_of "or_neg" = Or_Neg
   | verit_rule_of "not_equiv1" = Not_Equiv1
   | verit_rule_of "not_equiv2" = Not_Equiv2
   | verit_rule_of "not_implies1" = Not_Implies1
   | verit_rule_of "not_implies2" = Not_Implies2
   | verit_rule_of "implies_neg1" = Implies_Neg1
   | verit_rule_of "implies_neg2" = Implies_Neg2
   | verit_rule_of "implies" = Implies
   | verit_rule_of "bfun_elim" = Bfun_Elim
   | verit_rule_of "ite1" = ITE1
   | verit_rule_of "ite2" = ITE2
   | verit_rule_of "not_ite1" = Not_ITE1
   | verit_rule_of "not_ite2" = Not_ITE2
   | verit_rule_of "ite_pos1" = ITE_Pos1
   | verit_rule_of "ite_pos2" = ITE_Pos2
   | verit_rule_of "ite_neg1" = ITE_Neg1
   | verit_rule_of "ite_neg2" = ITE_Neg2
   | verit_rule_of "la_disequality" = LA_Disequality
   | verit_rule_of "lia_generic" = LIA_Generic
   | verit_rule_of "la_generic" = LA_Generic
   | verit_rule_of "la_tautology" = LA_Tautology
   | verit_rule_of "la_totality" = LA_Totality
   | verit_rule_of "la_rw_eq"= LA_RW_Eq
   | verit_rule_of "nla_generic"= NLA_Generic
   | verit_rule_of "eq_transitive" = Eq_Transitive
   | verit_rule_of "qnt_rm_unused" = Qnt_Rm_Unused
   | verit_rule_of "onepoint" = Onepoint
   | verit_rule_of "qnt_join" = Qnt_Join
   | verit_rule_of "subproof" = Subproof
   | verit_rule_of "bool_simplify" = Bool_Simplify
   | verit_rule_of "or_simplify" = Or_Simplify
   | verit_rule_of "ite_simplify" = ITE_Simplify
   | verit_rule_of "and_simplify" = And_Simplify
   | verit_rule_of "not_simplify" = Not_Simplify
   | verit_rule_of "equiv_simplify" = Equiv_Simplify
   | verit_rule_of "eq_simplify" = Eq_Simplify
   | verit_rule_of "implies_simplify" = Implies_Simplify
   | verit_rule_of "connective_def" = Connective_Def
   | verit_rule_of "minus_simplify" = Minus_Simplify
   | verit_rule_of "sum_simplify" = Sum_Simplify
   | verit_rule_of "prod_simplify" = Prod_Simplify
   | verit_rule_of "comp_simplify" = Comp_Simplify
   | verit_rule_of "qnt_simplify" = Qnt_Simplify
   | verit_rule_of "tautology" = Tautological_Clause
   | 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 if r = Verit_Proof.theory_resolution2_rule then Theory_Resolution2
+     else if r = Verit_Proof.th_resolution_rule then Theory_Resolution
+     else if r = Verit_Proof.equiv_pos2_rule then Equiv_pos2
      else (@{print} ("Unsupport rule", r); Unsupported)
 
 fun string_of_verit_rule Bind = "Bind"
   | string_of_verit_rule Cong = "Cong"
   | string_of_verit_rule Refl = "Refl"
   | string_of_verit_rule Equiv1 = "Equiv1"
   | string_of_verit_rule Equiv2 = "Equiv2"
   | string_of_verit_rule Equiv_pos1 = "Equiv_pos1"
   | string_of_verit_rule Equiv_pos2 = "Equiv_pos2"
   | string_of_verit_rule Equiv_neg1 = "Equiv_neg1"
   | string_of_verit_rule Equiv_neg2 = "Equiv_neg2"
   | string_of_verit_rule Skolem_Forall = "Skolem_Forall"
   | string_of_verit_rule Skolem_Ex = "Skolem_Ex"
   | string_of_verit_rule Eq_Reflexive = "Eq_Reflexive"
   | string_of_verit_rule Theory_Resolution = "Theory_Resolution"
+  | string_of_verit_rule Theory_Resolution2 = "Theory_Resolution2"
   | string_of_verit_rule Forall_Inst = "forall_inst"
   | string_of_verit_rule Or = "Or"
   | string_of_verit_rule Not_Or = "Not_Or"
   | string_of_verit_rule Resolution = "Resolution"
   | string_of_verit_rule Eq_Congruent = "eq_congruent"
   | string_of_verit_rule Trans = "trans"
   | string_of_verit_rule False = "false"
   | string_of_verit_rule And = "and"
   | string_of_verit_rule And_Pos = "and_pos"
   | string_of_verit_rule Not_And = "not_and"
   | string_of_verit_rule And_Neg = "and_neg"
   | string_of_verit_rule Or_Pos = "or_pos"
   | string_of_verit_rule Or_Neg = "or_neg"
   | string_of_verit_rule AC_Simp = "ac_simp"
   | string_of_verit_rule Not_Equiv1 = "not_equiv1"
   | string_of_verit_rule Not_Equiv2 = "not_equiv2"
   | string_of_verit_rule Not_Implies1 = "not_implies1"
   | string_of_verit_rule Not_Implies2 = "not_implies2"
   | string_of_verit_rule Implies_Neg1 = "implies_neg1"
   | string_of_verit_rule Implies_Neg2 = "implies_neg2"
   | string_of_verit_rule Implies = "implies"
   | string_of_verit_rule Bfun_Elim = "bfun_elim"
   | string_of_verit_rule ITE1 = "ite1"
   | string_of_verit_rule ITE2 = "ite2"
   | string_of_verit_rule Not_ITE1 = "not_ite1"
   | string_of_verit_rule Not_ITE2 = "not_ite2"
   | string_of_verit_rule ITE_Pos1 = "ite_pos1"
   | string_of_verit_rule ITE_Pos2 = "ite_pos2"
   | string_of_verit_rule ITE_Neg1 = "ite_neg1"
   | string_of_verit_rule ITE_Neg2 = "ite_neg2"
   | string_of_verit_rule ITE_Intro = "ite_intro"
   | string_of_verit_rule LA_Disequality = "la_disequality"
   | string_of_verit_rule LA_Generic = "la_generic"
   | string_of_verit_rule LIA_Generic = "lia_generic"
   | string_of_verit_rule LA_Tautology = "la_tautology"
   | string_of_verit_rule LA_RW_Eq = "la_rw_eq"
   | string_of_verit_rule LA_Totality = "LA_Totality"
   | string_of_verit_rule NLA_Generic = "nla_generic"
   | string_of_verit_rule Eq_Transitive = "eq_transitive"
   | string_of_verit_rule Qnt_Rm_Unused = "qnt_remove_unused"
   | string_of_verit_rule Onepoint = "onepoint"
   | string_of_verit_rule Qnt_Join = "qnt_join"
   | string_of_verit_rule Eq_Congruent_Pred = "eq_congruent_pred"
   | string_of_verit_rule Normalized_Input = Verit_Proof.normalized_input_rule
   | string_of_verit_rule Local_Input = Verit_Proof.local_input_rule
   | string_of_verit_rule Subproof = "subproof"
   | string_of_verit_rule Bool_Simplify = "bool_simplify"
   | string_of_verit_rule Equiv_Simplify = "equiv_simplify"
   | string_of_verit_rule Eq_Simplify = "eq_simplify"
   | string_of_verit_rule Not_Simplify = "not_simplify"
   | string_of_verit_rule And_Simplify = "and_simplify"
   | string_of_verit_rule Or_Simplify = "or_simplify"
   | string_of_verit_rule ITE_Simplify = "ite_simplify"
   | string_of_verit_rule Implies_Simplify = "implies_simplify"
   | string_of_verit_rule Connective_Def = "connective_def"
   | string_of_verit_rule Minus_Simplify = "minus_simplify"
   | string_of_verit_rule Sum_Simplify = "sum_simplify"
   | 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 = Verit_Proof.not_not_rule
   | string_of_verit_rule Tautological_Clause = "tautology"
   | 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
 
 fun replay_error ctxt msg rule thms t =
   SMT_Replay_Methods.replay_error ctxt msg (string_of_verit_rule rule) thms t
 
 
 (* utility function *)
 
 fun eqsubst_all ctxt thms =
    K ((REPEAT o HEADGOAL) (EqSubst.eqsubst_asm_tac ctxt [0] thms))
    THEN' K ((REPEAT o HEADGOAL) (EqSubst.eqsubst_tac ctxt [0] thms))
 
 fun simplify_tac ctxt thms =
   ctxt
   |> empty_simpset
   |> put_simpset HOL_basic_ss
   |> (fn ctxt => ctxt addsimps @{thms simp_thms} addsimps thms)
   |> Simplifier.asm_full_simp_tac
 
 (* sko_forall requires the assumptions to be able to prove the equivalence in case of double
 skolemization. See comment below. *)
 fun requires_subproof_assms _ t =
   member (op =) ["refl", "sko_forall", "sko_ex", "cong"] t
 
 fun requires_local_input _ t =
   member (op =) [Verit_Proof.local_input_rule] t
 
 (*This is a weaker simplification form. It is weaker, but is also less likely to loop*)
 fun partial_simplify_tac ctxt thms =
   ctxt
   |> empty_simpset
   |> put_simpset HOL_basic_ss
   |> (fn ctxt => ctxt addsimps @{thms simp_thms} addsimps thms)
   |> Simplifier.full_simp_tac
 
 val try_provers = SMT_Replay_Methods.try_provers "verit"
 
 fun TRY' tac = fn i => TRY (tac i)
 fun REPEAT' tac = fn i => REPEAT (tac i)
 fun REPEAT_CHANGED tac = fn i => REPEAT (CHANGED (tac i))
 
 
 (* Bind *)
 
 (*The bind rule is non-obvious due to the handling of quantifiers:
   "\<And>x y a. x = y ==> (\<forall>b. P a b x) \<longleftrightarrow> (\<forall>b. P' a b y)"
   ------------------------------------------------------
             \<forall>a. (\<forall>b x. P a b x) \<longleftrightarrow> (\<forall>b y. P' a b y)
 is a valid application.*)
 
 val bind_thms =
   [@{lemma \<open>(\<And>x x'. x = x' \<Longrightarrow> P x = Q x') \<Longrightarrow> (\<forall>x. P x) = (\<forall>y. Q y)\<close> by blast},
    @{lemma \<open>(\<And>x x'. x = x' \<Longrightarrow> P x = Q x') \<Longrightarrow> (\<exists>x. P x) = (\<exists>y. Q y)\<close> by blast},
    @{lemma \<open>(\<And>x x'. x = x' \<Longrightarrow> P x = Q x') \<Longrightarrow> (\<exists>x. P x = Q x)\<close> by blast},
    @{lemma \<open>(\<And>x x'. x = x' \<Longrightarrow> P x = Q x') \<Longrightarrow> (\<forall>x. P x = Q x)\<close> by blast}]
 
 val bind_thms_same_name =
   [@{lemma \<open>(\<And>x. P x = Q x) \<Longrightarrow> (\<forall>x. P x) = (\<forall>y. Q y)\<close> by blast},
    @{lemma \<open>(\<And>x. P x = Q x) \<Longrightarrow> (\<exists>x. P x) = (\<exists>y. Q y)\<close> by blast},
    @{lemma \<open>(\<And>x. P x = Q x) \<Longrightarrow> (\<exists>x. P x = Q x)\<close> by blast},
    @{lemma \<open>(\<And>x. P x = Q x) \<Longrightarrow> (\<forall>x. P x = Q x)\<close> by blast}]
 
 fun extract_quantified_names_q (_ $ Abs (name, _, t)) =
    apfst (curry (op ::) name) (extract_quantified_names_q t)
   | extract_quantified_names_q t = ([], t)
 
 fun extract_forall_quantified_names_q (Const(\<^const_name>\<open>HOL.All\<close>, _) $ Abs (name, ty, t)) =
    (name,  ty) :: (extract_forall_quantified_names_q t)
   | extract_forall_quantified_names_q _ = []
 
 fun extract_all_forall_quantified_names_q (Const(\<^const_name>\<open>HOL.All\<close>, _) $ Abs (name, _, t)) =
       name :: (extract_all_forall_quantified_names_q t)
   | extract_all_forall_quantified_names_q (t $ u) =
       extract_all_forall_quantified_names_q t @ extract_all_forall_quantified_names_q u
   | extract_all_forall_quantified_names_q _ = []
 
 val extract_quantified_names_ba =
   SMT_Replay_Methods.dest_prop
   #> extract_quantified_names_q
   ##> HOLogic.dest_eq
   ##> fst
   ##> extract_quantified_names_q
   ##> fst
 
 val extract_quantified_names =
   extract_quantified_names_ba
   #> (op @)
 
 val extract_all_forall_quantified_names =
   SMT_Replay_Methods.dest_prop
   #> HOLogic.dest_eq
   #> fst
   #> extract_all_forall_quantified_names_q
 
 
 fun extract_all_exists_quantified_names_q (Const(\<^const_name>\<open>HOL.Ex\<close>, _) $ Abs (name, _, t)) =
       name :: (extract_all_exists_quantified_names_q t)
   | extract_all_exists_quantified_names_q (t $ u) =
       extract_all_exists_quantified_names_q t @ extract_all_exists_quantified_names_q u
   | extract_all_exists_quantified_names_q _ = []
 
 val extract_all_exists_quantified_names =
   SMT_Replay_Methods.dest_prop
   #> HOLogic.dest_eq
   #> fst
   #> extract_all_exists_quantified_names_q
 
 
 val extract_bind_names =
    HOLogic.dest_eq
    #> apply2 (fn (Free (name, _)) => name)
 
 fun combine_quant ctxt ((n1, n2) :: bounds) (n1' :: formula) =
     TRY' (if n1 = n1'
      then if n1 <> n2
        then
          resolve_tac ctxt bind_thms
          THEN' TRY'(resolve_tac ctxt [@{thm refl}])
          THEN' combine_quant ctxt bounds formula
        else resolve_tac ctxt bind_thms_same_name THEN' combine_quant ctxt bounds formula
      else resolve_tac ctxt @{thms allI} THEN' combine_quant ctxt ((n1, n2) :: bounds) formula)
   | combine_quant _ _ _ = K all_tac
 
 fun bind_quants ctxt args t =
   combine_quant ctxt (map extract_bind_names args) (extract_quantified_names t)
 
 fun generalize_prems_q [] prems = prems
   | generalize_prems_q (_ :: quants) prems =
       generalize_prems_q quants (@{thm spec} OF [prems])
 
 fun generalize_prems t = generalize_prems_q (fst (extract_quantified_names_ba t))
 
 fun bind ctxt [prems] args t =
   SMT_Replay_Methods.prove ctxt t (fn _ =>
     bind_quants ctxt args t
     THEN' TRY' (SOLVED' (resolve_tac ctxt [generalize_prems t prems]
       THEN_ALL_NEW TRY' (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms refl}))))
  | bind ctxt thms _ t = replay_error ctxt "invalid bind application" Bind thms t
 
 
 (* Congruence/Refl *)
 
 fun cong ctxt thms = try_provers ctxt
     (string_of_verit_rule Cong) [
   ("basic", SMT_Replay_Methods.cong_basic ctxt thms),
   ("unfolding then reflexivity", SMT_Replay_Methods.cong_unfolding_trivial ctxt thms),
   ("unfolding then auto", SMT_Replay_Methods.cong_unfolding_first ctxt thms),
   ("full", SMT_Replay_Methods.cong_full ctxt thms)] thms
 
 fun refl ctxt thm t =
   (case find_first (fn thm => t = Thm.full_prop_of thm) thm of
       SOME thm => thm
     | NONE =>
         (case try (fn t => SMT_Replay_Methods.match_instantiate ctxt t @{thm refl}) t of
           NONE => cong ctxt thm t
         | SOME thm => thm))
 
 
 (* Instantiation *)
 
 local
 fun dropWhile _ [] = []
   | dropWhile f (x :: xs) = if f x then dropWhile f xs else x :: xs
 in
 
 fun forall_inst ctxt _ _ insts t =
   let
     fun instantiate_and_solve i ({context = ctxt, prems = [prem], ...}: Subgoal.focus) =
         let
           val t = Thm.prop_of prem
           val quants = t
             |> SMT_Replay_Methods.dest_prop
             |> extract_forall_quantified_names_q
           val insts = map (Symtab.lookup insts o fst) (rev quants)
             |> dropWhile (curry (op =) NONE)
             |> rev
           fun option_map _ NONE = NONE
             | option_map f (SOME a) = SOME (f a)
           fun instantiate_with inst prem =
             Drule.infer_instantiate' ctxt [NONE, inst] @{thm spec} OF [prem]
           val inst_thm =
             fold instantiate_with
               (map (option_map (Thm.cterm_of ctxt)) insts)
               prem
         in
            (Method.insert_tac ctxt [inst_thm]
            THEN' TRY' (fn i => assume_tac ctxt i)
            THEN' TRY' (partial_simplify_tac ctxt @{thms eq_commute})) i
         end
      | instantiate_and_solve _ ({context = ctxt, prems = thms, ...}: Subgoal.focus) =
          replay_error ctxt "invalid application" Forall_Inst thms t
   in
     SMT_Replay_Methods.prove ctxt t (fn _ =>
       match_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF [@{thm impI}]]
       THEN' (fn i => Subgoal.FOCUS (instantiate_and_solve i) ctxt i))
   end
 end
 
 
 (* Or *)
 
 fun or _ (thm :: _) _ = thm
   | or ctxt thms t = replay_error ctxt "invalid bind application" Or thms t
 
 
 (* Implication *)
 
 val implies_pos_thm =
   [@{lemma \<open>\<not>(A \<longrightarrow> B) \<or> \<not>A \<or> B\<close> by blast},
   @{lemma \<open>\<not>(\<not>A \<longrightarrow> B) \<or> A \<or> B\<close> by blast}]
 
 fun implies_pos ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
   resolve_tac ctxt implies_pos_thm)
 
 fun extract_rewrite_rule_assumption _ thms =
   let
     fun is_rewrite_rule thm =
       (case Thm.prop_of thm of
         \<^term>\<open>Trueprop\<close> $ (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ Free(_, _)) => true
       | _ => false)
     fun is_context_rule thm =
       (case Thm.prop_of thm of
         \<^term>\<open>Trueprop\<close> $ (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ Free(_, _) $ Free(_, _)) => true
       | _ => false)
     val ctxt_eq =
       thms
       |> filter is_context_rule
     val rew =
       thms
       |> filter_out is_context_rule
       |> filter is_rewrite_rule
   in
     (ctxt_eq, rew)
   end
 
 local
   fun rewrite_all_skolems thm_indirect ctxt (SOME thm :: thms) =
      EqSubst.eqsubst_tac ctxt [0] [thm_indirect OF [thm]]
      THEN' (partial_simplify_tac ctxt (@{thms eq_commute}))
      THEN' rewrite_all_skolems thm_indirect ctxt thms
    | rewrite_all_skolems thm_indirect ctxt (NONE :: thms) = rewrite_all_skolems thm_indirect ctxt thms
    | rewrite_all_skolems _ _ [] = K (all_tac)
 
    fun extract_var_name (thm :: thms) =
        let val name = Thm.concl_of thm
          |> SMT_Replay_Methods.dest_prop
          |> HOLogic.dest_eq
          |> fst
          |> (fn Const(_,_) $ Abs(name, _, _) => [(name,@{thm sym} OF [thm])]
              | _ => [])
        in name :: extract_var_name thms end
     | extract_var_name [] = []
 
 fun skolem_tac extractor thm1 thm2 ctxt thms t  =
   let
     val (ctxt_eq, ts) = extract_rewrite_rule_assumption ctxt thms
     fun ordered_definitions () =
       let
         val var_order = extractor t
         val thm_names_with_var = extract_var_name ts |> flat
       in map (AList.lookup (op =) thm_names_with_var) var_order end
 
   in
     SMT_Replay_Methods.prove ctxt t (fn _ =>
       K (unfold_tac ctxt ctxt_eq)
       THEN' ((SOLVED' (K (unfold_tac ctxt (map (fn thm => thm1 OF [@{thm sym} OF [thm]]) ts))))
         ORELSE'
           (rewrite_all_skolems thm2 ctxt (ordered_definitions ())
           THEN' partial_simplify_tac ctxt @{thms eq_commute})))
   end
 in
 
 val skolem_forall =
   skolem_tac extract_all_forall_quantified_names @{thm verit_sko_forall_indirect}
     @{thm verit_sko_forall_indirect2}
 
 val skolem_ex =
   skolem_tac extract_all_exists_quantified_names @{thm verit_sko_ex_indirect}
     @{thm verit_sko_ex_indirect2}
 
 end
 
 fun eq_reflexive ctxt _ t = SMT_Replay_Methods.match_instantiate ctxt t @{thm refl}
 
 local
   fun not_not_prove ctxt _ =
     K (unfold_tac ctxt @{thms not_not})
     THEN' match_tac ctxt @{thms verit_or_simplify_1}
 
   fun duplicate_literals_prove ctxt prems =
     Method.insert_tac ctxt prems
     THEN' match_tac ctxt @{thms ccontr}
     THEN' K (unfold_tac ctxt @{thms de_Morgan_disj not_not})
     THEN' TRY o CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ctxt @{thms conjE})
     THEN' CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ctxt @{thms disjE})
     THEN' REPEAT' (ematch_tac ctxt @{thms notE} THEN' TRY' (assume_tac ctxt))
 
   fun tautological_clause_prove ctxt _ =
     match_tac ctxt @{thms verit_or_neg}
     THEN' K (unfold_tac ctxt @{thms not_not disj_assoc[symmetric]})
     THEN' TRY' (match_tac ctxt @{thms notE} THEN_ALL_NEW assume_tac ctxt)
+
+  val theory_resolution2_lemma = @{lemma \<open>a \<Longrightarrow> a = b \<Longrightarrow> b\<close> by blast}
 in
 
 fun prove_abstract abstracter tac ctxt thms t =
   let
     val thms = map (Conv.fconv_rule Thm.eta_long_conversion) thms
     val t' = Thm.eta_long_conversion (Object_Logic.dest_judgment ctxt (Thm.cterm_of ctxt t))
     val (_, t2) = Logic.dest_equals (Thm.prop_of t')
     val thm =
       SMT_Replay_Methods.prove_abstract ctxt thms t2 tac (
         fold_map (abstracter o SMT_Replay_Methods.dest_thm) thms ##>>
         abstracter (SMT_Replay_Methods.dest_prop t2))
   in
     @{thm verit_Pure_trans} OF [t', thm]
   end
 
 val not_not = prove_abstract SMT_Replay_Methods.abstract_bool_shallow not_not_prove
 
 val tautological_clause =
   prove_abstract SMT_Replay_Methods.abstract_bool_shallow tautological_clause_prove
 
 val duplicate_literals =
   prove_abstract SMT_Replay_Methods.abstract_bool_shallow duplicate_literals_prove
 
 val unit_res = prove_abstract SMT_Replay_Methods.abstract_bool_shallow SMT_Replay_Methods.prop_tac
 
+(*match_instantiate does not work*)
+fun theory_resolution2 ctxt prems t =
+  SMT_Replay_Methods.prove ctxt t (fn _ => match_tac ctxt [theory_resolution2_lemma OF prems])
+
 end
 
 
 fun normalized_input ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
   Method.insert_tac ctxt prems
   THEN' TRY' (K (unfold_tac ctxt @{thms SMT.trigger_def}))
   THEN' TRY' (partial_simplify_tac ctxt @{thms eq_commute}))
 
 val false_rule_thm = @{lemma \<open>\<not>False\<close> by blast}
 
 fun false_rule ctxt _ t = SMT_Replay_Methods.match_instantiate ctxt t false_rule_thm
 
 
 (* Transitivity *)
 
 val trans_bool_thm =
   @{lemma \<open>P = Q \<Longrightarrow> Q \<Longrightarrow> P\<close> by blast}
 
 fun trans ctxt thms t =
   let
     val prop_of = HOLogic.dest_Trueprop o Thm.full_prop_of
     fun combine_thms [thm1, thm2] =
           (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 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) =
           combine_thms (combine_thms [thm1, thm2] :: thms)
       | combine_thms thms = replay_error ctxt "invalid bind application" Trans thms t
      val t' = Thm.eta_long_conversion (Object_Logic.dest_judgment ctxt (Thm.cterm_of ctxt t))
      val (_, t2) = Logic.dest_equals (Thm.prop_of t')
      val thms = map (Conv.fconv_rule Thm.eta_long_conversion) thms
      val trans_thm = combine_thms thms
   in
      (case (prop_of trans_thm, t2) of
        ((Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ _),
              (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t3 $ _)) =>
        if t1 aconv t3 then trans_thm else trans_thm RS sym
       | _ => trans_thm (*to be on the safe side*))
   end
 
 
 fun tmp_AC_rule ctxt thms t =
   SMT_Replay_Methods.prove ctxt t (fn _ =>
     Method.insert_tac ctxt thms
     THEN' REPEAT_ALL_NEW (partial_simplify_tac ctxt @{thms eq_commute}
     THEN' TRY' (simplify_tac ctxt @{thms ac_simps conj_ac})
     THEN' TRY' (Classical.fast_tac ctxt)))
 
 
 (* And/Or *)
 
 local
   fun not_and_rule_prove ctxt prems =
      Method.insert_tac ctxt prems
      THEN' K (unfold_tac ctxt @{thms de_Morgan_conj})
      THEN_ALL_NEW TRY' (assume_tac ctxt)
 
   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 de_Morgan_disj not_not})
      THEN' TRY' (assume_tac ctxt)
 
   fun not_or_rule_prove ctxt prems =
      Method.insert_tac ctxt prems
      THEN' K (unfold_tac ctxt @{thms de_Morgan_disj not_not})
      THEN' TRY' (REPEAT' (match_tac ctxt @{thms conjI}))
      THEN_ALL_NEW ((REPEAT' (ematch_tac ctxt @{thms conjE}))
        THEN' TRY' (assume_tac ctxt))
 
   fun and_rule_prove ctxt prems =
      Method.insert_tac ctxt prems
      THEN' (fn i => REPEAT (dresolve_tac ctxt @{thms conjE} i THEN assume_tac ctxt (i+1)))
      THEN' TRY' (assume_tac ctxt)
 
   fun and_neg_rule_prove ctxt _ =
      match_tac ctxt @{thms verit_and_neg}
      THEN' K (unfold_tac ctxt @{thms de_Morgan_conj not_not})
      THEN' TRY' (assume_tac ctxt)
 
   fun prover tac = prove_abstract SMT_Replay_Methods.abstract_prop tac
 
 in
 
 val and_rule = prover and_rule_prove
 
 val not_and_rule = prover not_and_rule_prove
 
 val not_or_rule = prover not_or_rule_prove
 
 val or_pos_rule = prover or_pos_prove
 
 val and_neg_rule = prover and_neg_rule_prove
 
 val or_neg_rule = prove_abstract SMT_Replay_Methods.abstract_bool (fn ctxt => fn _ =>
   resolve_tac ctxt @{thms verit_or_neg}
   THEN' K (unfold_tac ctxt @{thms not_not})
   THEN_ALL_NEW
     (REPEAT'
       (SOLVED' (match_tac ctxt @{thms disjI1} THEN_ALL_NEW assume_tac ctxt)
        ORELSE' (match_tac ctxt @{thms disjI2} THEN' TRY' (assume_tac ctxt)))))
 
 fun and_pos ctxt _ t =
   SMT_Replay_Methods.prove ctxt t (fn _ =>
   REPEAT_CHANGED (resolve_tac ctxt @{thms verit_and_pos})
   THEN' TRY' (assume_tac ctxt))
 
 end
 
 
 (* Equivalence Transformation *)
 
 local
   fun prove_equiv equiv_thm ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ =>
         Method.insert_tac ctxt [equiv_thm OF [thm]]
         THEN' TRY' (assume_tac ctxt))
     | prove_equiv _ ctxt thms t = replay_error ctxt "invalid application in some equiv rule" Unsupported thms t
 in
 
 val not_equiv1 = prove_equiv @{lemma \<open>\<not>(A \<longleftrightarrow> B) \<Longrightarrow> A \<or> B\<close> by blast}
 val not_equiv2 = prove_equiv @{lemma \<open>\<not>(A \<longleftrightarrow> B) \<Longrightarrow> \<not>A \<or> \<not>B\<close> by blast}
 val equiv1  = prove_equiv @{lemma \<open>(A \<longleftrightarrow> B) \<Longrightarrow> \<not>A \<or> B\<close> by blast}
 val equiv2 = prove_equiv @{lemma \<open>(A \<longleftrightarrow> B) \<Longrightarrow> A \<or> \<not>B\<close> by blast}
 val not_implies1 = prove_equiv @{lemma \<open>\<not>(A \<longrightarrow> B) \<Longrightarrow> A\<close> by blast}
 val not_implies2 = prove_equiv @{lemma \<open>\<not>(A \<longrightarrow>B) \<Longrightarrow> \<not>B\<close> by blast}
 
 end
 
 
 (* Equivalence Lemma *)
 (*equiv_pos2 is very important for performance. We have tried various tactics, including
 a specialisation of SMT_Replay_Methods.match_instantiate, but there never was a measurable
 and consistent gain.*)
 local
   fun prove_equiv_pos_neg2 thm ctxt _ t =
     SMT_Replay_Methods.match_instantiate ctxt t thm
 in
 
 val equiv_pos1_thm = @{lemma \<open>\<not>(a \<longleftrightarrow> b) \<or> a \<or> \<not>b\<close> by blast+}
 val equiv_pos1 = prove_equiv_pos_neg2 equiv_pos1_thm
 
 val equiv_pos2_thm = @{lemma \<open>\<And>a b. (a \<noteq> b) \<or> \<not>a \<or> b\<close> by blast+}
 val equiv_pos2 = prove_equiv_pos_neg2 equiv_pos2_thm
 
 val equiv_neg1_thm = @{lemma \<open>(a \<longleftrightarrow> b) \<or> \<not>a \<or> \<not>b\<close> by blast+}
 val equiv_neg1 = prove_equiv_pos_neg2 equiv_neg1_thm
 
 val equiv_neg2_thm = @{lemma \<open>(a \<longleftrightarrow> b) \<or> a \<or> b\<close> by blast}
 val equiv_neg2 = prove_equiv_pos_neg2 equiv_neg2_thm
 
 end
 
 
 local
   fun implies_pos_neg_term ctxt thm (\<^term>\<open>Trueprop\<close> $
          (\<^term>\<open>HOL.disj\<close> $ (\<^term>\<open>HOL.implies\<close> $ a $ b) $ _)) =
          Drule.infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt) [a, b]) thm
      | implies_pos_neg_term ctxt thm  t =
         replay_error ctxt "invalid application in Implies" Unsupported [thm] t
 
   fun prove_implies_pos_neg thm ctxt _ t =
     let val thm = implies_pos_neg_term ctxt thm t
     in
       SMT_Replay_Methods.prove ctxt t (fn _ =>
         Method.insert_tac ctxt [thm]
         THEN' TRY' (assume_tac ctxt))
     end
 in
 
 val implies_neg1_thm = @{lemma \<open>(a \<longrightarrow> b) \<or> a\<close> by blast}
 val implies_neg1  = prove_implies_pos_neg implies_neg1_thm
 
 val implies_neg2_thm = @{lemma \<open>(a \<longrightarrow> b) \<or> \<not>b\<close> by blast}
 val implies_neg2 = prove_implies_pos_neg implies_neg2_thm
 
 val implies_thm = @{lemma \<open>(a \<longrightarrow> b) \<Longrightarrow> \<not>a \<or> b\<close> by blast}
 fun implies_rules ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
   Method.insert_tac ctxt [implies_thm OF prems]
   THEN' TRY' (assume_tac ctxt))
 
 end
 
 
 (* BFun *)
 
 local
   val bfun_theorems = @{thms verit_bfun_elim}
 in
 
 fun bfun_elim ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
   Method.insert_tac ctxt prems
   THEN' TRY' (eqsubst_all ctxt bfun_theorems)
   THEN' TRY' (simplify_tac ctxt @{thms eq_commute all_conj_distrib ex_disj_distrib}))
 
 end
 
 
 (* If-Then-Else *)
 
 local
   fun prove_ite ite_thm thm ctxt =
   resolve_tac ctxt [ite_thm OF [thm]]
   THEN' K (unfold_tac ctxt @{thms not_not})
   THEN' TRY' (assume_tac ctxt)
 in
 
 val ite_pos1_thm =
   @{lemma \<open>\<not>(if x then P else Q) \<or> x \<or> Q\<close> by auto}
 
 fun ite_pos1 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
   resolve_tac ctxt [ite_pos1_thm])
 
 val ite_pos2_thms =
   @{lemma \<open>\<not>(if x then P else Q) \<or> \<not>x \<or> P\<close> \<open>\<not>(if \<not>x then P else Q) \<or> x \<or> P\<close> by auto}
 
 fun ite_pos2 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => resolve_tac ctxt ite_pos2_thms)
 
 val ite_neg1_thms =
   @{lemma \<open>(if x then P else Q) \<or> x \<or> \<not>Q\<close> \<open>(if x then P else \<not>Q) \<or> x \<or> Q\<close> by auto}
 
 fun ite_neg1 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => resolve_tac ctxt ite_neg1_thms)
 
 val ite_neg2_thms =
   @{lemma \<open>(if x then P else Q) \<or> \<not>x \<or> \<not>P\<close> \<open>(if \<not>x then P else Q) \<or> x \<or> \<not>P\<close>
           \<open>(if x then \<not>P else Q) \<or> \<not>x \<or> P\<close> \<open>(if \<not>x then \<not>P else Q) \<or> x \<or> P\<close>
       by auto}
 
 fun ite_neg2 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => resolve_tac ctxt ite_neg2_thms)
 
 val ite1_thm =
   @{lemma \<open>(if x then P else Q) \<Longrightarrow> x \<or> Q\<close> by (auto split: if_splits) }
 
 fun ite1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => prove_ite ite1_thm thm ctxt)
 
 val ite2_thm =
   @{lemma \<open>(if x then P else Q) \<Longrightarrow> \<not>x \<or> P\<close> by (auto split: if_splits) }
 
 fun ite2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => prove_ite ite2_thm thm ctxt)
 
 val not_ite1_thm =
   @{lemma \<open>\<not>(if x then P else Q) \<Longrightarrow> x \<or> \<not>Q\<close> by (auto split: if_splits) }
 
 fun not_ite1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => prove_ite not_ite1_thm thm ctxt)
 
 val not_ite2_thm =
   @{lemma \<open>\<not>(if x then P else Q) \<Longrightarrow> \<not>x \<or> \<not>P\<close> by (auto split: if_splits) }
 
 fun not_ite2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => prove_ite not_ite2_thm thm ctxt)
 
 (*ite_intro can introduce new terms that are in the proof exactly the sames as the old one, but are
 not internally, hence the possible reordering.*)
 fun ite_intro ctxt _ t =
   let
     fun simplify_ite ctxt thms =
       ctxt
       |> empty_simpset
       |> put_simpset HOL_basic_ss
       |> (fn ctxt => ctxt addsimps thms @ @{thms if_True if_False refl simp_thms if_cancel})
       |> Raw_Simplifier.add_eqcong @{thm verit_ite_if_cong}
       |> Simplifier.full_simp_tac
   in
     SMT_Replay_Methods.prove ctxt t (fn _ => simplify_ite ctxt []
        THEN' TRY' (simplify_ite ctxt @{thms eq_commute}))
   end
 end
 
 
 (* Quantifiers *)
 
 local
   val rm_unused = @{lemma \<open>(\<forall>x. P) = P\<close> \<open>(\<exists>x. P) = P\<close> by blast+}
 
   fun qnt_cnf_tac ctxt =
     simplify_tac ctxt @{thms de_Morgan_conj de_Morgan_disj imp_conv_disj
       iff_conv_conj_imp if_bool_eq_disj ex_simps all_simps ex_disj_distrib
       verit_connective_def(3) all_conj_distrib}
     THEN' TRY' (Blast.blast_tac ctxt)
 in
 fun qnt_rm_unused ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
   K (unfold_tac ctxt rm_unused))
 
 fun onepoint ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ =>
   Method.insert_tac ctxt prems
   THEN' Simplifier.full_simp_tac (put_simpset HOL_basic_ss (empty_simpset ctxt)
     addsimps @{thms HOL.simp_thms HOL.all_simps}
     addsimprocs [@{simproc HOL.defined_All}, @{simproc HOL.defined_Ex}])
   THEN' TRY' (Blast.blast_tac ctxt)
   THEN' TRY' (Metis_Tactic.metis_tac [] ATP_Problem_Generate.combsN ctxt []))
 
 fun qnt_join ctxt _ t = SMT_Replay_Methods.prove ctxt t Classical.fast_tac
 
 fun qnt_cnf ctxt _ t = SMT_Replay_Methods.prove ctxt t qnt_cnf_tac
 
 fun qnt_simplify ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ =>
     partial_simplify_tac ctxt [])
 
 end
 
 (* Equality *)
 
 fun eq_transitive ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn  _ =>
   REPEAT_CHANGED (resolve_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF @{thms impI}])
   THEN' REPEAT' (resolve_tac ctxt @{thms impI})
   THEN' REPEAT' (eresolve_tac ctxt @{thms conjI})
   THEN' REPEAT' (fn i => dresolve_tac ctxt @{thms verit_eq_transitive} i THEN assume_tac ctxt (i+1))
   THEN' resolve_tac ctxt @{thms refl})
 
 local
   fun find_rew rews t t' =
     (case AList.lookup (op =) rews (t, t') of
       SOME thm => SOME (thm COMP @{thm symmetric})
     | NONE =>
       (case AList.lookup (op =) rews (t', t) of
         SOME thm => SOME thm
       | NONE => NONE))
 
   fun eq_pred_conv rews t ctxt ctrm =
     (case find_rew rews t (Thm.term_of ctrm) of
       SOME thm => Conv.rewr_conv thm ctrm
     | NONE =>
       (case t of
         f $ arg =>
           (Conv.fun_conv (eq_pred_conv rews f ctxt) then_conv
              Conv.arg_conv (eq_pred_conv rews arg ctxt)) ctrm
       | _ => Conv.all_conv ctrm))
 
   fun eq_pred_rewrite_tac ({context = ctxt, prems, concl, ...}: Subgoal.focus) =
     let
       val rews = prems
        |> map_filter (try (apfst (HOLogic.dest_eq o Thm.term_of o Object_Logic.dest_judgment ctxt o
             Thm.cconcl_of) o `(fn x => x)))
        |> map (apsnd (fn x => @{thm eq_reflection} OF [x]))
       fun conv_left conv = Conv.arg_conv (Conv.arg_conv conv)
       fun conv_left_neg conv = Conv.arg_conv (Conv.arg_conv (Conv.arg_conv conv))
       val (t1, conv_term) =
         (case Thm.term_of (Object_Logic.dest_judgment ctxt concl) of
           Const(_, _) $ (Const(\<^const_name>\<open>HOL.Not\<close>, _) $ t1) $ _ => (t1, conv_left)
         | Const(_, _) $ t1 $ (Const(\<^const_name>\<open>HOL.Not\<close>, _) $ _) => (t1, conv_left_neg)
         | Const(_, _) $ t1 $ _ => (t1, conv_left)
         | t1 => (t1, conv_left))
     fun throwing_CONVERSION cv i st = Seq.single (Conv.gconv_rule cv i st)
     in
       throwing_CONVERSION (conv_term (eq_pred_conv rews t1 ctxt))
     end
 in
 
 fun eq_congruent_pred ctxt _ t =
    SMT_Replay_Methods.prove ctxt t (fn _ =>
    REPEAT' (resolve_tac ctxt [@{thm disj_not1[of \<open>_ = _\<close>]} RSN (1, @{thm iffD2}) OF @{thms impI}])
    THEN' (fn i => Subgoal.FOCUS (fn focus => eq_pred_rewrite_tac focus i) ctxt i)
    THEN' (resolve_tac ctxt @{thms refl excluded_middle excluded_middle[of \<open>\<not>_\<close>, unfolded not_not]}
      ORELSE' assume_tac ctxt))
 
 val eq_congruent = eq_congruent_pred
 
 end
 
 
 (* Subproof *)
 
 fun subproof ctxt [prem] t =
      SMT_Replay_Methods.prove ctxt t (fn _ =>
       (resolve_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF [@{thm impI}],
            @{thm disj_not1[of \<open>\<not>_\<close>, unfolded not_not]} RSN (1, @{thm iffD2}) OF [@{thm impI}]]
         THEN' resolve_tac ctxt [prem]
         THEN_ALL_NEW assume_tac ctxt
         THEN' TRY' (assume_tac ctxt))
       ORELSE' TRY' (Method.insert_tac ctxt [prem] THEN' Blast.blast_tac ctxt))
   | subproof ctxt prems t =
       replay_error ctxt "invalid application, only one assumption expected" Subproof prems t
 
 
 (* Simplifying Steps *)
 
 (* The reconstruction is a bit tricky: At first we only rewrite only based on the rules that are
 passed as argument. Then we simply use simp_thms to reconstruct all the proofs (and these theorems
 cover all the simplification below).
 *)
 local
   fun rewrite_only_thms ctxt thms =
     ctxt
     |> empty_simpset
     |> put_simpset HOL_basic_ss
     |> (fn ctxt => ctxt addsimps thms)
     |> Simplifier.full_simp_tac
   fun rewrite_thms ctxt thms =
     ctxt
     |> empty_simpset
     |> put_simpset HOL_basic_ss
     |> Raw_Simplifier.add_eqcong @{thm eq_reflection[OF imp_cong]}
     |> (fn ctxt => ctxt addsimps thms addsimps @{thms simp_thms})
     |> Simplifier.full_simp_tac
 
   fun chain_rewrite_thms ctxt thms =
     TRY' (rewrite_only_thms ctxt thms)
     THEN' TRY' (rewrite_thms ctxt thms)
 
   fun chain_rewrite_two_step_with_ac_simps ctxt thms1 thms2 =
     TRY' (rewrite_only_thms ctxt thms1)
     THEN' TRY' (rewrite_thms ctxt thms2)
 
   fun chain_rewrite_thms_two_step ctxt thms1 thms2 thms3 thms4 =
     chain_rewrite_two_step_with_ac_simps ctxt thms1 thms2
     THEN' TRY' (chain_rewrite_two_step_with_ac_simps ctxt thms3 thms4)
 
   val imp_refl = @{lemma \<open>(P \<longrightarrow> P) = True\<close> by blast}
 
 in
 fun rewrite_bool_simplify ctxt _ t =
   SMT_Replay_Methods.prove ctxt t (fn _ =>
    (chain_rewrite_thms ctxt @{thms verit_bool_simplify}))
 
 fun rewrite_and_simplify ctxt _ t =
   SMT_Replay_Methods.prove ctxt t (fn _ =>
    (chain_rewrite_two_step_with_ac_simps ctxt @{thms verit_and_simplify verit_and_simplify1}
      @{thms verit_and_simplify}))
 
 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})
     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 _ =>
    (rewrite_only_thms ctxt @{thms verit_not_simplify}))
 
 fun rewrite_equiv_simplify ctxt _ t =
   SMT_Replay_Methods.prove ctxt t (fn _ =>
    (rewrite_only_thms ctxt @{thms verit_equiv_simplify}))
 
 fun rewrite_eq_simplify ctxt _ t =
   SMT_Replay_Methods.prove ctxt t (fn _ =>
    (chain_rewrite_two_step_with_ac_simps ctxt
       @{thms verit_eq_simplify}
       (Named_Theorems.get ctxt @{named_theorems ac_simps})))
 
 fun rewrite_implies_simplify ctxt _ t =
   SMT_Replay_Methods.prove ctxt t (fn _ =>
     (rewrite_only_thms ctxt @{thms verit_implies_simplify}))
 
 (* It is more efficient to first fold the implication symbols.
    That is however not enough when symbols appears within
    expressions, hence we also unfold implications in the
    other direction. *)
 fun rewrite_connective_def ctxt _ t =
     SMT_Replay_Methods.prove ctxt t (fn _ =>
       chain_rewrite_thms_two_step ctxt
         (imp_refl :: @{thms not_not verit_connective_def[symmetric]})
         (@{thms verit_connective_def[symmetric]})
         (imp_refl :: @{thms not_not verit_connective_def})
         (@{thms verit_connective_def}))
 
 fun rewrite_minus_simplify ctxt _ t =
     SMT_Replay_Methods.prove ctxt t (fn _ =>
       chain_rewrite_two_step_with_ac_simps ctxt
          @{thms arith_simps verit_minus_simplify}
          (Named_Theorems.get ctxt @{named_theorems ac_simps} @
           @{thms numerals arith_simps arith_special
              numeral_class.numeral.numeral_One}))
 
 fun rewrite_comp_simplify ctxt _ t =
     SMT_Replay_Methods.prove ctxt t (fn _ =>
         chain_rewrite_thms ctxt @{thms verit_comp_simplify})
 
 fun rewrite_ite_simplify ctxt _ t =
   SMT_Replay_Methods.prove ctxt t (fn _ =>
    (rewrite_only_thms ctxt @{thms verit_ite_simplify}))
 end
 
 
 (* Simplifications *)
 
 local
   fun simplify_arith ctxt thms = partial_simplify_tac ctxt
     (thms @ Named_Theorems.get ctxt @{named_theorems ac_simps} @ @{thms arith_simps})
 in
 
 fun sum_simplify ctxt _ t =
   SMT_Replay_Methods.prove ctxt t (fn _ =>
     simplify_arith ctxt @{thms verit_sum_simplify arith_special})
 
 fun prod_simplify ctxt _ t =
   SMT_Replay_Methods.prove ctxt t (fn _ =>
     simplify_arith ctxt @{thms verit_prod_simplify})
 
 end
 
 
 (* Arithmetics *)
 local
 
 val la_rw_eq_thm = @{lemma \<open>(a :: nat) = b \<or> (a \<le> b) \<or> (a \<ge> b)\<close> by auto}
 in
 fun la_rw_eq ctxt _ t = SMT_Replay_Methods.match_instantiate ctxt t la_rw_eq_thm
 
 fun la_generic_prove args ctxt _ = SMT_Replay_Arith.la_farkas args ctxt
 
 fun la_generic ctxt _ args =
   prove_abstract (SMT_Replay_Methods.abstract_arith_shallow ctxt) (la_generic_prove args) ctxt []
 
 fun lia_generic ctxt _ t =
   SMT_Replay_Methods.prove_arith_rewrite SMT_Replay_Methods.abstract_neq ctxt t
 
 fun la_disequality ctxt _ t =
   SMT_Replay_Methods.match_instantiate ctxt t @{thm verit_la_disequality}
 
 end
 
 (* Combining all together *)
 
 fun unsupported rule ctxt thms _ _ _ = SMT_Replay_Methods.replay_error ctxt "Unsupported verit rule"
   rule thms
 
 fun ignore_args f ctxt thm _ _ _ t = f ctxt thm t
 fun ignore_decls f ctxt thm args insts _ t = f ctxt thm args insts t
 fun ignore_insts f ctxt thm args _ _ t = f ctxt thm args t
 
 fun choose And = ignore_args and_rule
   | choose And_Neg = ignore_args and_neg_rule
   | choose And_Pos = ignore_args and_pos
   | choose And_Simplify = ignore_args rewrite_and_simplify
   | choose Bind = ignore_insts bind
   | choose Bool_Simplify = ignore_args rewrite_bool_simplify
   | choose Comp_Simplify = ignore_args rewrite_comp_simplify
   | choose Cong = ignore_args cong
   | choose Connective_Def = ignore_args rewrite_connective_def
   | choose Duplicate_Literals = ignore_args duplicate_literals
   | choose Eq_Congruent = ignore_args eq_congruent
   | choose Eq_Congruent_Pred = ignore_args eq_congruent_pred
   | choose Eq_Reflexive = ignore_args eq_reflexive
   | choose Eq_Simplify = ignore_args rewrite_eq_simplify
   | choose Eq_Transitive = ignore_args eq_transitive
   | choose Equiv1 = ignore_args equiv1
   | choose Equiv2 = ignore_args equiv2
   | choose Equiv_neg1 = ignore_args equiv_neg1
   | choose Equiv_neg2 = ignore_args equiv_neg2
   | choose Equiv_pos1 = ignore_args equiv_pos1
   | choose Equiv_pos2 = ignore_args equiv_pos2
   | choose Equiv_Simplify = ignore_args rewrite_equiv_simplify
   | choose False = ignore_args false_rule
   | choose Forall_Inst = ignore_decls forall_inst
   | choose Implies = ignore_args implies_rules
   | choose Implies_Neg1 = ignore_args implies_neg1
   | choose Implies_Neg2 = ignore_args implies_neg2
   | choose Implies_Pos = ignore_args implies_pos
   | choose Implies_Simplify = ignore_args rewrite_implies_simplify
   | choose ITE1 = ignore_args ite1
   | choose ITE2 = ignore_args ite2
   | choose ITE_Intro = ignore_args ite_intro
   | choose ITE_Neg1 = ignore_args ite_neg1
   | choose ITE_Neg2 = ignore_args ite_neg2
   | choose ITE_Pos1 = ignore_args ite_pos1
   | choose ITE_Pos2 = ignore_args ite_pos2
   | choose ITE_Simplify = ignore_args rewrite_ite_simplify
   | choose LA_Disequality = ignore_args la_disequality
   | choose LA_Generic = ignore_insts la_generic
   | choose LA_RW_Eq = ignore_args la_rw_eq
   | choose LA_Tautology = ignore_args SMT_Replay_Methods.arith_th_lemma_wo_shallow
   | choose LA_Totality = ignore_args SMT_Replay_Methods.arith_th_lemma_wo_shallow
   | choose LIA_Generic = ignore_args lia_generic
   | choose Local_Input = ignore_args refl
   | choose Minus_Simplify = ignore_args rewrite_minus_simplify
   | choose NLA_Generic = ignore_args SMT_Replay_Methods.arith_th_lemma_wo_shallow
   | choose Normalized_Input = ignore_args normalized_input
   | choose Not_And = ignore_args not_and_rule
   | choose Not_Equiv1 = ignore_args not_equiv1
   | choose Not_Equiv2 = ignore_args not_equiv2
   | choose Not_Implies1 = ignore_args not_implies1
   | choose Not_Implies2 = ignore_args not_implies2
   | choose Not_ITE1 = ignore_args not_ite1
   | choose Not_ITE2 = ignore_args not_ite2
   | choose Not_Not = ignore_args not_not
   | choose Not_Or = ignore_args not_or_rule
   | choose Not_Simplify = ignore_args rewrite_not_simplify
   | choose Or = ignore_args or
   | choose Or_Neg = ignore_args or_neg_rule
   | choose Or_Pos = ignore_args or_pos_rule
   | choose Or_Simplify = ignore_args rewrite_or_simplify
+  | choose Theory_Resolution2 = ignore_args theory_resolution2
   | choose Prod_Simplify = ignore_args prod_simplify
   | choose Qnt_Join = ignore_args qnt_join
   | choose Qnt_Rm_Unused = ignore_args qnt_rm_unused
   | choose Onepoint = ignore_args onepoint
   | choose Qnt_Simplify = ignore_args qnt_simplify
   | choose Refl = ignore_args refl
   | choose Resolution = ignore_args unit_res
   | choose Skolem_Ex = ignore_args skolem_ex
   | choose Skolem_Forall = ignore_args skolem_forall
   | choose Subproof = ignore_args subproof
   | choose Sum_Simplify = ignore_args sum_simplify
   | choose Tautological_Clause = ignore_args tautological_clause
   | choose Theory_Resolution = ignore_args unit_res
   | choose AC_Simp = ignore_args tmp_AC_rule
   | choose Bfun_Elim = ignore_args bfun_elim
   | choose Qnt_CNF = ignore_args qnt_cnf
   | choose Trans = ignore_args trans
   | choose r = unsupported (string_of_verit_rule r)
 
 type verit_method = Proof.context -> thm list -> term -> thm
 type abs_context = int * term Termtab.table
 
 fun with_tracing rule method ctxt thms args insts decls t =
   let val _ = SMT_Replay_Methods.trace_goal ctxt rule thms t
   in method ctxt thms args insts decls t end
 
 fun method_for rule = with_tracing rule (choose (verit_rule_of rule))
 
 fun discharge ctxt [thm] t =
   SMT_Replay_Methods.prove ctxt t (fn _ =>
     resolve_tac ctxt [thm] THEN_ALL_NEW (resolve_tac ctxt @{thms refl}))
 
 end;