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

+#2 := false
+#11 := 0::int
+decl uf_2 :: int
+#7 := uf_2
+#42 := -1::int
+#45 := (* -1::int uf_2)
+decl uf_1 :: int
+#5 := uf_1
+#46 := (+ uf_1 #45)
+#63 := (>= #46 0::int)
+#83 := (iff #63 false)
+#44 := -4::int
+#79 := (>= -4::int 0::int)
+#81 := (iff #79 false)
+#82 := [rewrite]: #81
+#77 := (iff #63 #79)
+#47 := (= #46 -4::int)
+#8 := 4::int
+#9 := (+ uf_1 4::int)
+#10 := (= uf_2 #9)
+#49 := (iff #10 #47)
+#32 := (+ 4::int uf_1)
+#39 := (= uf_2 #32)
+#43 := (iff #39 #47)
+#48 := [rewrite]: #43
+#40 := (iff #10 #39)
+#37 := (= #9 #32)
+#38 := [rewrite]: #37
+#41 := [monotonicity #38]: #40
+#50 := [trans #41 #48]: #49
+#31 := [asserted]: #10
+#51 := [mp #31 #50]: #47
+#80 := [monotonicity #51]: #77
+#84 := [trans #80 #82]: #83
+#12 := (- uf_2 uf_1)
+#13 := (< 0::int #12)
+#14 := (not #13)
+#74 := (iff #14 #63)
+#53 := (* -1::int uf_1)
+#54 := (+ #53 uf_2)
+#57 := (< 0::int #54)
+#60 := (not #57)
+#72 := (iff #60 #63)
+#64 := (not #63)
+#67 := (not #64)
+#70 := (iff #67 #63)
+#71 := [rewrite]: #70
+#68 := (iff #60 #67)
+#65 := (iff #57 #64)
+#66 := [rewrite]: #65
+#69 := [monotonicity #66]: #68
+#73 := [trans #69 #71]: #72
+#61 := (iff #14 #60)
+#58 := (iff #13 #57)
+#55 := (= #12 #54)
+#56 := [rewrite]: #55
+#59 := [monotonicity #56]: #58
+#62 := [monotonicity #59]: #61
+#75 := [trans #62 #73]: #74
+#52 := [asserted]: #14
+#76 := [mp #52 #75]: #63
+[mp #76 #84]: false
+unsat