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

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_arith_quant_18.proof	Tue Oct 20 10:11:30 2009 +0200
@@ -0,0 +1,112 @@
+#2 := false
+#43 := 0::int
+decl ?x1!0 :: int
+#78 := ?x1!0
+#56 := -2::int
+#113 := (* -2::int ?x1!0)
+decl uf_1 :: int
+#6 := uf_1
+#8 := 2::int
+#10 := (* 2::int uf_1)
+#114 := (+ #10 #113)
+#115 := (<= #114 0::int)
+#120 := (not #115)
+#41 := -1::int
+#100 := (* -1::int ?x1!0)
+#101 := (+ uf_1 #100)
+#102 := (<= #101 0::int)
+#123 := (or #102 #120)
+#126 := (not #123)
+#59 := (* -2::int uf_1)
+#79 := (* 2::int ?x1!0)
+#80 := (+ #79 #59)
+#81 := (>= #80 0::int)
+#82 := (not #81)
+#45 := (* -1::int uf_1)
+#83 := (+ ?x1!0 #45)
+#84 := (>= #83 0::int)
+#85 := (or #84 #82)
+#86 := (not #85)
+#127 := (iff #86 #126)
+#124 := (iff #85 #123)
+#121 := (iff #82 #120)
+#118 := (iff #81 #115)
+#107 := (+ #59 #79)
+#110 := (>= #107 0::int)
+#116 := (iff #110 #115)
+#117 := [rewrite]: #116
+#111 := (iff #81 #110)
+#108 := (= #80 #107)
+#109 := [rewrite]: #108
+#112 := [monotonicity #109]: #111
+#119 := [trans #112 #117]: #118
+#122 := [monotonicity #119]: #121
+#105 := (iff #84 #102)
+#94 := (+ #45 ?x1!0)
+#97 := (>= #94 0::int)
+#103 := (iff #97 #102)
+#104 := [rewrite]: #103
+#98 := (iff #84 #97)
+#95 := (= #83 #94)
+#96 := [rewrite]: #95
+#99 := [monotonicity #96]: #98
+#106 := [trans #99 #104]: #105
+#125 := [monotonicity #106 #122]: #124
+#128 := [monotonicity #125]: #127
+#4 := (:var 0 int)
+#5 := (pattern #4)
+#9 := (* 2::int #4)
+#60 := (+ #9 #59)
+#58 := (>= #60 0::int)
+#57 := (not #58)
+#46 := (+ #4 #45)
+#44 := (>= #46 0::int)
+#63 := (or #44 #57)
+#66 := (forall (vars (?x1 int)) (:pat #5) #63)
+#69 := (not #66)
+#87 := (~ #69 #86)
+#88 := [sk]: #87
+#11 := (< #9 #10)
+#7 := (< #4 uf_1)
+#12 := (implies #7 #11)
+#13 := (forall (vars (?x1 int)) (:pat #5) #12)
+#14 := (not #13)
+#72 := (iff #14 #69)
+#31 := (not #7)
+#32 := (or #31 #11)
+#35 := (forall (vars (?x1 int)) (:pat #5) #32)
+#38 := (not #35)
+#70 := (iff #38 #69)
+#67 := (iff #35 #66)
+#64 := (iff #32 #63)
+#61 := (iff #11 #57)
+#62 := [rewrite]: #61
+#54 := (iff #31 #44)
+#42 := (not #44)
+#49 := (not #42)
+#52 := (iff #49 #44)
+#53 := [rewrite]: #52
+#50 := (iff #31 #49)
+#47 := (iff #7 #42)
+#48 := [rewrite]: #47
+#51 := [monotonicity #48]: #50
+#55 := [trans #51 #53]: #54
+#65 := [monotonicity #55 #62]: #64
+#68 := [quant-intro #65]: #67
+#71 := [monotonicity #68]: #70
+#39 := (iff #14 #38)
+#36 := (iff #13 #35)
+#33 := (iff #12 #32)
+#34 := [rewrite]: #33
+#37 := [quant-intro #34]: #36
+#40 := [monotonicity #37]: #39
+#73 := [trans #40 #71]: #72
+#30 := [asserted]: #14
+#74 := [mp #30 #73]: #69
+#91 := [mp~ #74 #88]: #86
+#92 := [mp #91 #128]: #126
+#130 := [not-or-elim #92]: #115
+#93 := (not #102)
+#129 := [not-or-elim #92]: #93
+[th-lemma #129 #130]: false
+unsat