--- a/src/HOL/SMT/Examples/cert/z3_arith_quant_18.proof Tue Feb 02 18:11:21 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,112 +0,0 @@
-#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