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

+#2 := false
+#5 := 0::real
+decl uf_1 :: real
+#4 := uf_1
+#94 := (<= uf_1 0::real)
+#17 := 2::real
+#40 := (* 2::real uf_1)
+#102 := (<= #40 0::real)
+#103 := (>= #40 0::real)
+#105 := (not #103)
+#104 := (not #102)
+#106 := (or #104 #105)
+#107 := (not #106)
+#88 := (= #40 0::real)
+#108 := (iff #88 #107)
+#109 := [rewrite]: #108
+#16 := 4::real
+#11 := (- uf_1)
+#10 := (< uf_1 0::real)
+#12 := (ite #10 #11 uf_1)
+#9 := 1::real
+#13 := (< 1::real #12)
+#14 := (not #13)
+#15 := (or #13 #14)
+#18 := (ite #15 4::real 2::real)
+#19 := (* #18 uf_1)
+#8 := (+ uf_1 uf_1)
+#20 := (= #8 #19)
+#21 := (not #20)
+#22 := (not #21)
+#89 := (iff #22 #88)
+#70 := (* 4::real uf_1)
+#73 := (= #40 #70)
+#86 := (iff #73 #88)
+#87 := [rewrite]: #86
+#84 := (iff #22 #73)
+#76 := (not #73)
+#79 := (not #76)
+#82 := (iff #79 #73)
+#83 := [rewrite]: #82
+#80 := (iff #22 #79)
+#77 := (iff #21 #76)
+#74 := (iff #20 #73)
+#71 := (= #19 #70)
+#68 := (= #18 4::real)
+#1 := true
+#63 := (ite true 4::real 2::real)
+#66 := (= #63 4::real)
+#67 := [rewrite]: #66
+#64 := (= #18 #63)
+#61 := (iff #15 true)
+#43 := -1::real
+#44 := (* -1::real uf_1)
+#47 := (ite #10 #44 uf_1)
+#50 := (< 1::real #47)
+#53 := (not #50)
+#56 := (or #50 #53)
+#59 := (iff #56 true)
+#60 := [rewrite]: #59
+#57 := (iff #15 #56)
+#54 := (iff #14 #53)
+#51 := (iff #13 #50)
+#48 := (= #12 #47)
+#45 := (= #11 #44)
+#46 := [rewrite]: #45
+#49 := [monotonicity #46]: #48
+#52 := [monotonicity #49]: #51
+#55 := [monotonicity #52]: #54
+#58 := [monotonicity #52 #55]: #57
+#62 := [trans #58 #60]: #61
+#65 := [monotonicity #62]: #64
+#69 := [trans #65 #67]: #68
+#72 := [monotonicity #69]: #71
+#41 := (= #8 #40)
+#42 := [rewrite]: #41
+#75 := [monotonicity #42 #72]: #74
+#78 := [monotonicity #75]: #77
+#81 := [monotonicity #78]: #80
+#85 := [trans #81 #83]: #84
+#90 := [trans #85 #87]: #89
+#39 := [asserted]: #22
+#91 := [mp #39 #90]: #88
+#110 := [mp #91 #109]: #107
+#111 := [not-or-elim #110]: #102
+#127 := (or #94 #104)
+#128 := [th-lemma]: #127
+#129 := [unit-resolution #128 #111]: #94
+#92 := (>= uf_1 0::real)
+#112 := [not-or-elim #110]: #103
+#130 := (or #92 #105)
+#131 := [th-lemma]: #130
+#132 := [unit-resolution #131 #112]: #92
+#114 := (not #94)
+#113 := (not #92)
+#115 := (or #113 #114)
+#95 := (and #92 #94)
+#98 := (not #95)
+#124 := (iff #98 #115)
+#116 := (not #115)
+#119 := (not #116)
+#122 := (iff #119 #115)
+#123 := [rewrite]: #122
+#120 := (iff #98 #119)
+#117 := (iff #95 #116)
+#118 := [rewrite]: #117
+#121 := [monotonicity #118]: #120
+#125 := [trans #121 #123]: #124
+#6 := (= uf_1 0::real)
+#7 := (not #6)
+#99 := (iff #7 #98)
+#96 := (iff #6 #95)
+#97 := [rewrite]: #96
+#100 := [monotonicity #97]: #99
+#38 := [asserted]: #7
+#101 := [mp #38 #100]: #98
+#126 := [mp #101 #125]: #115
+[unit-resolution #126 #132 #129]: false
+unsat