src/HOL/SMT/Examples/cert/z3_linarith_11.proof

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_linarith_11.proof	Tue Oct 20 10:11:30 2009 +0200
@@ -0,0 +1,45 @@
+#2 := false
+#11 := 4::real
+decl uf_2 :: real
+#8 := uf_2
+#7 := 7::real
+#9 := (* 7::real uf_2)
+decl uf_1 :: real
+#5 := uf_1
+#4 := 3::real
+#6 := (* 3::real uf_1)
+#10 := (+ #6 #9)
+#41 := (>= #10 4::real)
+#39 := (not #41)
+#12 := (< #10 4::real)
+#40 := (iff #12 #39)
+#37 := [rewrite]: #40
+#34 := [asserted]: #12
+#38 := [mp #34 #37]: #39
+#13 := 2::real
+#14 := (* 2::real uf_1)
+#43 := (<= #14 3::real)
+#44 := (not #43)
+#15 := (< 3::real #14)
+#45 := (iff #15 #44)
+#46 := [rewrite]: #45
+#35 := [asserted]: #15
+#47 := [mp #35 #46]: #44
+#16 := 0::real
+#51 := (>= uf_2 0::real)
+#17 := (< uf_2 0::real)
+#18 := (not #17)
+#58 := (iff #18 #51)
+#49 := (not #51)
+#53 := (not #49)
+#56 := (iff #53 #51)
+#57 := [rewrite]: #56
+#54 := (iff #18 #53)
+#50 := (iff #17 #49)
+#52 := [rewrite]: #50
+#55 := [monotonicity #52]: #54
+#59 := [trans #55 #57]: #58
+#36 := [asserted]: #18
+#60 := [mp #36 #59]: #51
+[th-lemma #60 #47 #38]: false
+unsat