--- a/src/HOL/SMT/Examples/cert/z3_linarith_04.proof Tue Feb 02 18:11:21 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-#2 := false
-decl uf_1 :: int
-#4 := uf_1
-decl uf_3 :: int
-#6 := uf_3
-#9 := (+ uf_3 uf_1)
-decl uf_2 :: int
-#5 := uf_2
-#10 := (+ uf_2 #9)
-#7 := (+ uf_2 uf_3)
-#8 := (+ uf_1 #7)
-#11 := (= #8 #10)
-#12 := (not #11)
-#51 := (iff #12 false)
-#1 := true
-#46 := (not true)
-#49 := (iff #46 false)
-#50 := [rewrite]: #49
-#47 := (iff #12 #46)
-#44 := (iff #11 true)
-#39 := (= #8 #8)
-#42 := (iff #39 true)
-#43 := [rewrite]: #42
-#40 := (iff #11 #39)
-#37 := (= #10 #8)
-#29 := (+ uf_1 uf_3)
-#32 := (+ uf_2 #29)
-#35 := (= #32 #8)
-#36 := [rewrite]: #35
-#33 := (= #10 #32)
-#30 := (= #9 #29)
-#31 := [rewrite]: #30
-#34 := [monotonicity #31]: #33
-#38 := [trans #34 #36]: #37
-#41 := [monotonicity #38]: #40
-#45 := [trans #41 #43]: #44
-#48 := [monotonicity #45]: #47
-#52 := [trans #48 #50]: #51
-#28 := [asserted]: #12
-[mp #28 #52]: false
-unsat