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

+#2 := false
+#23 := 3::int
+decl uf_2 :: (-> T1 int)
+decl uf_3 :: T1
+#21 := uf_3
+#22 := (uf_2 uf_3)
+#137 := (>= #22 3::int)
+#135 := (not #137)
+#24 := (< #22 3::int)
+#136 := (iff #24 #135)
+#138 := [rewrite]: #136
+#132 := [asserted]: #24
+#139 := [mp #132 #138]: #135
+#9 := 0::int
+decl uf_1 :: (-> int T1)
+#25 := 2::int
+#26 := (* 2::int #22)
+#27 := (uf_1 #26)
+#28 := (uf_2 #27)
+#297 := -1::int
+#633 := (* -1::int #28)
+#635 := (+ #26 #633)
+#278 := (>= #635 0::int)
+#291 := (= #635 0::int)
+#315 := (>= #26 0::int)
+#279 := (= #28 0::int)
+#627 := (not #279)
+#624 := (<= #28 0::int)
+#281 := (not #624)
+#29 := 7::int
+#143 := (>= #28 7::int)
+#30 := (< #28 7::int)
+#31 := (not #30)
+#150 := (iff #31 #143)
+#141 := (not #143)
+#145 := (not #141)
+#148 := (iff #145 #143)
+#149 := [rewrite]: #148
+#146 := (iff #31 #145)
+#142 := (iff #30 #141)
+#144 := [rewrite]: #142
+#147 := [monotonicity #144]: #146
+#151 := [trans #147 #149]: #150
+#133 := [asserted]: #31
+#152 := [mp #133 #151]: #143
+#618 := (or #281 #141)
+#265 := [th-lemma]: #618
+#266 := [unit-resolution #265 #152]: #281
+#625 := (or #627 #624)
+#628 := [th-lemma]: #625
+#614 := [unit-resolution #628 #266]: #627
+#10 := (:var 0 int)
+#12 := (uf_1 #10)
+#649 := (pattern #12)
+#73 := (>= #10 0::int)
+#13 := (uf_2 #12)
+#18 := (= #13 0::int)
+#121 := (or #18 #73)
+#656 := (forall (vars (?x3 int)) (:pat #649) #121)
+#126 := (forall (vars (?x3 int)) #121)
+#659 := (iff #126 #656)
+#657 := (iff #121 #121)
+#658 := [refl]: #657
+#660 := [quant-intro #658]: #659
+#154 := (~ #126 #126)
+#170 := (~ #121 #121)
+#171 := [refl]: #170
+#155 := [nnf-pos #171]: #154
+#17 := (< #10 0::int)
+#19 := (implies #17 #18)
+#20 := (forall (vars (?x3 int)) #19)
+#129 := (iff #20 #126)
+#92 := (= 0::int #13)
+#98 := (not #17)
+#99 := (or #98 #92)
+#104 := (forall (vars (?x3 int)) #99)
+#127 := (iff #104 #126)
+#124 := (iff #99 #121)
+#118 := (or #73 #18)
+#122 := (iff #118 #121)
+#123 := [rewrite]: #122
+#119 := (iff #99 #118)
+#116 := (iff #92 #18)
+#117 := [rewrite]: #116
+#114 := (iff #98 #73)
+#74 := (not #73)
+#109 := (not #74)
+#112 := (iff #109 #73)
+#113 := [rewrite]: #112
+#110 := (iff #98 #109)
+#107 := (iff #17 #74)
+#108 := [rewrite]: #107
+#111 := [monotonicity #108]: #110
+#115 := [trans #111 #113]: #114
+#120 := [monotonicity #115 #117]: #119
+#125 := [trans #120 #123]: #124
+#128 := [quant-intro #125]: #127
+#105 := (iff #20 #104)
+#102 := (iff #19 #99)
+#95 := (implies #17 #92)
+#100 := (iff #95 #99)
+#101 := [rewrite]: #100
+#96 := (iff #19 #95)
+#93 := (iff #18 #92)
+#94 := [rewrite]: #93
+#97 := [monotonicity #94]: #96
+#103 := [trans #97 #101]: #102
+#106 := [quant-intro #103]: #105
+#130 := [trans #106 #128]: #129
+#91 := [asserted]: #20
+#131 := [mp #91 #130]: #126
+#172 := [mp~ #131 #155]: #126
+#661 := [mp #172 #660]: #656
+#619 := (not #656)
+#620 := (or #619 #279 #315)
+#280 := (or #279 #315)
+#621 := (or #619 #280)
+#617 := (iff #621 #620)
+#623 := [rewrite]: #617
+#622 := [quant-inst]: #621
+#260 := [mp #622 #623]: #620
+#615 := [unit-resolution #260 #661 #614]: #315
+#316 := (not #315)
+#302 := (or #291 #316)
+#55 := (= #10 #13)
+#80 := (or #55 #74)
+#650 := (forall (vars (?x2 int)) (:pat #649) #80)
+#85 := (forall (vars (?x2 int)) #80)
+#653 := (iff #85 #650)
+#651 := (iff #80 #80)
+#652 := [refl]: #651
+#654 := [quant-intro #652]: #653
+#153 := (~ #85 #85)
+#167 := (~ #80 #80)
+#168 := [refl]: #167
+#134 := [nnf-pos #168]: #153
+#14 := (= #13 #10)
+#11 := (<= 0::int #10)
+#15 := (implies #11 #14)
+#16 := (forall (vars (?x2 int)) #15)
+#88 := (iff #16 #85)
+#62 := (not #11)
+#63 := (or #62 #55)
+#68 := (forall (vars (?x2 int)) #63)
+#86 := (iff #68 #85)
+#83 := (iff #63 #80)
+#77 := (or #74 #55)
+#81 := (iff #77 #80)
+#82 := [rewrite]: #81
+#78 := (iff #63 #77)
+#75 := (iff #62 #74)
+#71 := (iff #11 #73)
+#72 := [rewrite]: #71
+#76 := [monotonicity #72]: #75
+#79 := [monotonicity #76]: #78
+#84 := [trans #79 #82]: #83
+#87 := [quant-intro #84]: #86
+#69 := (iff #16 #68)
+#66 := (iff #15 #63)
+#59 := (implies #11 #55)
+#64 := (iff #59 #63)
+#65 := [rewrite]: #64
+#60 := (iff #15 #59)
+#57 := (iff #14 #55)
+#58 := [rewrite]: #57
+#61 := [monotonicity #58]: #60
+#67 := [trans #61 #65]: #66
+#70 := [quant-intro #67]: #69
+#89 := [trans #70 #87]: #88
+#54 := [asserted]: #16
+#90 := [mp #54 #89]: #85
+#169 := [mp~ #90 #134]: #85
+#655 := [mp #169 #654]: #650
+#637 := (not #650)
+#638 := (or #637 #291 #316)
+#314 := (= #26 #28)
+#318 := (or #314 #316)
+#639 := (or #637 #318)
+#290 := (iff #639 #638)
+#640 := (or #637 #302)
+#294 := (iff #640 #638)
+#631 := [rewrite]: #294
+#630 := (iff #639 #640)
+#303 := (iff #318 #302)
+#422 := (iff #314 #291)
+#629 := [rewrite]: #422
+#636 := [monotonicity #629]: #303
+#289 := [monotonicity #636]: #630
+#632 := [trans #289 #631]: #290
+#634 := [quant-inst]: #639
+#274 := [mp #634 #632]: #638
+#322 := [unit-resolution #274 #655]: #302
+#337 := [unit-resolution #322 #615]: #291
+#338 := (not #291)
+#339 := (or #338 #278)
+#340 := [th-lemma]: #339
+#232 := [unit-resolution #340 #337]: #278
+[th-lemma #152 #232 #139]: false
+unsat