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

class Outer_Keyword wraps symbol interpretation, lexicon, keyword table;

#2 := false
#9 := 0::int
#11 := 4::int
decl uf_1 :: int
#4 := uf_1
#189 := (div uf_1 4::int)
#210 := -4::int
#211 := (* -4::int #189)
#12 := (mod uf_1 4::int)
#134 := -1::int
#209 := (* -1::int #12)
#212 := (+ #209 #211)
#213 := (+ uf_1 #212)
#214 := (<= #213 0::int)
#215 := (not #214)
#208 := (>= #213 0::int)
#207 := (not #208)
#216 := (or #207 #215)
#217 := (not #216)
#1 := true
#36 := [true-axiom]: true
#393 := (or false #217)
#394 := [th-lemma]: #393
#395 := [unit-resolution #394 #36]: #217
#224 := (or #216 #214)
#225 := [def-axiom]: #224
#396 := [unit-resolution #225 #395]: #214
#222 := (or #216 #208)
#223 := [def-axiom]: #222
#397 := [unit-resolution #223 #395]: #208
#250 := (>= #12 4::int)
#251 := (not #250)
#398 := (or false #251)
#399 := [th-lemma]: #398
#400 := [unit-resolution #399 #36]: #251
#13 := 3::int
#90 := (>= #12 3::int)
#92 := (not #90)
#89 := (<= #12 3::int)
#91 := (not #89)
#93 := (or #91 #92)
#94 := (not #93)
#14 := (= #12 3::int)
#95 := (iff #14 #94)
#96 := [rewrite]: #95
#38 := [asserted]: #14
#97 := [mp #38 #96]: #94
#99 := [not-or-elim #97]: #90
#7 := 2::int
#261 := (div uf_1 2::int)
#140 := -2::int
#276 := (* -2::int #261)
#15 := (mod uf_1 2::int)
#275 := (* -1::int #15)
#277 := (+ #275 #276)
#278 := (+ uf_1 #277)
#279 := (<= #278 0::int)
#280 := (not #279)
#274 := (>= #278 0::int)
#273 := (not #274)
#281 := (or #273 #280)
#282 := (not #281)
#408 := (or false #282)
#409 := [th-lemma]: #408
#410 := [unit-resolution #409 #36]: #282
#289 := (or #281 #279)
#290 := [def-axiom]: #289
#411 := [unit-resolution #290 #410]: #279
#287 := (or #281 #274)
#288 := [def-axiom]: #287
#412 := [unit-resolution #288 #410]: #274
#16 := 1::int
#55 := (>= #15 1::int)
#100 := (not #55)
decl uf_2 :: int
#5 := uf_2
#18 := (mod uf_2 2::int)
#61 := (<= #18 1::int)
#102 := (not #61)
#375 := [hypothesis]: #102
#358 := (>= #18 2::int)
#359 := (not #358)
#403 := (or false #359)
#404 := [th-lemma]: #403
#405 := [unit-resolution #404 #36]: #359
#406 := [th-lemma #405 #375]: false
#407 := [lemma #406]: #61
#413 := (or #100 #102)
#62 := (>= #18 1::int)
#315 := (div uf_2 2::int)
#330 := (* -2::int #315)
#329 := (* -1::int #18)
#331 := (+ #329 #330)
#332 := (+ uf_2 #331)
#333 := (<= #332 0::int)
#334 := (not #333)
#328 := (>= #332 0::int)
#327 := (not #328)
#335 := (or #327 #334)
#336 := (not #335)
#376 := (or false #336)
#377 := [th-lemma]: #376
#378 := [unit-resolution #377 #36]: #336
#343 := (or #335 #333)
#344 := [def-axiom]: #343
#379 := [unit-resolution #344 #378]: #333
#341 := (or #335 #328)
#342 := [def-axiom]: #341
#380 := [unit-resolution #342 #378]: #328
#103 := (not #62)
#381 := [hypothesis]: #103
#352 := (>= #18 0::int)
#382 := (or false #352)
#383 := [th-lemma]: #382
#384 := [unit-resolution #383 #36]: #352
#6 := (+ uf_1 uf_2)
#116 := (div #6 2::int)
#141 := (* -2::int #116)
#8 := (mod #6 2::int)
#139 := (* -1::int #8)
#142 := (+ #139 #141)
#143 := (+ uf_2 #142)
#144 := (+ uf_1 #143)
#138 := (<= #144 0::int)
#136 := (not #138)
#137 := (>= #144 0::int)
#135 := (not #137)
#145 := (or #135 #136)
#146 := (not #145)
#385 := (or false #146)
#386 := [th-lemma]: #385
#387 := [unit-resolution #386 #36]: #146
#153 := (or #145 #138)
#154 := [def-axiom]: #153
#388 := [unit-resolution #154 #387]: #138
#151 := (or #145 #137)
#152 := [def-axiom]: #151
#389 := [unit-resolution #152 #387]: #137
#78 := (<= #8 0::int)
#79 := (>= #8 0::int)
#81 := (not #79)
#80 := (not #78)
#82 := (or #80 #81)
#83 := (not #82)
#10 := (= #8 0::int)
#84 := (iff #10 #83)
#85 := [rewrite]: #84
#37 := [asserted]: #10
#86 := [mp #37 #85]: #83
#87 := [not-or-elim #86]: #78
#390 := (or false #79)
#391 := [th-lemma]: #390
#392 := [unit-resolution #391 #36]: #79
#401 := [th-lemma #99 #400 #397 #396 #392 #87 #389 #388 #384 #381 #380 #379]: false
#402 := [lemma #401]: #62
#57 := (<= #15 1::int)
#101 := (not #57)
#369 := [hypothesis]: #101
#304 := (>= #15 2::int)
#305 := (not #304)
#370 := (or false #305)
#371 := [th-lemma]: #370
#372 := [unit-resolution #371 #36]: #305
#373 := [th-lemma #372 #369]: false
#374 := [lemma #373]: #57
#104 := (or #100 #101 #102 #103)
#69 := (and #55 #57 #61 #62)
#74 := (not #69)
#113 := (iff #74 #104)
#105 := (not #104)
#108 := (not #105)
#111 := (iff #108 #104)
#112 := [rewrite]: #111
#109 := (iff #74 #108)
#106 := (iff #69 #105)
#107 := [rewrite]: #106
#110 := [monotonicity #107]: #109
#114 := [trans #110 #112]: #113
#19 := (= #18 1::int)
#17 := (= #15 1::int)
#20 := (and #17 #19)
#21 := (not #20)
#75 := (iff #21 #74)
#72 := (iff #20 #69)
#63 := (and #61 #62)
#58 := (and #55 #57)
#66 := (and #58 #63)
#70 := (iff #66 #69)
#71 := [rewrite]: #70
#67 := (iff #20 #66)
#64 := (iff #19 #63)
#65 := [rewrite]: #64
#59 := (iff #17 #58)
#60 := [rewrite]: #59
#68 := [monotonicity #60 #65]: #67
#73 := [trans #68 #71]: #72
#76 := [monotonicity #73]: #75
#39 := [asserted]: #21
#77 := [mp #39 #76]: #74
#115 := [mp #77 #114]: #104
#414 := [unit-resolution #115 #374 #402]: #413
#415 := [unit-resolution #414 #407]: #100
#298 := (>= #15 0::int)
#416 := (or false #298)
#417 := [th-lemma]: #416
#418 := [unit-resolution #417 #36]: #298
[th-lemma #418 #415 #412 #411 #99 #400 #397 #396]: false
unsat