# HG changeset patch
# User wenzelm
# Date 1266349364 -3600
# Node ID 3011b2149089b11e1266daa01a8b029226a68edf
# Parent  52ab455915d85f8022a0f6426bcaf77ebeae4b94# Parent  eee63670b5aa7786c2b05aefe3f88c1d5d2f342b
merged

diff -r eee63670b5aa -r 3011b2149089 etc/components
--- a/etc/components	Tue Feb 16 20:41:52 2010 +0100
+++ b/etc/components	Tue Feb 16 20:42:44 2010 +0100
@@ -13,6 +13,7 @@
 #misc components
 src/Tools/Code
 src/Tools/WWW_Find
+src/Tools/Cache_IO
 src/HOL/Tools/ATP_Manager
 src/HOL/Mirabelle
 src/HOL/Library/Sum_Of_Squares
diff -r eee63670b5aa -r 3011b2149089 src/HOL/Boogie/Examples/Boogie_Dijkstra.certs
--- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.certs	Tue Feb 16 20:41:52 2010 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.certs	Tue Feb 16 20:42:44 2010 +0100
@@ -1,4 +1,4 @@
-2/jIbDaU00KSkSih1o9sXg 193550
+JinTdmjIiorL0/vvOyf3+w 6542 0
 #2 := false
 decl up_6 :: (-> T4 T2 bool)
 decl ?x47!7 :: (-> T2 T2)
@@ -6541,4 +6541,3 @@
 #23081 := [unit-resolution #19916 #27207]: #17029
 [unit-resolution #23081 #23182 #18055 #27235]: false
 unsat
-
diff -r eee63670b5aa -r 3011b2149089 src/HOL/Boogie/Examples/Boogie_Max.certs
--- a/src/HOL/Boogie/Examples/Boogie_Max.certs	Tue Feb 16 20:41:52 2010 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Max.certs	Tue Feb 16 20:42:44 2010 +0100
@@ -1,4 +1,4 @@
-yJC0k+R1r4pWViX9DxewEQ 62526
+iks4GfP7O/NgNFyGZ4ynjQ 2224 0
 #2 := false
 #4 := 0::int
 decl uf_3 :: (-> int int)
@@ -2223,4 +2223,3 @@
 #2015 := [unit-resolution #2013 #2021]: #2041
 [th-lemma #2015 #2047 #2043]: false
 unsat
-
diff -r eee63670b5aa -r 3011b2149089 src/HOL/Boogie/Examples/VCC_Max.certs
--- a/src/HOL/Boogie/Examples/VCC_Max.certs	Tue Feb 16 20:41:52 2010 +0100
+++ b/src/HOL/Boogie/Examples/VCC_Max.certs	Tue Feb 16 20:42:44 2010 +0100
@@ -1,4 +1,4 @@
-8ZKUEUSWY0Pcw6t0NqCjrQ 253722
+6Q8QWdFv463DpfVfkr0XnA 7790 0
 #2 := false
 decl uf_110 :: (-> T4 T5 int)
 decl uf_66 :: (-> T5 int T3 T5)
@@ -7789,4 +7789,3 @@
 #30656 := [unit-resolution #30273 #30655 #30643]: #30496
 [unit-resolution #30529 #30656 #30639]: false
 unsat
-
diff -r eee63670b5aa -r 3011b2149089 src/HOL/Boogie/Examples/VCC_Max.thy
--- a/src/HOL/Boogie/Examples/VCC_Max.thy	Tue Feb 16 20:41:52 2010 +0100
+++ b/src/HOL/Boogie/Examples/VCC_Max.thy	Tue Feb 16 20:42:44 2010 +0100
@@ -57,4 +57,4 @@
 
 boogie_end
 
-end
\ No newline at end of file
+end
diff -r eee63670b5aa -r 3011b2149089 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Feb 16 20:41:52 2010 +0100
+++ b/src/HOL/IsaMakefile	Tue Feb 16 20:42:44 2010 +0100
@@ -1226,7 +1226,8 @@
   SMT/Tools/smt_solver.ML SMT/Tools/cvc3_solver.ML                      \
   SMT/Tools/yices_solver.ML SMT/Tools/z3_proof_terms.ML                 \
   SMT/Tools/z3_proof_rules.ML SMT/Tools/z3_proof.ML                     \
-  SMT/Tools/z3_model.ML SMT/Tools/z3_interface.ML SMT/Tools/z3_solver.ML
+  SMT/Tools/z3_model.ML SMT/Tools/z3_interface.ML			\
+  SMT/Tools/z3_solver.ML $(SRC)/Tools/Cache_IO/cache_io.ML
 	@cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT
 
 
diff -r eee63670b5aa -r 3011b2149089 src/HOL/Multivariate_Analysis/Determinants.thy
--- a/src/HOL/Multivariate_Analysis/Determinants.thy	Tue Feb 16 20:41:52 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Tue Feb 16 20:42:44 2010 +0100
@@ -121,7 +121,7 @@
 (* Basic determinant properties.                                             *)
 (* ------------------------------------------------------------------------- *)
 
-lemma det_transp: "det (transp A) = det (A::'a::comm_ring_1 ^'n^'n)"
+lemma det_transpose: "det (transpose A) = det (A::'a::comm_ring_1 ^'n^'n)"
 proof-
   let ?di = "\<lambda>A i j. A$i$j"
   let ?U = "(UNIV :: 'n set)"
@@ -133,18 +133,18 @@
     from permutes_inj[OF pU]
     have pi: "inj_on p ?U" by (blast intro: subset_inj_on)
     from permutes_image[OF pU]
-    have "setprod (\<lambda>i. ?di (transp A) i (inv p i)) ?U = setprod (\<lambda>i. ?di (transp A) i (inv p i)) (p ` ?U)" by simp
-    also have "\<dots> = setprod ((\<lambda>i. ?di (transp A) i (inv p i)) o p) ?U"
+    have "setprod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U = setprod (\<lambda>i. ?di (transpose A) i (inv p i)) (p ` ?U)" by simp
+    also have "\<dots> = setprod ((\<lambda>i. ?di (transpose A) i (inv p i)) o p) ?U"
       unfolding setprod_reindex[OF pi] ..
     also have "\<dots> = setprod (\<lambda>i. ?di A i (p i)) ?U"
     proof-
       {fix i assume i: "i \<in> ?U"
         from i permutes_inv_o[OF pU] permutes_in_image[OF pU]
-        have "((\<lambda>i. ?di (transp A) i (inv p i)) o p) i = ?di A i (p i)"
-          unfolding transp_def by (simp add: expand_fun_eq)}
-      then show "setprod ((\<lambda>i. ?di (transp A) i (inv p i)) o p) ?U = setprod (\<lambda>i. ?di A i (p i)) ?U" by (auto intro: setprod_cong)
+        have "((\<lambda>i. ?di (transpose A) i (inv p i)) o p) i = ?di A i (p i)"
+          unfolding transpose_def by (simp add: expand_fun_eq)}
+      then show "setprod ((\<lambda>i. ?di (transpose A) i (inv p i)) o p) ?U = setprod (\<lambda>i. ?di A i (p i)) ?U" by (auto intro: setprod_cong)
     qed
-    finally have "of_int (sign (inv p)) * (setprod (\<lambda>i. ?di (transp A) i (inv p i)) ?U) = of_int (sign p) * (setprod (\<lambda>i. ?di A i (p i)) ?U)" using sth
+    finally have "of_int (sign (inv p)) * (setprod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U) = of_int (sign p) * (setprod (\<lambda>i. ?di A i (p i)) ?U)" using sth
       by simp}
   then show ?thesis unfolding det_def apply (subst setsum_permutations_inverse)
   apply (rule setsum_cong2) by blast
@@ -267,12 +267,12 @@
   shows "det(\<chi> i j. A$i$ p j :: 'a^'n^'n) = of_int (sign p) * det A"
 proof-
   let ?Ap = "\<chi> i j. A$i$ p j :: 'a^'n^'n"
-  let ?At = "transp A"
-  have "of_int (sign p) * det A = det (transp (\<chi> i. transp A $ p i))"
-    unfolding det_permute_rows[OF p, of ?At] det_transp ..
+  let ?At = "transpose A"
+  have "of_int (sign p) * det A = det (transpose (\<chi> i. transpose A $ p i))"
+    unfolding det_permute_rows[OF p, of ?At] det_transpose ..
   moreover
-  have "?Ap = transp (\<chi> i. transp A $ p i)"
-    by (simp add: transp_def Cart_eq)
+  have "?Ap = transpose (\<chi> i. transpose A $ p i)"
+    by (simp add: transpose_def Cart_eq)
   ultimately show ?thesis by simp
 qed
 
@@ -299,9 +299,9 @@
   assumes ij: "i \<noteq> j"
   and r: "column i A = column j A"
   shows "det A = 0"
-apply (subst det_transp[symmetric])
+apply (subst det_transpose[symmetric])
 apply (rule det_identical_rows[OF ij])
-by (metis row_transp r)
+by (metis row_transpose r)
 
 lemma det_zero_row:
   fixes A :: "'a::{idom, ring_char_0}^'n^'n"
@@ -317,9 +317,9 @@
   fixes A :: "'a::{idom,ring_char_0}^'n^'n"
   assumes r: "column i A = 0"
   shows "det A = 0"
-  apply (subst det_transp[symmetric])
+  apply (subst det_transpose[symmetric])
   apply (rule det_zero_row [of i])
-  by (metis row_transp r)
+  by (metis row_transpose r)
 
 lemma det_row_add:
   fixes a b c :: "'n::finite \<Rightarrow> _ ^ 'n"
@@ -489,7 +489,7 @@
 qed
 
 lemma det_dependent_columns: assumes d: "dependent(columns (A::'a::linordered_idom^'n^'n))" shows "det A = 0"
-by (metis d det_dependent_rows rows_transp det_transp)
+by (metis d det_dependent_rows rows_transpose det_transpose)
 
 (* ------------------------------------------------------------------------- *)
 (* Multilinearity and the multiplication formula.                            *)
@@ -760,7 +760,7 @@
 (* Cramer's rule.                                                            *)
 (* ------------------------------------------------------------------------- *)
 
-lemma cramer_lemma_transp:
+lemma cramer_lemma_transpose:
   fixes A:: "'a::linordered_idom^'n^'n" and x :: "'a ^'n"
   shows "det ((\<chi> i. if i = k then setsum (\<lambda>i. x$i *s row i A) (UNIV::'n set)
                            else row i A)::'a^'n^'n) = x$k * det A"
@@ -801,13 +801,13 @@
   shows "det((\<chi> i j. if j = k then (A *v x)$i else A$i$j):: 'a^'n^'n) = x$k * det A"
 proof-
   let ?U = "UNIV :: 'n set"
-  have stupid: "\<And>c. setsum (\<lambda>i. c i *s row i (transp A)) ?U = setsum (\<lambda>i. c i *s column i A) ?U"
-    by (auto simp add: row_transp intro: setsum_cong2)
+  have stupid: "\<And>c. setsum (\<lambda>i. c i *s row i (transpose A)) ?U = setsum (\<lambda>i. c i *s column i A) ?U"
+    by (auto simp add: row_transpose intro: setsum_cong2)
   show ?thesis  unfolding matrix_mult_vsum
-  unfolding cramer_lemma_transp[of k x "transp A", unfolded det_transp, symmetric]
+  unfolding cramer_lemma_transpose[of k x "transpose A", unfolded det_transpose, symmetric]
   unfolding stupid[of "\<lambda>i. x$i"]
-  apply (subst det_transp[symmetric])
-  apply (rule cong[OF refl[of det]]) by (vector transp_def column_def row_def)
+  apply (subst det_transpose[symmetric])
+  apply (rule cong[OF refl[of det]]) by (vector transpose_def column_def row_def)
 qed
 
 lemma cramer:
@@ -840,13 +840,13 @@
   apply (simp add: real_vector_norm_def)
   by (simp add: dot_norm  linear_add[symmetric])
 
-definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow> transp Q ** Q = mat 1 \<and> Q ** transp Q = mat 1"
+definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow> transpose Q ** Q = mat 1 \<and> Q ** transpose Q = mat 1"
 
-lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n)  \<longleftrightarrow> transp Q ** Q = mat 1"
+lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n)  \<longleftrightarrow> transpose Q ** Q = mat 1"
   by (metis matrix_left_right_inverse orthogonal_matrix_def)
 
 lemma orthogonal_matrix_id: "orthogonal_matrix (mat 1 :: _^'n^'n)"
-  by (simp add: orthogonal_matrix_def transp_mat matrix_mul_lid)
+  by (simp add: orthogonal_matrix_def transpose_mat matrix_mul_lid)
 
 lemma orthogonal_matrix_mul:
   fixes A :: "real ^'n^'n"
@@ -854,7 +854,7 @@
   and oB: "orthogonal_matrix B"
   shows "orthogonal_matrix(A ** B)"
   using oA oB
-  unfolding orthogonal_matrix matrix_transp_mul
+  unfolding orthogonal_matrix matrix_transpose_mul
   apply (subst matrix_mul_assoc)
   apply (subst matrix_mul_assoc[symmetric])
   by (simp add: matrix_mul_rid)
@@ -873,7 +873,7 @@
     from ot have lf: "linear f" and fd: "\<forall>v w. f v \<bullet> f w = v \<bullet> w"
       unfolding  orthogonal_transformation_def orthogonal_matrix by blast+
     {fix i j
-      let ?A = "transp ?mf ** ?mf"
+      let ?A = "transpose ?mf ** ?mf"
       have th0: "\<And>b (x::'a::comm_ring_1). (if b then 1 else 0)*x = (if b then x else 0)"
         "\<And>b (x::'a::comm_ring_1). x*(if b then 1 else 0) = (if b then x else 0)"
         by simp_all
@@ -908,9 +908,9 @@
     also have "\<dots> \<longleftrightarrow> x = 1 \<or> x = - 1" unfolding th0 th1 by simp
     finally show "?ths x" ..
   qed
-  from oQ have "Q ** transp Q = mat 1" by (metis orthogonal_matrix_def)
-  hence "det (Q ** transp Q) = det (mat 1:: 'a^'n^'n)" by simp
-  hence "det Q * det Q = 1" by (simp add: det_mul det_I det_transp)
+  from oQ have "Q ** transpose Q = mat 1" by (metis orthogonal_matrix_def)
+  hence "det (Q ** transpose Q) = det (mat 1:: 'a^'n^'n)" by simp
+  hence "det Q * det Q = 1" by (simp add: det_mul det_I det_transpose)
   then show ?thesis unfolding th .
 qed
 
diff -r eee63670b5aa -r 3011b2149089 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Tue Feb 16 20:41:52 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Tue Feb 16 20:42:44 2010 +0100
@@ -2029,7 +2029,8 @@
   where "v v* m == (\<chi> j. setsum (\<lambda>i. ((m$i)$j) * (v$i)) (UNIV :: 'm set)) :: 'a^'n"
 
 definition "(mat::'a::zero => 'a ^'n^'n) k = (\<chi> i j. if i = j then k else 0)"
-definition "(transp::'a^'n^'m \<Rightarrow> 'a^'m^'n) A = (\<chi> i j. ((A$j)$i))"
+definition transpose where 
+  "(transpose::'a^'n^'m \<Rightarrow> 'a^'m^'n) A = (\<chi> i j. ((A$j)$i))"
 definition "(row::'m => 'a ^'n^'m \<Rightarrow> 'a ^'n) i A = (\<chi> j. ((A$i)$j))"
 definition "(column::'n =>'a^'n^'m =>'a^'m) j A = (\<chi> i. ((A$i)$j))"
 definition "rows(A::'a^'n^'m) = { row i A | i. i \<in> (UNIV :: 'm set)}"
@@ -2071,8 +2072,8 @@
   by (simp add: cond_value_iff cond_application_beta
     setsum_delta' cong del: if_weak_cong)
 
-lemma matrix_transp_mul: "transp(A ** B) = transp B ** transp (A::'a::comm_semiring_1^_^_)"
-  by (simp add: matrix_matrix_mult_def transp_def Cart_eq mult_commute)
+lemma matrix_transpose_mul: "transpose(A ** B) = transpose B ** transpose (A::'a::comm_semiring_1^_^_)"
+  by (simp add: matrix_matrix_mult_def transpose_def Cart_eq mult_commute)
 
 lemma matrix_eq:
   fixes A B :: "'a::semiring_1 ^ 'n ^ 'm"
@@ -2094,26 +2095,26 @@
   apply (subst setsum_commute)
   by simp
 
-lemma transp_mat: "transp (mat n) = mat n"
-  by (vector transp_def mat_def)
-
-lemma transp_transp: "transp(transp A) = A"
-  by (vector transp_def)
-
-lemma row_transp:
+lemma transpose_mat: "transpose (mat n) = mat n"
+  by (vector transpose_def mat_def)
+
+lemma transpose_transpose: "transpose(transpose A) = A"
+  by (vector transpose_def)
+
+lemma row_transpose:
   fixes A:: "'a::semiring_1^_^_"
-  shows "row i (transp A) = column i A"
-  by (simp add: row_def column_def transp_def Cart_eq)
-
-lemma column_transp:
+  shows "row i (transpose A) = column i A"
+  by (simp add: row_def column_def transpose_def Cart_eq)
+
+lemma column_transpose:
   fixes A:: "'a::semiring_1^_^_"
-  shows "column i (transp A) = row i A"
-  by (simp add: row_def column_def transp_def Cart_eq)
-
-lemma rows_transp: "rows(transp (A::'a::semiring_1^_^_)) = columns A"
-by (auto simp add: rows_def columns_def row_transp intro: set_ext)
-
-lemma columns_transp: "columns(transp (A::'a::semiring_1^_^_)) = rows A" by (metis transp_transp rows_transp)
+  shows "column i (transpose A) = row i A"
+  by (simp add: row_def column_def transpose_def Cart_eq)
+
+lemma rows_transpose: "rows(transpose (A::'a::semiring_1^_^_)) = columns A"
+by (auto simp add: rows_def columns_def row_transpose intro: set_ext)
+
+lemma columns_transpose: "columns(transpose (A::'a::semiring_1^_^_)) = rows A" by (metis transpose_transpose rows_transpose)
 
 text{* Two sometimes fruitful ways of looking at matrix-vector multiplication. *}
 
@@ -2176,19 +2177,19 @@
   using lf lg linear_compose[OF lf lg] matrix_works[OF linear_compose[OF lf lg]]
   by (simp  add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def)
 
-lemma matrix_vector_column:"(A::'a::comm_semiring_1^'n^_) *v x = setsum (\<lambda>i. (x$i) *s ((transp A)$i)) (UNIV:: 'n set)"
-  by (simp add: matrix_vector_mult_def transp_def Cart_eq mult_commute)
-
-lemma adjoint_matrix: "adjoint(\<lambda>x. (A::'a::comm_ring_1^'n^'m) *v x) = (\<lambda>x. transp A *v x)"
+lemma matrix_vector_column:"(A::'a::comm_semiring_1^'n^_) *v x = setsum (\<lambda>i. (x$i) *s ((transpose A)$i)) (UNIV:: 'n set)"
+  by (simp add: matrix_vector_mult_def transpose_def Cart_eq mult_commute)
+
+lemma adjoint_matrix: "adjoint(\<lambda>x. (A::'a::comm_ring_1^'n^'m) *v x) = (\<lambda>x. transpose A *v x)"
   apply (rule adjoint_unique[symmetric])
   apply (rule matrix_vector_mul_linear)
-  apply (simp add: transp_def dot_def matrix_vector_mult_def setsum_left_distrib setsum_right_distrib)
+  apply (simp add: transpose_def dot_def matrix_vector_mult_def setsum_left_distrib setsum_right_distrib)
   apply (subst setsum_commute)
   apply (auto simp add: mult_ac)
   done
 
 lemma matrix_adjoint: assumes lf: "linear (f :: 'a::comm_ring_1^'n \<Rightarrow> 'a ^'m)"
-  shows "matrix(adjoint f) = transp(matrix f)"
+  shows "matrix(adjoint f) = transpose(matrix f)"
   apply (subst matrix_vector_mul[OF lf])
   unfolding adjoint_matrix matrix_of_matrix_vector_mul ..
 
@@ -4317,13 +4318,13 @@
 
 (* Detailed theorems about left and right invertibility in general case.     *)
 
-lemma left_invertible_transp:
-  "(\<exists>(B). B ** transp (A) = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). A ** B = mat 1)"
-  by (metis matrix_transp_mul transp_mat transp_transp)
-
-lemma right_invertible_transp:
-  "(\<exists>(B). transp (A) ** B = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). B ** A = mat 1)"
-  by (metis matrix_transp_mul transp_mat transp_transp)
+lemma left_invertible_transpose:
+  "(\<exists>(B). B ** transpose (A) = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). A ** B = mat 1)"
+  by (metis matrix_transpose_mul transpose_mat transpose_transpose)
+
+lemma right_invertible_transpose:
+  "(\<exists>(B). transpose (A) ** B = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). B ** A = mat 1)"
+  by (metis matrix_transpose_mul transpose_mat transpose_transpose)
 
 lemma linear_injective_left_inverse:
   assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'m)" and fi: "inj f"
@@ -4438,9 +4439,9 @@
 lemma matrix_right_invertible_independent_rows:
   fixes A :: "real^'n^'m"
   shows "(\<exists>(B::real^'m^'n). A ** B = mat 1) \<longleftrightarrow> (\<forall>c. setsum (\<lambda>i. c i *s row i A) (UNIV :: 'm set) = 0 \<longrightarrow> (\<forall>i. c i = 0))"
-  unfolding left_invertible_transp[symmetric]
+  unfolding left_invertible_transpose[symmetric]
     matrix_left_invertible_independent_columns
-  by (simp add: column_transp)
+  by (simp add: column_transpose)
 
 lemma matrix_right_invertible_span_columns:
   "(\<exists>(B::real ^'n^'m). (A::real ^'m^'n) ** B = mat 1) \<longleftrightarrow> span (columns A) = UNIV" (is "?lhs = ?rhs")
@@ -4506,8 +4507,8 @@
 
 lemma matrix_left_invertible_span_rows:
   "(\<exists>(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> span (rows A) = UNIV"
-  unfolding right_invertible_transp[symmetric]
-  unfolding columns_transp[symmetric]
+  unfolding right_invertible_transpose[symmetric]
+  unfolding columns_transpose[symmetric]
   unfolding matrix_right_invertible_span_columns
  ..
 
@@ -4728,12 +4729,12 @@
 
 definition "columnvector v = (\<chi> i j. (v$i))"
 
-lemma transp_columnvector:
- "transp(columnvector v) = rowvector v"
-  by (simp add: transp_def rowvector_def columnvector_def Cart_eq)
-
-lemma transp_rowvector: "transp(rowvector v) = columnvector v"
-  by (simp add: transp_def columnvector_def rowvector_def Cart_eq)
+lemma transpose_columnvector:
+ "transpose(columnvector v) = rowvector v"
+  by (simp add: transpose_def rowvector_def columnvector_def Cart_eq)
+
+lemma transpose_rowvector: "transpose(rowvector v) = columnvector v"
+  by (simp add: transpose_def columnvector_def rowvector_def Cart_eq)
 
 lemma dot_rowvector_columnvector:
   "columnvector (A *v v) = A ** columnvector v"
@@ -4745,9 +4746,9 @@
 lemma dot_matrix_vector_mul:
   fixes A B :: "real ^'n ^'n" and x y :: "real ^'n"
   shows "(A *v x) \<bullet> (B *v y) =
-      (((rowvector x :: real^'n^1) ** ((transp A ** B) ** (columnvector y :: real ^1^'n)))$1)$1"
-unfolding dot_matrix_product transp_columnvector[symmetric]
-  dot_rowvector_columnvector matrix_transp_mul matrix_mul_assoc ..
+      (((rowvector x :: real^'n^1) ** ((transpose A ** B) ** (columnvector y :: real ^1^'n)))$1)$1"
+unfolding dot_matrix_product transpose_columnvector[symmetric]
+  dot_rowvector_columnvector matrix_transpose_mul matrix_mul_assoc ..
 
 (* Infinity norm.                                                            *)
 
