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

+#2 := false
+#104 := -1::int
+decl ?x1!1 :: int
+#86 := ?x1!1
+#106 := -4::int
+#107 := (* -4::int ?x1!1)
+decl ?x2!0 :: int
+#85 := ?x2!0
+#7 := 6::int
+#105 := (* 6::int ?x2!0)
+#108 := (+ #105 #107)
+#168 := (<= #108 -1::int)
+#109 := (= #108 -1::int)
+#12 := 1::int
+#33 := -6::int
+#87 := (* -6::int ?x2!0)
+#4 := 4::int
+#88 := (* 4::int ?x1!1)
+#89 := (+ #88 #87)
+#90 := (= #89 1::int)
+#112 := (iff #90 #109)
+#98 := (+ #87 #88)
+#101 := (= #98 1::int)
+#110 := (iff #101 #109)
+#111 := [rewrite]: #110
+#102 := (iff #90 #101)
+#99 := (= #89 #98)
+#100 := [rewrite]: #99
+#103 := [monotonicity #100]: #102
+#113 := [trans #103 #111]: #112
+#53 := (:var 0 int)
+#54 := (* -6::int #53)
+#9 := (:var 1 int)
+#55 := (* 4::int #9)
+#56 := (+ #55 #54)
+#76 := (= #56 1::int)
+#74 := (exists (vars (?x1 int) (?x2 int)) #76)
+#91 := (~ #74 #90)
+#92 := [sk]: #91
+#8 := (- 6::int)
+#10 := (* #8 #9)
+#5 := (:var 2 int)
+#6 := (* 4::int #5)
+#11 := (+ #6 #10)
+#13 := (= #11 1::int)
+#14 := (exists (vars (?x1 int) (?x2 int) (?x3 int)) #13)
+#15 := (not #14)
+#16 := (not #15)
+#79 := (iff #16 #74)
+#57 := (= 1::int #56)
+#58 := (exists (vars (?x1 int) (?x2 int)) #57)
+#77 := (iff #58 #74)
+#75 := (iff #57 #76)
+#73 := [rewrite]: #75
+#78 := [quant-intro #73]: #77
+#71 := (iff #16 #58)
+#63 := (not #58)
+#66 := (not #63)
+#69 := (iff #66 #58)
+#70 := [rewrite]: #69
+#67 := (iff #16 #66)
+#64 := (iff #15 #63)
+#61 := (iff #14 #58)
+#36 := (* -6::int #9)
+#39 := (+ #6 #36)
+#45 := (= 1::int #39)
+#50 := (exists (vars (?x1 int) (?x2 int) (?x3 int)) #45)
+#59 := (iff #50 #58)
+#60 := [elim-unused]: #59
+#51 := (iff #14 #50)
+#48 := (iff #13 #45)
+#42 := (= #39 1::int)
+#46 := (iff #42 #45)
+#47 := [rewrite]: #46
+#43 := (iff #13 #42)
+#40 := (= #11 #39)
+#37 := (= #10 #36)
+#34 := (= #8 -6::int)
+#35 := [rewrite]: #34
+#38 := [monotonicity #35]: #37
+#41 := [monotonicity #38]: #40
+#44 := [monotonicity #41]: #43
+#49 := [trans #44 #47]: #48
+#52 := [quant-intro #49]: #51
+#62 := [trans #52 #60]: #61
+#65 := [monotonicity #62]: #64
+#68 := [monotonicity #65]: #67
+#72 := [trans #68 #70]: #71
+#80 := [trans #72 #78]: #79
+#32 := [asserted]: #16
+#81 := [mp #32 #80]: #74
+#95 := [mp~ #81 #92]: #90
+#96 := [mp #95 #113]: #109
+#170 := (not #109)
+#171 := (or #170 #168)
+#172 := [th-lemma]: #171
+#173 := [unit-resolution #172 #96]: #168
+#169 := (>= #108 -1::int)
+#174 := (or #170 #169)
+#175 := [th-lemma]: #174
+#176 := [unit-resolution #175 #96]: #169
+[th-lemma #176 #173]: false
+unsat