--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_linarith_18.proof Thu Nov 05 15:24:49 2009 +0100
@@ -0,0 +1,52 @@
+#2 := false
+#55 := 0::int
+#7 := 2::int
+decl uf_1 :: int
+#4 := uf_1
+#8 := (mod uf_1 2::int)
+#9 := (* 2::int #8)
+#56 := (>= #9 0::int)
+#51 := (not #56)
+#5 := 1::int
+#10 := (+ #9 1::int)
+#11 := (+ uf_1 #10)
+#6 := (+ uf_1 1::int)
+#12 := (<= #6 #11)
+#13 := (not #12)
+#58 := (iff #13 #51)
+#39 := (+ uf_1 #9)
+#40 := (+ 1::int #39)
+#30 := (+ 1::int uf_1)
+#45 := (<= #30 #40)
+#48 := (not #45)
+#52 := (iff #48 #51)
+#53 := (iff #45 #56)
+#54 := [rewrite]: #53
+#57 := [monotonicity #54]: #52
+#49 := (iff #13 #48)
+#46 := (iff #12 #45)
+#43 := (= #11 #40)
+#33 := (+ 1::int #9)
+#36 := (+ uf_1 #33)
+#41 := (= #36 #40)
+#42 := [rewrite]: #41
+#37 := (= #11 #36)
+#34 := (= #10 #33)
+#35 := [rewrite]: #34
+#38 := [monotonicity #35]: #37
+#44 := [trans #38 #42]: #43
+#31 := (= #6 #30)
+#32 := [rewrite]: #31
+#47 := [monotonicity #32 #44]: #46
+#50 := [monotonicity #47]: #49
+#59 := [trans #50 #57]: #58
+#29 := [asserted]: #13
+#60 := [mp #29 #59]: #51
+#107 := (>= #8 0::int)
+#1 := true
+#28 := [true-axiom]: true
+#135 := (or false #107)
+#136 := [th-lemma]: #135
+#137 := [unit-resolution #136 #28]: #107
+[th-lemma #137 #60]: false
+unsat