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

+#2 := false
+#4 := 2::int
+decl ?x1!1 :: int
+#85 := ?x1!1
+decl ?x2!0 :: int
+#84 := ?x2!0
+#101 := (+ ?x2!0 ?x1!1)
+#107 := (>= #101 2::int)
+#113 := (<= #101 2::int)
+#116 := (not #113)
+#110 := (not #107)
+#104 := (= #101 2::int)
+#119 := (or #104 #110 #116)
+#122 := (not #119)
+#86 := (+ ?x1!1 ?x2!0)
+#87 := (<= #86 2::int)
+#88 := (not #87)
+#89 := (>= #86 2::int)
+#90 := (not #89)
+#91 := (= #86 2::int)
+#92 := (or #91 #90 #88)
+#93 := (not #92)
+#123 := (iff #93 #122)
+#120 := (iff #92 #119)
+#117 := (iff #88 #116)
+#114 := (iff #87 #113)
+#102 := (= #86 #101)
+#103 := [rewrite]: #102
+#115 := [monotonicity #103]: #114
+#118 := [monotonicity #115]: #117
+#111 := (iff #90 #110)
+#108 := (iff #89 #107)
+#109 := [monotonicity #103]: #108
+#112 := [monotonicity #109]: #111
+#105 := (iff #91 #104)
+#106 := [monotonicity #103]: #105
+#121 := [monotonicity #106 #112 #118]: #120
+#124 := [monotonicity #121]: #123
+#6 := (:var 0 int)
+#5 := (:var 1 int)
+#7 := (+ #5 #6)
+#56 := (<= #7 2::int)
+#58 := (not #56)
+#54 := (>= #7 2::int)
+#51 := (not #54)
+#9 := (= #7 2::int)
+#67 := (or #9 #51 #58)
+#72 := (forall (vars (?x1 int) (?x2 int)) #67)
+#75 := (not #72)
+#94 := (~ #75 #93)
+#95 := [sk]: #94
+#10 := (< #7 2::int)
+#11 := (or #9 #10)
+#8 := (< 2::int #7)
+#12 := (or #8 #11)
+#13 := (forall (vars (?x1 int) (?x2 int)) #12)
+#14 := (not #13)
+#78 := (iff #14 #75)
+#31 := (= 2::int #7)
+#37 := (or #10 #31)
+#42 := (or #8 #37)
+#45 := (forall (vars (?x1 int) (?x2 int)) #42)
+#48 := (not #45)
+#76 := (iff #48 #75)
+#73 := (iff #45 #72)
+#70 := (iff #42 #67)
+#61 := (or #51 #9)
+#64 := (or #58 #61)
+#68 := (iff #64 #67)
+#69 := [rewrite]: #68
+#65 := (iff #42 #64)
+#62 := (iff #37 #61)
+#55 := (iff #31 #9)
+#57 := [rewrite]: #55
+#53 := (iff #10 #51)
+#52 := [rewrite]: #53
+#63 := [monotonicity #52 #57]: #62
+#59 := (iff #8 #58)
+#60 := [rewrite]: #59
+#66 := [monotonicity #60 #63]: #65
+#71 := [trans #66 #69]: #70
+#74 := [quant-intro #71]: #73
+#77 := [monotonicity #74]: #76
+#49 := (iff #14 #48)
+#46 := (iff #13 #45)
+#43 := (iff #12 #42)
+#40 := (iff #11 #37)
+#34 := (or #31 #10)
+#38 := (iff #34 #37)
+#39 := [rewrite]: #38
+#35 := (iff #11 #34)
+#32 := (iff #9 #31)
+#33 := [rewrite]: #32
+#36 := [monotonicity #33]: #35
+#41 := [trans #36 #39]: #40
+#44 := [monotonicity #41]: #43
+#47 := [quant-intro #44]: #46
+#50 := [monotonicity #47]: #49
+#79 := [trans #50 #77]: #78
+#30 := [asserted]: #14
+#80 := [mp #30 #79]: #75
+#98 := [mp~ #80 #95]: #93
+#99 := [mp #98 #124]: #122
+#126 := [not-or-elim #99]: #107
+#100 := (not #104)
+#125 := [not-or-elim #99]: #100
+#127 := [not-or-elim #99]: #113
+#183 := (or #104 #116 #110)
+#184 := [th-lemma]: #183
+[unit-resolution #184 #127 #125 #126]: false
+unsat