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

+#2 := false
+#16 := (not false)
+decl uf_2 :: int
+#8 := uf_2
+#4 := 0::int
+#12 := (<= 0::int uf_2)
+#13 := (not #12)
+#14 := (or #13 #12)
+#6 := 1::int
+#7 := (- 1::int)
+#9 := (* #7 uf_2)
+decl uf_1 :: int
+#5 := uf_1
+#10 := (+ uf_1 #9)
+#11 := (<= 0::int #10)
+#15 := (or #11 #14)
+#17 := (iff #15 #16)
+#18 := (not #17)
+#70 := (iff #18 false)
+#1 := true
+#65 := (not true)
+#68 := (iff #65 false)
+#69 := [rewrite]: #68
+#66 := (iff #18 #65)
+#63 := (iff #17 true)
+#58 := (iff true true)
+#61 := (iff #58 true)
+#62 := [rewrite]: #61
+#59 := (iff #17 #58)
+#56 := (iff #16 true)
+#57 := [rewrite]: #56
+#54 := (iff #15 true)
+#35 := -1::int
+#38 := (* -1::int uf_2)
+#41 := (+ uf_1 #38)
+#44 := (<= 0::int #41)
+#49 := (or #44 true)
+#52 := (iff #49 true)
+#53 := [rewrite]: #52
+#50 := (iff #15 #49)
+#47 := (iff #14 true)
+#48 := [rewrite]: #47
+#45 := (iff #11 #44)
+#42 := (= #10 #41)
+#39 := (= #9 #38)
+#36 := (= #7 -1::int)
+#37 := [rewrite]: #36
+#40 := [monotonicity #37]: #39
+#43 := [monotonicity #40]: #42
+#46 := [monotonicity #43]: #45
+#51 := [monotonicity #46 #48]: #50
+#55 := [trans #51 #53]: #54
+#60 := [monotonicity #55 #57]: #59
+#64 := [trans #60 #62]: #63
+#67 := [monotonicity #64]: #66
+#71 := [trans #67 #69]: #70
+#34 := [asserted]: #18
+[mp #34 #71]: false
+unsat