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

removed fixme - quick-and-dirty flag is appropriate

#2 := false
#9 := 1::int
decl ?x1!1 :: int
#91 := ?x1!1
#68 := -2::int
#129 := (* -2::int ?x1!1)
decl ?x2!0 :: int
#90 := ?x2!0
#7 := 2::int
#128 := (* 2::int ?x2!0)
#130 := (+ #128 #129)
#131 := (<= #130 1::int)
#136 := (not #131)
#55 := 0::int
#53 := -1::int
#115 := (* -1::int ?x1!1)
#116 := (+ ?x2!0 #115)
#117 := (<= #116 0::int)
#139 := (or #117 #136)
#142 := (not #139)
#92 := (* -2::int ?x2!0)
#93 := (* 2::int ?x1!1)
#94 := (+ #93 #92)
#95 := (>= #94 -1::int)
#96 := (not #95)
#97 := (* -1::int ?x2!0)
#98 := (+ ?x1!1 #97)
#99 := (>= #98 0::int)
#100 := (or #99 #96)
#101 := (not #100)
#143 := (iff #101 #142)
#140 := (iff #100 #139)
#137 := (iff #96 #136)
#134 := (iff #95 #131)
#122 := (+ #92 #93)
#125 := (>= #122 -1::int)
#132 := (iff #125 #131)
#133 := [rewrite]: #132
#126 := (iff #95 #125)
#123 := (= #94 #122)
#124 := [rewrite]: #123
#127 := [monotonicity #124]: #126
#135 := [trans #127 #133]: #134
#138 := [monotonicity #135]: #137
#120 := (iff #99 #117)
#109 := (+ #97 ?x1!1)
#112 := (>= #109 0::int)
#118 := (iff #112 #117)
#119 := [rewrite]: #118
#113 := (iff #99 #112)
#110 := (= #98 #109)
#111 := [rewrite]: #110
#114 := [monotonicity #111]: #113
#121 := [trans #114 #119]: #120
#141 := [monotonicity #121 #138]: #140
#144 := [monotonicity #141]: #143
#5 := (:var 0 int)
#71 := (* -2::int #5)
#4 := (:var 1 int)
#8 := (* 2::int #4)
#72 := (+ #8 #71)
#70 := (>= #72 -1::int)
#69 := (not #70)
#57 := (* -1::int #5)
#58 := (+ #4 #57)
#56 := (>= #58 0::int)
#75 := (or #56 #69)
#78 := (forall (vars (?x1 int) (?x2 int)) #75)
#81 := (not #78)
#102 := (~ #81 #101)
#103 := [sk]: #102
#11 := (* 2::int #5)
#10 := (+ #8 1::int)
#12 := (< #10 #11)
#6 := (< #4 #5)
#13 := (implies #6 #12)
#14 := (forall (vars (?x1 int) (?x2 int)) #13)
#15 := (not #14)
#84 := (iff #15 #81)
#32 := (+ 1::int #8)
#35 := (< #32 #11)
#41 := (not #6)
#42 := (or #41 #35)
#47 := (forall (vars (?x1 int) (?x2 int)) #42)
#50 := (not #47)
#82 := (iff #50 #81)
#79 := (iff #47 #78)
#76 := (iff #42 #75)
#73 := (iff #35 #69)
#74 := [rewrite]: #73
#66 := (iff #41 #56)
#54 := (not #56)
#61 := (not #54)
#64 := (iff #61 #56)
#65 := [rewrite]: #64
#62 := (iff #41 #61)
#59 := (iff #6 #54)
#60 := [rewrite]: #59
#63 := [monotonicity #60]: #62
#67 := [trans #63 #65]: #66
#77 := [monotonicity #67 #74]: #76
#80 := [quant-intro #77]: #79
#83 := [monotonicity #80]: #82
#51 := (iff #15 #50)
#48 := (iff #14 #47)
#45 := (iff #13 #42)
#38 := (implies #6 #35)
#43 := (iff #38 #42)
#44 := [rewrite]: #43
#39 := (iff #13 #38)
#36 := (iff #12 #35)
#33 := (= #10 #32)
#34 := [rewrite]: #33
#37 := [monotonicity #34]: #36
#40 := [monotonicity #37]: #39
#46 := [trans #40 #44]: #45
#49 := [quant-intro #46]: #48
#52 := [monotonicity #49]: #51
#85 := [trans #52 #83]: #84
#31 := [asserted]: #15
#86 := [mp #31 #85]: #81
#106 := [mp~ #86 #103]: #101
#107 := [mp #106 #144]: #142
#146 := [not-or-elim #107]: #131
#108 := (not #117)
#145 := [not-or-elim #107]: #108
[th-lemma #145 #146]: false
unsat