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

adopting Sequences

#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