(set-logic QF_BV)
; benchmark generated from python API
(set-info :status unknown)
(declare-fun e0 () (_ BitVec 8))
(declare-fun f0 () (_ BitVec 8))
(declare-fun e1 () (_ BitVec 8))
(declare-fun f1 () (_ BitVec 8))
(declare-fun e2 () (_ BitVec 8))
(declare-fun f2 () (_ BitVec 8))
(declare-fun e3 () (_ BitVec 8))
(declare-fun f3 () (_ BitVec 8))
(declare-fun e4 () (_ BitVec 8))
(declare-fun f4 () (_ BitVec 8))
(declare-fun e5 () (_ BitVec 8))
(declare-fun f5 () (_ BitVec 8))
(declare-fun e6 () (_ BitVec 8))
(declare-fun f6 () (_ BitVec 8))
(declare-fun e7 () (_ BitVec 8))
(declare-fun f7 () (_ BitVec 8))
(declare-fun e8 () (_ BitVec 8))
(declare-fun f8 () (_ BitVec 8))
(declare-fun e9 () (_ BitVec 8))
(declare-fun f9 () (_ BitVec 8))
(declare-fun e10 () (_ BitVec 8))
(declare-fun f10 () (_ BitVec 8))
(declare-fun e11 () (_ BitVec 8))
(declare-fun f11 () (_ BitVec 8))
(declare-fun e12 () (_ BitVec 8))
(declare-fun f12 () (_ BitVec 8))
(declare-fun e13 () (_ BitVec 8))
(declare-fun f13 () (_ BitVec 8))
(declare-fun e14 () (_ BitVec 8))
(declare-fun f14 () (_ BitVec 8))
(declare-fun e15 () (_ BitVec 8))
(declare-fun f15 () (_ BitVec 8))
(declare-fun e16 () (_ BitVec 8))
(declare-fun f16 () (_ BitVec 8))
(declare-fun e17 () (_ BitVec 8))
(declare-fun f17 () (_ BitVec 8))
(declare-fun e18 () (_ BitVec 8))
(declare-fun f18 () (_ BitVec 8))
(declare-fun e19 () (_ BitVec 8))
(declare-fun f19 () (_ BitVec 8))
(declare-fun e20 () (_ BitVec 8))
(declare-fun f20 () (_ BitVec 8))
(declare-fun e21 () (_ BitVec 8))
(declare-fun f21 () (_ BitVec 8))
(declare-fun e22 () (_ BitVec 8))
(declare-fun f22 () (_ BitVec 8))
(declare-fun e23 () (_ BitVec 8))
(declare-fun f23 () (_ BitVec 8))
(declare-fun e24 () (_ BitVec 8))
(declare-fun f24 () (_ BitVec 8))
(declare-fun e25 () (_ BitVec 8))
(declare-fun f25 () (_ BitVec 8))
(declare-fun e26 () (_ BitVec 8))
(declare-fun f26 () (_ BitVec 8))
(declare-fun e27 () (_ BitVec 8))
(declare-fun f27 () (_ BitVec 8))
(declare-fun e28 () (_ BitVec 8))
(declare-fun f28 () (_ BitVec 8))
(declare-fun e29 () (_ BitVec 8))
(declare-fun f29 () (_ BitVec 8))
(declare-fun e30 () (_ BitVec 8))
(declare-fun f30 () (_ BitVec 8))
(declare-fun e31 () (_ BitVec 8))
(declare-fun f31 () (_ BitVec 8))
(assert
 (bvule e0 (_ bv225 8)))
(assert
 (bvule f0 (_ bv225 8)))
(assert
 (bvule e1 (_ bv225 8)))
(assert
 (bvule f1 (_ bv225 8)))
(assert
 (bvule e2 (_ bv225 8)))
(assert
 (bvule f2 (_ bv225 8)))
(assert
 (bvule e3 (_ bv225 8)))
(assert
 (bvule f3 (_ bv225 8)))
