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

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