43550507f510d81bc4fb9ef8c1fd14424eaa9070 37 0
#2 := false
#10 := 0::Int
decl f3 :: Int
#7 := f3
#12 := (<= f3 0::Int)
#54 := (not #12)
decl f4 :: Int
#8 := f4
#13 := (<= f4 0::Int)
#9 := (* f3 f4)
#11 := (<= #9 0::Int)
#37 := (not #11)
#44 := (or #37 #12 #13)
#47 := (not #44)
#14 := (or #12 #13)
#15 := (implies #11 #14)
#16 := (not #15)
#50 := (iff #16 #47)
#38 := (or #37 #14)
#41 := (not #38)
#48 := (iff #41 #47)
#45 := (iff #38 #44)
#46 := [rewrite]: #45
#49 := [monotonicity #46]: #48
#42 := (iff #16 #41)
#39 := (iff #15 #38)
#40 := [rewrite]: #39
#43 := [monotonicity #40]: #42
#51 := [trans #43 #49]: #50
#36 := [asserted]: #16
#52 := [mp #36 #51]: #47
#55 := [not-or-elim #52]: #54
#56 := (not #13)
#57 := [not-or-elim #52]: #56
#53 := [not-or-elim #52]: #11
[th-lemma arith farkas 1 1 1 #53 #57 #55]: false
unsat