(assert
 (bvule e4 (_ bv225 8)))
(assert
 (bvule f4 (_ bv225 8)))
(assert
 (bvule e5 (_ bv225 8)))
(assert
 (bvule f5 (_ bv225 8)))
(assert
 (bvule e6 (_ bv225 8)))
(assert
 (bvule f6 (_ bv225 8)))
(assert
 (bvule e7 (_ bv225 8)))
(assert
 (bvule f7 (_ bv225 8)))
(assert
 (bvule e8 (_ bv225 8)))
(assert
 (bvule f8 (_ bv225 8)))
(assert
 (bvule e9 (_ bv225 8)))
(assert
 (bvule f9 (_ bv225 8)))
(assert
 (bvule e10 (_ bv225 8)))
(assert
 (bvule f10 (_ bv225 8)))
(assert
 (bvule e11 (_ bv225 8)))
(assert
 (bvule f11 (_ bv225 8)))
(assert
 (bvule e12 (_ bv225 8)))
(assert
 (bvule f12 (_ bv225 8)))
(assert
 (bvule e13 (_ bv225 8)))
(assert
 (bvule f13 (_ bv225 8)))
(assert
 (bvule e14 (_ bv225 8)))
(assert
 (bvule f14 (_ bv225 8)))
(assert
 (bvule e15 (_ bv225 8)))
(assert
 (bvule f15 (_ bv225 8)))
(assert
 (bvule e16 (_ bv225 8)))
(assert
 (bvule f16 (_ bv225 8)))
(assert
 (bvule e17 (_ bv225 8)))
(assert
 (bvule f17 (_ bv225 8)))
(assert
 (bvule e18 (_ bv225 8)))
(assert
 (bvule f18 (_ bv225 8)))
(assert
 (bvule e19 (_ bv225 8)))
(assert
 (bvule f19 (_ bv225 8)))
(assert
 (bvule e20 (_ bv225 8)))
(assert
 (bvule f20 (_ bv225 8)))
(assert
 (bvule e21 (_ bv225 8)))
(assert
 (bvule f21 (_ bv225 8)))
(assert
 (bvule e22 (_ bv225 8)))
(assert
 (bvule f22 (_ bv225 8)))
(assert
 (bvule e23 (_ bv225 8)))
(assert
 (bvule f23 (_ bv225 8)))
(assert
 (bvule e24 (_ bv225 8)))
(assert
 (bvule f24 (_ bv225 8)))
(assert
 (bvule e25 (_ bv225 8)))
(assert
 (bvule f25 (_ bv225 8)))
(assert
 (bvule e26 (_ bv225 8)))
(assert
 (bvule f26 (_ bv225 8)))
(assert
 (bvule e27 (_ bv225 8)))
(assert
 (bvule f27 (_ bv225 8)))
(assert
 (bvule e28 (_ bv225 8)))
(assert
 (bvule f28 (_ bv225 8)))
(assert
 (bvule e29 (_ bv225 8)))
(assert
 (bvule f29 (_ bv225 8)))
(assert
 (bvule e30 (_ bv225 8)))
(assert
 (bvule f30 (_ bv225 8)))
(assert
 (bvule e31 (_ bv225 8)))
(assert
 (bvule f31 (_ bv225 8)))
