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

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_arith_quant_17.proof	Tue Oct 20 10:11:30 2009 +0200
@@ -0,0 +1,148 @@
+#2 := false
+#144 := (not false)
+#7 := 0::int
+#5 := (:var 0 int)
+#52 := (<= #5 0::int)
+#53 := (not #52)
+#147 := (or #53 #144)
+#150 := (not #147)
+#153 := (forall (vars (?x1 int)) #150)
+#180 := (iff #153 false)
+#175 := (forall (vars (?x1 int)) false)
+#178 := (iff #175 false)
+#179 := [elim-unused]: #178
+#176 := (iff #153 #175)
+#173 := (iff #150 false)
+#1 := true
+#168 := (not true)
+#171 := (iff #168 false)
+#172 := [rewrite]: #171
+#169 := (iff #150 #168)
+#166 := (iff #147 true)
+#161 := (or #53 true)
+#164 := (iff #161 true)
+#165 := [rewrite]: #164
+#162 := (iff #147 #161)
+#159 := (iff #144 true)
+#160 := [rewrite]: #159
+#163 := [monotonicity #160]: #162
+#167 := [trans #163 #165]: #166
+#170 := [monotonicity #167]: #169
+#174 := [trans #170 #172]: #173
+#177 := [quant-intro #174]: #176
+#181 := [trans #177 #179]: #180
+#56 := -1::int
+#57 := (* -1::int #5)
+#4 := (:var 1 int)
+#58 := (+ #4 #57)
+#59 := (<= #58 0::int)
+#62 := (not #59)
+#68 := (or #53 #62)
+#73 := (forall (vars (?x2 int)) #68)
+#76 := (not #73)
+#79 := (or #53 #76)
+#105 := (not #79)
+#123 := (forall (vars (?x1 int)) #105)
+#156 := (iff #123 #153)
+#127 := (forall (vars (?x2 int)) #53)
+#130 := (not #127)
+#133 := (or #53 #130)
+#136 := (not #133)
+#139 := (forall (vars (?x1 int)) #136)
+#154 := (iff #139 #153)
+#155 := [rewrite]: #154
+#140 := (iff #123 #139)
+#141 := [rewrite]: #140
+#157 := [trans #141 #155]: #156
+#116 := (and #52 #73)
+#119 := (forall (vars (?x1 int)) #116)
+#124 := (iff #119 #123)
+#113 := (iff #116 #105)
+#122 := [rewrite]: #113
+#125 := [quant-intro #122]: #124
+#94 := (not #53)
+#104 := (and #94 #73)
+#108 := (forall (vars (?x1 int)) #104)
+#120 := (iff #108 #119)
+#117 := (iff #104 #116)
+#114 := (iff #94 #52)
+#115 := [rewrite]: #114
+#118 := [monotonicity #115]: #117
+#121 := [quant-intro #118]: #120
+#82 := (exists (vars (?x1 int)) #79)
+#85 := (not #82)
+#109 := (~ #85 #108)
+#106 := (~ #105 #104)
+#101 := (not #76)
+#102 := (~ #101 #73)
+#99 := (~ #73 #73)
+#97 := (~ #68 #68)
+#98 := [refl]: #97
+#100 := [nnf-pos #98]: #99
+#103 := [nnf-neg #100]: #102
+#95 := (~ #94 #94)
+#96 := [refl]: #95
+#107 := [nnf-neg #96 #103]: #106
+#110 := [nnf-neg #107]: #109
+#8 := (< 0::int #5)
+#6 := (<= #4 #5)
+#9 := (implies #6 #8)
+#10 := (forall (vars (?x2 int)) #9)
+#11 := (implies #10 #8)
+#12 := (exists (vars (?x1 int)) #11)
+#13 := (not #12)
+#88 := (iff #13 #85)
+#30 := (not #6)
+#31 := (or #30 #8)
+#34 := (forall (vars (?x2 int)) #31)
+#40 := (not #34)
+#41 := (or #8 #40)
+#46 := (exists (vars (?x1 int)) #41)
+#49 := (not #46)
+#86 := (iff #49 #85)
+#83 := (iff #46 #82)
+#80 := (iff #41 #79)
+#77 := (iff #40 #76)
+#74 := (iff #34 #73)
+#71 := (iff #31 #68)
+#65 := (or #62 #53)
+#69 := (iff #65 #68)
+#70 := [rewrite]: #69
+#66 := (iff #31 #65)
+#54 := (iff #8 #53)
+#55 := [rewrite]: #54
+#63 := (iff #30 #62)
+#60 := (iff #6 #59)
+#61 := [rewrite]: #60
+#64 := [monotonicity #61]: #63
+#67 := [monotonicity #64 #55]: #66
+#72 := [trans #67 #70]: #71
+#75 := [quant-intro #72]: #74
+#78 := [monotonicity #75]: #77
+#81 := [monotonicity #55 #78]: #80
+#84 := [quant-intro #81]: #83
+#87 := [monotonicity #84]: #86
+#50 := (iff #13 #49)
+#47 := (iff #12 #46)
+#44 := (iff #11 #41)
+#37 := (implies #34 #8)
+#42 := (iff #37 #41)
+#43 := [rewrite]: #42
+#38 := (iff #11 #37)
+#35 := (iff #10 #34)
+#32 := (iff #9 #31)
+#33 := [rewrite]: #32
+#36 := [quant-intro #33]: #35
+#39 := [monotonicity #36]: #38
+#45 := [trans #39 #43]: #44
+#48 := [quant-intro #45]: #47
+#51 := [monotonicity #48]: #50
+#89 := [trans #51 #87]: #88
+#29 := [asserted]: #13
+#90 := [mp #29 #89]: #85
+#111 := [mp~ #90 #110]: #108
+#112 := [mp #111 #121]: #119
+#126 := [mp #112 #125]: #123
+#158 := [mp #126 #157]: #153
+[mp #158 #181]: false
+unsat