#2 := false
#6 := 5::int
#4 := 2::int
#5 := (+ 2::int 2::int)
#7 := (= #5 5::int)
#8 := (not #7)
#9 := (not #8)
#48 := (iff #9 false)
#1 := true
#43 := (not true)
#46 := (iff #43 false)
#47 := [rewrite]: #46
#44 := (iff #9 #43)
#41 := (iff #8 true)
#36 := (not false)
#39 := (iff #36 true)
#40 := [rewrite]: #39
#37 := (iff #8 #36)
#34 := (iff #7 false)
#26 := 4::int
#29 := (= 4::int 5::int)
#32 := (iff #29 false)
#33 := [rewrite]: #32
#30 := (iff #7 #29)
#27 := (= #5 4::int)
#28 := [rewrite]: #27
#31 := [monotonicity #28]: #30
#35 := [trans #31 #33]: #34
#38 := [monotonicity #35]: #37
#42 := [trans #38 #40]: #41
#45 := [monotonicity #42]: #44
#49 := [trans #45 #47]: #48
#25 := [asserted]: #9
[mp #25 #49]: false
unsat