(set-logic QF_BV)
(declare-fun v1 () (_ BitVec 1))
(declare-fun v2 () (_ BitVec 1))
(declare-fun v3 () (_ BitVec 1))
(declare-fun v4 () (_ BitVec 9))
(declare-fun v5 () (_ BitVec 1))
(declare-fun v6 () (_ BitVec 9))
(define-fun $e7 () (_ BitVec 5) (_ bv30 5))
(define-fun $e8 () (_ BitVec 4) (_ bv0 4))
(define-fun $e9 () (_ BitVec 5) (_ bv2 5))
(define-fun $e10 () (_ BitVec 1) (bvand v2 v3))
(define-fun $e11 () (_ BitVec 1) (ite (= v4 v6) #b1 #b0))
(define-fun $e12 () (_ BitVec 1) (bvand v3 $e11))
(define-fun $e13 () (_ BitVec 1) (bvand (bvnot $e10) (bvnot $e12)))
(define-fun $e14 () (_ BitVec 1) (bvand (bvnot v1) $e13))
(define-fun $e15 () (_ BitVec 5) (concat $e8 v5))
(define-fun $e16 () (_ BitVec 5) (bvadd (bvnot $e7) (bvnot $e15)))
(define-fun $e17 () (_ BitVec 5) (bvadd (bvnot $e7) (bvnot $e16)))
(define-fun $e18 () (_ BitVec 1) ((_ extract 4 4) $e17))
(define-fun $e19 () (_ BitVec 1) ((_ extract 4 4) $e16))
(define-fun $e20 () (_ BitVec 1) (bvand $e18 (bvnot $e19)))
(define-fun $e21 () (_ BitVec 1) (bvand (bvnot $e18) (bvnot $e19)))
(define-fun $e22 () (_ BitVec 4) ((_ extract 3 0) $e17))
(define-fun $e23 () (_ BitVec 4) ((_ extract 3 0) $e16))
(define-fun $e24 () (_ BitVec 1) (ite (bvult $e22 $e23) #b1 #b0))
(define-fun $e25 () (_ BitVec 1) (bvand $e21 $e24))
(define-fun $e26 () (_ BitVec 1) (bvand $e18 $e19))
(define-fun $e27 () (_ BitVec 1) (bvand $e24 $e26))
(define-fun $e28 () (_ BitVec 1) (bvand (bvnot $e25) (bvnot $e27)))
(define-fun $e29 () (_ BitVec 1) (bvand (bvnot $e20) $e28))
(define-fun $e30 () (_ BitVec 1) (bvand $e14 (bvnot $e29)))
(define-fun $e31 () (_ BitVec 5) (bvadd $e9 (bvnot $e15)))
(define-fun $e32 () (_ BitVec 1) ((_ extract 4 4) $e31))
(define-fun $e33 () (_ BitVec 1) (ite (= v5 $e32) #b1 #b0))
(assert (not (= (bvnot $e30) #b0)))
(assert (not (= $e33 #b0)))
(check-sat)
(exit)