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

+#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