#2 := false

 #4 := 0::int

 decl ?x1!0 :: int

 #78 := ?x1!0

 #83 := (<= ?x1!0 0::int)

 #146 := (not #83)

 #155 := [hypothesis]: #83

 #7 := 1::int

 #81 := (>= ?x1!0 1::int)

 #82 := (not #81)

 #156 := (or #82 #146)

 #157 := [th-lemma]: #156

 #158 := [unit-resolution #157 #155]: #82

 #159 := (or #146 #81)

 #49 := -1::int

 #79 := (<= ?x1!0 -1::int)

 #80 := (not #79)

 #84 := (ite #83 #82 #80)

 #85 := (not #84)

 #5 := (:var 0 int)

 #50 := (<= #5 -1::int)

 #51 := (not #50)

 #55 := (>= #5 1::int)

 #54 := (not #55)

 #45 := (<= #5 0::int)

 #61 := (ite #45 #54 #51)

 #66 := (forall (vars (?x1 int)) #61)

 #69 := (not #66)

 #86 := (~ #69 #85)

 #87 := [sk]: #86

 #10 := (< #5 1::int)

 #8 := (+ #5 1::int)

 #9 := (< 0::int #8)

 #6 := (< 0::int #5)

 #11 := (ite #6 #9 #10)

 #12 := (forall (vars (?x1 int)) #11)

 #13 := (not #12)

 #72 := (iff #13 #69)

 #30 := (+ 1::int #5)

 #33 := (< 0::int #30)

 #36 := (ite #6 #33 #10)

 #39 := (forall (vars (?x1 int)) #36)

 #42 := (not #39)

 #70 := (iff #42 #69)

 #67 := (iff #39 #66)

 #64 := (iff #36 #61)

 #46 := (not #45)

 #58 := (ite #46 #51 #54)

 #62 := (iff #58 #61)

 #63 := [rewrite]: #62

 #59 := (iff #36 #58)

 #56 := (iff #10 #54)

 #57 := [rewrite]: #56

 #52 := (iff #33 #51)

 #53 := [rewrite]: #52

 #47 := (iff #6 #46)

 #48 := [rewrite]: #47

 #60 := [monotonicity #48 #53 #57]: #59

 #65 := [trans #60 #63]: #64

 #68 := [quant-intro #65]: #67

 #71 := [monotonicity #68]: #70

 #43 := (iff #13 #42)

 #40 := (iff #12 #39)

 #37 := (iff #11 #36)

 #34 := (iff #9 #33)

 #31 := (= #8 #30)

 #32 := [rewrite]: #31

 #35 := [monotonicity #32]: #34

 #38 := [monotonicity #35]: #37

 #41 := [quant-intro #38]: #40

 #44 := [monotonicity #41]: #43

 #73 := [trans #44 #71]: #72

 #29 := [asserted]: #13

 #74 := [mp #29 #73]: #69

 #90 := [mp~ #74 #87]: #85

 #151 := (or #84 #146 #81)

 #152 := [def-axiom]: #151

 #160 := [unit-resolution #152 #90]: #159

 #161 := [unit-resolution #160 #158 #155]: false

 #162 := [lemma #161]: #146

 #163 := (or #80 #83)

 #164 := [th-lemma]: #163

 #165 := [unit-resolution #164 #162]: #80

 #166 := (or #83 #79)

 #153 := (or #84 #83 #79)

 #154 := [def-axiom]: #153

 #167 := [unit-resolution #154 #90]: #166

 [unit-resolution #167 #165 #162]: false

 unsat