#2 := false
#5 := 0::real
decl uf_1 :: real
#4 := uf_1
#94 := (<= uf_1 0::real)
#17 := 2::real
#40 := (* 2::real uf_1)
#102 := (<= #40 0::real)
#103 := (>= #40 0::real)
#105 := (not #103)
#104 := (not #102)
#106 := (or #104 #105)
#107 := (not #106)
#88 := (= #40 0::real)
#108 := (iff #88 #107)
#109 := [rewrite]: #108
#16 := 4::real
#11 := (- uf_1)
#10 := (< uf_1 0::real)
#12 := (ite #10 #11 uf_1)
#9 := 1::real
#13 := (< 1::real #12)
#14 := (not #13)
#15 := (or #13 #14)
#18 := (ite #15 4::real 2::real)
#19 := (* #18 uf_1)
#8 := (+ uf_1 uf_1)
#20 := (= #8 #19)
#21 := (not #20)
#22 := (not #21)
#89 := (iff #22 #88)
#70 := (* 4::real uf_1)
#73 := (= #40 #70)
#86 := (iff #73 #88)
#87 := [rewrite]: #86
#84 := (iff #22 #73)
#76 := (not #73)
#79 := (not #76)
#82 := (iff #79 #73)
#83 := [rewrite]: #82
#80 := (iff #22 #79)
#77 := (iff #21 #76)
#74 := (iff #20 #73)
#71 := (= #19 #70)
#68 := (= #18 4::real)
#1 := true
#63 := (ite true 4::real 2::real)
#66 := (= #63 4::real)
#67 := [rewrite]: #66
#64 := (= #18 #63)
#61 := (iff #15 true)
#43 := -1::real
#44 := (* -1::real uf_1)
#47 := (ite #10 #44 uf_1)
#50 := (< 1::real #47)
#53 := (not #50)
#56 := (or #50 #53)
#59 := (iff #56 true)
#60 := [rewrite]: #59
#57 := (iff #15 #56)
#54 := (iff #14 #53)
#51 := (iff #13 #50)
#48 := (= #12 #47)
#45 := (= #11 #44)
#46 := [rewrite]: #45
#49 := [monotonicity #46]: #48
#52 := [monotonicity #49]: #51
#55 := [monotonicity #52]: #54
#58 := [monotonicity #52 #55]: #57
#62 := [trans #58 #60]: #61
#65 := [monotonicity #62]: #64
#69 := [trans #65 #67]: #68
#72 := [monotonicity #69]: #71
#41 := (= #8 #40)
#42 := [rewrite]: #41
#75 := [monotonicity #42 #72]: #74
#78 := [monotonicity #75]: #77
#81 := [monotonicity #78]: #80
#85 := [trans #81 #83]: #84
#90 := [trans #85 #87]: #89
#39 := [asserted]: #22
#91 := [mp #39 #90]: #88
#110 := [mp #91 #109]: #107
#111 := [not-or-elim #110]: #102
#127 := (or #94 #104)
#128 := [th-lemma]: #127
#129 := [unit-resolution #128 #111]: #94
#92 := (>= uf_1 0::real)
#112 := [not-or-elim #110]: #103
#130 := (or #92 #105)
#131 := [th-lemma]: #130
#132 := [unit-resolution #131 #112]: #92
#114 := (not #94)
#113 := (not #92)
#115 := (or #113 #114)
#95 := (and #92 #94)
#98 := (not #95)
#124 := (iff #98 #115)
#116 := (not #115)
#119 := (not #116)
#122 := (iff #119 #115)
#123 := [rewrite]: #122
#120 := (iff #98 #119)
#117 := (iff #95 #116)
#118 := [rewrite]: #117
#121 := [monotonicity #118]: #120
#125 := [trans #121 #123]: #124
#6 := (= uf_1 0::real)
#7 := (not #6)
#99 := (iff #7 #98)
#96 := (iff #6 #95)
#97 := [rewrite]: #96
#100 := [monotonicity #97]: #99
#38 := [asserted]: #7
#101 := [mp #38 #100]: #98
#126 := [mp #101 #125]: #115
[unit-resolution #126 #132 #129]: false
unsat