adapted Function_Lib (cf. b8cdd3d73022);
#2 := false
#6 := 0::int
decl uf_1 :: (-> bv[2] int)
#4 := bv[0:2]
#5 := (uf_1 bv[0:2])
#225 := (<= #5 0::int)
#311 := (not #225)
#20 := (:var 0 bv[2])
#21 := (uf_1 #20)
#640 := (pattern #21)
#54 := (<= #21 0::int)
#55 := (not #54)
#641 := (forall (vars (?x1 bv[2])) (:pat #640) #55)
#58 := (forall (vars (?x1 bv[2])) #55)
#644 := (iff #58 #641)
#642 := (iff #55 #55)
#643 := [refl]: #642
#645 := [quant-intro #643]: #644
#113 := (~ #58 #58)
#115 := (~ #55 #55)
#116 := [refl]: #115
#114 := [nnf-pos #116]: #113
#22 := (< 0::int #21)
#23 := (forall (vars (?x1 bv[2])) #22)
#59 := (iff #23 #58)
#56 := (iff #22 #55)
#57 := [rewrite]: #56
#60 := [quant-intro #57]: #59
#51 := [asserted]: #23
#61 := [mp #51 #60]: #58
#111 := [mp~ #61 #114]: #58
#646 := [mp #111 #645]: #641
#227 := (not #641)
#313 := (or #227 #311)
#304 := [quant-inst]: #313
#635 := [unit-resolution #304 #646]: #311
#7 := (= #5 0::int)
#47 := [asserted]: #7
#638 := (not #7)
#633 := (or #638 #225)
#639 := [th-lemma]: #633
[unit-resolution #639 #47 #635]: false
unsat