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

adopting Sequences

#2 := false
#7 := 0::real
decl uf_2 :: real
#5 := uf_2
#143 := 2::real
#144 := (* 2::real uf_2)
#165 := (<= #144 0::real)
#188 := (not #165)
#88 := (>= uf_2 0::real)
#166 := (or #88 #165)
#191 := (not #166)
decl uf_1 :: real
#4 := uf_1
#76 := (>= uf_1 0::real)
#89 := (not #88)
#146 := (* 2::real uf_1)
#167 := (<= #146 0::real)
#199 := (not #167)
#263 := [hypothesis]: #88
#147 := (+ #146 #144)
#168 := (<= #147 0::real)
#169 := (ite #88 #167 #168)
#194 := (not #169)
#186 := (or #166 #89)
#187 := [def-axiom]: #186
#271 := [unit-resolution #187 #263]: #166
#170 := (ite #76 #166 #169)
#205 := (not #170)
#6 := (+ uf_1 uf_2)
#64 := (>= #6 0::real)
#269 := (or #64 #89)
#65 := (not #64)
#262 := [hypothesis]: #65
#174 := (>= #144 0::real)
#175 := (or #89 #174)
#230 := (not #175)
#257 := [hypothesis]: #230
#225 := (or #175 #88)
#226 := [def-axiom]: #225
#258 := [unit-resolution #226 #257]: #88
#227 := (not #174)
#228 := (or #175 #227)
#229 := [def-axiom]: #228
#259 := [unit-resolution #229 #257]: #227
#260 := [th-lemma #259 #258]: false
#261 := [lemma #260]: #175
#172 := (>= #146 0::real)
#171 := (>= #147 0::real)
#173 := (ite #88 #171 #172)
#176 := (ite #76 #173 #175)
#233 := (not #176)
#264 := (or #64 #233)
#177 := (ite #64 #170 #176)
#182 := (not #177)
#36 := -1::real
#38 := (* -1::real uf_2)
#95 := (ite #88 uf_2 #38)
#107 := (* -1::real #95)
#37 := (* -1::real uf_1)
#83 := (ite #76 uf_1 #37)
#106 := (* -1::real #83)
#108 := (+ #106 #107)
#39 := (+ #37 #38)
#71 := (ite #64 #6 #39)
#109 := (+ #71 #108)
#110 := (<= #109 0::real)
#115 := (not #110)
#183 := (iff #115 #182)
#180 := (iff #110 #177)
#150 := -2::real
#152 := (* -2::real uf_2)
#155 := (ite #88 #152 0::real)
#151 := (* -2::real uf_1)
#153 := (+ #151 #152)
#154 := (ite #88 #153 #151)
#156 := (ite #76 #154 #155)
#148 := (ite #88 #146 #147)
#145 := (ite #88 0::real #144)
#149 := (ite #76 #145 #148)
#157 := (ite #64 #149 #156)
#162 := (<= #157 0::real)
#178 := (iff #162 #177)
#179 := [rewrite]: #178
#163 := (iff #110 #162)
#160 := (= #109 #157)
#133 := (+ uf_1 #38)
#134 := (ite #88 #133 #6)
#131 := (+ #37 uf_2)
#132 := (ite #88 #39 #131)
#135 := (ite #76 #132 #134)
#140 := (+ #71 #135)
#158 := (= #140 #157)
#159 := [rewrite]: #158
#141 := (= #109 #140)
#138 := (= #108 #135)
#125 := (ite #88 #38 uf_2)
#123 := (ite #76 #37 uf_1)
#128 := (+ #123 #125)
#136 := (= #128 #135)
#137 := [rewrite]: #136
#129 := (= #108 #128)
#126 := (= #107 #125)
#127 := [rewrite]: #126
#121 := (= #106 #123)
#124 := [rewrite]: #121
#130 := [monotonicity #124 #127]: #129
#139 := [trans #130 #137]: #138
#142 := [monotonicity #139]: #141
#161 := [trans #142 #159]: #160
#164 := [monotonicity #161]: #163
#181 := [trans #164 #179]: #180
#184 := [monotonicity #181]: #183
#15 := (- uf_2)
#14 := (< uf_2 0::real)
#16 := (ite #14 #15 uf_2)
#12 := (- uf_1)
#11 := (< uf_1 0::real)
#13 := (ite #11 #12 uf_1)
#17 := (+ #13 #16)
#9 := (- #6)
#8 := (< #6 0::real)
#10 := (ite #8 #9 #6)
#18 := (<= #10 #17)
#19 := (not #18)
#118 := (iff #19 #115)
#52 := (ite #14 #38 uf_2)
#47 := (ite #11 #37 uf_1)
#55 := (+ #47 #52)
#42 := (ite #8 #39 #6)
#58 := (<= #42 #55)
#61 := (not #58)
#116 := (iff #61 #115)
#113 := (iff #58 #110)
#100 := (+ #83 #95)
#103 := (<= #71 #100)
#111 := (iff #103 #110)
#112 := [rewrite]: #111
#104 := (iff #58 #103)
#101 := (= #55 #100)
#98 := (= #52 #95)
#92 := (ite #89 #38 uf_2)
#96 := (= #92 #95)
#97 := [rewrite]: #96
#93 := (= #52 #92)
#90 := (iff #14 #89)
#91 := [rewrite]: #90
#94 := [monotonicity #91]: #93
#99 := [trans #94 #97]: #98
#86 := (= #47 #83)
#77 := (not #76)
#80 := (ite #77 #37 uf_1)
#84 := (= #80 #83)
#85 := [rewrite]: #84
#81 := (= #47 #80)
#78 := (iff #11 #77)
#79 := [rewrite]: #78
#82 := [monotonicity #79]: #81
#87 := [trans #82 #85]: #86
#102 := [monotonicity #87 #99]: #101
#74 := (= #42 #71)
#68 := (ite #65 #39 #6)
#72 := (= #68 #71)
#73 := [rewrite]: #72
#69 := (= #42 #68)
#66 := (iff #8 #65)
#67 := [rewrite]: #66
#70 := [monotonicity #67]: #69
#75 := [trans #70 #73]: #74
#105 := [monotonicity #75 #102]: #104
#114 := [trans #105 #112]: #113
#117 := [monotonicity #114]: #116
#62 := (iff #19 #61)
#59 := (iff #18 #58)
#56 := (= #17 #55)
#53 := (= #16 #52)
#50 := (= #15 #38)
#51 := [rewrite]: #50
#54 := [monotonicity #51]: #53
#48 := (= #13 #47)
#45 := (= #12 #37)
#46 := [rewrite]: #45
#49 := [monotonicity #46]: #48
#57 := [monotonicity #49 #54]: #56
#43 := (= #10 #42)
#40 := (= #9 #39)
#41 := [rewrite]: #40
#44 := [monotonicity #41]: #43
#60 := [monotonicity #44 #57]: #59
#63 := [monotonicity #60]: #62
#119 := [trans #63 #117]: #118
#35 := [asserted]: #19
#120 := [mp #35 #119]: #115
#185 := [mp #120 #184]: #182
#248 := (or #177 #64 #233)
#249 := [def-axiom]: #248
#265 := [unit-resolution #249 #185]: #264
#266 := [unit-resolution #265 #262]: #233
#240 := (or #176 #76 #230)
#241 := [def-axiom]: #240
#267 := [unit-resolution #241 #266 #261]: #76
#268 := [th-lemma #267 #263 #262]: false
#270 := [lemma #268]: #269
#272 := [unit-resolution #270 #263]: #64
#273 := (or #65 #205)
#246 := (or #177 #65 #205)
#247 := [def-axiom]: #246
#274 := [unit-resolution #247 #185]: #273
#275 := [unit-resolution #274 #272]: #205
#255 := (or #170 #194 #191)
#250 := [hypothesis]: #169
#251 := [hypothesis]: #205
#252 := [hypothesis]: #166
#210 := (or #170 #77 #191)
#211 := [def-axiom]: #210
#253 := [unit-resolution #211 #251 #252]: #77
#212 := (or #170 #76 #194)
#213 := [def-axiom]: #212
#254 := [unit-resolution #213 #253 #251 #250]: false
#256 := [lemma #254]: #255
#276 := [unit-resolution #256 #275 #271]: #194
#200 := (or #169 #89 #199)
#201 := [def-axiom]: #200
#277 := [unit-resolution #201 #276 #263]: #199
#278 := [unit-resolution #211 #275 #271]: #77
#279 := [th-lemma #278 #277]: false
#280 := [lemma #279]: #89
#281 := [hypothesis]: #77
#282 := [unit-resolution #241 #281 #261]: #176
#283 := [unit-resolution #265 #282]: #64
#284 := [th-lemma #281 #283 #280]: false
#285 := [lemma #284]: #76
#222 := (not #172)
#286 := [hypothesis]: #222
#287 := [th-lemma #285 #286]: false
#288 := [lemma #287]: #172
#223 := (or #173 #88 #222)
#224 := [def-axiom]: #223
#289 := [unit-resolution #224 #288 #280]: #173
#214 := (not #173)
#238 := (or #176 #77 #214)
#239 := [def-axiom]: #238
#290 := [unit-resolution #239 #289 #285]: #176
#291 := [unit-resolution #265 #290]: #64
#292 := [unit-resolution #274 #291]: #205
#293 := [unit-resolution #211 #292 #285]: #191
#189 := (or #166 #188)
#190 := [def-axiom]: #189
#294 := [unit-resolution #190 #293]: #188
[th-lemma #280 #294]: false
unsat