diff -r eee63670b5aa -r 3011b2149089 src/HOL/SMT/Examples/SMT_Examples.certs
--- a/src/HOL/SMT/Examples/SMT_Examples.certs	Tue Feb 16 20:41:52 2010 +0100
+++ b/src/HOL/SMT/Examples/SMT_Examples.certs	Tue Feb 16 20:42:44 2010 +0100
@@ -1,4 +1,4 @@
-yknPpoG47N1CXnUaEL9RvQ 133
+Fg1W6egjwo9zhhAmUXOW+w 8 0
 #2 := false
 #1 := true
 #4 := (not true)
@@ -7,8 +7,7 @@
 #20 := [asserted]: #4
 [mp #20 #22]: false
 unsat
-
-ymB2ZiCSl9aUjMXP3tIpZA 359
+2+cndY9nzS72l7VvBCGRAw 19 0
 #2 := false
 decl up_1 :: bool
 #4 := up_1
@@ -28,8 +27,7 @@
 #23 := [asserted]: #7
 [mp #23 #32]: false
 unsat
-
-XC3j0tGm4Y5klDm8sMkzVg 510
+0vJQrobUDcQ9PkGJO8aM8g 25 0
 #2 := false
 decl up_1 :: bool
 #4 := up_1
@@ -55,8 +53,7 @@
 #23 := [asserted]: #7
 [mp #23 #38]: false
 unsat
-
-y5d/Jtt47lXm/wUEvH5fHw 794
+AGGnpwEv208Vqxly7wTWHA 38 0
 #2 := false
 decl up_2 :: bool
 #5 := up_2
@@ -95,11 +92,9 @@
 #30 := [and-elim #31]: #6
 [mp #30 #52]: false
 unsat
-
-mDaukNkyA4glYbkfEOtcAw 7
-unsat
-
-TmB9YjKjdtDMIh0j9rMVPw 1530
+wakXeIy1uoPgglzOQGFhJQ 1 0
+unsat
+cpSlDe0l7plVktRNxGU5dA 71 0
 #2 := false
 decl up_1 :: bool
 #4 := up_1
@@ -171,8 +166,7 @@
 #31 := [asserted]: #15
 [mp #31 #82]: false
 unsat
-
-olufSxMlwMAAqyArYWPVOA 1300
+pg19mjJfV75T2QDrgWd4JA 57 0
 #2 := false
 decl up_1 :: bool
 #4 := up_1
@@ -230,8 +224,7 @@
 #30 := [asserted]: #14
 [mp #30 #70]: false
 unsat
-
-agKJ550QwZ1mvlK8gw+tjQ 4627
+Mj1B8X1MaN7xU/W4Kz3FoQ 194 0
 #2 := false
 decl up_1 :: bool
 #4 := up_1
@@ -426,8 +419,7 @@
 #237 := [mp #83 #236]: #75
 [mp #237 #247]: false
 unsat
-
-+R/oj2I+uFZAw/Eu+3ULdw 1160
+JkhYJB8FDavTZkizO1/9IA 52 0
 #2 := false
 decl uf_1 :: (-> T1 T1 T1)
 decl uf_2 :: T1
@@ -480,8 +472,7 @@
 #113 := [quant-inst]: #199
 [unit-resolution #113 #536 #49]: false
 unsat
-
-c67Ar5f1aFkzAZ2wYy62Wg 56943
+0ZdSZH2DbtjHNTyrDkZmXg 1667 0
 #2 := false
 decl up_54 :: bool
 #126 := up_54
@@ -2149,8 +2140,7 @@
 #2371 := [unit-resolution #891 #2369]: #166
 [unit-resolution #2159 #2371 #2370 #2358 #2357]: false
 unsat
-
-NdJwa8pysYWhn57eCXiqFA 1731
+R3pmBDBlU9XdUrxJXhj7nA 78 0
 #2 := false
 decl up_1 :: (-> int bool)
 decl ?x1!0 :: int
@@ -2229,8 +2219,7 @@
 #82 := [and-elim #81]: #55
 [unit-resolution #82 #95]: false
 unsat
-
-dWWXDEA5bUZjEafLPXbSkA 3321
+IBRj/loev6P6r0J+HOit6A 135 0
 #2 := false
 decl up_1 :: (-> T1 T2 bool)
 #5 := (:var 0 T2)
@@ -2366,9 +2355,7 @@
 #176 := [quant-inst]: #538
 [unit-resolution #176 #252 #535]: false
 unsat
-
-iGZ7b2jaCnn82lPL6oIDZA 3465
-WARNING: failed to find a pattern for quantifier (quantifier id: k!11)
+72504KVBixGB/87pOYiU/A 135 2
 #2 := false
 decl up_1 :: (-> T1 T2 bool)
 #5 := (:var 0 T2)
@@ -2504,8 +2491,9 @@
 #235 := [quant-inst]: #597
 [unit-resolution #235 #311 #594]: false
 unsat
+WARNING: failed to find a pattern for quantifier (quantifier id: k!12)
 
-eTjcfu6S5eyz+xNJ7SVluw 1246
+RaQLz4GxtUICnOD5WoYnzQ 56 0
 #2 := false
 decl up_1 :: (-> T1 bool)
 decl uf_2 :: T1
@@ -2562,8 +2550,7 @@
 #120 := [quant-inst]: #206
 [unit-resolution #120 #542 #41]: false
 unsat
-
-anG1bKU/YVTHEmc1Eh/ZXw 331
+NPQIgVPhSpgSLeS+u/EatQ 17 0
 #2 := false
 #4 := 3::int
 #5 := (= 3::int 3::int)
@@ -2581,8 +2568,7 @@
 #22 := [asserted]: #6
 [mp #22 #31]: false
 unsat
-
-lHpRCTa744ODgmii2zARAw 334
+Lc9NwVtwY2Wo0G7UbFD1oA 17 0
 #2 := false
 #4 := 3::real
 #5 := (= 3::real 3::real)
@@ -2600,8 +2586,7 @@
 #22 := [asserted]: #6
 [mp #22 #31]: false
 unsat
-
-AinXomcY4W1L/t0ZtkDhBg 524
+pYVrUflpYrrZEWALJDnvPw 26 0
 #2 := false
 #7 := 4::int
 #5 := 1::int
@@ -2628,8 +2613,7 @@
 #25 := [asserted]: #9
 [mp #25 #40]: false
 unsat
-
-WxMdOusjxqQwBPorpXBkFQ 815
+FIqzVlbN8RT0iWarmBEpjw 41 0
 #2 := false
 decl uf_1 :: int
 #4 := uf_1
@@ -2671,8 +2655,7 @@
 #28 := [asserted]: #12
 [mp #28 #52]: false
 unsat
-
-K7g37p4yZoVyQcabYS4I2w 754
+HWVNtxMa8xktQsg8pHG+1w 35 0
 #2 := false
 #5 := 3::int
 #6 := 8::int
@@ -2708,8 +2691,7 @@
 #26 := [asserted]: #10
 [mp #26 #51]: false
 unsat
-
-eCmVy21SUmWImXZDJNOfzA 6496
+M71YYpEc8u/aEIH3MOQrcg 250 0
 #2 := false
 #7 := 0::real
 decl uf_2 :: real
@@ -2960,8 +2942,7 @@
 #294 := [unit-resolution #190 #293]: #188
 [th-lemma #280 #294]: false
 unsat
-
-eBRZKSXriNPK3BNu3AWMmQ 3017
+G00bTqBjtW66EmwIZbXbOg 124 0
 #2 := false
 decl uf_1 :: (-> T1 T2)
 decl uf_3 :: T1
@@ -3086,8 +3067,7 @@
 #34 := [asserted]: #11
 [unit-resolution #34 #536]: false
 unsat
-
-CjDkjvq1e9i+SJ3L9ESARg 1146
+6QdzkSy/RtEjUu+wUKIKqA 54 0
 #2 := false
 #9 := 1::int
 decl uf_1 :: int
@@ -3142,8 +3122,7 @@
 #28 := [asserted]: #12
 [mp #28 #67]: false
 unsat
-
-nonk4MmmwlBqL8YtiJY/Qw 1339
+xoSwaSeELbR0PHe0zb/BSg 63 0
 #2 := false
 #11 := 0::int
 decl uf_2 :: int
@@ -3207,8 +3186,7 @@
 #76 := [mp #52 #75]: #63
 [mp #76 #84]: false
 unsat
-
-dCX9jxibjKl6gmr8okzk0w 727
+ciHqmDSmPpA15rO932dhvA 35 0
 #2 := false
 #6 := 5::int
 #4 := 2::int
@@ -3244,8 +3222,7 @@
 #25 := [asserted]: #9
 [mp #25 #49]: false
 unsat
-
-/kLzs8f/jQjEM38PdppYPA 912
+HzwFy7SRHqpspkYnzyeF4w 45 0
 #2 := false
 #11 := 4::real
 decl uf_2 :: real
@@ -3291,8 +3268,7 @@
 #60 := [mp #36 #59]: #51
 [th-lemma #60 #47 #38]: false
 unsat
-
-iT8vKYi503k30rQLczD7yw 1245
+XW7QIWmzYjfQXaHHPc98eA 59 0
 #2 := false
 #16 := (not false)
 decl uf_2 :: int
@@ -3352,8 +3328,94 @@
 #34 := [asserted]: #18
 [mp #34 #71]: false
 unsat
-
-6R4JcV7tL9QRH7WWPAKM5g 5413
+ZGL00TLLioiLlWFiXUnbxg 86 0
+#2 := false
+decl uf_1 :: int
+#5 := uf_1
+#7 := 2::int
+#29 := (* 2::int uf_1)
+#4 := 0::int
+#54 := (= 0::int #29)
+#55 := (not #54)
+#61 := (= #29 0::int)
+#104 := (not #61)
+#110 := (iff #104 #55)
+#108 := (iff #61 #54)
+#109 := [commutativity]: #108
+#111 := [monotonicity #109]: #110
+#62 := (<= #29 0::int)
+#100 := (not #62)
+#30 := (<= uf_1 0::int)
+#31 := (not #30)
+#6 := (< 0::int uf_1)
+#32 := (iff #6 #31)
+#33 := [rewrite]: #32
+#27 := [asserted]: #6
+#34 := [mp #27 #33]: #31
+#101 := (or #100 #30)
+#102 := [th-lemma]: #101
+#103 := [unit-resolution #102 #34]: #100
+#105 := (or #104 #62)
+#106 := [th-lemma]: #105
+#107 := [unit-resolution #106 #103]: #104
+#112 := [mp #107 #111]: #55
+#56 := (= uf_1 #29)
+#57 := (not #56)
+#53 := (= 0::int uf_1)
+#50 := (not #53)
+#58 := (and #50 #55 #57)
+#69 := (not #58)
+#42 := (distinct 0::int uf_1 #29)
+#47 := (not #42)
+#9 := (- uf_1 uf_1)
+#8 := (* uf_1 2::int)
+#10 := (distinct uf_1 #8 #9)
+#11 := (not #10)
+#48 := (iff #11 #47)
+#45 := (iff #10 #42)
+#39 := (distinct uf_1 #29 0::int)
+#43 := (iff #39 #42)
+#44 := [rewrite]: #43
+#40 := (iff #10 #39)
+#37 := (= #9 0::int)
+#38 := [rewrite]: #37
+#35 := (= #8 #29)
+#36 := [rewrite]: #35
+#41 := [monotonicity #36 #38]: #40
+#46 := [trans #41 #44]: #45
+#49 := [monotonicity #46]: #48
+#28 := [asserted]: #11
+#52 := [mp #28 #49]: #47
+#80 := (or #42 #69)
+#81 := [def-axiom]: #80
+#82 := [unit-resolution #81 #52]: #69
+#59 := (= uf_1 0::int)
+#83 := (not #59)
+#89 := (iff #83 #50)
+#87 := (iff #59 #53)
+#88 := [commutativity]: #87
+#90 := [monotonicity #88]: #89
+#84 := (or #83 #30)
+#85 := [th-lemma]: #84
+#86 := [unit-resolution #85 #34]: #83
+#91 := [mp #86 #90]: #50
+#64 := -1::int
+#65 := (* -1::int #29)
+#66 := (+ uf_1 #65)
+#68 := (>= #66 0::int)
+#92 := (not #68)
+#93 := (or #92 #30)
+#94 := [th-lemma]: #93
+#95 := [unit-resolution #94 #34]: #92
+#96 := (or #57 #68)
+#97 := [th-lemma]: #96
+#98 := [unit-resolution #97 #95]: #57
+#76 := (or #58 #53 #54 #56)
+#77 := [def-axiom]: #76
+#99 := [unit-resolution #77 #98 #91 #82]: #54
+[unit-resolution #99 #112]: false
+unsat
+DWt5rIK6NWlI4vrw+691Zg 212 0
 #2 := false
 decl uf_4 :: T1
 #13 := uf_4
@@ -3566,96 +3628,7 @@
 #519 := [unit-resolution #521 #518]: #547
 [unit-resolution #519 #522]: false
 unsat
-
-eOXl5Nf4A2Sq4Q+Wh5XNfA 2026
-#2 := false
-decl uf_1 :: int
-#5 := uf_1
-#7 := 2::int
-#29 := (* 2::int uf_1)
-#4 := 0::int
-#54 := (= 0::int #29)
-#55 := (not #54)
-#61 := (= #29 0::int)
-#104 := (not #61)
-#110 := (iff #104 #55)
-#108 := (iff #61 #54)
-#109 := [commutativity]: #108
-#111 := [monotonicity #109]: #110
-#62 := (<= #29 0::int)
-#100 := (not #62)
-#30 := (<= uf_1 0::int)
-#31 := (not #30)
-#6 := (< 0::int uf_1)
-#32 := (iff #6 #31)
-#33 := [rewrite]: #32
-#27 := [asserted]: #6
-#34 := [mp #27 #33]: #31
-#101 := (or #100 #30)
-#102 := [th-lemma]: #101
-#103 := [unit-resolution #102 #34]: #100
-#105 := (or #104 #62)
-#106 := [th-lemma]: #105
-#107 := [unit-resolution #106 #103]: #104
-#112 := [mp #107 #111]: #55
-#56 := (= uf_1 #29)
-#57 := (not #56)
-#53 := (= 0::int uf_1)
-#50 := (not #53)
-#58 := (and #50 #55 #57)
-#69 := (not #58)
-#42 := (distinct 0::int uf_1 #29)
-#47 := (not #42)
-#9 := (- uf_1 uf_1)
-#8 := (* uf_1 2::int)
-#10 := (distinct uf_1 #8 #9)
-#11 := (not #10)
-#48 := (iff #11 #47)
-#45 := (iff #10 #42)
-#39 := (distinct uf_1 #29 0::int)
-#43 := (iff #39 #42)
-#44 := [rewrite]: #43
-#40 := (iff #10 #39)
-#37 := (= #9 0::int)
-#38 := [rewrite]: #37
-#35 := (= #8 #29)
-#36 := [rewrite]: #35
-#41 := [monotonicity #36 #38]: #40
-#46 := [trans #41 #44]: #45
-#49 := [monotonicity #46]: #48
-#28 := [asserted]: #11
-#52 := [mp #28 #49]: #47
-#80 := (or #42 #69)
-#81 := [def-axiom]: #80
-#82 := [unit-resolution #81 #52]: #69
-#59 := (= uf_1 0::int)
-#83 := (not #59)
-#89 := (iff #83 #50)
-#87 := (iff #59 #53)
-#88 := [commutativity]: #87
-#90 := [monotonicity #88]: #89
-#84 := (or #83 #30)
-#85 := [th-lemma]: #84
-#86 := [unit-resolution #85 #34]: #83
-#91 := [mp #86 #90]: #50
-#64 := -1::int
-#65 := (* -1::int #29)
-#66 := (+ uf_1 #65)
-#68 := (>= #66 0::int)
-#92 := (not #68)
-#93 := (or #92 #30)
-#94 := [th-lemma]: #93
-#95 := [unit-resolution #94 #34]: #92
-#96 := (or #57 #68)
-#97 := [th-lemma]: #96
-#98 := [unit-resolution #97 #95]: #57
-#76 := (or #58 #53 #54 #56)
-#77 := [def-axiom]: #76
-#99 := [unit-resolution #77 #98 #91 #82]: #54
-[unit-resolution #99 #112]: false
-unsat
-
-TwJgkTydtls9Q94iw4a3jw 17377
+PaSeDRf7Set5ywlblDOoTg 673 0
 #2 := false
 #169 := 0::int
 decl uf_2 :: int
@@ -4329,8 +4302,7 @@
 #410 := [mp #349 #409]: #405
 [unit-resolution #410 #710 #709 #697 #706]: false
 unsat
-
-ib5n9nvBAC5jXuKIpV/54g 82870
+U7jSPEM53XYq3qs03aUczw 2291 0
 #2 := false
 #6 := 0::int
 decl z3name!0 :: int
@@ -6622,8 +6594,7 @@
 #2323 := [unit-resolution #918 #2322]: #100
 [unit-resolution #917 #2323 #2318]: false
 unsat
-
-SqgPFdiZeq8SOFuTISQN5g 1109
+eqE7IAqFr0UIBuUsVDgHvw 52 0
 #2 := false
 #8 := 1::real
 decl uf_1 :: real
@@ -6676,26 +6647,15 @@
 #29 := [asserted]: #13
 [mp #29 #65]: false
 unsat
-
-rOkYPs+Q++z/M3OPR/88JQ 1654
+ADs4ZPiuUr7Xu7tk71NnEw 59 0
 #2 := false
 #55 := 0::int
 #7 := 2::int
 decl uf_1 :: int
 #4 := uf_1
 #8 := (mod uf_1 2::int)
-#67 := (>= #8 0::int)
-#1 := true
-#156 := (iff #67 true)
-#158 := (iff #156 #67)
-#159 := [rewrite]: #158
-#28 := [true-axiom]: true
-#153 := (or false #67)
-#154 := [th-lemma]: #153
-#155 := [unit-resolution #154 #28]: #67
-#157 := [iff-true #155]: #156
-#160 := [mp #157 #159]: #67
-#70 := (not #67)
+#58 := (>= #8 0::int)
+#61 := (not #58)
 #5 := 1::int
 #9 := (* 2::int #8)
 #10 := (+ #9 1::int)
@@ -6703,35 +6663,24 @@
 #6 := (+ uf_1 1::int)
 #12 := (<= #6 #11)
 #13 := (not #12)
-#77 := (iff #13 #70)
+#66 := (iff #13 #61)
 #39 := (+ uf_1 #9)
 #40 := (+ 1::int #39)
 #30 := (+ 1::int uf_1)
 #45 := (<= #30 #40)
 #48 := (not #45)
-#75 := (iff #48 #70)
-#58 := (* 1::int #8)
-#59 := (>= #58 0::int)
-#62 := (not #59)
-#71 := (iff #62 #70)
-#68 := (iff #59 #67)
-#65 := (= #58 #8)
-#66 := [rewrite]: #65
-#69 := [monotonicity #66]: #68
-#72 := [monotonicity #69]: #71
-#73 := (iff #48 #62)
+#64 := (iff #48 #61)
 #56 := (>= #9 0::int)
 #51 := (not #56)
-#63 := (iff #51 #62)
-#60 := (iff #56 #59)
-#61 := [rewrite]: #60
-#64 := [monotonicity #61]: #63
+#62 := (iff #51 #61)
+#59 := (iff #56 #58)
+#60 := [rewrite]: #59
+#63 := [monotonicity #60]: #62
 #52 := (iff #48 #51)
 #53 := (iff #45 #56)
 #54 := [rewrite]: #53
 #57 := [monotonicity #54]: #52
-#74 := [trans #57 #64]: #73
-#76 := [trans #74 #72]: #75
+#65 := [trans #57 #63]: #64
 #49 := (iff #13 #48)
 #46 := (iff #12 #45)
 #43 := (= #11 #40)
@@ -6748,38 +6697,39 @@
 #32 := [rewrite]: #31
 #47 := [monotonicity #32 #44]: #46
 #50 := [monotonicity #47]: #49
-#78 := [trans #50 #76]: #77
+#67 := [trans #50 #65]: #66
 #29 := [asserted]: #13
-#79 := [mp #29 #78]: #70
-[unit-resolution #79 #160]: false
-unsat
-
-oSBTeiF6GKDeHPsMxXHXtQ 1064
+#68 := [mp #29 #67]: #61
+#1 := true
+#28 := [true-axiom]: true
+#142 := (or false #58)
+#143 := [th-lemma]: #142
+#144 := [unit-resolution #143 #28]: #58
+[unit-resolution #144 #68]: false
+unsat
+x2NmsblNl28xPXP2EG22rA 54 0
 #2 := false
 #5 := 2::int
 decl uf_1 :: int
 #4 := uf_1
 #6 := (mod uf_1 2::int)
-#122 := (>= #6 2::int)
-#123 := (not #122)
-#1 := true
-#27 := [true-axiom]: true
-#133 := (or false #123)
-#134 := [th-lemma]: #133
-#135 := [unit-resolution #134 #27]: #123
+#55 := (>= #6 2::int)
 #9 := 3::int
-#29 := (* 2::int #6)
-#48 := (>= #29 3::int)
 #10 := (+ uf_1 3::int)
 #7 := (+ #6 #6)
 #8 := (+ uf_1 #7)
 #11 := (< #8 #10)
 #12 := (not #11)
-#55 := (iff #12 #48)
+#60 := (iff #12 #55)
 #35 := (+ 3::int uf_1)
+#29 := (* 2::int #6)
 #32 := (+ uf_1 #29)
 #38 := (< #32 #35)
 #41 := (not #38)
+#58 := (iff #41 #55)
+#48 := (>= #29 3::int)
+#56 := (iff #48 #55)
+#57 := [rewrite]: #56
 #53 := (iff #41 #48)
 #46 := (not #48)
 #45 := (not #46)
@@ -6790,6 +6740,7 @@
 #44 := [rewrite]: #47
 #50 := [monotonicity #44]: #49
 #54 := [trans #50 #52]: #53
+#59 := [trans #54 #57]: #58
 #42 := (iff #12 #41)
 #39 := (iff #11 #38)
 #36 := (= #10 #35)
@@ -6800,13 +6751,18 @@
 #34 := [monotonicity #31]: #33
 #40 := [monotonicity #34 #37]: #39
 #43 := [monotonicity #40]: #42
-#56 := [trans #43 #54]: #55
+#61 := [trans #43 #59]: #60
 #28 := [asserted]: #12
-#57 := [mp #28 #56]: #48
-[th-lemma #57 #135]: false
-unsat
-
-hqH9yBHvmZgES3pBkvsqVQ 2715
+#62 := [mp #28 #61]: #55
+#127 := (not #55)
+#1 := true
+#27 := [true-axiom]: true
+#137 := (or false #127)
+#138 := [th-lemma]: #137
+#139 := [unit-resolution #138 #27]: #127
+[unit-resolution #139 #62]: false
+unsat
+kfLiOGBz3RZx9wt+FS+hfg 118 0
 #2 := false
 #5 := 0::real
 decl uf_1 :: real
@@ -6925,8 +6881,7 @@
 #126 := [mp #101 #125]: #115
 [unit-resolution #126 #132 #129]: false
 unsat
-
-ar4IlNF9IylWgGSPOf9paw 5159
+FPTJq9aN3ES4iIrHgaTv+A 208 0
 #2 := false
 #9 := 0::int
 #11 := 4::int
@@ -7135,8 +7090,7 @@
 #418 := [unit-resolution #417 #36]: #298
 [th-lemma #418 #415 #412 #411 #99 #400 #397 #396]: false
 unsat
-
-o9WM91Nq0O5f08PEA0qA6w 515
+yN0aj3KferzvOSp2KlyNwg 24 0
 #2 := false
 #4 := (exists (vars (?x1 int)) false)
 #5 := (not #4)
@@ -7161,8 +7115,7 @@
 #22 := [asserted]: #6
 [mp #22 #38]: false
 unsat
-
-SJxvvXYE4z1G4iLRBCPerg 516
+7iMPasu6AIeHm45slLCByA 24 0
 #2 := false
 #4 := (exists (vars (?x1 real)) false)
 #5 := (not #4)
@@ -7187,17 +7140,13 @@
 #22 := [asserted]: #6
 [mp #22 #38]: false
 unsat
-
-Fr3hfDrqfMuGDpDYbXAHwg 7
-unsat
-
-bFuFCRUoQSRWyp0iCwo+PA 7
-unsat
-
-NJEgv3p5NO4/yEATNBBDNw 7
-unsat
-
-RC1LWjyqEEsh1xhocCgPmQ 1633
+cv2pC2I0gIUYtVwtXngvXg 1 0
+unsat
+4r8/IxBBDH1ZqF0YfzLLTg 1 0
+unsat
+uj7n+C4nG462DNJy9Divrg 1 0
+unsat
+dn/LVwy1BXEOmtqdUBNhLw 73 0
 #2 := false
 #5 := 0::int
 #8 := 1::int
@@ -7271,8 +7220,7 @@
 #144 := [trans #142 #82]: #143
 [mp #144 #146]: false
 unsat
-
-6pnpFuE9SN6Jr5Upml9T0A 1896
+VzZ1W5SEEis1AJp1qZz86g 82 0
 #2 := false
 #5 := (:var 0 int)
 #7 := 0::int
@@ -7355,100 +7303,52 @@
 #30 := [asserted]: #14
 [mp #30 #96]: false
 unsat
-
-sHpY0IFBgZUNhP56aRB+/w 2968
+UoXgZh5LkmyNCmQEfEtnig 78 0
 #2 := false
-#9 := 1::int
-decl ?x1!1 :: int
-#91 := ?x1!1
-#68 := -2::int
-#129 := (* -2::int ?x1!1)
-decl ?x2!0 :: int
-#90 := ?x2!0
+#5 := (:var 0 int)
 #7 := 2::int
-#128 := (* 2::int ?x2!0)
-#130 := (+ #128 #129)
-#131 := (<= #130 1::int)
-#136 := (not #131)
-#55 := 0::int
-#53 := -1::int
-#115 := (* -1::int ?x1!1)
-#116 := (+ ?x2!0 #115)
-#117 := (<= #116 0::int)
-#139 := (or #117 #136)
-#142 := (not #139)
-#92 := (* -2::int ?x2!0)
-#93 := (* 2::int ?x1!1)
-#94 := (+ #93 #92)
-#95 := (>= #94 -1::int)
-#96 := (not #95)
-#97 := (* -1::int ?x2!0)
-#98 := (+ ?x1!1 #97)
-#99 := (>= #98 0::int)
-#100 := (or #99 #96)
-#101 := (not #100)
-#143 := (iff #101 #142)
-#140 := (iff #100 #139)
-#137 := (iff #96 #136)
-#134 := (iff #95 #131)
-#122 := (+ #92 #93)
-#125 := (>= #122 -1::int)
-#132 := (iff #125 #131)
-#133 := [rewrite]: #132
-#126 := (iff #95 #125)
-#123 := (= #94 #122)
-#124 := [rewrite]: #123
-#127 := [monotonicity #124]: #126
-#135 := [trans #127 #133]: #134
-#138 := [monotonicity #135]: #137
-#120 := (iff #99 #117)
-#109 := (+ #97 ?x1!1)
-#112 := (>= #109 0::int)
-#118 := (iff #112 #117)
-#119 := [rewrite]: #118
-#113 := (iff #99 #112)
-#110 := (= #98 #109)
-#111 := [rewrite]: #110
-#114 := [monotonicity #111]: #113
-#121 := [trans #114 #119]: #120
-#141 := [monotonicity #121 #138]: #140
-#144 := [monotonicity #141]: #143
-#5 := (:var 0 int)
-#71 := (* -2::int #5)
+#11 := (* 2::int #5)
+#9 := 1::int
 #4 := (:var 1 int)
 #8 := (* 2::int #4)
-#72 := (+ #8 #71)
-#70 := (>= #72 -1::int)
-#69 := (not #70)
-#57 := (* -1::int #5)
-#58 := (+ #4 #57)
-#56 := (>= #58 0::int)
-#75 := (or #56 #69)
-#78 := (forall (vars (?x1 int) (?x2 int)) #75)
-#81 := (not #78)
-#102 := (~ #81 #101)
-#103 := [sk]: #102
-#11 := (* 2::int #5)
 #10 := (+ #8 1::int)
 #12 := (< #10 #11)
 #6 := (< #4 #5)
 #13 := (implies #6 #12)
 #14 := (forall (vars (?x1 int) (?x2 int)) #13)
 #15 := (not #14)
-#84 := (iff #15 #81)
+#91 := (iff #15 false)
 #32 := (+ 1::int #8)
 #35 := (< #32 #11)
 #41 := (not #6)
 #42 := (or #41 #35)
 #47 := (forall (vars (?x1 int) (?x2 int)) #42)
 #50 := (not #47)
-#82 := (iff #50 #81)
-#79 := (iff #47 #78)
-#76 := (iff #42 #75)
-#73 := (iff #35 #69)
+#89 := (iff #50 false)
+#1 := true
+#84 := (not true)
+#87 := (iff #84 false)
+#88 := [rewrite]: #87
+#85 := (iff #50 #84)
+#82 := (iff #47 true)
+#77 := (forall (vars (?x1 int) (?x2 int)) true)
+#80 := (iff #77 true)
+#81 := [elim-unused]: #80
+#78 := (iff #47 #77)
+#75 := (iff #42 true)
+#55 := 0::int
+#53 := -1::int
+#57 := (* -1::int #5)
+#58 := (+ #4 #57)
+#56 := (>= #58 0::int)
+#54 := (not #56)
+#69 := (or #56 #54)
+#73 := (iff #69 true)
 #74 := [rewrite]: #73
+#71 := (iff #42 #69)
+#70 := (iff #35 #54)
+#68 := [rewrite]: #70
 #66 := (iff #41 #56)
-#54 := (not #56)
 #61 := (not #54)
 #64 := (iff #61 #56)
 #65 := [rewrite]: #64
@@ -7457,9 +7357,12 @@
 #60 := [rewrite]: #59
 #63 := [monotonicity #60]: #62
 #67 := [trans #63 #65]: #66
-#77 := [monotonicity #67 #74]: #76
-#80 := [quant-intro #77]: #79
-#83 := [monotonicity #80]: #82
+#72 := [monotonicity #67 #68]: #71
+#76 := [trans #72 #74]: #75
+#79 := [quant-intro #76]: #78
+#83 := [trans #79 #81]: #82
+#86 := [monotonicity #83]: #85
+#90 := [trans #86 #88]: #89
 #51 := (iff #15 #50)
 #48 := (iff #14 #47)
 #45 := (iff #13 #42)
@@ -7475,89 +7378,53 @@
 #46 := [trans #40 #44]: #45
 #49 := [quant-intro #46]: #48
 #52 := [monotonicity #49]: #51
-#85 := [trans #52 #83]: #84
+#92 := [trans #52 #90]: #91
 #31 := [asserted]: #15
-#86 := [mp #31 #85]: #81
-#106 := [mp~ #86 #103]: #101
-#107 := [mp #106 #144]: #142
-#146 := [not-or-elim #107]: #131
-#108 := (not #117)
-#145 := [not-or-elim #107]: #108
-[th-lemma #145 #146]: false
-unsat
-
-7GSX+dyn9XwHWNcjJ4X1ww 2292
+[mp #31 #92]: false
+unsat
+Qv4gVhCmOzC39uufV9ZpDA 61 0
 #2 := false
-#7 := 1::int
-decl ?x1!1 :: int
-#74 := ?x1!1
-#51 := -2::int
-#96 := (* -2::int ?x1!1)
-decl ?x2!0 :: int
-#73 := ?x2!0
+#9 := (:var 0 int)
 #4 := 2::int
-#95 := (* 2::int ?x2!0)
-#97 := (+ #95 #96)
-#166 := (<= #97 1::int)
-#94 := (= #97 1::int)
-#53 := -1::int
-#75 := (* -2::int ?x2!0)
-#76 := (* 2::int ?x1!1)
-#77 := (+ #76 #75)
-#78 := (= #77 -1::int)
-#79 := (not #78)
-#80 := (not #79)
-#110 := (iff #80 #94)
-#102 := (not #94)
-#105 := (not #102)
-#108 := (iff #105 #94)
-#109 := [rewrite]: #108
-#106 := (iff #80 #105)
-#103 := (iff #79 #102)
-#100 := (iff #78 #94)
-#88 := (+ #75 #76)
-#91 := (= #88 -1::int)
-#98 := (iff #91 #94)
-#99 := [rewrite]: #98
-#92 := (iff #78 #91)
-#89 := (= #77 #88)
-#90 := [rewrite]: #89
-#93 := [monotonicity #90]: #92
-#101 := [trans #93 #99]: #100
-#104 := [monotonicity #101]: #103
-#107 := [monotonicity #104]: #106
-#111 := [trans #107 #109]: #110
-#9 := (:var 0 int)
-#55 := (* -2::int #9)
+#10 := (* 2::int #9)
+#7 := 1::int
 #5 := (:var 1 int)
 #6 := (* 2::int #5)
-#56 := (+ #6 #55)
-#54 := (= #56 -1::int)
-#58 := (not #54)
-#61 := (forall (vars (?x1 int) (?x2 int)) #58)
-#64 := (not #61)
-#81 := (~ #64 #80)
-#82 := [sk]: #81
-#10 := (* 2::int #9)
 #8 := (+ #6 1::int)
 #11 := (= #8 #10)
 #12 := (not #11)
 #13 := (forall (vars (?x1 int) (?x2 int)) #12)
 #14 := (not #13)
-#67 := (iff #14 #64)
+#74 := (iff #14 false)
 #31 := (+ 1::int #6)
 #37 := (= #10 #31)
 #42 := (not #37)
 #45 := (forall (vars (?x1 int) (?x2 int)) #42)
 #48 := (not #45)
-#65 := (iff #48 #64)
-#62 := (iff #45 #61)
-#59 := (iff #42 #58)
-#52 := (iff #37 #54)
-#57 := [rewrite]: #52
-#60 := [monotonicity #57]: #59
-#63 := [quant-intro #60]: #62
-#66 := [monotonicity #63]: #65
+#72 := (iff #48 false)
+#1 := true
+#67 := (not true)
+#70 := (iff #67 false)
+#71 := [rewrite]: #70
+#68 := (iff #48 #67)
+#65 := (iff #45 true)
+#60 := (forall (vars (?x1 int) (?x2 int)) true)
+#63 := (iff #60 true)
+#64 := [elim-unused]: #63
+#61 := (iff #45 #60)
+#58 := (iff #42 true)
+#51 := (not false)
+#56 := (iff #51 true)
+#57 := [rewrite]: #56
+#52 := (iff #42 #51)
+#53 := (iff #37 false)
+#54 := [rewrite]: #53
+#55 := [monotonicity #54]: #52
+#59 := [trans #55 #57]: #58
+#62 := [quant-intro #59]: #61
+#66 := [trans #62 #64]: #65
+#69 := [monotonicity #66]: #68
+#73 := [trans #69 #71]: #72
 #49 := (iff #14 #48)
 #46 := (iff #13 #45)
 #43 := (iff #12 #42)
@@ -7573,22 +7440,11 @@
 #44 := [monotonicity #41]: #43
 #47 := [quant-intro #44]: #46
 #50 := [monotonicity #47]: #49
-#68 := [trans #50 #66]: #67
+#75 := [trans #50 #73]: #74
 #30 := [asserted]: #14
-#69 := [mp #30 #68]: #64
-#85 := [mp~ #69 #82]: #80
-#86 := [mp #85 #111]: #94
-#168 := (or #102 #166)
-#169 := [th-lemma]: #168
-#170 := [unit-resolution #169 #86]: #166
-#167 := (>= #97 1::int)
-#171 := (or #102 #167)
-#172 := [th-lemma]: #171
-#173 := [unit-resolution #172 #86]: #167
-[th-lemma #173 #170]: false
-unsat
-
-oieid3+1h5s04LTQ9d796Q 2636
+[mp #30 #75]: false
+unsat
++j+tSj7aUImWej2XcTL9dw 111 0
 #2 := false
 #4 := 2::int
 decl ?x1!1 :: int
@@ -7700,8 +7556,7 @@
 #184 := [th-lemma]: #183
 [unit-resolution #184 #127 #125 #126]: false
 unsat
-
-+RiWXCcHPvuSeYUjZ4Ky/g 2113
+kQRsBd9oowc7exsvsEgTUg 89 0
 #2 := false
 #4 := 0::int
 decl ?x1!0 :: int
@@ -7791,9 +7646,7 @@
 #167 := [unit-resolution #154 #90]: #166
 [unit-resolution #167 #165 #162]: false
 unsat
-
-hlG1vHDJCcXbyvxKYDWifg 2036
-WARNING: failed to find a pattern for quantifier (quantifier id: k!1)
+VPjD8BtzPcTZKIRT4SA3Nw 83 2
 #2 := false
 #5 := 0::int
 #4 := (:var 0 int)
@@ -7877,9 +7730,9 @@
 #62 := [mp~ #54 #61]: #49
 [unit-resolution #62 #174]: false
 unsat
+WARNING: failed to find a pattern for quantifier (quantifier id: k!2)
 
-oOC8ghGUYboMezGio2exAg 4464
-WARNING: failed to find a pattern for quantifier (quantifier id: k!1)
+DCV5zpDW3cC2A61VghqFkA 180 2
 #2 := false
 #4 := 0::int
 #5 := (:var 0 int)
@@ -8060,63 +7913,40 @@
 #585 := [unit-resolution #128 #581]: #55
 [unit-resolution #585 #307]: false
 unsat
+WARNING: failed to find a pattern for quantifier (quantifier id: k!2)
 
-4Dtb5Y1TTRPWZcHG9Griog 2407
+lYXJpXHB9nLXJbOsr9VH1w 68 0
 #2 := false
-#104 := -1::int
-decl ?x1!1 :: int
-#86 := ?x1!1
-#106 := -4::int
-#107 := (* -4::int ?x1!1)
-decl ?x2!0 :: int
-#85 := ?x2!0
-#7 := 6::int
-#105 := (* 6::int ?x2!0)
-#108 := (+ #105 #107)
-#168 := (<= #108 -1::int)
-#109 := (= #108 -1::int)
 #12 := 1::int
-#33 := -6::int
-#87 := (* -6::int ?x2!0)
-#4 := 4::int
-#88 := (* 4::int ?x1!1)
-#89 := (+ #88 #87)
-#90 := (= #89 1::int)
-#112 := (iff #90 #109)
-#98 := (+ #87 #88)
-#101 := (= #98 1::int)
-#110 := (iff #101 #109)
-#111 := [rewrite]: #110
-#102 := (iff #90 #101)
-#99 := (= #89 #98)
-#100 := [rewrite]: #99
-#103 := [monotonicity #100]: #102
-#113 := [trans #103 #111]: #112
-#53 := (:var 0 int)
-#54 := (* -6::int #53)
 #9 := (:var 1 int)
-#55 := (* 4::int #9)
-#56 := (+ #55 #54)
-#76 := (= #56 1::int)
-#74 := (exists (vars (?x1 int) (?x2 int)) #76)
-#91 := (~ #74 #90)
-#92 := [sk]: #91
+#7 := 6::int
 #8 := (- 6::int)
 #10 := (* #8 #9)
 #5 := (:var 2 int)
+#4 := 4::int
 #6 := (* 4::int #5)
 #11 := (+ #6 #10)
 #13 := (= #11 1::int)
 #14 := (exists (vars (?x1 int) (?x2 int) (?x3 int)) #13)
 #15 := (not #14)
 #16 := (not #15)
-#79 := (iff #16 #74)
+#82 := (iff #16 false)
+#53 := (:var 0 int)
+#33 := -6::int
+#54 := (* -6::int #53)
+#55 := (* 4::int #9)
+#56 := (+ #55 #54)
 #57 := (= 1::int #56)
 #58 := (exists (vars (?x1 int) (?x2 int)) #57)
-#77 := (iff #58 #74)
-#75 := (iff #57 #76)
-#73 := [rewrite]: #75
-#78 := [quant-intro #73]: #77
+#80 := (iff #58 false)
+#76 := (exists (vars (?x1 int) (?x2 int)) false)
+#78 := (iff #76 false)
+#79 := [elim-unused]: #78
+#77 := (iff #58 #76)
+#73 := (iff #57 false)
+#74 := [rewrite]: #73
+#75 := [quant-intro #74]: #77
+#81 := [trans #75 #79]: #80
 #71 := (iff #16 #58)
 #63 := (not #58)
 #66 := (not #63)
@@ -8150,23 +7980,11 @@
 #65 := [monotonicity #62]: #64
 #68 := [monotonicity #65]: #67
 #72 := [trans #68 #70]: #71
-#80 := [trans #72 #78]: #79
+#83 := [trans #72 #81]: #82
 #32 := [asserted]: #16
-#81 := [mp #32 #80]: #74
-#95 := [mp~ #81 #92]: #90
-#96 := [mp #95 #113]: #109
-#170 := (not #109)
-#171 := (or #170 #168)
-#172 := [th-lemma]: #171
-#173 := [unit-resolution #172 #96]: #168
-#169 := (>= #108 -1::int)
-#174 := (or #170 #169)
-#175 := [th-lemma]: #174
-#176 := [unit-resolution #175 #96]: #169
-[th-lemma #176 #173]: false
-unsat
-
-dbOre63OdVavsqL3lG2ttw 2516
+[mp #32 #83]: false
+unsat
+jNvpOd8qnh73F8B6mQDrRw 107 0
 #2 := false
 #4 := 0::int
 decl ?x2!1 :: int
@@ -8274,8 +8092,7 @@
 #123 := [and-elim #101]: #88
 [th-lemma #123 #124 #125]: false
 unsat
-
-LtM5szEGH9QAF1TwsVtH4w 2764
+QWWPBUGjgvTCpxqJ9oPGdQ 117 0
 #2 := false
 #4 := 0::int
 decl ?x2!1 :: int
@@ -8393,8 +8210,7 @@
 #188 := [unit-resolution #187 #110]: #98
 [unit-resolution #188 #130]: false
 unsat
-
-ibIqbnIUB+oyERADdbFW6w 3631
+3r4MsKEvDJc1RWnNRxu/3Q 148 0
 #2 := false
 #144 := (not false)
 #7 := 0::int
@@ -8543,8 +8359,7 @@
 #158 := [mp #126 #157]: #153
 [mp #158 #181]: false
 unsat
-
-1HbJvLWS/aG8IZEVLDIWyA 1506
+Q+cnHyqIFLGWsSlQkp3fEg 67 0
 #2 := false
 #4 := (:var 0 int)
 #5 := (pattern #4)
@@ -8581,12 +8396,12 @@
 #46 := (+ #4 #45)
 #44 := (>= #46 0::int)
 #42 := (not #44)
-#60 := (or #44 #42)
-#61 := (iff #60 true)
+#57 := (or #44 #42)
+#61 := (iff #57 true)
 #62 := [rewrite]: #61
-#56 := (iff #32 #60)
+#59 := (iff #32 #57)
 #58 := (iff #11 #42)
-#59 := [rewrite]: #58
+#56 := [rewrite]: #58
 #54 := (iff #31 #44)
 #49 := (not #42)
 #52 := (iff #49 #44)
@@ -8596,8 +8411,8 @@
 #48 := [rewrite]: #47
 #51 := [monotonicity #48]: #50
 #55 := [trans #51 #53]: #54
-#57 := [monotonicity #55 #59]: #56
-#64 := [trans #57 #62]: #63
+#60 := [monotonicity #55 #56]: #59
+#64 := [trans #60 #62]: #63
 #67 := [quant-intro #64]: #66
 #71 := [trans #67 #69]: #70
 #74 := [monotonicity #71]: #73
@@ -8612,11 +8427,9 @@
 #30 := [asserted]: #14
 [mp #30 #80]: false
 unsat
-
-K7kWge9RT44bPFRy+hxaqg 7
-unsat
-
-+rwKUm5bOzD9paEkmogLyw 1562
+Q7HDzu4ER2dw+lHHM6YgFg 1 0
+unsat
+saejIG5KeeVxOolEIo3gtw 75 0
 #2 := false
 #6 := 1::int
 decl uf_3 :: int
@@ -8692,8 +8505,7 @@
 #32 := [asserted]: #16
 [mp #32 #86]: false
 unsat
-
-iRJ30NP1Enylq9tZfpCPTA 1288
+PPaoU5CzQFYr3LRpOsGPhQ 62 0
 #2 := false
 decl uf_2 :: real
 #6 := uf_2
@@ -8756,8 +8568,7 @@
 #32 := [asserted]: #16
 [mp #32 #74]: false
 unsat
-
-Ff1vqDiuUnet19j/x+mXkA 3029
+hXKzem5+KYZMOj+GKxjszQ 141 0
 #2 := false
 decl uf_4 :: int
 #9 := uf_4
@@ -8899,8 +8710,7 @@
 #45 := [asserted]: #29
 [mp #45 #150]: false
 unsat
-
-iPZ87GNdi7uQw4ehEpbTPQ 7012
+3D8WhjZTO7T824d7mwXcCA 252 0
 #2 := false
 #9 := 0::int
 decl uf_2 :: (-> T1 int)
@@ -8915,19 +8725,19 @@
 #295 := -1::int
 #274 := (* -1::int #293)
 #610 := (+ #24 #274)
-#315 := (<= #610 0::int)
+#594 := (<= #610 0::int)
 #612 := (= #610 0::int)
-#255 := (>= #23 0::int)
-#317 := (= #293 0::int)
-#522 := (not #317)
-#577 := (<= #293 0::int)
-#519 := (not #577)
+#606 := (>= #23 0::int)
+#237 := (= #293 0::int)
+#549 := (not #237)
+#588 := (<= #293 0::int)
+#457 := (not #588)
 #26 := 1::int
-#553 := (>= #293 1::int)
-#552 := (= #293 1::int)
+#558 := (>= #293 1::int)
+#555 := (= #293 1::int)
 #27 := (uf_1 1::int)
-#420 := (uf_2 #27)
-#565 := (= #420 1::int)
+#589 := (uf_2 #27)
+#301 := (= #589 1::int)
 #10 := (:var 0 int)
 #12 := (uf_1 #10)
 #626 := (pattern #12)
@@ -8983,57 +8793,57 @@
 #87 := [mp #51 #86]: #82
 #146 := [mp~ #87 #130]: #82
 #632 := [mp #146 #631]: #627
-#237 := (not #627)
-#442 := (or #237 #565)
-#578 := (>= 1::int 0::int)
-#419 := (not #578)
-#421 := (= 1::int #420)
-#563 := (or #421 #419)
-#443 := (or #237 #563)
-#550 := (iff #443 #442)
-#547 := (iff #442 #442)
-#548 := [rewrite]: #547
-#559 := (iff #563 #565)
-#554 := (or #565 false)
-#558 := (iff #554 #565)
-#556 := [rewrite]: #558
-#555 := (iff #563 #554)
-#400 := (iff #419 false)
+#609 := (not #627)
+#578 := (or #609 #301)
+#311 := (>= 1::int 0::int)
+#585 := (not #311)
+#586 := (= 1::int #589)
+#590 := (or #586 #585)
+#419 := (or #609 #590)
+#421 := (iff #419 #578)
+#564 := (iff #578 #578)
+#565 := [rewrite]: #564
+#577 := (iff #590 #301)
+#574 := (or #301 false)
+#571 := (iff #574 #301)
+#576 := [rewrite]: #571
+#575 := (iff #590 #574)
+#584 := (iff #585 false)
 #1 := true
-#567 := (not true)
-#569 := (iff #567 false)
-#398 := [rewrite]: #569
-#568 := (iff #419 #567)
-#560 := (iff #578 true)
-#561 := [rewrite]: #560
-#562 := [monotonicity #561]: #568
-#401 := [trans #562 #398]: #400
-#564 := (iff #421 #565)
-#566 := [rewrite]: #564
-#557 := [monotonicity #566 #401]: #555
-#441 := [trans #557 #556]: #559
-#452 := [monotonicity #441]: #550
-#551 := [trans #452 #548]: #550
-#402 := [quant-inst]: #443
-#436 := [mp #402 #551]: #442
-#524 := [unit-resolution #436 #632]: #565
-#526 := (= #293 #420)
+#582 := (not true)
+#583 := (iff #582 false)
+#580 := [rewrite]: #583
+#296 := (iff #585 #582)
+#303 := (iff #311 true)
+#581 := [rewrite]: #303
+#579 := [monotonicity #581]: #296
+#573 := [trans #579 #580]: #584
+#300 := (iff #586 #301)
+#302 := [rewrite]: #300
+#570 := [monotonicity #302 #573]: #575
+#572 := [trans #570 #576]: #577
+#563 := [monotonicity #572]: #421
+#566 := [trans #563 #565]: #421
+#420 := [quant-inst]: #419
+#560 := [mp #420 #566]: #578
+#442 := [unit-resolution #560 #632]: #301
+#443 := (= #293 #589)
 #28 := (= #25 #27)
 #129 := [asserted]: #28
-#527 := [monotonicity #129]: #526
-#528 := [trans #527 #524]: #552
-#529 := (not #552)
-#525 := (or #529 #553)
-#530 := [th-lemma]: #525
-#516 := [unit-resolution #530 #528]: #553
-#517 := (not #553)
-#520 := (or #517 #519)
-#521 := [th-lemma]: #520
-#518 := [unit-resolution #521 #516]: #519
-#502 := (or #522 #577)
-#503 := [th-lemma]: #502
-#505 := [unit-resolution #503 #518]: #522
-#300 := (or #255 #317)
+#436 := [monotonicity #129]: #443
+#451 := [trans #436 #442]: #555
+#453 := (not #555)
+#454 := (or #453 #558)
+#447 := [th-lemma]: #454
+#455 := [unit-resolution #447 #451]: #558
+#456 := (not #558)
+#458 := (or #456 #457)
+#459 := [th-lemma]: #458
+#552 := [unit-resolution #459 #455]: #457
+#553 := (or #549 #588)
+#540 := [th-lemma]: #553
+#542 := [unit-resolution #540 #552]: #549
+#603 := (or #237 #606)
 #18 := (= #13 0::int)
 #118 := (or #18 #70)
 #633 := (forall (vars (?x3 int)) (:pat #626) #118)
@@ -9090,95 +8900,70 @@
 #128 := [mp #88 #127]: #123
 #149 := [mp~ #128 #134]: #123
 #638 := [mp #149 #637]: #633
-#582 := (not #633)
-#296 := (or #582 #255 #317)
+#604 := (not #633)
+#602 := (or #604 #237 #606)
 #204 := (>= #24 0::int)
-#210 := (or #317 #204)
-#579 := (or #582 #210)
-#570 := (iff #579 #296)
-#580 := (or #582 #300)
-#574 := (iff #580 #296)
-#575 := [rewrite]: #574
-#584 := (iff #579 #580)
-#303 := (iff #210 #300)
-#606 := (* 1::int #23)
-#279 := (>= #606 0::int)
-#311 := (or #279 #317)
-#301 := (iff #311 #300)
-#256 := (iff #279 #255)
-#251 := (= #606 #23)
-#593 := [rewrite]: #251
-#257 := [monotonicity #593]: #256
-#302 := [monotonicity #257]: #301
-#586 := (iff #210 #311)
-#587 := (or #317 #279)
-#585 := (iff #587 #311)
-#589 := [rewrite]: #585
-#588 := (iff #210 #587)
-#280 := (iff #204 #279)
-#613 := [rewrite]: #280
-#310 := [monotonicity #613]: #588
-#590 := [trans #310 #589]: #586
-#581 := [trans #590 #302]: #303
-#573 := [monotonicity #581]: #584
-#571 := [trans #573 #575]: #570
-#583 := [quant-inst]: #579
-#576 := [mp #583 #571]: #296
-#506 := [unit-resolution #576 #638]: #300
-#507 := [unit-resolution #506 #505]: #255
-#258 := (not #255)
-#597 := (or #258 #612)
-#601 := (or #237 #258 #612)
+#601 := (or #237 #204)
+#605 := (or #604 #601)
+#317 := (iff #605 #602)
+#592 := (or #604 #603)
+#315 := (iff #592 #602)
+#316 := [rewrite]: #315
+#299 := (iff #605 #592)
+#242 := (iff #601 #603)
+#279 := (iff #204 #606)
+#280 := [rewrite]: #279
+#243 := [monotonicity #280]: #242
+#314 := [monotonicity #243]: #299
+#210 := [trans #314 #316]: #317
+#591 := [quant-inst]: #605
+#587 := [mp #591 #210]: #602
+#534 := [unit-resolution #587 #638]: #603
+#531 := [unit-resolution #534 #542]: #606
+#613 := (not #606)
+#607 := (or #613 #612)
+#251 := (or #609 #613 #612)
 #289 := (not #204)
 #294 := (= #24 #293)
 #291 := (or #294 #289)
-#603 := (or #237 #291)
-#592 := (iff #603 #601)
-#243 := (or #237 #597)
-#605 := (iff #243 #601)
-#591 := [rewrite]: #605
-#604 := (iff #603 #243)
-#594 := (iff #291 #597)
-#614 := (not #279)
-#266 := (or #614 #612)
-#598 := (iff #266 #597)
-#595 := (iff #614 #258)
-#596 := [monotonicity #257]: #595
-#599 := [monotonicity #596]: #598
-#267 := (iff #291 #266)
-#611 := (or #612 #614)
-#271 := (iff #611 #266)
-#608 := [rewrite]: #271
-#617 := (iff #291 #611)
-#615 := (iff #289 #614)
-#616 := [monotonicity #613]: #615
+#593 := (or #609 #291)
+#597 := (iff #593 #251)
+#256 := (or #609 #607)
+#595 := (iff #256 #251)
+#596 := [rewrite]: #595
+#257 := (iff #593 #256)
+#608 := (iff #291 #607)
+#616 := (or #612 #613)
+#266 := (iff #616 #607)
+#271 := [rewrite]: #266
+#611 := (iff #291 #616)
+#614 := (iff #289 #613)
+#615 := [monotonicity #280]: #614
 #268 := (iff #294 #612)
 #399 := [rewrite]: #268
-#607 := [monotonicity #399 #616]: #617
-#609 := [trans #607 #608]: #267
-#600 := [trans #609 #599]: #594
-#602 := [monotonicity #600]: #604
-#299 := [trans #602 #591]: #592
-#242 := [quant-inst]: #603
-#314 := [mp #242 #299]: #601
-#508 := [unit-resolution #314 #632]: #597
-#509 := [unit-resolution #508 #507]: #612
-#510 := (not #612)
-#511 := (or #510 #315)
-#512 := [th-lemma]: #511
-#513 := [unit-resolution #512 #509]: #315
-#316 := (>= #610 0::int)
-#514 := (or #510 #316)
-#504 := [th-lemma]: #514
-#515 := [unit-resolution #504 #509]: #316
-#549 := (<= #293 1::int)
-#493 := (or #529 #549)
-#494 := [th-lemma]: #493
-#496 := [unit-resolution #494 #528]: #549
-[th-lemma #516 #496 #515 #513]: false
-unsat
-
-kDuOn7kAggfP4Um8ghhv5A 6068
+#617 := [monotonicity #399 #615]: #611
+#267 := [trans #617 #271]: #608
+#258 := [monotonicity #267]: #257
+#598 := [trans #258 #596]: #597
+#255 := [quant-inst]: #593
+#599 := [mp #255 #598]: #251
+#533 := [unit-resolution #599 #632]: #607
+#543 := [unit-resolution #533 #531]: #612
+#544 := (not #612)
+#545 := (or #544 #594)
+#541 := [th-lemma]: #545
+#546 := [unit-resolution #541 #543]: #594
+#600 := (>= #610 0::int)
+#535 := (or #544 #600)
+#536 := [th-lemma]: #535
+#537 := [unit-resolution #536 #543]: #600
+#557 := (<= #293 1::int)
+#538 := (or #453 #557)
+#532 := [th-lemma]: #538
+#539 := [unit-resolution #532 #451]: #557
+[th-lemma #455 #539 #537 #546]: false
+unsat
+kyphS4o71h68g2YhvYbQQQ 223 0
 #2 := false
 #23 := 3::int
 decl uf_2 :: (-> T1 int)
@@ -9201,13 +8986,13 @@
 #632 := -1::int
 #634 := (* -1::int #28)
 #290 := (+ #26 #634)
-#609 := (>= #290 0::int)
+#623 := (>= #290 0::int)
 #421 := (= #290 0::int)
-#273 := (>= #22 0::int)
-#610 := (= #28 0::int)
-#588 := (not #610)
-#441 := (<= #28 0::int)
-#443 := (not #441)
+#302 := (>= #22 0::int)
+#625 := (= #28 0::int)
+#318 := (not #625)
+#322 := (<= #28 0::int)
+#324 := (not #322)
 #29 := 7::int
 #143 := (>= #28 7::int)
 #30 := (< #28 7::int)
@@ -9224,12 +9009,12 @@
 #151 := [trans #147 #149]: #150
 #133 := [asserted]: #31
 #152 := [mp #133 #151]: #143
-#585 := (or #443 #141)
-#586 := [th-lemma]: #585
-#587 := [unit-resolution #586 #152]: #443
-#582 := (or #588 #441)
-#583 := [th-lemma]: #582
-#589 := [unit-resolution #583 #587]: #588
+#325 := (or #324 #141)
+#603 := [th-lemma]: #325
+#604 := [unit-resolution #603 #152]: #324
+#601 := (or #318 #322)
+#605 := [th-lemma]: #601
+#602 := [unit-resolution #605 #604]: #318
 #10 := (:var 0 int)
 #12 := (uf_1 #10)
 #648 := (pattern #12)
@@ -9292,45 +9077,33 @@
 #131 := [mp #91 #130]: #126
 #172 := [mp~ #131 #155]: #126
 #660 := [mp #172 #659]: #655
-#605 := (not #655)
-#602 := (or #605 #273 #610)
+#337 := (not #655)
+#338 := (or #337 #302 #625)
 #315 := (>= #26 0::int)
-#332 := (or #610 #315)
-#606 := (or #605 #332)
-#599 := (iff #606 #602)
-#323 := (or #273 #610)
-#596 := (or #605 #323)
-#593 := (iff #596 #602)
-#598 := [rewrite]: #593
-#597 := (iff #606 #596)
-#318 := (iff #332 #323)
-#302 := 1::int
-#635 := (* 1::int #22)
-#636 := (>= #635 0::int)
-#333 := (or #610 #636)
-#603 := (iff #333 #323)
-#608 := (or #610 #273)
-#324 := (iff #608 #323)
-#325 := [rewrite]: #324
-#612 := (iff #333 #608)
-#615 := (iff #636 #273)
-#289 := (= #635 #22)
-#631 := [rewrite]: #289
-#277 := [monotonicity #631]: #615
-#322 := [monotonicity #277]: #612
-#604 := [trans #322 #325]: #603
-#607 := (iff #332 #333)
-#637 := (iff #315 #636)
-#638 := [rewrite]: #637
-#611 := [monotonicity #638]: #607
-#601 := [trans #611 #604]: #318
-#592 := [monotonicity #601]: #597
-#594 := [trans #592 #598]: #599
-#595 := [quant-inst]: #606
-#600 := [mp #595 #594]: #602
-#590 := [unit-resolution #600 #660 #589]: #273
-#278 := (not #273)
-#620 := (or #278 #421)
+#264 := (or #625 #315)
+#339 := (or #337 #264)
+#611 := (iff #339 #338)
+#627 := (or #302 #625)
+#609 := (or #337 #627)
+#333 := (iff #609 #338)
+#607 := [rewrite]: #333
+#610 := (iff #339 #609)
+#321 := (iff #264 #627)
+#265 := (or #625 #302)
+#613 := (iff #265 #627)
+#614 := [rewrite]: #613
+#626 := (iff #264 #265)
+#635 := (iff #315 #302)
+#636 := [rewrite]: #635
+#624 := [monotonicity #636]: #626
+#336 := [trans #624 #614]: #321
+#332 := [monotonicity #336]: #610
+#608 := [trans #332 #607]: #611
+#231 := [quant-inst]: #339
+#612 := [mp #231 #608]: #338
+#606 := [unit-resolution #612 #660 #602]: #302
+#637 := (not #302)
+#293 := (or #637 #421)
 #55 := (= #10 #13)
 #80 := (or #55 #74)
 #649 := (forall (vars (?x2 int)) (:pat #648) #80)
@@ -9380,50 +9153,41 @@
 #90 := [mp #54 #89]: #85
 #169 := [mp~ #90 #134]: #85
 #654 := [mp #169 #653]: #649
-#264 := (not #649)
-#265 := (or #264 #278 #421)
+#615 := (not #649)
+#277 := (or #615 #637 #421)
 #243 := (not #315)
 #317 := (= #26 #28)
 #296 := (or #317 #243)
-#626 := (or #264 #296)
-#337 := (iff #626 #265)
-#627 := (or #264 #620)
-#321 := (iff #627 #265)
-#336 := [rewrite]: #321
-#613 := (iff #626 #627)
-#623 := (iff #296 #620)
-#633 := (not #636)
-#288 := (or #421 #633)
-#622 := (iff #288 #620)
-#617 := (or #421 #278)
-#621 := (iff #617 #620)
-#616 := [rewrite]: #621
-#618 := (iff #288 #617)
-#279 := (iff #633 #278)
-#280 := [monotonicity #277]: #279
-#619 := [monotonicity #280]: #618
-#259 := [trans #619 #616]: #622
-#293 := (iff #296 #288)
-#639 := (iff #243 #633)
-#629 := [monotonicity #638]: #639
+#278 := (or #615 #296)
+#621 := (iff #278 #277)
+#280 := (or #615 #293)
+#619 := (iff #280 #277)
+#620 := [rewrite]: #619
+#617 := (iff #278 #280)
+#631 := (iff #296 #293)
+#639 := (or #421 #637)
+#630 := (iff #639 #293)
+#289 := [rewrite]: #630
+#629 := (iff #296 #639)
+#638 := (iff #243 #637)
+#633 := [monotonicity #636]: #638
 #628 := (iff #317 #421)
 #301 := [rewrite]: #628
-#630 := [monotonicity #301 #629]: #293
-#625 := [trans #630 #259]: #623
-#614 := [monotonicity #625]: #613
-#338 := [trans #614 #336]: #337
-#624 := [quant-inst]: #626
-#339 := [mp #624 #338]: #265
-#584 := [unit-resolution #339 #654]: #620
-#591 := [unit-resolution #584 #590]: #421
-#420 := (not #421)
-#422 := (or #420 #609)
-#423 := [th-lemma]: #422
-#576 := [unit-resolution #423 #591]: #609
-[th-lemma #152 #576 #139]: false
-unsat
-
-aiB004AWADNjynNrqCDsxw 9284
+#288 := [monotonicity #301 #633]: #629
+#273 := [trans #288 #289]: #631
+#618 := [monotonicity #273]: #617
+#616 := [trans #618 #620]: #621
+#279 := [quant-inst]: #278
+#622 := [mp #279 #616]: #277
+#595 := [unit-resolution #622 #654]: #293
+#596 := [unit-resolution #595 #606]: #421
+#597 := (not #421)
+#592 := (or #597 #623)
+#593 := [th-lemma]: #592
+#598 := [unit-resolution #593 #596]: #623
+[th-lemma #152 #598 #139]: false
+unsat
+M8P5WxpiY5AWxaJDBtXoLQ 367 0
 #2 := false
 #9 := 0::int
 decl uf_2 :: (-> T1 int)
@@ -9791,8 +9555,7 @@
 #456 := [th-lemma]: #455
 [unit-resolution #456 #464 #452]: false
 unsat
-
-twoPNF2RBLeff4yYfubpfg 7634
+Xs4JZCKb5egkcPabsrodXg 302 0
 #2 := false
 #9 := 0::int
 decl uf_2 :: (-> T1 int)
@@ -10095,8 +9858,7 @@
 #601 := [unit-resolution #615 #613]: #683
 [th-lemma #623 #188 #601 #628]: false
 unsat
-
-ZcLxnpFewGGQ0H47MfRXGw 12389
+clMAi2WqMi360EjFURRGLg 458 0
 #2 := false
 #9 := 0::int
 decl uf_2 :: (-> T1 int)
@@ -10110,8 +9872,8 @@
 #297 := (uf_2 #141)
 #357 := (= #297 0::int)
 #166 := (uf_1 0::int)
-#454 := (uf_2 #166)
-#515 := (= #454 0::int)
+#531 := (uf_2 #166)
+#537 := (= #531 0::int)
 #10 := (:var 0 int)
 #12 := (uf_1 #10)
 #672 := (pattern #12)
@@ -10168,40 +9930,40 @@
 #192 := [mp~ #95 #175]: #90
 #678 := [mp #192 #677]: #673
 #650 := (not #673)
-#468 := (or #650 #515)
-#528 := (>= 0::int 0::int)
-#508 := (not #528)
-#509 := (= 0::int #454)
-#490 := (or #509 #508)
-#469 := (or #650 #490)
-#471 := (iff #469 #468)
-#473 := (iff #468 #468)
-#474 := [rewrite]: #473
-#462 := (iff #490 #515)
-#495 := (or #515 false)
-#486 := (iff #495 #515)
-#507 := [rewrite]: #486
-#496 := (iff #490 #495)
-#492 := (iff #508 false)
+#528 := (or #650 #537)
+#529 := (>= 0::int 0::int)
+#530 := (not #529)
+#534 := (= 0::int #531)
+#535 := (or #534 #530)
+#508 := (or #650 #535)
+#509 := (iff #508 #528)
+#514 := (iff #528 #528)
+#515 := [rewrite]: #514
+#527 := (iff #535 #537)
+#520 := (or #537 false)
+#525 := (iff #520 #537)
+#526 := [rewrite]: #525
+#521 := (iff #535 #520)
+#519 := (iff #530 false)
 #1 := true
-#491 := (not true)
-#483 := (iff #491 false)
-#485 := [rewrite]: #483
-#450 := (iff #508 #491)
-#516 := (iff #528 true)
-#484 := [rewrite]: #516
-#481 := [monotonicity #484]: #450
-#494 := [trans #481 #485]: #492
-#514 := (iff #509 #515)
-#510 := [rewrite]: #514
-#506 := [monotonicity #510 #494]: #496
-#463 := [trans #506 #507]: #462
-#472 := [monotonicity #463]: #471
-#475 := [trans #472 #474]: #471
-#470 := [quant-inst]: #469
-#476 := [mp #470 #475]: #468
-#351 := [unit-resolution #476 #678]: #515
-#287 := (= #297 #454)
+#512 := (not true)
+#517 := (iff #512 false)
+#518 := [rewrite]: #517
+#513 := (iff #530 #512)
+#538 := (iff #529 true)
+#511 := [rewrite]: #538
+#406 := [monotonicity #511]: #513
+#524 := [trans #406 #518]: #519
+#536 := (iff #534 #537)
+#532 := [rewrite]: #536
+#522 := [monotonicity #532 #524]: #521
+#523 := [trans #522 #526]: #527
+#490 := [monotonicity #523]: #509
+#510 := [trans #490 #515]: #509
+#454 := [quant-inst]: #508
+#516 := [mp #454 #510]: #528
+#394 := [unit-resolution #516 #678]: #537
+#355 := (= #297 #531)
 #250 := (= #141 #166)
 #26 := 2::int
 #144 := (* 2::int #22)
@@ -10212,24 +9974,29 @@
 #161 := (uf_1 #156)
 #336 := (= #161 #166)
 #327 := (not #336)
-#568 := (uf_2 #161)
-#537 := (= #568 0::int)
-#354 := (= #568 #454)
-#352 := [hypothesis]: #336
-#344 := [monotonicity #352]: #354
-#355 := [trans #344 #351]: #537
-#368 := (not #537)
-#527 := (<= #568 0::int)
-#375 := (not #527)
-#566 := (>= #150 0::int)
-#447 := (>= #22 0::int)
-#421 := (= #22 0::int)
+#588 := (uf_2 #161)
+#555 := (= #588 0::int)
+#398 := (= #588 #531)
+#395 := [hypothesis]: #336
+#387 := [monotonicity #395]: #398
+#399 := [trans #387 #394]: #555
+#390 := (not #555)
+#547 := (<= #588 0::int)
+#403 := (not #547)
+#595 := (>= #150 0::int)
+#302 := -1::int
+#618 := (* -1::int #150)
+#624 := (+ #144 #618)
+#488 := (<= #624 0::int)
+#465 := (= #624 0::int)
+#609 := (>= #22 0::int)
+#442 := (= #22 0::int)
 #660 := (uf_1 #22)
-#451 := (uf_2 #660)
-#452 := (= #451 0::int)
-#603 := (not #447)
-#424 := [hypothesis]: #603
-#455 := (or #447 #452)
+#495 := (uf_2 #660)
+#496 := (= #495 0::int)
+#612 := (not #609)
+#451 := [hypothesis]: #612
+#506 := (or #496 #609)
 #18 := (= #13 0::int)
 #126 := (or #18 #78)
 #679 := (forall (vars (?x3 int)) (:pat #672) #126)
@@ -10287,23 +10054,15 @@
 #195 := [mp~ #136 #180]: #131
 #684 := [mp #195 #683]: #679
 #346 := (not #679)
-#458 := (or #346 #447 #452)
-#453 := (or #452 #447)
-#459 := (or #346 #453)
-#434 := (iff #459 #458)
-#443 := (or #346 #455)
-#432 := (iff #443 #458)
-#433 := [rewrite]: #432
-#461 := (iff #459 #443)
-#456 := (iff #453 #455)
-#457 := [rewrite]: #456
-#431 := [monotonicity #457]: #461
-#436 := [trans #431 #433]: #434
-#460 := [quant-inst]: #459
-#437 := [mp #460 #436]: #458
-#420 := [unit-resolution #437 #684]: #455
-#425 := [unit-resolution #420 #424]: #452
-#405 := (= #22 #451)
+#462 := (or #346 #496 #609)
+#463 := (or #346 #506)
+#469 := (iff #463 #462)
+#470 := [rewrite]: #469
+#468 := [quant-inst]: #463
+#471 := [mp #468 #470]: #462
+#452 := [unit-resolution #471 #684]: #506
+#453 := [unit-resolution #452 #451]: #496
+#456 := (= #22 #495)
 #661 := (= uf_3 #660)
 #4 := (:var 0 T1)
 #5 := (uf_2 #4)
@@ -10334,136 +10093,117 @@
 #663 := (not #665)
 #653 := (or #663 #661)
 #312 := [quant-inst]: #653
-#415 := [unit-resolution #312 #671]: #661
-#407 := [monotonicity #415]: #405
-#408 := [trans #407 #425]: #421
-#411 := (not #421)
-#412 := (or #411 #447)
-#416 := [th-lemma]: #412
-#409 := [unit-resolution #416 #424 #408]: false
-#417 := [lemma #409]: #447
-#302 := -1::int
-#618 := (* -1::int #150)
-#624 := (+ #144 #618)
-#595 := (<= #624 0::int)
-#465 := (= #624 0::int)
-#489 := (or #603 #465)
-#482 := (or #650 #603 #465)
+#455 := [unit-resolution #312 #671]: #661
+#457 := [monotonicity #455]: #456
+#458 := [trans #457 #453]: #442
+#459 := (not #442)
+#460 := (or #459 #609)
+#443 := [th-lemma]: #460
+#461 := [unit-resolution #443 #451 #458]: false
+#431 := [lemma #461]: #609
+#613 := (or #465 #612)
+#615 := (or #650 #465 #612)
 #616 := (>= #144 0::int)
 #617 := (not #616)
 #622 := (= #144 #150)
 #623 := (or #622 #617)
-#497 := (or #650 #623)
-#504 := (iff #497 #482)
-#500 := (or #650 #489)
-#502 := (iff #500 #482)
-#503 := [rewrite]: #502
-#493 := (iff #497 #500)
-#594 := (iff #623 #489)
-#609 := (* 1::int #22)
-#610 := (>= #609 0::int)
-#606 := (not #610)
-#614 := (or #465 #606)
-#498 := (iff #614 #489)
-#605 := (or #465 #603)
-#448 := (iff #605 #489)
-#596 := [rewrite]: #448
-#487 := (iff #614 #605)
-#604 := (iff #606 #603)
-#600 := (iff #610 #447)
-#444 := (= #609 #22)
-#446 := [rewrite]: #444
-#601 := [monotonicity #446]: #600
-#602 := [monotonicity #601]: #604
-#488 := [monotonicity #602]: #487
-#593 := [trans #488 #596]: #498
-#608 := (iff #623 #614)
-#607 := (iff #617 #606)
-#611 := (iff #616 #610)
-#612 := [rewrite]: #611
-#613 := [monotonicity #612]: #607
+#444 := (or #650 #623)
+#602 := (iff #444 #615)
+#447 := (or #650 #613)
+#603 := (iff #447 #615)
+#604 := [rewrite]: #603
+#600 := (iff #444 #447)
+#614 := (iff #623 #613)
+#606 := (iff #617 #612)
+#610 := (iff #616 #609)
+#611 := [rewrite]: #610
+#607 := [monotonicity #611]: #606
 #466 := (iff #622 #465)
 #467 := [rewrite]: #466
-#615 := [monotonicity #467 #613]: #608
-#597 := [trans #615 #593]: #594
-#501 := [monotonicity #597]: #493
-#505 := [trans #501 #503]: #504
-#499 := [quant-inst]: #497
-#598 := [mp #499 #505]: #482
-#404 := [unit-resolution #598 #678]: #489
-#386 := [unit-resolution #404 #417]: #465
-#388 := (not #465)
-#389 := (or #388 #595)
-#390 := [th-lemma]: #389
-#391 := [unit-resolution #390 #386]: #595
-#395 := (not #595)
-#413 := (or #566 #603 #395)
-#403 := [th-lemma]: #413
-#373 := [unit-resolution #403 #391 #417]: #566
-#553 := -3::int
-#551 := (* -1::int #568)
-#552 := (+ #150 #551)
-#535 := (<= #552 -3::int)
-#554 := (= #552 -3::int)
-#557 := (>= #150 -3::int)
+#608 := [monotonicity #467 #607]: #614
+#601 := [monotonicity #608]: #600
+#605 := [trans #601 #604]: #602
+#446 := [quant-inst]: #444
+#487 := [mp #446 #605]: #615
+#439 := [unit-resolution #487 #678]: #613
+#435 := [unit-resolution #439 #431]: #465
+#440 := (not #465)
+#419 := (or #440 #488)
+#422 := [th-lemma]: #419
+#426 := [unit-resolution #422 #435]: #488
+#430 := (not #488)
+#433 := (or #595 #612 #430)
+#438 := [th-lemma]: #433
+#402 := [unit-resolution #438 #431 #426]: #595
+#590 := -3::int
+#579 := (* -1::int #588)
+#589 := (+ #150 #579)
+#553 := (<= #589 -3::int)
+#591 := (= #589 -3::int)
+#581 := (>= #150 -3::int)
 #644 := (>= #22 -1::int)
-#392 := (or #603 #644)
-#393 := [th-lemma]: #392
-#394 := [unit-resolution #393 #417]: #644
+#428 := (or #612 #644)
+#429 := [th-lemma]: #428
+#427 := [unit-resolution #429 #431]: #644
 #646 := (not #644)
-#396 := (or #557 #646 #395)
-#397 := [th-lemma]: #396
-#398 := [unit-resolution #397 #391 #394]: #557
-#560 := (not #557)
-#539 := (or #554 #560)
-#543 := (or #650 #554 #560)
-#567 := (>= #156 0::int)
-#564 := (not #567)
-#548 := (= #156 #568)
-#549 := (or #548 #564)
-#544 := (or #650 #549)
-#530 := (iff #544 #543)
-#546 := (or #650 #539)
-#533 := (iff #546 #543)
-#529 := [rewrite]: #533
-#541 := (iff #544 #546)
-#540 := (iff #549 #539)
-#550 := (iff #564 #560)
-#558 := (iff #567 #557)
-#559 := [rewrite]: #558
-#561 := [monotonicity #559]: #550
-#555 := (iff #548 #554)
-#556 := [rewrite]: #555
-#542 := [monotonicity #556 #561]: #540
-#547 := [monotonicity #542]: #541
-#531 := [trans #547 #529]: #530
-#545 := [quant-inst]: #544
-#534 := [mp #545 #531]: #543
-#387 := [unit-resolution #534 #678]: #539
-#399 := [unit-resolution #387 #398]: #554
-#376 := (not #554)
-#378 := (or #376 #535)
-#379 := [th-lemma]: #378
-#380 := [unit-resolution #379 #399]: #535
-#365 := (not #535)
-#364 := (not #566)
-#366 := (or #375 #364 #365)
-#358 := [th-lemma]: #366
-#367 := [unit-resolution #358 #380 #373]: #375
-#359 := (or #368 #527)
-#369 := [th-lemma]: #359
-#350 := [unit-resolution #369 #367]: #368
-#321 := [unit-resolution #350 #355]: false
-#323 := [lemma #321]: #327
+#418 := (or #581 #646 #430)
+#421 := [th-lemma]: #418
+#423 := [unit-resolution #421 #426 #427]: #581
+#584 := (not #581)
+#573 := (or #584 #591)
+#562 := (or #650 #584 #591)
+#599 := (>= #156 0::int)
+#586 := (not #599)
+#580 := (= #156 #588)
+#577 := (or #580 #586)
+#563 := (or #650 #577)
+#549 := (iff #563 #562)
+#566 := (or #650 #573)
+#568 := (iff #566 #562)
+#548 := [rewrite]: #568
+#567 := (iff #563 #566)
+#571 := (iff #577 #573)
+#569 := (or #591 #584)
+#574 := (iff #569 #573)
+#575 := [rewrite]: #574
+#570 := (iff #577 #569)
+#578 := (iff #586 #584)
+#582 := (iff #599 #581)
+#583 := [rewrite]: #582
+#585 := [monotonicity #583]: #578
+#587 := (iff #580 #591)
+#592 := [rewrite]: #587
+#572 := [monotonicity #592 #585]: #570
+#576 := [trans #572 #575]: #571
+#564 := [monotonicity #576]: #567
+#551 := [trans #564 #548]: #549
+#565 := [quant-inst]: #563
+#552 := [mp #565 #551]: #562
+#424 := [unit-resolution #552 #678]: #573
+#420 := [unit-resolution #424 #423]: #591
+#425 := (not #591)
+#415 := (or #425 #553)
+#405 := [th-lemma]: #415
+#407 := [unit-resolution #405 #420]: #553
+#404 := (not #553)
+#401 := (not #595)
+#386 := (or #403 #401 #404)
+#388 := [th-lemma]: #386
+#389 := [unit-resolution #388 #407 #402]: #403
+#391 := (or #390 #547)
+#392 := [th-lemma]: #391
+#393 := [unit-resolution #392 #389]: #390
+#376 := [unit-resolution #393 #399]: false
+#378 := [lemma #376]: #327
 #249 := (= #141 #161)
 #334 := (not #249)
-#343 := (= #297 #568)
-#322 := [hypothesis]: #249
-#333 := [monotonicity #322]: #343
-#315 := (not #343)
-#414 := (+ #297 #551)
-#401 := (>= #414 0::int)
-#372 := (not #401)
+#396 := (= #297 #588)
+#385 := [hypothesis]: #249
+#370 := [monotonicity #385]: #396
+#380 := (not #396)
+#434 := (+ #297 #579)
+#280 := (>= #434 0::int)
+#414 := (not #280)
 #303 := (* -1::int #297)
 #304 := (+ #22 #303)
 #356 := (>= #304 -1::int)
@@ -10492,21 +10232,21 @@
 #256 := [trans #360 #362]: #363
 #637 := [quant-inst]: #651
 #633 := [mp #637 #256]: #648
-#381 := [unit-resolution #633 #678]: #649
-#382 := [unit-resolution #381 #394]: #641
-#383 := (not #641)
-#384 := (or #383 #356)
-#377 := [th-lemma]: #384
-#385 := [unit-resolution #377 #382]: #356
-#370 := [hypothesis]: #401
-#371 := [th-lemma #398 #370 #385 #380 #391]: false
-#374 := [lemma #371]: #372
-#328 := (or #315 #401)
-#329 := [th-lemma]: #328
-#332 := [unit-resolution #329 #374]: #315
-#316 := [unit-resolution #332 #333]: false
-#318 := [lemma #316]: #334
-#295 := (or #249 #250 #336)
+#408 := [unit-resolution #633 #678]: #649
+#411 := [unit-resolution #408 #427]: #641
+#412 := (not #641)
+#416 := (or #412 #356)
+#409 := [th-lemma]: #416
+#417 := [unit-resolution #409 #411]: #356
+#410 := [hypothesis]: #280
+#413 := [th-lemma #423 #410 #417 #407 #426]: false
+#400 := [lemma #413]: #414
+#381 := (or #380 #280)
+#382 := [th-lemma]: #381
+#377 := [unit-resolution #382 #400]: #380
+#371 := [unit-resolution #377 #370]: false
+#372 := [lemma #371]: #334
+#352 := (or #249 #250 #336)
 #335 := (not #250)
 #338 := (and #334 #335 #327)
 #339 := (not #338)
@@ -10554,31 +10294,30 @@
 #177 := [mp #137 #174]: #172
 #326 := (or #169 #339)
 #659 := [def-axiom]: #326
-#294 := [unit-resolution #659 #177]: #339
+#351 := [unit-resolution #659 #177]: #339
 #314 := (or #338 #249 #250 #336)
 #445 := [def-axiom]: #314
-#293 := [unit-resolution #445 #294]: #295
-#296 := [unit-resolution #293 #318 #323]: #250
-#290 := [monotonicity #296]: #287
-#285 := [trans #290 #351]: #357
-#310 := (not #357)
+#343 := [unit-resolution #445 #351]: #352
+#353 := [unit-resolution #343 #372 #378]: #250
+#321 := [monotonicity #353]: #355
+#323 := [trans #321 #394]: #357
+#368 := (not #357)
 #620 := (<= #297 0::int)
-#305 := (not #620)
+#364 := (not #620)
 #634 := (<= #304 -1::int)
-#319 := (or #383 #634)
-#298 := [th-lemma]: #319
-#300 := [unit-resolution #298 #382]: #634
-#306 := (not #634)
-#307 := (or #305 #603 #306)
-#308 := [th-lemma]: #307
-#309 := [unit-resolution #308 #300 #417]: #305
-#299 := (or #310 #620)
-#311 := [th-lemma]: #299
-#292 := [unit-resolution #311 #309]: #310
-[unit-resolution #292 #285]: false
-unsat
-
-ipe8HUL/t33OoeNl/z0smQ 4011
+#374 := (or #412 #634)
+#373 := [th-lemma]: #374
+#375 := [unit-resolution #373 #411]: #634
+#365 := (not #634)
+#366 := (or #364 #612 #365)
+#358 := [th-lemma]: #366
+#367 := [unit-resolution #358 #375 #431]: #364
+#359 := (or #368 #620)
+#369 := [th-lemma]: #359
+#350 := [unit-resolution #369 #367]: #368
+[unit-resolution #350 #323]: false
+unsat
+mu7O1os0t3tPqWZhwizjxw 161 0
 #2 := false
 #9 := 0::int
 decl uf_3 :: int
@@ -10740,8 +10479,7 @@
 #361 := [unit-resolution #639 #655]: #647
 [th-lemma #656 #361 #261]: false
 unsat
-
-9FrZeHP8ZKJM+JmhfAjimQ 14889
+08cmOtIT4NYs2PG/F3zeZw 557 0
 #2 := false
 #9 := 0::int
 decl uf_2 :: (-> T1 int)
@@ -10753,46 +10491,46 @@
 #38 := (* 4::int #37)
 #39 := (uf_1 #38)
 #40 := (uf_2 #39)
-#504 := (= #40 0::int)
-#995 := (not #504)
-#475 := (<= #40 0::int)
-#990 := (not #475)
+#527 := (= #40 0::int)
+#976 := (not #527)
+#502 := (<= #40 0::int)
+#971 := (not #502)
 #22 := 1::int
 #186 := (+ 1::int #40)
 #189 := (uf_1 #186)
-#467 := (uf_2 #189)
-#380 := (<= #467 1::int)
-#893 := (not #380)
+#506 := (uf_2 #189)
+#407 := (<= #506 1::int)
+#876 := (not #407)
 decl up_4 :: (-> T1 T1 bool)
 #4 := (:var 0 T1)
-#386 := (up_4 #4 #189)
-#374 := (pattern #386)
-#382 := (not #386)
-#385 := (= #4 #189)
+#408 := (up_4 #4 #189)
+#393 := (pattern #408)
+#413 := (= #4 #189)
+#414 := (not #408)
 #26 := (uf_1 1::int)
 #27 := (= #4 #26)
-#845 := (or #27 #385 #382)
-#848 := (forall (vars (?x5 T1)) (:pat #374) #845)
-#851 := (not #848)
-#854 := (or #380 #851)
-#857 := (not #854)
+#392 := (or #27 #414 #413)
+#397 := (forall (vars (?x5 T1)) (:pat #393) #392)
+#383 := (not #397)
+#382 := (or #383 #407)
+#375 := (not #382)
 decl up_3 :: (-> T1 bool)
 #192 := (up_3 #189)
-#840 := (not #192)
-#860 := (or #840 #857)
+#404 := (not #192)
+#841 := (or #404 #375)
 decl ?x5!0 :: (-> T1 T1)
-#392 := (?x5!0 #189)
-#397 := (up_4 #392 #189)
-#390 := (not #397)
-#396 := (= #26 #392)
-#395 := (= #189 #392)
-#866 := (or #395 #396 #390)
-#869 := (not #866)
-#872 := (or #192 #380 #869)
-#875 := (not #872)
-#863 := (not #860)
-#878 := (or #863 #875)
-#881 := (not #878)
+#422 := (?x5!0 #189)
+#434 := (= #189 #422)
+#417 := (up_4 #422 #189)
+#418 := (not #417)
+#415 := (= #26 #422)
+#847 := (or #415 #418 #434)
+#850 := (not #847)
+#853 := (or #192 #407 #850)
+#856 := (not #853)
+#844 := (not #841)
+#859 := (or #844 #856)
+#862 := (not #859)
 #5 := (uf_2 #4)
 #787 := (pattern #5)
 #21 := (up_3 #4)
@@ -10971,59 +10709,64 @@
 #314 := [mp #267 #313]: #311
 #839 := [mp #314 #838]: #836
 #589 := (not #836)
-#884 := (or #589 #881)
-#398 := (or #390 #396 #395)
-#383 := (not #398)
-#381 := (or #192 #380 #383)
-#384 := (not #381)
-#387 := (or #382 #27 #385)
-#376 := (forall (vars (?x5 T1)) (:pat #374) #387)
-#377 := (not #376)
-#375 := (or #380 #377)
-#378 := (not #375)
-#841 := (or #840 #378)
-#842 := (not #841)
-#843 := (or #842 #384)
-#844 := (not #843)
-#885 := (or #589 #844)
-#887 := (iff #885 #884)
-#889 := (iff #884 #884)
-#890 := [rewrite]: #889
-#882 := (iff #844 #881)
-#879 := (iff #843 #878)
-#876 := (iff #384 #875)
-#873 := (iff #381 #872)
-#870 := (iff #383 #869)
-#867 := (iff #398 #866)
-#868 := [rewrite]: #867
-#871 := [monotonicity #868]: #870
-#874 := [monotonicity #871]: #873
-#877 := [monotonicity #874]: #876
-#864 := (iff #842 #863)
-#861 := (iff #841 #860)
-#858 := (iff #378 #857)
-#855 := (iff #375 #854)
-#852 := (iff #377 #851)
-#849 := (iff #376 #848)
-#846 := (iff #387 #845)
-#847 := [rewrite]: #846
-#850 := [quant-intro #847]: #849
-#853 := [monotonicity #850]: #852
-#856 := [monotonicity #853]: #855
-#859 := [monotonicity #856]: #858
-#862 := [monotonicity #859]: #861
-#865 := [monotonicity #862]: #864
-#880 := [monotonicity #865 #877]: #879
-#883 := [monotonicity #880]: #882
-#888 := [monotonicity #883]: #887
-#891 := [trans #888 #890]: #887
-#886 := [quant-inst]: #885
-#892 := [mp #886 #891]: #884
-#966 := [unit-resolution #892 #839]: #881
-#924 := (or #878 #860)
-#925 := [def-axiom]: #924
-#967 := [unit-resolution #925 #966]: #860
-#970 := (or #863 #857)
+#865 := (or #589 #862)
+#416 := (or #418 #415 #434)
+#419 := (not #416)
+#409 := (or #192 #407 #419)
+#410 := (not #409)
+#389 := (or #414 #27 #413)
+#394 := (forall (vars (?x5 T1)) (:pat #393) #389)
+#399 := (not #394)
+#401 := (or #407 #399)
+#402 := (not #401)
+#400 := (or #404 #402)
+#405 := (not #400)
+#388 := (or #405 #410)
+#391 := (not #388)
+#866 := (or #589 #391)
+#868 := (iff #866 #865)
+#870 := (iff #865 #865)
+#871 := [rewrite]: #870
+#863 := (iff #391 #862)
+#860 := (iff #388 #859)
+#857 := (iff #410 #856)
+#854 := (iff #409 #853)
+#851 := (iff #419 #850)
+#848 := (iff #416 #847)
+#849 := [rewrite]: #848
+#852 := [monotonicity #849]: #851
+#855 := [monotonicity #852]: #854
+#858 := [monotonicity #855]: #857
+#845 := (iff #405 #844)
+#842 := (iff #400 #841)
+#378 := (iff #402 #375)
+#376 := (iff #401 #382)
+#384 := (or #407 #383)
+#387 := (iff #384 #382)
+#374 := [rewrite]: #387
+#385 := (iff #401 #384)
+#380 := (iff #399 #383)
+#390 := (iff #394 #397)
+#395 := (iff #389 #392)
+#396 := [rewrite]: #395
+#398 := [quant-intro #396]: #390
+#381 := [monotonicity #398]: #380
+#386 := [monotonicity #381]: #385
+#377 := [trans #386 #374]: #376
+#840 := [monotonicity #377]: #378
+#843 := [monotonicity #840]: #842
+#846 := [monotonicity #843]: #845
+#861 := [monotonicity #846 #858]: #860
+#864 := [monotonicity #861]: #863
+#869 := [monotonicity #864]: #868
+#872 := [trans #869 #871]: #868
+#867 := [quant-inst]: #866
+#873 := [mp #867 #872]: #865
+#947 := [unit-resolution #873 #839]: #862
+#905 := (or #859 #841)
+#906 := [def-axiom]: #905
+#948 := [unit-resolution #906 #947]: #841
+#951 := (or #844 #375)
 #41 := (+ #40 1::int)
 #42 := (uf_1 #41)
 #43 := (up_3 #42)
@@ -11035,30 +10778,30 @@
 #194 := [monotonicity #191]: #193
 #185 := [asserted]: #43
 #197 := [mp #185 #194]: #192
-#904 := (or #863 #840 #857)
-#905 := [def-axiom]: #904
-#971 := [unit-resolution #905 #197]: #970
-#972 := [unit-resolution #971 #967]: #857
-#894 := (or #854 #893)
-#895 := [def-axiom]: #894
-#973 := [unit-resolution #895 #972]: #893
+#885 := (or #844 #404 #375)
+#886 := [def-axiom]: #885
+#952 := [unit-resolution #886 #197]: #951
+#953 := [unit-resolution #952 #948]: #375
+#877 := (or #382 #876)
+#878 := [def-axiom]: #877
+#954 := [unit-resolution #878 #953]: #876
 #542 := -1::int
-#446 := (* -1::int #467)
-#447 := (+ #40 #446)
-#416 := (>= #447 -1::int)
-#438 := (= #447 -1::int)
-#453 := (>= #40 -1::int)
-#419 := (= #467 0::int)
-#978 := (not #419)
-#388 := (<= #467 0::int)
-#974 := (not #388)
-#975 := (or #974 #380)
-#976 := [th-lemma]: #975
-#977 := [unit-resolution #976 #973]: #974
-#979 := (or #978 #388)
-#980 := [th-lemma]: #979
-#981 := [unit-resolution #980 #977]: #978
-#409 := (or #419 #453)
+#508 := (* -1::int #506)
+#493 := (+ #40 #508)
+#438 := (>= #493 -1::int)
+#494 := (= #493 -1::int)
+#496 := (>= #40 -1::int)
+#451 := (= #506 0::int)
+#959 := (not #451)
+#432 := (<= #506 0::int)
+#955 := (not #432)
+#956 := (or #955 #407)
+#957 := [th-lemma]: #956
+#958 := [unit-resolution #957 #954]: #955
+#960 := (or #959 #432)
+#961 := [th-lemma]: #960
+#962 := [unit-resolution #961 #958]: #959
+#453 := (or #451 #496)
 #10 := (:var 0 int)
 #12 := (uf_1 #10)
 #795 := (pattern #12)
@@ -11121,28 +10864,28 @@
 #145 := [mp #105 #144]: #140
 #227 := [mp~ #145 #208]: #140
 #807 := [mp #227 #806]: #802
-#496 := (not #802)
-#408 := (or #496 #419 #453)
-#476 := (>= #186 0::int)
-#407 := (or #419 #476)
-#414 := (or #496 #407)
-#404 := (iff #414 #408)
-#393 := (or #496 #409)
-#401 := (iff #393 #408)
-#402 := [rewrite]: #401
-#394 := (iff #414 #393)
-#410 := (iff #407 #409)
-#454 := (iff #476 #453)
-#455 := [rewrite]: #454
-#413 := [monotonicity #455]: #410
-#399 := [monotonicity #413]: #394
-#400 := [trans #399 #402]: #404
-#389 := [quant-inst]: #414
-#405 := [mp #389 #400]: #408
-#982 := [unit-resolution #405 #807]: #409
-#983 := [unit-resolution #982 #981]: #453
-#445 := (not #453)
-#441 := (or #438 #445)
+#514 := (not #802)
+#445 := (or #514 #451 #496)
+#504 := (>= #186 0::int)
+#452 := (or #451 #504)
+#456 := (or #514 #452)
+#429 := (iff #456 #445)
+#441 := (or #514 #453)
+#423 := (iff #441 #445)
+#428 := [rewrite]: #423
+#442 := (iff #456 #441)
+#454 := (iff #452 #453)
+#498 := (iff #504 #496)
+#487 := [rewrite]: #498
+#455 := [monotonicity #487]: #454
+#421 := [monotonicity #455]: #442
+#430 := [trans #421 #428]: #429
+#439 := [quant-inst]: #456
+#431 := [mp #439 #430]: #445
+#963 := [unit-resolution #431 #807]: #453
+#964 := [unit-resolution #963 #962]: #496
+#488 := (not #496)
+#490 := (or #494 #488)
 #69 := (= #10 #13)
 #94 := (or #69 #88)
 #796 := (forall (vars (?x2 int)) (:pat #795) #94)
@@ -11192,48 +10935,48 @@
 #104 := [mp #68 #103]: #99
 #224 := [mp~ #104 #196]: #99
 #801 := [mp #224 #800]: #796
-#514 := (not #796)
-#423 := (or #514 #438 #445)
-#477 := (not #476)
-#478 := (= #186 #467)
-#444 := (or #478 #477)
-#428 := (or #514 #444)
-#434 := (iff #428 #423)
-#430 := (or #514 #441)
-#433 := (iff #430 #423)
-#422 := [rewrite]: #433
-#431 := (iff #428 #430)
-#442 := (iff #444 #441)
-#456 := (iff #477 #445)
-#439 := [monotonicity #455]: #456
-#451 := (iff #478 #438)
-#452 := [rewrite]: #451
-#421 := [monotonicity #452 #439]: #442
-#432 := [monotonicity #421]: #431
-#415 := [trans #432 #422]: #434
-#429 := [quant-inst]: #428
-#417 := [mp #429 #415]: #423
-#984 := [unit-resolution #417 #801]: #441
-#985 := [unit-resolution #984 #983]: #438
-#986 := (not #438)
-#987 := (or #986 #416)
-#988 := [th-lemma]: #987
-#989 := [unit-resolution #988 #985]: #416
-#991 := (not #416)
-#992 := (or #990 #380 #991)
-#993 := [th-lemma]: #992
-#994 := [unit-resolution #993 #989 #973]: #990
-#996 := (or #995 #475)
-#997 := [th-lemma]: #996
-#998 := [unit-resolution #997 #994]: #995
-#536 := (>= #37 0::int)
-#525 := (not #536)
+#530 := (not #796)
+#492 := (or #530 #494 #488)
+#505 := (not #504)
+#507 := (= #186 #506)
+#500 := (or #507 #505)
+#473 := (or #530 #500)
+#478 := (iff #473 #492)
+#475 := (or #530 #490)
+#477 := (iff #475 #492)
+#467 := [rewrite]: #477
+#466 := (iff #473 #475)
+#491 := (iff #500 #490)
+#489 := (iff #505 #488)
+#481 := [monotonicity #487]: #489
+#495 := (iff #507 #494)
+#497 := [rewrite]: #495
+#482 := [monotonicity #497 #481]: #491
+#476 := [monotonicity #482]: #466
+#444 := [trans #476 #467]: #478
+#474 := [quant-inst]: #473
+#446 := [mp #474 #444]: #492
+#965 := [unit-resolution #446 #801]: #490
+#966 := [unit-resolution #965 #964]: #494
+#967 := (not #494)
+#968 := (or #967 #438)
+#969 := [th-lemma]: #968
+#970 := [unit-resolution #969 #966]: #438
+#972 := (not #438)
+#973 := (or #971 #407 #972)
+#974 := [th-lemma]: #973
+#975 := [unit-resolution #974 #970 #954]: #971
+#977 := (or #976 #502)
+#978 := [th-lemma]: #977
+#979 := [unit-resolution #978 #975]: #976
+#553 := (>= #37 0::int)
+#546 := (not #553)
 #545 := (* -1::int #40)
 #549 := (+ #38 #545)
 #551 := (= #549 0::int)
-#1003 := (not #551)
-#503 := (>= #549 0::int)
-#999 := (not #503)
+#984 := (not #551)
+#524 := (>= #549 0::int)
+#980 := (not #524)
 #201 := (>= #37 1::int)
 #202 := (not #201)
 #44 := (<= 1::int #37)
@@ -11244,157 +10987,107 @@
 #204 := [monotonicity #200]: #203
 #195 := [asserted]: #45
 #205 := [mp #195 #204]: #202
-#1000 := (or #999 #201 #380 #991)
-#1001 := [th-lemma]: #1000
-#1002 := [unit-resolution #1001 #205 #989 #973]: #999
-#1004 := (or #1003 #503)
-#1005 := [th-lemma]: #1004
-#1006 := [unit-resolution #1005 #1002]: #1003
-#527 := (or #525 #551)
-#515 := (or #514 #525 #551)
+#981 := (or #980 #201 #407 #972)
+#982 := [th-lemma]: #981
+#983 := [unit-resolution #982 #205 #970 #954]: #980
+#985 := (or #984 #524)
+#986 := [th-lemma]: #985
+#987 := [unit-resolution #986 #983]: #984
+#548 := (or #551 #546)
+#531 := (or #530 #551 #546)
 #403 := (>= #38 0::int)
 #562 := (not #403)
 #558 := (= #38 #40)
 #563 := (or #558 #562)
-#516 := (or #514 #563)
+#534 := (or #530 #563)
+#537 := (iff #534 #531)
+#539 := (or #530 #548)
+#533 := (iff #539 #531)
+#536 := [rewrite]: #533
+#532 := (iff #534 #539)
+#538 := (iff #563 #548)
+#547 := (iff #562 #546)
+#541 := (iff #403 #553)
+#544 := [rewrite]: #541
+#543 := [monotonicity #544]: #547
+#552 := (iff #558 #551)
+#550 := [rewrite]: #552
+#528 := [monotonicity #550 #543]: #538
+#540 := [monotonicity #528]: #532
+#523 := [trans #540 #536]: #537
+#535 := [quant-inst]: #534
+#525 := [mp #535 #523]: #531
+#988 := [unit-resolution #525 #801]: #548
+#989 := [unit-resolution #988 #987]: #546
+#511 := (or #527 #553)
+#515 := (or #514 #527 #553)
+#509 := (or #527 #403)
+#516 := (or #514 #509)
 #522 := (iff #516 #515)
-#518 := (or #514 #527)
+#518 := (or #514 #511)
 #521 := (iff #518 #515)
 #510 := [rewrite]: #521
 #519 := (iff #516 #518)
-#512 := (iff #563 #527)
-#553 := (* 1::int #37)
-#541 := (>= #553 0::int)
-#547 := (not #541)
-#531 := (or #547 #551)
-#509 := (iff #531 #527)
-#526 := (iff #547 #525)
-#537 := (iff #541 #536)
-#540 := (= #553 #37)
-#533 := [rewrite]: #540
-#523 := [monotonicity #533]: #537
-#524 := [monotonicity #523]: #526
-#511 := [monotonicity #524]: #509
-#539 := (iff #563 #531)
-#538 := (or #551 #547)
-#534 := (iff #538 #531)
-#535 := [rewrite]: #534
-#528 := (iff #563 #538)
-#543 := (iff #562 #547)
-#544 := (iff #403 #541)
-#546 := [rewrite]: #544
-#548 := [monotonicity #546]: #543
-#552 := (iff #558 #551)
-#550 := [rewrite]: #552
-#530 := [monotonicity #550 #548]: #528
-#532 := [trans #530 #535]: #539
-#513 := [trans #532 #511]: #512
+#512 := (iff #509 #511)
+#513 := [monotonicity #544]: #512
 #520 := [monotonicity #513]: #519
 #499 := [trans #520 #510]: #522
 #517 := [quant-inst]: #516
 #501 := [mp #517 #499]: #515
-#1007 := [unit-resolution #501 #801]: #527
-#1008 := [unit-resolution #1007 #1006]: #525
-#508 := (or #504 #536)
-#498 := (or #496 #504 #536)
-#505 := (or #504 #403)
-#487 := (or #496 #505)
-#492 := (iff #487 #498)
-#489 := (or #496 #508)
-#491 := (iff #489 #498)
-#482 := [rewrite]: #491
-#481 := (iff #487 #489)
-#495 := (iff #505 #508)
-#506 := (or #504 #541)
-#493 := (iff #506 #508)
-#494 := [monotonicity #523]: #493
-#507 := (iff #505 #506)
-#500 := [monotonicity #546]: #507
-#497 := [trans #500 #494]: #495
-#490 := [monotonicity #497]: #481
-#473 := [trans #490 #482]: #492
-#488 := [quant-inst]: #487
-#474 := [mp #488 #473]: #498
-#1009 := [unit-resolution #474 #807]: #508
-[unit-resolution #1009 #1008 #998]: false
-unsat
-
-uq2MbDTgTG1nxWdwzZtWew 7
-unsat
-
-E5BydeDaPocMMvChMGY+og 7
-unsat
-
-p81EQzqwJrGunGO7GuNt3g 7
-unsat
-
-KpYfvnTcz2WncWNg3dJDCA 7
-unsat
-
-ybGRm230DLO0wH6aROKBBw 7
-unsat
-
-goFtZfJ6kkxA8sqBVpZutw 7
-unsat
-
-0+nmgsMqioeTuwam1ScP7g 7
-unsat
-
-nI63LP/VCL//bjsS1gNB2A 7
-unsat
-
-9+2QHvrRgbKz97Zg0kfybw 7
-unsat
-
-6kquszLXeBUhTwzaw6gd2Q 7
-unsat
-
-j5Z04lpza+N5I1cpno5mtw 7
-unsat
-
-mapbfUM6Ils30x5nEBJmaw 7
-unsat
-
-e8P++0FczY3zhNhEVclACw 7
-unsat
-
-yXMQNOyCylhI+EH8hNYxHA 7
-unsat
-
-GkYN9j7cjrR2KR/lb04/qw 7
-unsat
-
-PajzgNjLWHwVHpjoje+gnA 7
-unsat
-
-URpJYU7D8PO0VRnciRgE5A 7
-unsat
-
-D9ZGhymoV3L6zbWsJlwG2A 7
-unsat
-
-0QLuovrnnANWnCkUY3l10g 7
-unsat
-
-CYprps2G0Au5F3Z7n3KTRg 7
-unsat
-
-iyIMuJd6zijfEao8zKnx2w 7
-unsat
-
-49jzsAwAEfR6NSFBhBEisQ 7
-unsat
-
-T0j6xFgrghxif91jL+2yAw 7
-unsat
-
-md/M3rVve0+8sQ6oqIoL2w 7
-unsat
-
-pY7C8PCf5lVVaim6q7PJcQ 7
-unsat
-
-4zCFLQf4Jrov/gmEvsBm4Q 1036
+#990 := [unit-resolution #501 #807]: #511
+[unit-resolution #990 #989 #979]: false
+unsat
+8HdmSMHHP2B8XMFzjNuw5Q 1 0
+unsat
+O4aM0+/isn2q5CrIefZjzg 1 0
+unsat
+t/ni9djl2DqxH0iKupZSwg 1 0
+unsat
+RumBGekdxZQaBF1HNa3x9w 1 0
+unsat
+Q9d+IbQ8chjKld71X6/zqw 1 0
+unsat
+PhC8zQV8hnJ6E2YYjZPGjQ 1 0
+unsat
+mieI2RhSp3bYaojlWH1A4A 1 0
+unsat
+pRSV6nBLconzrQz2zUrJ6g 1 0
+unsat
+Js0JfdwDoKq3YuilPPgeZw 1 0
+unsat
+GRIqjLUJiqXbo+pXhAeKIw 1 0
+unsat
+Bg5scsmPFp82+7Y2ScL6Wg 1 0
+unsat
+XD6zX6850dLxyfZSfNv30A 1 0
+unsat
+BG/HwJYnumvDICXxtBu/tA 1 0
+unsat
+YMc4t19sUMWbUkx3woxCmQ 1 0
+unsat
+YyD9IF72pKXGGKZTO7FY5Q 1 0
+unsat
+zRPsIUi+TEoz5fPWP0H9bQ 1 0
+unsat
+8ipTE8BOXpvSo/U6D4p3lA 1 0
+unsat
+MSzQywedZPsOE0CDxrrO0g 1 0
+unsat
+SryZuXv48ItET8NPIv07pA 1 0
+unsat
+qOMUQN18hYFl/wWt54lvbA 1 0
+unsat
++njWXdn6fETK3/AjtiHjcA 1 0
+unsat
+5cQ7gJ33gzYTIIPA3hbBmQ 1 0
+unsat
+ZznT34cvumrP00mXZ3gcjw 1 0
+unsat
+//LQca1Et5RfhQJZA+CGCA 1 0
+unsat
+3ntxKz+kaQNfTrLzY9sVXw 1 0
+unsat
+4lL2Qo8ngE1EH1UdeN1Qng 43 0
 #2 := false
 #6 := 0::int
 decl uf_1 :: (-> bv[2] int)
@@ -11438,11 +11131,9 @@
 #287 := [th-lemma]: #627
 [unit-resolution #287 #47 #635]: false
 unsat
-
-czvSLyjMowmFNi82us4N2Q 7
-unsat
-
-aU+7kcyE8oAPbs5RjfuwIw 1160
++xe3O927LrflFUE6NDqRlA 1 0
+unsat
+JPoL7fPYhqhAkjUiVF+THQ 50 0
 #2 := false
 decl uf_6 :: T2
 #23 := uf_6
@@ -11493,8 +11184,7 @@
 #66 := [asserted]: #26
 [unit-resolution #66 #235]: false
 unsat
-
-dXfueqZAXkudfE6G0VKkwg 2559
+l23ZDmd0VbO/Q+uO5EtabA 105 0
 #2 := false
 decl uf_6 :: (-> T4 T2)
 decl uf_10 :: T4
@@ -11600,8 +11290,7 @@
 #110 := [asserted]: #46
 [unit-resolution #110 #238]: false
 unsat
-
-Dc/6bNJffjYYplvoitScJQ 4578
+GZjffeZPQnL3OyLCvxdCpg 181 0
 #2 := false
 decl uf_1 :: (-> T1 T2 T3)
 decl uf_3 :: T2
@@ -11783,8 +11472,7 @@
 #76 := [asserted]: #38
 [unit-resolution #76 #489]: false
 unsat
-
-jdmsd1j41Osn+WzTtqTUSQ 1352
+i6jCzzRosHYE0w7sF1Nraw 62 0
 #2 := false
 decl up_4 :: (-> T1 T2 bool)
 decl uf_3 :: T2
@@ -11847,8 +11535,7 @@
 #73 := [unit-resolution #71 #68]: #72
 [unit-resolution #73 #59 #61]: false
 unsat
-
-EA8ecQ7czWL46/C3k7D7tg 2697
+YZHSyhN2TGlpe+vpkzWrgQ 115 0
 #2 := false
 decl up_2 :: (-> T2 bool)
 decl uf_3 :: T2
@@ -11964,8 +11651,7 @@
 #560 := [mp #344 #559]: #557
 [unit-resolution #560 #576 #561]: false
 unsat
-
-mNfbN3NQCB4ik2xJmLE1UQ 11936
+TibRlXkU+X+1+zGPYTiT0g 464 0
 #2 := false
 decl uf_2 :: (-> T2 T3 T3)
 decl uf_4 :: T3
@@ -12430,8 +12116,7 @@
 #177 := [asserted]: #53
 [unit-resolution #177 #793]: false
 unsat
-
-Jtmz+P173L9nRQkQk52h+Q 420
+DJPKxi9AO25zGBcs5kxUrw 21 0
 #2 := false
 decl up_1 :: (-> T1 bool)
 #4 := (:var 0 T1)
@@ -12453,8 +12138,7 @@
 #25 := [asserted]: #9
 [mp #25 #34]: false
 unsat
-
-YG20f6Uf93koN6rVg/alpA 9742
+i5PnMbuM9mWv5LnVszz9+g 366 0
 #2 := false
 decl uf_1 :: (-> int T1)
 #37 := 6::int
@@ -12469,18 +12153,18 @@
 #35 := (uf_1 #34)
 #36 := (uf_3 #35)
 #39 := (= #36 #38)
-#484 := (uf_3 #38)
-#372 := (= #484 #38)
-#485 := (= #38 #484)
-#592 := (uf_2 #38)
+#476 := (uf_3 #38)
+#403 := (= #476 #38)
+#531 := (= #38 #476)
+#620 := (uf_2 #38)
 #142 := -10::int
-#496 := (+ -10::int #592)
-#497 := (uf_1 #496)
-#498 := (uf_3 #497)
-#499 := (= #484 #498)
+#513 := (+ -10::int #620)
+#472 := (uf_1 #513)
+#503 := (uf_3 #472)
+#505 := (= #476 #503)
 #22 := 10::int
-#500 := (>= #592 10::int)
-#501 := (ite #500 #499 #485)
+#507 := (>= #620 10::int)
+#514 := (ite #507 #505 #531)
 #4 := (:var 0 T1)
 #21 := (uf_3 #4)
 #707 := (pattern #21)
@@ -12554,12 +12238,12 @@
 #212 := [mp #207 #211]: #193
 #713 := [mp #212 #712]: #708
 #336 := (not #708)
-#463 := (or #336 #501)
-#464 := [quant-inst]: #463
-#444 := [unit-resolution #464 #713]: #501
-#473 := (not #500)
-#453 := (<= #592 6::int)
-#597 := (= #592 6::int)
+#518 := (or #336 #514)
+#528 := [quant-inst]: #518
+#477 := [unit-resolution #528 #713]: #514
+#529 := (not #507)
+#498 := (<= #620 6::int)
+#610 := (= #620 6::int)
 #10 := (:var 0 int)
 #12 := (uf_1 #10)
 #694 := (pattern #12)
@@ -12617,79 +12301,79 @@
 #201 := [mp~ #99 #183]: #94
 #700 := [mp #201 #699]: #695
 #673 := (not #695)
-#576 := (or #673 #597)
-#607 := (>= 6::int 0::int)
-#591 := (not #607)
-#594 := (= 6::int #592)
-#595 := (or #594 #591)
-#577 := (or #673 #595)
-#579 := (iff #577 #576)
-#581 := (iff #576 #576)
-#582 := [rewrite]: #581
-#574 := (iff #595 #597)
-#586 := (or #597 false)
-#571 := (iff #586 #597)
-#573 := [rewrite]: #571
-#590 := (iff #595 #586)
-#588 := (iff #591 false)
+#591 := (or #673 #610)
+#526 := (>= 6::int 0::int)
+#527 := (not #526)
+#617 := (= 6::int #620)
+#621 := (or #617 #527)
+#592 := (or #673 #621)
+#595 := (iff #592 #591)
+#597 := (iff #591 #591)
+#593 := [rewrite]: #597
+#600 := (iff #621 #610)
+#614 := (or #610 false)
+#605 := (iff #614 #610)
+#606 := [rewrite]: #605
+#603 := (iff #621 #614)
+#613 := (iff #527 false)
 #1 := true
 #663 := (not true)
 #666 := (iff #663 false)
 #667 := [rewrite]: #666
-#585 := (iff #591 #663)
-#598 := (iff #607 true)
-#584 := [rewrite]: #598
-#587 := [monotonicity #584]: #585
-#589 := [trans #587 #667]: #588
-#596 := (iff #594 #597)
-#593 := [rewrite]: #596
-#570 := [monotonicity #593 #589]: #590
-#575 := [trans #570 #573]: #574
-#580 := [monotonicity #575]: #579
-#572 := [trans #580 #582]: #579
-#578 := [quant-inst]: #577
-#583 := [mp #578 #572]: #576
-#448 := [unit-resolution #583 #700]: #597
-#445 := (not #597)
-#446 := (or #445 #453)
-#442 := [th-lemma]: #446
-#447 := [unit-resolution #442 #448]: #453
-#437 := (not #453)
-#427 := (or #437 #473)
-#429 := [th-lemma]: #427
-#430 := [unit-resolution #429 #447]: #473
-#471 := (not #501)
-#477 := (or #471 #500 #485)
-#478 := [def-axiom]: #477
-#433 := [unit-resolution #478 #430 #444]: #485
-#373 := [symm #433]: #372
-#374 := (= #36 #484)
+#611 := (iff #527 #663)
+#599 := (iff #526 true)
+#601 := [rewrite]: #599
+#612 := [monotonicity #601]: #611
+#609 := [trans #612 #667]: #613
+#608 := (iff #617 #610)
+#602 := [rewrite]: #608
+#604 := [monotonicity #602 #609]: #603
+#607 := [trans #604 #606]: #600
+#596 := [monotonicity #607]: #595
+#598 := [trans #596 #593]: #595
+#594 := [quant-inst]: #592
+#584 := [mp #594 #598]: #591
+#478 := [unit-resolution #584 #700]: #610
+#453 := (not #610)
+#454 := (or #453 #498)
+#455 := [th-lemma]: #454
+#456 := [unit-resolution #455 #478]: #498
+#458 := (not #498)
+#459 := (or #458 #529)
+#460 := [th-lemma]: #459
+#302 := [unit-resolution #460 #456]: #529
+#508 := (not #514)
+#490 := (or #508 #507 #531)
+#491 := [def-axiom]: #490
+#461 := [unit-resolution #491 #302 #477]: #531
+#404 := [symm #461]: #403
+#405 := (= #36 #476)
 #649 := (uf_2 #35)
-#554 := (+ -10::int #649)
-#549 := (uf_1 #554)
-#545 := (uf_3 #549)
-#381 := (= #545 #484)
-#395 := (= #549 #38)
-#394 := (= #554 6::int)
+#582 := (+ -10::int #649)
+#553 := (uf_1 #582)
+#556 := (uf_3 #553)
+#401 := (= #556 #476)
+#417 := (= #553 #38)
+#415 := (= #582 6::int)
 #335 := (uf_2 #31)
 #647 := -1::int
-#459 := (* -1::int #335)
-#460 := (+ #33 #459)
-#302 := (<= #460 0::int)
-#458 := (= #33 #335)
-#426 := (= #32 #31)
-#555 := (= #31 #32)
-#551 := (+ -10::int #335)
-#552 := (uf_1 #551)
-#553 := (uf_3 #552)
-#556 := (= #32 #553)
-#557 := (>= #335 10::int)
-#558 := (ite #557 #556 #555)
-#560 := (or #336 #558)
-#533 := [quant-inst]: #560
-#434 := [unit-resolution #533 #713]: #558
-#535 := (not #557)
-#531 := (<= #335 4::int)
+#502 := (* -1::int #335)
+#463 := (+ #33 #502)
+#464 := (<= #463 0::int)
+#486 := (= #33 #335)
+#445 := (= #32 #31)
+#574 := (= #31 #32)
+#575 := (+ -10::int #335)
+#576 := (uf_1 #575)
+#577 := (uf_3 #576)
+#578 := (= #32 #577)
+#579 := (>= #335 10::int)
+#580 := (ite #579 #578 #574)
+#572 := (or #336 #580)
+#583 := [quant-inst]: #572
+#457 := [unit-resolution #583 #713]: #580
+#562 := (not #579)
+#554 := (<= #335 4::int)
 #324 := (= #335 4::int)
 #659 := (or #673 #324)
 #678 := (>= 4::int 0::int)
@@ -12719,125 +12403,109 @@
 #277 := [trans #383 #385]: #382
 #367 := [quant-inst]: #660
 #655 := [mp #367 #277]: #659
-#438 := [unit-resolution #655 #700]: #324
-#431 := (not #324)
-#439 := (or #431 #531)
-#432 := [th-lemma]: #439
-#435 := [unit-resolution #432 #438]: #531
-#436 := (not #531)
-#422 := (or #436 #535)
-#424 := [th-lemma]: #422
-#425 := [unit-resolution #424 #435]: #535
-#534 := (not #558)
-#540 := (or #534 #557 #555)
-#541 := [def-axiom]: #540
-#423 := [unit-resolution #541 #425 #434]: #555
-#408 := [symm #423]: #426
-#410 := [monotonicity #408]: #458
-#411 := (not #458)
-#412 := (or #411 #302)
-#413 := [th-lemma]: #412
-#414 := [unit-resolution #413 #410]: #302
-#461 := (>= #460 0::int)
-#415 := (or #411 #461)
-#416 := [th-lemma]: #415
-#417 := [unit-resolution #416 #410]: #461
-#512 := (>= #335 4::int)
-#418 := (or #431 #512)
-#419 := [th-lemma]: #418
-#420 := [unit-resolution #419 #438]: #512
+#462 := [unit-resolution #655 #700]: #324
+#441 := (not #324)
+#444 := (or #441 #554)
+#448 := [th-lemma]: #444
+#450 := [unit-resolution #448 #462]: #554
+#451 := (not #554)
+#449 := (or #451 #562)
+#452 := [th-lemma]: #449
+#440 := [unit-resolution #452 #450]: #562
+#561 := (not #580)
+#566 := (or #561 #579 #574)
+#567 := [def-axiom]: #566
+#443 := [unit-resolution #567 #440 #457]: #574
+#446 := [symm #443]: #445
+#442 := [monotonicity #446]: #486
+#447 := (not #486)
+#437 := (or #447 #464)
+#427 := [th-lemma]: #437
+#429 := [unit-resolution #427 #442]: #464
+#471 := (>= #463 0::int)
+#430 := (or #447 #471)
+#433 := [th-lemma]: #430
+#434 := [unit-resolution #433 #442]: #471
+#560 := (>= #335 4::int)
+#438 := (or #441 #560)
+#431 := [th-lemma]: #438
+#439 := [unit-resolution #431 #462]: #560
 #651 := (* -1::int #649)
 #648 := (+ #34 #651)
-#521 := (<= #648 0::int)
+#625 := (<= #648 0::int)
 #652 := (= #648 0::int)
-#630 := (>= #33 0::int)
-#421 := (not #461)
-#409 := (not #512)
-#398 := (or #630 #409 #421)
-#400 := [th-lemma]: #398
-#401 := [unit-resolution #400 #420 #417]: #630
-#468 := (not #630)
-#623 := (or #468 #652)
-#509 := (or #673 #468 #652)
+#643 := (>= #33 0::int)
+#435 := (not #471)
+#432 := (not #560)
+#436 := (or #643 #432 #435)
+#422 := [th-lemma]: #436
+#424 := [unit-resolution #422 #439 #434]: #643
+#644 := (not #643)
+#489 := (or #644 #652)
+#628 := (or #673 #644 #652)
 #370 := (>= #34 0::int)
 #371 := (not #370)
 #650 := (= #34 #649)
 #364 := (or #650 #371)
-#510 := (or #673 #364)
-#619 := (iff #510 #509)
-#470 := (or #673 #623)
-#615 := (iff #470 #509)
-#616 := [rewrite]: #615
-#618 := (iff #510 #470)
-#624 := (iff #364 #623)
-#643 := 1::int
-#638 := (* 1::int #33)
-#639 := (>= #638 0::int)
-#640 := (not #639)
-#632 := (or #640 #652)
-#625 := (iff #632 #623)
-#469 := (iff #640 #468)
-#637 := (iff #639 #630)
-#635 := (= #638 #33)
-#636 := [rewrite]: #635
-#466 := [monotonicity #636]: #637
-#622 := [monotonicity #466]: #469
-#626 := [monotonicity #622]: #625
-#628 := (iff #364 #632)
-#488 := (or #652 #640)
-#633 := (iff #488 #632)
-#634 := [rewrite]: #633
-#489 := (iff #364 #488)
-#646 := (iff #371 #640)
-#644 := (iff #370 #639)
-#645 := [rewrite]: #644
-#487 := [monotonicity #645]: #646
+#629 := (or #673 #364)
+#469 := (iff #629 #628)
+#636 := (or #673 #489)
+#466 := (iff #636 #628)
+#468 := [rewrite]: #466
+#630 := (iff #629 #636)
+#633 := (iff #364 #489)
+#646 := (or #652 #644)
+#631 := (iff #646 #489)
+#632 := [rewrite]: #631
+#487 := (iff #364 #646)
+#645 := (iff #371 #644)
+#638 := (iff #370 #643)
+#639 := [rewrite]: #638
+#640 := [monotonicity #639]: #645
 #641 := (iff #650 #652)
 #642 := [rewrite]: #641
-#631 := [monotonicity #642 #487]: #489
-#629 := [trans #631 #634]: #628
-#627 := [trans #629 #626]: #624
-#520 := [monotonicity #627]: #618
-#504 := [trans #520 #616]: #619
-#511 := [quant-inst]: #510
-#519 := [mp #511 #504]: #509
-#402 := [unit-resolution #519 #700]: #623
-#403 := [unit-resolution #402 #401]: #652
-#404 := (not #652)
-#405 := (or #404 #521)
-#406 := [th-lemma]: #405
-#399 := [unit-resolution #406 #403]: #521
-#522 := (>= #648 0::int)
-#407 := (or #404 #522)
-#392 := [th-lemma]: #407
-#393 := [unit-resolution #392 #403]: #522
-#396 := [th-lemma #393 #399 #420 #435 #417 #414]: #394
-#397 := [monotonicity #396]: #395
-#391 := [monotonicity #397]: #381
-#550 := (= #36 #545)
-#559 := (= #35 #36)
-#530 := (>= #649 10::int)
-#476 := (ite #530 #550 #559)
-#536 := (or #336 #476)
-#537 := [quant-inst]: #536
-#386 := [unit-resolution #537 #713]: #476
-#387 := (not #521)
-#388 := (or #530 #387 #409 #421)
-#380 := [th-lemma]: #388
-#389 := [unit-resolution #380 #399 #420 #417]: #530
-#538 := (not #530)
-#532 := (not #476)
-#506 := (or #532 #538 #550)
-#513 := [def-axiom]: #506
-#390 := [unit-resolution #513 #389 #386]: #550
-#365 := [trans #390 #391]: #374
-#375 := [trans #365 #373]: #39
+#488 := [monotonicity #642 #640]: #487
+#634 := [trans #488 #632]: #633
+#637 := [monotonicity #634]: #630
+#622 := [trans #637 #468]: #469
+#635 := [quant-inst]: #629
+#623 := [mp #635 #622]: #628
+#425 := [unit-resolution #623 #700]: #489
+#423 := [unit-resolution #425 #424]: #652
+#426 := (not #652)
+#408 := (or #426 #625)
+#410 := [th-lemma]: #408
+#411 := [unit-resolution #410 #423]: #625
+#626 := (>= #648 0::int)
+#412 := (or #426 #626)
+#413 := [th-lemma]: #412
+#414 := [unit-resolution #413 #423]: #626
+#416 := [th-lemma #414 #411 #439 #450 #434 #429]: #415
+#418 := [monotonicity #416]: #417
+#402 := [monotonicity #418]: #401
+#557 := (= #36 #556)
+#581 := (= #35 #36)
+#558 := (>= #649 10::int)
+#559 := (ite #558 #557 #581)
+#533 := (or #336 #559)
+#534 := [quant-inst]: #533
+#419 := [unit-resolution #534 #713]: #559
+#420 := (not #625)
+#409 := (or #558 #420 #432 #435)
+#421 := [th-lemma]: #409
+#398 := [unit-resolution #421 #411 #439 #434]: #558
+#428 := (not #558)
+#535 := (not #559)
+#539 := (or #535 #428 #557)
+#540 := [def-axiom]: #539
+#400 := [unit-resolution #540 #398 #419]: #557
+#406 := [trans #400 #402]: #405
+#399 := [trans #406 #404]: #39
 #40 := (not #39)
 #182 := [asserted]: #40
-[unit-resolution #182 #375]: false
-unsat
-
-/fwo5o8vhLVHyS4oYEs4QA 10902
+[unit-resolution #182 #399]: false
+unsat
+K2SXMHU6QCZJ8TRs6zjKRg 408 0
 #2 := false
 #22 := 0::int
 #8 := 2::int
@@ -12913,18 +12581,18 @@
 #604 := [trans #593 #597]: #562
 #603 := [quant-inst]: #596
 #606 := [mp #603 #604]: #628
-#516 := [unit-resolution #606 #817]: #566
-#498 := (not #566)
-#432 := (or #498 #608)
-#411 := [th-lemma]: #432
-#413 := [unit-resolution #411 #516]: #608
+#528 := [unit-resolution #606 #817]: #566
+#521 := (not #566)
+#464 := (or #521 #608)
+#456 := [th-lemma]: #464
+#465 := [unit-resolution #456 #528]: #608
 decl uf_10 :: int
 #52 := uf_10
 #57 := (mod uf_10 2::int)
 #243 := (* -1::int #57)
 #244 := (+ #56 #243)
 #447 := (>= #244 0::int)
-#372 := (not #447)
+#387 := (not #447)
 #245 := (= #244 0::int)
 #248 := (not #245)
 #218 := (* -1::int #55)
@@ -12944,9 +12612,9 @@
 #662 := (not #672)
 #1 := true
 #81 := [true-axiom]: true
-#514 := (or false #662)
-#515 := [th-lemma]: #514
-#513 := [unit-resolution #515 #81]: #662
+#520 := (or false #662)
+#523 := [th-lemma]: #520
+#524 := [unit-resolution #523 #81]: #662
 #701 := (* -1::int #613)
 #204 := -2::int
 #691 := (* -2::int #222)
@@ -12959,58 +12627,82 @@
 #546 := [th-lemma]: #545
 #548 := [unit-resolution #546 #81]: #692
 #549 := (not #692)
-#482 := (or #549 #694)
-#483 := [th-lemma]: #482
-#484 := [unit-resolution #483 #548]: #694
+#497 := (or #549 #694)
+#482 := [th-lemma]: #497
+#483 := [unit-resolution #482 #548]: #694
 #536 := (not #448)
-#382 := [hypothesis]: #536
+#395 := [hypothesis]: #536
 #555 := (* -1::int uf_10)
 #573 := (+ #51 #555)
 #543 := (<= #573 0::int)
 #53 := (= #51 uf_10)
 #256 := (not #253)
 #259 := (or #248 #256)
+#502 := 1::int
 #731 := (div uf_10 2::int)
-#723 := (* -2::int #731)
-#521 := (* -2::int #624)
-#529 := (+ #521 #723)
+#515 := (* -1::int #731)
+#513 := (+ #640 #515)
 #618 := (div #51 2::int)
-#583 := (* -2::int #618)
-#522 := (+ #583 #529)
-#528 := (* -2::int #57)
-#525 := (+ #528 #522)
-#524 := (* 2::int #56)
-#526 := (+ #524 #525)
-#523 := (* 2::int uf_10)
-#512 := (+ #523 #526)
-#520 := (>= #512 2::int)
+#514 := (* -1::int #618)
+#516 := (+ #514 #513)
+#498 := (+ #243 #516)
+#500 := (+ #56 #498)
+#501 := (+ uf_10 #500)
+#503 := (>= #501 1::int)
+#486 := (not #503)
+#361 := (<= #244 0::int)
 #453 := (not #259)
-#519 := [hypothesis]: #453
+#517 := [hypothesis]: #453
 #440 := (or #259 #245)
 #451 := [def-axiom]: #440
-#470 := [unit-resolution #451 #519]: #245
-#465 := (or #248 #447)
-#466 := [th-lemma]: #465
-#457 := [unit-resolution #466 #470]: #447
-#544 := (>= #573 0::int)
-#441 := (not #544)
+#519 := [unit-resolution #451 #517]: #245
+#478 := (or #248 #361)
+#470 := [th-lemma]: #478
+#479 := [unit-resolution #470 #519]: #361
+#449 := (>= #252 0::int)
 #452 := (or #259 #253)
 #380 := [def-axiom]: #452
-#481 := [unit-resolution #380 #519]: #253
-#467 := (or #256 #448)
-#434 := [th-lemma]: #467
-#436 := [unit-resolution #434 #481]: #448
-#532 := (or #543 #536)
-#695 := (>= #699 0::int)
-#550 := (or #549 #695)
-#393 := [th-lemma]: #550
-#551 := [unit-resolution #393 #548]: #695
-#547 := (not #543)
-#552 := [hypothesis]: #547
+#480 := [unit-resolution #380 #517]: #253
+#471 := (or #256 #449)
+#481 := [th-lemma]: #471
+#462 := [unit-resolution #481 #480]: #449
+#487 := (not #361)
+#485 := (not #449)
+#476 := (or #486 #485 #487)
+#607 := (<= #620 0::int)
+#529 := (or #521 #607)
+#522 := [th-lemma]: #529
+#525 := [unit-resolution #522 #528]: #607
+#723 := (* -2::int #731)
+#724 := (+ #243 #723)
+#718 := (+ uf_10 #724)
+#720 := (<= #718 0::int)
+#722 := (= #718 0::int)
+#526 := (or false #722)
+#512 := [th-lemma]: #526
+#504 := [unit-resolution #512 #81]: #722
+#505 := (not #722)
+#506 := (or #505 #720)
+#507 := [th-lemma]: #506
+#508 := [unit-resolution #507 #504]: #720
+#509 := [hypothesis]: #361
+#583 := (* -2::int #618)
+#584 := (+ #583 #640)
+#585 := (+ #51 #584)
+#587 := (<= #585 0::int)
+#582 := (= #585 0::int)
+#510 := (or false #582)
+#499 := [th-lemma]: #510
+#511 := [unit-resolution #499 #81]: #582
+#488 := (not #582)
+#490 := (or #488 #587)
+#491 := [th-lemma]: #490
+#492 := [unit-resolution #491 #511]: #587
+#493 := [hypothesis]: #503
 #649 := (* -2::int #60)
 #644 := (+ #218 #649)
 #650 := (+ #51 #644)
-#631 := (<= #650 0::int)
+#636 := (>= #650 0::int)
 #623 := (= #650 0::int)
 #43 := (uf_7 uf_2 #35)
 #44 := (uf_6 #34 #43)
@@ -13071,6 +12763,33 @@
 #630 := [quant-inst]: #629
 #531 := [unit-resolution #630 #824]: #623
 #534 := (not #623)
+#494 := (or #534 #636)
+#495 := [th-lemma]: #494
+#496 := [unit-resolution #495 #531]: #636
+#489 := [hypothesis]: #449
+#484 := [th-lemma #483 #489 #496 #493 #492 #509 #508 #525 #524]: false
+#477 := [lemma #484]: #476
+#463 := [unit-resolution #477 #462 #479]: #486
+#727 := (>= #718 0::int)
+#466 := (or #505 #727)
+#457 := [th-lemma]: #466
+#467 := [unit-resolution #457 #504]: #727
+#434 := (or #248 #447)
+#436 := [th-lemma]: #434
+#437 := [unit-resolution #436 #519]: #447
+#544 := (>= #573 0::int)
+#445 := (not #544)
+#428 := (or #256 #448)
+#441 := [th-lemma]: #428
+#442 := [unit-resolution #441 #480]: #448
+#532 := (or #543 #536)
+#695 := (>= #699 0::int)
+#550 := (or #549 #695)
+#393 := [th-lemma]: #550
+#551 := [unit-resolution #393 #548]: #695
+#547 := (not #543)
+#552 := [hypothesis]: #547
+#631 := (<= #650 0::int)
 #538 := (or #534 #631)
 #540 := [th-lemma]: #538
 #541 := [unit-resolution #540 #531]: #631
@@ -13081,8 +12800,8 @@
 #533 := [unit-resolution #530 #81]: #666
 #535 := [th-lemma #533 #539 #541 #552 #551]: false
 #537 := [lemma #535]: #532
-#437 := [unit-resolution #537 #436]: #543
-#444 := (or #547 #441)
+#443 := [unit-resolution #537 #442]: #543
+#429 := (or #547 #445)
 #764 := (not #53)
 #771 := (or #764 #259)
 #262 := (iff #53 #259)
@@ -13135,121 +12854,67 @@
 #438 := (or #764 #259 #433)
 #439 := [def-axiom]: #438
 #772 := [unit-resolution #439 #267]: #771
-#428 := [unit-resolution #772 #519]: #764
-#442 := (or #53 #547 #441)
-#443 := [th-lemma]: #442
-#445 := [unit-resolution #443 #428]: #444
-#435 := [unit-resolution #445 #437]: #441
-#584 := (+ #583 #640)
-#585 := (+ #51 #584)
+#444 := [unit-resolution #772 #517]: #764
+#435 := (or #53 #547 #445)
+#446 := [th-lemma]: #435
+#431 := [unit-resolution #446 #444]: #429
+#432 := [unit-resolution #431 #443]: #445
 #588 := (>= #585 0::int)
-#582 := (= #585 0::int)
-#499 := (or false #582)
-#511 := [th-lemma]: #499
-#488 := [unit-resolution #511 #81]: #582
-#490 := (not #582)
-#446 := (or #490 #588)
-#429 := [th-lemma]: #446
-#431 := [unit-resolution #429 #488]: #588
-#724 := (+ #243 #723)
-#718 := (+ uf_10 #724)
-#727 := (>= #718 0::int)
-#722 := (= #718 0::int)
-#503 := (or false #722)
-#504 := [th-lemma]: #503
-#505 := [unit-resolution #504 #81]: #722
-#506 := (not #722)
-#418 := (or #506 #727)
-#419 := [th-lemma]: #418
-#420 := [unit-resolution #419 #505]: #727
-#421 := [th-lemma #420 #413 #431 #435 #457]: #520
-#485 := (not #520)
-#361 := (<= #244 0::int)
-#479 := (or #248 #361)
-#480 := [th-lemma]: #479
-#471 := [unit-resolution #480 #470]: #361
-#449 := (>= #252 0::int)
-#462 := (or #256 #449)
-#463 := [th-lemma]: #462
-#464 := [unit-resolution #463 #481]: #449
-#476 := (not #361)
-#487 := (not #449)
-#477 := (or #485 #487 #476)
-#607 := (<= #620 0::int)
-#500 := (or #498 #607)
-#501 := [th-lemma]: #500
-#502 := [unit-resolution #501 #516]: #607
-#720 := (<= #718 0::int)
-#507 := (or #506 #720)
-#508 := [th-lemma]: #507
-#509 := [unit-resolution #508 #505]: #720
-#510 := [hypothesis]: #361
-#587 := (<= #585 0::int)
-#491 := (or #490 #587)
-#492 := [th-lemma]: #491
-#493 := [unit-resolution #492 #488]: #587
-#494 := [hypothesis]: #520
-#636 := (>= #650 0::int)
-#495 := (or #534 #636)
-#496 := [th-lemma]: #495
-#489 := [unit-resolution #496 #531]: #636
-#497 := [hypothesis]: #449
-#486 := [th-lemma #484 #497 #489 #494 #493 #510 #509 #502 #513]: false
-#478 := [lemma #486]: #477
-#456 := [unit-resolution #478 #464 #471]: #485
-#422 := [unit-resolution #456 #421]: false
-#423 := [lemma #422]: #259
+#411 := (or #488 #588)
+#413 := [th-lemma]: #411
+#418 := [unit-resolution #413 #511]: #588
+#419 := [th-lemma #418 #432 #437 #467 #465 #463]: false
+#420 := [lemma #419]: #259
 #427 := (or #53 #453)
 #768 := (or #53 #453 #433)
 #770 := [def-axiom]: #768
 #557 := [unit-resolution #770 #267]: #427
-#399 := [unit-resolution #557 #423]: #53
-#385 := (or #764 #543)
-#386 := [th-lemma]: #385
-#387 := [unit-resolution #386 #399]: #543
-#379 := [th-lemma #489 #387 #382 #484 #513]: false
-#388 := [lemma #379]: #448
-#381 := (or #253 #536)
-#397 := [hypothesis]: #487
-#400 := (or #764 #544)
-#403 := [th-lemma]: #400
-#398 := [unit-resolution #403 #399]: #544
-#404 := [th-lemma #398 #397 #533 #551 #541]: false
-#378 := [lemma #404]: #449
-#395 := (or #253 #536 #487)
-#377 := [th-lemma]: #395
-#658 := [unit-resolution #377 #378]: #381
-#653 := [unit-resolution #658 #388]: #253
+#406 := [unit-resolution #557 #420]: #53
+#377 := (or #764 #543)
+#381 := [th-lemma]: #377
+#382 := [unit-resolution #381 #406]: #543
+#385 := [th-lemma #496 #382 #395 #483 #524]: false
+#386 := [lemma #385]: #448
+#390 := (or #253 #536)
+#408 := [hypothesis]: #485
+#409 := (or #764 #544)
+#397 := [th-lemma]: #409
+#399 := [unit-resolution #397 #406]: #544
+#400 := [th-lemma #399 #408 #533 #551 #541]: false
+#403 := [lemma #400]: #449
+#392 := (or #253 #536 #485)
+#394 := [th-lemma]: #392
+#657 := [unit-resolution #394 #403]: #390
+#658 := [unit-resolution #657 #386]: #253
 #450 := (or #453 #248 #256)
 #454 := [def-axiom]: #450
-#664 := [unit-resolution #454 #423]: #259
-#665 := [unit-resolution #664 #653]: #248
-#373 := (or #245 #372)
-#708 := (+ #57 #640)
-#705 := (>= #708 0::int)
-#560 := (= #57 #624)
-#408 := (= #624 #57)
-#406 := [monotonicity #399]: #408
-#409 := [symm #406]: #560
-#706 := (not #560)
-#655 := (or #706 #705)
-#569 := [th-lemma]: #655
-#570 := [unit-resolution #569 #409]: #705
-#383 := [hypothesis]: #476
-#384 := [th-lemma #502 #383 #570]: false
-#389 := [lemma #384]: #361
-#369 := (or #245 #476 #372)
-#370 := [th-lemma]: #369
-#374 := [unit-resolution #370 #389]: #373
-#375 := [unit-resolution #374 #665]: #372
-#610 := (<= #708 0::int)
-#371 := (or #706 #610)
-#376 := [th-lemma]: #371
-#363 := [unit-resolution #376 #409]: #610
-[th-lemma #363 #375 #413]: false
-unsat
-
-s8LL71+1HTN+eIuEYeKhUw 1251
+#762 := [unit-resolution #454 #420]: #259
+#664 := [unit-resolution #762 #658]: #248
+#372 := (or #245 #387)
+#560 := (+ #57 #640)
+#610 := (>= #560 0::int)
+#742 := (= #57 #624)
+#424 := (= #624 #57)
+#405 := [monotonicity #406]: #424
+#407 := [symm #405]: #742
+#705 := (not #742)
+#706 := (or #705 #610)
+#568 := [th-lemma]: #706
+#569 := [unit-resolution #568 #407]: #610
+#398 := [hypothesis]: #487
+#404 := [th-lemma #525 #398 #569]: false
+#378 := [lemma #404]: #361
+#379 := (or #245 #487 #387)
+#388 := [th-lemma]: #379
+#369 := [unit-resolution #388 #378]: #372
+#370 := [unit-resolution #369 #664]: #387
+#708 := (<= #560 0::int)
+#373 := (or #705 #708)
+#374 := [th-lemma]: #373
+#375 := [unit-resolution #374 #407]: #708
+[th-lemma #375 #370 #465]: false
+unsat
+1DhSL9G2fGRGmuI8IaMNOA 50 0
 #2 := false
 decl up_35 :: (-> int bool)
 #112 := 1::int
@@ -13300,8 +12965,7 @@
 #504 := [quant-inst]: #503
 [unit-resolution #504 #916 #297]: false
 unsat
-
-MZYsU5krlrOK4MkB71Ikeg 12985
+dyXROdcPFSd36N3K7dpmDw 506 0
 #2 := false
 decl uf_17 :: (-> T8 T3)
 decl uf_18 :: (-> T1 T8)
@@ -13808,4 +13472,3 @@
 #325 := [asserted]: #108
 [unit-resolution #325 #554]: false
 unsat
-
diff -r eee63670b5aa -r 3011b2149089 src/HOL/SMT/SMT_Base.thy
--- a/src/HOL/SMT/SMT_Base.thy	Tue Feb 16 20:41:52 2010 +0100
+++ b/src/HOL/SMT/SMT_Base.thy	Tue Feb 16 20:42:44 2010 +0100
@@ -8,6 +8,7 @@
 imports Real "~~/src/HOL/Word/Word"
   "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
 uses
+  "~~/src/Tools/Cache_IO/cache_io.ML"
   ("Tools/smt_normalize.ML")
   ("Tools/smt_monomorph.ML")
   ("Tools/smt_translate.ML")
diff -r eee63670b5aa -r 3011b2149089 src/HOL/SMT/Tools/smt_solver.ML
--- a/src/HOL/SMT/Tools/smt_solver.ML	Tue Feb 16 20:41:52 2010 +0100
+++ b/src/HOL/SMT/Tools/smt_solver.ML	Tue Feb 16 20:42:44 2010 +0100
@@ -20,7 +20,7 @@
   type solver_config = {
     command: {env_var: string, remote_name: string option},
     arguments: string list,
-    interface: interface,
+    interface: string list -> interface,
     reconstruct: proof_data -> thm }
 
   (*options*)
@@ -28,8 +28,10 @@
   val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
   val trace: bool Config.T
   val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
+
+  (*certificates*)
   val record: bool Config.T
-  val certificates: string Config.T
+  val select_certificates: string -> Context.generic -> Context.generic
 
   (*solvers*)
   type solver = Proof.context -> thm list -> thm
@@ -71,7 +73,7 @@
 type solver_config = {
   command: {env_var: string, remote_name: string option},
   arguments: string list,
-  interface: interface,
+  interface: string list -> interface,
   reconstruct: proof_data -> thm }
 
 
@@ -88,30 +90,29 @@
 fun trace_msg ctxt f x =
   if Config.get ctxt trace then tracing (f x) else ()
 
+
+(* SMT certificates *)
+
 val (record, setup_record) = Attrib.config_bool "smt_record" true
-val no_certificates = ""
-val (certificates, setup_certificates) =
-  Attrib.config_string "smt_certificates" no_certificates
 
+structure Certificates = Generic_Data
+(
+  type T = Cache_IO.cache option
+  val empty = NONE
+  val extend = I
+  fun merge (s, _) = s
+)
+
+fun select_certificates name = Certificates.put (
+  if name = "" then NONE
+  else SOME (Cache_IO.make (Path.explode name)))
 
 
 (* interface to external solvers *)
 
 local
 
-fun with_files ctxt f =
-  let
-    val paths as (problem_path, proof_path) =
-      "smt-" ^ serial_string ()
-      |> (fn n => (n, n ^ ".proof"))
-      |> pairself (File.tmp_path o Path.explode)
-
-    val y = Exn.capture f (problem_path, proof_path)
-
-    val _ = pairself (try File.rm) paths
-  in Exn.release y end
-
-fun invoke ctxt output f (paths as (problem_path, proof_path)) =
+fun invoke ctxt output f problem_path =
   let
     fun pretty tag ls = Pretty.string_of (Pretty.big_list tag
       (map Pretty.str ls))
@@ -120,11 +121,10 @@
     val _ = trace_msg ctxt (pretty "SMT problem:" o split_lines o File.read)
       problem_path
 
-    val (s, _) = with_timeout ctxt f paths
-    val _ = trace_msg ctxt (pretty "SMT solver:") (split_lines s)
+    val (res, err) = with_timeout ctxt f problem_path
+    val _ = trace_msg ctxt (pretty "SMT solver:") err
 
-    fun lines_of path = the_default [] (try (File.fold_lines cons path) [])
-    val ls = rev (dropwhile (equal "") (lines_of proof_path))
+    val ls = rev (dropwhile (equal "") (rev res))
     val _ = trace_msg ctxt (pretty "SMT result:") ls
   in (x, ls) end
 
@@ -135,47 +135,53 @@
     val remote_url = getenv "REMOTE_SMT_URL"
   in
     if local_solver <> ""
-    then (["local", local_solver],
-      "Invoking local SMT solver " ^ quote local_solver ^ " ...")
-    else if remote_solver <> "" andalso remote_url <> ""
-    then (["remote", remote_solver],
-      "Invoking remote SMT solver " ^ quote remote_solver ^ " at " ^
-      quote remote_url ^ " ...")
+    then 
+     (tracing ("Invoking local SMT solver " ^ quote local_solver ^ " ...");
+      [local_solver])
+    else if remote_solver <> ""
+    then
+     (tracing ("Invoking remote SMT solver " ^ quote remote_solver ^ " at " ^
+        quote remote_url ^ " ...");
+      [getenv "REMOTE_SMT", remote_solver])
     else error ("Undefined Isabelle environment variable: " ^ quote env_var)
   end
 
-fun run ctxt cmd args (problem_path, proof_path) =
-  let
-    val certs = Config.get ctxt certificates
-    val certs' = 
-      if certs = no_certificates then "-"
-      else File.shell_path (Path.explode certs)
-    val (solver, msg) =
-      if certs = no_certificates orelse Config.get ctxt record
-      then choose cmd
-      else (["certificate"], "Using certificate from " ^ quote certs' ^ " ...")
-    val _ = tracing msg
+fun make_cmd solver args problem_path proof_path = space_implode " " (
+  map File.shell_quote (solver @ args) @
+  [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path])
+
+fun no_cmd _ _ = error ("Bad certificates cache: missing certificate")
+
+fun run ctxt cmd args problem_path =
+  let val certs = Certificates.get (Context.Proof ctxt)
   in
-    bash_output (space_implode " " (
-      File.shell_path (Path.explode (getenv "RUN_SMT_SOLVER")) :: certs' ::
-      map File.shell_quote (solver @ args) @
-      map File.shell_path [problem_path, proof_path]) ^ " 2>&1")
+    if is_none certs 
+    then Cache_IO.run' (make_cmd (choose cmd) args) problem_path
+    else if Config.get ctxt record
+    then Cache_IO.cached' (the certs) (make_cmd (choose cmd) args) problem_path
+    else
+     (tracing ("Using cached certificate from " ^
+        File.shell_path (Cache_IO.cache_path_of (the certs)) ^ " ...");
+      Cache_IO.cached' (the certs) no_cmd problem_path)
   end
 
 in
 
 fun run_solver ctxt cmd args output =
-  with_files ctxt (invoke ctxt output (run ctxt cmd args))
+  Cache_IO.with_tmp_file "smt-" (invoke ctxt output (run ctxt cmd args))
 
 end
 
 fun make_proof_data ctxt ((recon, thms), ls) =
   {context=ctxt, output=ls, recon=recon, assms=SOME thms}
 
-fun gen_solver solver ctxt prems =
+fun gen_solver name solver ctxt prems =
   let
     val {command, arguments, interface, reconstruct} = solver ctxt
-    val {normalize=nc, translate=tc} = interface
+    val comments = ("solver: " ^ name) ::
+      ("timeout: " ^ string_of_int (Config.get ctxt timeout)) ::
+      "arguments:" :: arguments
+    val {normalize=nc, translate=tc} = interface comments
     val thy = ProofContext.theory_of ctxt
   in
     SMT_Normalize.normalize nc ctxt prems
@@ -218,17 +224,19 @@
 
 val solver_name_of = Selected_Solver.get
 
-fun select_solver name gen =
-  if is_none (lookup_solver (Context.theory_of gen) name)
+fun select_solver name context =
+  if is_none (lookup_solver (Context.theory_of context) name)
   then error ("SMT solver not registered: " ^ quote name)
-  else Selected_Solver.map (K name) gen
+  else Selected_Solver.map (K name) context
 
-fun raw_solver_of gen =
-  (case lookup_solver (Context.theory_of gen) (solver_name_of gen) of
+fun raw_solver_of context name =
+  (case lookup_solver (Context.theory_of context) name of
     NONE => error "No SMT solver selected"
   | SOME (s, _) => s)
 
-val solver_of = gen_solver o raw_solver_of
+fun solver_of context =
+  let val name = solver_name_of context
+  in gen_solver name (raw_solver_of context name) end
 
 
 (* SMT tactic *)
@@ -278,7 +286,10 @@
   setup_timeout #>
   setup_trace #>
   setup_record #>
-  setup_certificates #>
+  Attrib.setup (Binding.name "smt_certificates")
+    (Scan.lift (OuterParse.$$$ "=" |-- Args.name) >>
+      (Thm.declaration_attribute o K o select_certificates))
+    "SMT certificates" #>
   Method.setup (Binding.name "smt") smt_method
     "Applies an SMT solver to the current goal."
 
diff -r eee63670b5aa -r 3011b2149089 src/HOL/SMT/Tools/smtlib_interface.ML
--- a/src/HOL/SMT/Tools/smtlib_interface.ML	Tue Feb 16 20:41:52 2010 +0100
+++ b/src/HOL/SMT/Tools/smtlib_interface.ML	Tue Feb 16 20:42:44 2010 +0100
@@ -8,9 +8,9 @@
 sig
   val basic_builtins: SMT_Translate.builtins
   val default_attributes: string list
-  val gen_interface: SMT_Translate.builtins -> string list ->
+  val gen_interface: SMT_Translate.builtins -> string list -> string list ->
     SMT_Solver.interface
-  val interface: SMT_Solver.interface
+  val interface: string list -> SMT_Solver.interface
 end
 
 structure SMTLIB_Interface: SMTLIB_INTERFACE =
@@ -118,12 +118,13 @@
           | wr_pat (T.SNoPat ts) = wrp "nopat" ts
       in par (wr_quant q #> fold wr_var vs #> wre b #> fold wr_pat ps) end)
 
-fun serialize attributes ({typs, funs, preds} : T.sign) ts stream =
+fun serialize attributes comments ({typs, funs, preds} : T.sign) ts stream =
   let
     fun wr_decl (n, Ts) = wr_line (sep (par (wr n #> fold wr1 Ts)))
   in
     stream
     |> wr_line (wr "(benchmark Isabelle")
+    |> wr_line (wr ":status unknown")
     |> fold (wr_line o wr) attributes
     |> length typs > 0 ?
          wr_line (wr ":extrasorts" #> par (fold wr1 typs))
@@ -138,6 +139,7 @@
     |> fold (fn t => wr ":assumption" #> wr_line (wr_expr false [] t)) ts
     |> wr_line (wr ":formula true")
     |> wr_line (wr ")")
+    |> fold (fn comment => wr_line (wr ("; " ^ comment))) comments
     |> K ()
   end
 
@@ -149,9 +151,9 @@
   builtin_num = builtin_num,
   builtin_fun = (fn true => builtin_funcs | false => builtin_preds) }
 
-val default_attributes = [":logic AUFLIRA", ":status unknown"]
+val default_attributes = [":logic AUFLIRA"]
 
-fun gen_interface builtins attributes = {
+fun gen_interface builtins attributes comments = {
   normalize = [
     SMT_Normalize.RewriteTrivialLets,
     SMT_Normalize.RewriteNegativeNumerals,
@@ -170,8 +172,9 @@
       term_marker = term_marker,
       formula_marker = formula_marker },
     builtins = builtins,
-    serialize = serialize attributes }}
+    serialize = serialize attributes comments }}
 
-val interface = gen_interface basic_builtins default_attributes
+fun interface comments =
+  gen_interface basic_builtins default_attributes comments
 
 end
diff -r eee63670b5aa -r 3011b2149089 src/HOL/SMT/Tools/z3_interface.ML
--- a/src/HOL/SMT/Tools/z3_interface.ML	Tue Feb 16 20:41:52 2010 +0100
+++ b/src/HOL/SMT/Tools/z3_interface.ML	Tue Feb 16 20:42:44 2010 +0100
@@ -6,7 +6,7 @@
 
 signature Z3_INTERFACE =
 sig
-  val interface: SMT_Solver.interface
+  val interface: string list -> SMT_Solver.interface
 end
 
 structure Z3_Interface: Z3_INTERFACE =
diff -r eee63670b5aa -r 3011b2149089 src/HOL/SMT/lib/scripts/run_smt_solver
--- a/src/HOL/SMT/lib/scripts/run_smt_solver	Tue Feb 16 20:41:52 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,93 +0,0 @@
-#!/usr/bin/env perl
-#
-# Author: Sascha Boehme, TU Muenchen
-#
-# Cache for prover results, based on discriminating problems using MD5.
-
-use strict;
-use warnings;
-use Digest::MD5;
-
-
-# arguments
-
-my $certs_file = shift @ARGV;
-my $location = shift @ARGV;
-my $result_file = pop @ARGV;
-my $problem_file = $ARGV[-1];
-
-my $use_certs = not ($certs_file eq "-");
-
-
-# create MD5 problem digest
-
-my $problem_digest = "";
-if ($use_certs) {
-  my $md5 = Digest::MD5->new;
-  open FILE, "<$problem_file" or
-    die "ERROR: Failed to open '$problem_file' ($!)";
-  $md5->addfile(*FILE);
-  close FILE;
-  $problem_digest = $md5->b64digest;
-}
-
-
-# lookup problem digest among existing certificates and
-# return a cached result (if there is a certificate for the problem)
-
-if ($use_certs and -e $certs_file) {
-  my $cached = 0;
-  open CERTS, "<$certs_file" or die "ERROR: Failed to open '$certs_file' ($!)";
-  while (<CERTS>) {
-    if (m/(\S+) (\d+)/) {
-      if ($1 eq $problem_digest) {
-        my $start = tell CERTS;
-        open FILE, ">$result_file" or
-          die "ERROR: Failed to open '$result_file ($!)";
-        while ((tell CERTS) - $start < $2) {
-          my $line = <CERTS>;
-          print FILE $line;
-        }
-        close FILE;
-        $cached = 1;
-        last;
-      }
-      else { seek CERTS, $2, 1; }
-    }
-    else { die "ERROR: Invalid file format in '$certs_file'"; }
-  }
-  close CERTS;
-  if ($cached) { exit 0; }
-}
-
-
-# invoke (remote or local) prover
-
-my $result;
-
-if ($location eq "remote") {
-  $result = system "$ENV{'REMOTE_SMT'} @ARGV >$result_file 2>&1";
-}
-elsif ($location eq "local") {
-  $result = system "@ARGV >$result_file 2>&1";
-}
-else { die "ERROR: No SMT solver invoked"; }
-
-
-# cache result
-
-if ($use_certs) {
-  open CERTS, ">>$certs_file" or
-    die "ERROR: Failed to open '$certs_file' ($!)";
-  print CERTS
-    ("$problem_digest " . ((-s $result_file) + (length "\n")) . "\n");
-
-  open FILE, "<$result_file" or
-    die "ERROR: Failed to open '$result_file' ($!)";
-  foreach (<FILE>) { print CERTS $_; }
-  close FILE; 
-
-  print CERTS "\n";
-  close CERTS;
-}
-
diff -r eee63670b5aa -r 3011b2149089 src/Tools/Cache_IO/cache_io.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Cache_IO/cache_io.ML	Tue Feb 16 20:42:44 2010 +0100
@@ -0,0 +1,121 @@
+(*  Title:      Tools/Cache_IO/cache_io.ML
+    Author:     Sascha Boehme, TU Muenchen
+
+Cache for output of external processes.
+*)
+
+signature CACHE_IO =
+sig
+  val with_tmp_file: string -> (Path.T -> 'a) -> 'a
+  val run: (Path.T -> string) -> Path.T -> string list
+  val run': (Path.T -> Path.T -> string) -> Path.T -> string list * string list
+
+  type cache
+  val make: Path.T -> cache
+  val cache_path_of: cache -> Path.T
+  val cached: cache -> (Path.T -> string) -> Path.T -> string list
+  val cached': cache -> (Path.T -> Path.T -> string) -> Path.T ->
+    string list * string list
+end
+
+structure Cache_IO : CACHE_IO =
+struct
+
+fun with_tmp_file name f =
+  let
+    val path = File.tmp_path (Path.explode (name ^ serial_string ()))
+    val x = Exn.capture f path
+    val _ = try File.rm path
+  in Exn.release x end
+
+fun run' make_cmd in_path =
+  with_tmp_file "cache-io-" (fn out_path =>
+    let
+      val (out2, _) = bash_output (make_cmd in_path out_path)
+      val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
+    in (out1, split_lines out2) end)
+
+fun run make_cmd = snd o run' (fn in_path => fn _ => make_cmd in_path)
+
+
+
+abstype cache = Cache of {
+  path: Path.T,
+  table: (int * (int * int * int) Symtab.table) Synchronized.var }
+with
+
+
+fun cache_path_of (Cache {path, ...}) = path
+
+
+fun load cache_path =
+  let
+    fun err () = error ("Cache IO: corrupted cache file: " ^
+      File.shell_path cache_path)
+
+    fun int_of_string s =
+      (case read_int (explode s) of
+        (i, []) => i
+      | _ => err ())    
+
+    fun split line =
+      (case space_explode " " line of
+        [key, len1, len2] => (key, int_of_string len1, int_of_string len2)
+      | _ => err ())
+
+    fun parse line ((i, l), tab) =
+      if i = l
+      then
+        let val (key, l1, l2) = split line
+        in ((i+1, l+l1+l2+1), Symtab.update (key, (i+1, l1, l2)) tab) end
+      else ((i+1, l), tab)
+  in apfst fst (File.fold_lines parse cache_path ((1, 1), Symtab.empty)) end 
+
+fun make path =
+  let val table = if File.exists path then load path else (1, Symtab.empty)
+  in Cache {path=path, table=Synchronized.var (Path.implode path) table} end
+
+
+fun get_hash_key path =
+  let
+    val arg = File.shell_path path
+    val (out, res) = bash_output (getenv "COMPUTE_HASH_KEY" ^ " " ^ arg)
+  in
+    if res = 0 then hd (split_lines out)
+    else error ("Cache IO: failed to generate hash key for file " ^ arg)
+  end
+
+fun load_cached_result cache_path (p, len1, len2) =
+  let
+    fun load line (i, xsp) =
+      if i < p then (i+1, xsp)
+      else if i < p + len1 then (i+1, apfst (cons line) xsp)
+      else if i < p + len2 then (i+1, apsnd (cons line) xsp)
+      else (i, xsp)
+  in pairself rev (snd (File.fold_lines load cache_path (1, ([], [])))) end
+
+fun cached' (Cache {path=cache_path, table}) make_cmd in_path =
+  let val key = get_hash_key in_path
+  in
+    (case Symtab.lookup (snd (Synchronized.value table)) key of
+      SOME pos => load_cached_result cache_path pos
+    | NONE =>
+        let
+          val res as (out, err) = run' make_cmd in_path
+          val (l1, l2) = pairself length res
+          val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2
+          val lines = map (suffix "\n") (header :: out @ err)
+
+          val _ = Synchronized.change table (fn (p, tab) =>
+            if Symtab.defined tab key then (p, tab)
+            else
+              let val _ = File.append_list cache_path lines
+              in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end)
+        in res end)
+  end
+
+fun cached cache make_cmd =
+  snd o cached' cache (fn in_path => fn _ => make_cmd in_path)
+
+end
+end
diff -r eee63670b5aa -r 3011b2149089 src/Tools/Cache_IO/etc/settings
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Cache_IO/etc/settings	Tue Feb 16 20:42:44 2010 +0100
@@ -0,0 +1,4 @@
+ISABELLE_CACHE_IO="$COMPONENT"
+
+COMPUTE_HASH_KEY="$ISABELLE_CACHE_IO/lib/scripts/compute_hash_key"
+
diff -r eee63670b5aa -r 3011b2149089 src/Tools/Cache_IO/lib/scripts/compute_hash_key
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Cache_IO/lib/scripts/compute_hash_key	Tue Feb 16 20:42:44 2010 +0100
@@ -0,0 +1,24 @@
+#!/usr/bin/env perl
+#
+# Author: Sascha Boehme, TU Muenchen
+#
+# Compute MD5 hash key.
+
+use strict;
+use warnings;
+use Digest::MD5;
+
+
+# argument
+
+my $file = $ARGV[0];
+
+
+# compute MD5 hash key
+
+my $md5 = Digest::MD5->new;
+open FILE, "<$file" or die "ERROR: Failed to open '$file' ($!)";
+$md5->addfile(*FILE);
+close FILE;
+print $md5->b64digest . "\n";
+