#2 := false
decl up_1 :: bool
#4 := up_1
#1 := true
#5 := (and up_1 true)
#6 := (iff #5 up_1)
#7 := (not #6)
#37 := (iff #7 false)
#32 := (not true)
#35 := (iff #32 false)
#36 := [rewrite]: #35
#33 := (iff #7 #32)
#30 := (iff #6 true)
#25 := (iff up_1 up_1)
#28 := (iff #25 true)
#29 := [rewrite]: #28
#26 := (iff #6 #25)
#24 := [rewrite]: #6
#27 := [monotonicity #24]: #26
#31 := [trans #27 #29]: #30
#34 := [monotonicity #31]: #33
#38 := [trans #34 #36]: #37
#23 := [asserted]: #7
[mp #23 #38]: false
unsat