(assert
 (let ((?x13389 (bvadd (bvadd (_ bv0 32) (bvadd ((_ zero_extend 24) e0) ((_ zero_extend 24) f0))) (bvadd ((_ zero_extend 24) e1) ((_ zero_extend 24) f1)))))
 (let ((?x7829 (bvadd (bvadd ?x13389 (bvadd ((_ zero_extend 24) e2) ((_ zero_extend 24) f2))) (bvadd ((_ zero_extend 24) e3) ((_ zero_extend 24) f3)))))
 (let ((?x2397 (bvadd (bvadd ?x7829 (bvadd ((_ zero_extend 24) e4) ((_ zero_extend 24) f4))) (bvadd ((_ zero_extend 24) e5) ((_ zero_extend 24) f5)))))
 (let ((?x5979 (bvadd (bvadd ?x2397 (bvadd ((_ zero_extend 24) e6) ((_ zero_extend 24) f6))) (bvadd ((_ zero_extend 24) e7) ((_ zero_extend 24) f7)))))
 (let ((?x10853 (bvadd (bvadd ?x5979 (bvadd ((_ zero_extend 24) e8) ((_ zero_extend 24) f8))) (bvadd ((_ zero_extend 24) e9) ((_ zero_extend 24) f9)))))
 (let ((?x10588 (bvadd (bvadd ?x10853 (bvadd ((_ zero_extend 24) e10) ((_ zero_extend 24) f10))) (bvadd ((_ zero_extend 24) e11) ((_ zero_extend 24) f11)))))
 (let ((?x8825 (bvadd (bvadd ?x10588 (bvadd ((_ zero_extend 24) e12) ((_ zero_extend 24) f12))) (bvadd ((_ zero_extend 24) e13) ((_ zero_extend 24) f13)))))
 (let ((?x8667 (bvadd (bvadd ?x8825 (bvadd ((_ zero_extend 24) e14) ((_ zero_extend 24) f14))) (bvadd ((_ zero_extend 24) e15) ((_ zero_extend 24) f15)))))
 (let ((?x1965 (bvadd (bvadd ?x8667 (bvadd ((_ zero_extend 24) e16) ((_ zero_extend 24) f16))) (bvadd ((_ zero_extend 24) e17) ((_ zero_extend 24) f17)))))
 (let ((?x5575 (bvadd (bvadd ?x1965 (bvadd ((_ zero_extend 24) e18) ((_ zero_extend 24) f18))) (bvadd ((_ zero_extend 24) e19) ((_ zero_extend 24) f19)))))
 (let ((?x6285 (bvadd (bvadd ?x5575 (bvadd ((_ zero_extend 24) e20) ((_ zero_extend 24) f20))) (bvadd ((_ zero_extend 24) e21) ((_ zero_extend 24) f21)))))
 (let ((?x375 (bvadd (bvadd ?x6285 (bvadd ((_ zero_extend 24) e22) ((_ zero_extend 24) f22))) (bvadd ((_ zero_extend 24) e23) ((_ zero_extend 24) f23)))))
 (let ((?x5977 (bvadd (bvadd ?x375 (bvadd ((_ zero_extend 24) e24) ((_ zero_extend 24) f24))) (bvadd ((_ zero_extend 24) e25) ((_ zero_extend 24) f25)))))
 (let ((?x7342 (bvadd (bvadd ?x5977 (bvadd ((_ zero_extend 24) e26) ((_ zero_extend 24) f26))) (bvadd ((_ zero_extend 24) e27) ((_ zero_extend 24) f27)))))
 (let ((?x25 (bvadd (bvadd ?x7342 (bvadd ((_ zero_extend 24) e28) ((_ zero_extend 24) f28))) (bvadd ((_ zero_extend 24) e29) ((_ zero_extend 24) f29)))))
 (let ((?x3944 (bvadd (bvadd ?x25 (bvadd ((_ zero_extend 24) e30) ((_ zero_extend 24) f30))) (bvadd ((_ zero_extend 24) e31) ((_ zero_extend 24) f31)))))
 (let ((?x10277 (bvadd (bvand (concat f29 f28) (_ bv255 16)) (bvlshr (concat f29 f28) (_ bv8 16)))))
 (let ((?x652 (bvadd (bvand (concat f13 f12) (_ bv255 16)) (bvlshr (concat f13 f12) (_ bv8 16)))))
 (let ((?x9063 (bvadd (bvand (concat f31 f30) (_ bv255 16)) (bvlshr (concat f31 f30) (_ bv8 16)))))
 (let ((?x7744 (bvadd (bvand (concat f15 f14) (_ bv255 16)) (bvlshr (concat f15 f14) (_ bv8 16)))))
 (let ((?x4858 (concat (bvadd (bvadd (_ bv0 16) ?x7744) ?x9063) (bvadd (bvadd (_ bv0 16) ?x652) ?x10277))))
 (let ((?x4924 (bvadd (bvand (concat e29 e28) (_ bv255 16)) (bvlshr (concat e29 e28) (_ bv8 16)))))
 (let ((?x6923 (bvadd (bvand (concat e13 e12) (_ bv255 16)) (bvlshr (concat e13 e12) (_ bv8 16)))))
 (let ((?x3710 (bvadd (bvand (concat e31 e30) (_ bv255 16)) (bvlshr (concat e31 e30) (_ bv8 16)))))
 (let ((?x11400 (bvadd (bvand (concat e15 e14) (_ bv255 16)) (bvlshr (concat e15 e14) (_ bv8 16)))))
 (let ((?x2073 (concat (bvadd (bvadd (_ bv0 16) ?x11400) ?x3710) (bvadd (bvadd (_ bv0 16) ?x6923) ?x4924))))
 (let ((?x12229 (bvadd (bvadd (bvand ?x2073 (_ bv65535 32)) (bvlshr ?x2073 (_ bv16 32))) (bvand ?x4858 (_ bv65535 32)))))
 (let ((?x5391 (bvadd (bvand (concat f25 f24) (_ bv255 16)) (bvlshr (concat f25 f24) (_ bv8 16)))))
 (let ((?x12048 (bvadd (bvand (concat f9 f8) (_ bv255 16)) (bvlshr (concat f9 f8) (_ bv8 16)))))
 (let ((?x4889 (bvadd (bvand (concat f27 f26) (_ bv255 16)) (bvlshr (concat f27 f26) (_ bv8 16)))))
 (let ((?x13529 (bvadd (bvand (concat f11 f10) (_ bv255 16)) (bvlshr (concat f11 f10) (_ bv8 16)))))
 (let ((?x9645 (concat (bvadd (bvadd (_ bv0 16) ?x13529) ?x4889) (bvadd (bvadd (_ bv0 16) ?x12048) ?x5391))))
 (let ((?x6694 (bvadd (bvand (concat e25 e24) (_ bv255 16)) (bvlshr (concat e25 e24) (_ bv8 16)))))
 (let ((?x2326 (bvadd (bvand (concat e9 e8) (_ bv255 16)) (bvlshr (concat e9 e8) (_ bv8 16)))))
 (let ((?x12724 (bvadd (bvand (concat e27 e26) (_ bv255 16)) (bvlshr (concat e27 e26) (_ bv8 16)))))
 (let ((?x4864 (bvadd (bvand (concat e11 e10) (_ bv255 16)) (bvlshr (concat e11 e10) (_ bv8 16)))))
 (let ((?x6092 (concat (bvadd (bvadd (_ bv0 16) ?x4864) ?x12724) (bvadd (bvadd (_ bv0 16) ?x2326) ?x6694))))
 (let ((?x12518 (bvadd (bvadd (bvand ?x6092 (_ bv65535 32)) (bvlshr ?x6092 (_ bv16 32))) (bvand ?x9645 (_ bv65535 32)))))
 (let ((?x5583 (bvadd (bvand (concat f21 f20) (_ bv255 16)) (bvlshr (concat f21 f20) (_ bv8 16)))))
 (let ((?x7720 (bvadd (bvand (concat f5 f4) (_ bv255 16)) (bvlshr (concat f5 f4) (_ bv8 16)))))
 (let ((?x12932 (bvadd (bvand (concat f23 f22) (_ bv255 16)) (bvlshr (concat f23 f22) (_ bv8 16)))))
 (let ((?x12072 (bvadd (bvand (concat f7 f6) (_ bv255 16)) (bvlshr (concat f7 f6) (_ bv8 16)))))
 (let ((?x13470 (concat (bvadd (bvadd (_ bv0 16) ?x12072) ?x12932) (bvadd (bvadd (_ bv0 16) ?x7720) ?x5583))))
 (let ((?x10468 (bvadd (bvand (concat e21 e20) (_ bv255 16)) (bvlshr (concat e21 e20) (_ bv8 16)))))
 (let ((?x9284 (bvadd (bvand (concat e5 e4) (_ bv255 16)) (bvlshr (concat e5 e4) (_ bv8 16)))))
 (let ((?x12088 (bvadd (bvand (concat e23 e22) (_ bv255 16)) (bvlshr (concat e23 e22) (_ bv8 16)))))
 (let ((?x2597 (bvadd (bvand (concat e7 e6) (_ bv255 16)) (bvlshr (concat e7 e6) (_ bv8 16)))))
 (let ((?x13946 (concat (bvadd (bvadd (_ bv0 16) ?x2597) ?x12088) (bvadd (bvadd (_ bv0 16) ?x9284) ?x10468))))
 (let ((?x6160 (bvadd (bvadd (bvand ?x13946 (_ bv65535 32)) (bvlshr ?x13946 (_ bv16 32))) (bvand ?x13470 (_ bv65535 32)))))
 (let ((?x1903 (bvadd (bvand (concat f17 f16) (_ bv255 16)) (bvlshr (concat f17 f16) (_ bv8 16)))))
 (let ((?x10660 (bvadd (bvand (concat f1 f0) (_ bv255 16)) (bvlshr (concat f1 f0) (_ bv8 16)))))
 (let ((?x8021 (bvadd (bvand (concat f19 f18) (_ bv255 16)) (bvlshr (concat f19 f18) (_ bv8 16)))))
 (let ((?x4750 (bvadd (bvand (concat f3 f2) (_ bv255 16)) (bvlshr (concat f3 f2) (_ bv8 16)))))
 (let ((?x3555 (concat (bvadd (bvadd (_ bv0 16) ?x4750) ?x8021) (bvadd (bvadd (_ bv0 16) ?x10660) ?x1903))))
 (let ((?x6169 (bvadd (bvand (concat e17 e16) (_ bv255 16)) (bvlshr (concat e17 e16) (_ bv8 16)))))
 (let ((?x4677 (bvadd (bvand (concat e1 e0) (_ bv255 16)) (bvlshr (concat e1 e0) (_ bv8 16)))))
 (let ((?x10238 (bvadd (bvand (concat e19 e18) (_ bv255 16)) (bvlshr (concat e19 e18) (_ bv8 16)))))
 (let ((?x7390 (bvadd (bvand (concat e3 e2) (_ bv255 16)) (bvlshr (concat e3 e2) (_ bv8 16)))))
 (let ((?x3676 (concat (bvadd (bvadd (_ bv0 16) ?x7390) ?x10238) (bvadd (bvadd (_ bv0 16) ?x4677) ?x6169))))
 (let ((?x11010 (bvadd (bvadd (bvand ?x3676 (_ bv65535 32)) (bvlshr ?x3676 (_ bv16 32))) (bvand ?x3555 (_ bv65535 32)))))
 (let ((?x12491 (bvadd (bvadd ?x11010 (bvlshr ?x3555 (_ bv16 32))) (bvadd ?x6160 (bvlshr ?x13470 (_ bv16 32))))))
 (let ((?x5723 (bvadd (bvadd ?x12491 (bvadd ?x12518 (bvlshr ?x9645 (_ bv16 32)))) (bvadd ?x12229 (bvlshr ?x4858 (_ bv16 32))))))
 (let ((?x10482 (bvadd (_ bv0 32) (bvadd (_ bv0 32) ?x5723))))
 (and (distinct (bvadd ?x10482 (_ bv1 32)) (bvadd (bvadd ?x3944 (_ bv1 32)) (_ bv1 32))) true)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)