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

+#2 := false
+#9 := 1::int
+decl uf_1 :: int
+#5 := uf_1
+#10 := (< uf_1 1::int)
+#6 := 3::int
+#7 := (+ uf_1 3::int)
+#4 := 4::int
+#8 := (<= 4::int #7)
+#11 := (or #8 #10)
+#12 := (not #11)
+#66 := (iff #12 false)
+#29 := (+ 3::int uf_1)
+#32 := (<= 4::int #29)
+#38 := (or #10 #32)
+#43 := (not #38)
+#64 := (iff #43 false)
+#1 := true
+#59 := (not true)
+#62 := (iff #59 false)
+#63 := [rewrite]: #62
+#60 := (iff #43 #59)
+#57 := (iff #38 true)
+#48 := (>= uf_1 1::int)
+#46 := (not #48)
+#52 := (or #46 #48)
+#55 := (iff #52 true)
+#56 := [rewrite]: #55
+#53 := (iff #38 #52)
+#50 := (iff #32 #48)
+#51 := [rewrite]: #50
+#47 := (iff #10 #46)
+#49 := [rewrite]: #47
+#54 := [monotonicity #49 #51]: #53
+#58 := [trans #54 #56]: #57
+#61 := [monotonicity #58]: #60
+#65 := [trans #61 #63]: #64
+#44 := (iff #12 #43)
+#41 := (iff #11 #38)
+#35 := (or #32 #10)
+#39 := (iff #35 #38)
+#40 := [rewrite]: #39
+#36 := (iff #11 #35)
+#33 := (iff #8 #32)
+#30 := (= #7 #29)
+#31 := [rewrite]: #30
+#34 := [monotonicity #31]: #33
+#37 := [monotonicity #34]: #36
+#42 := [trans #37 #40]: #41
+#45 := [monotonicity #42]: #44
+#67 := [trans #45 #65]: #66
+#28 := [asserted]: #12
+[mp #28 #67]: false
+unsat