(set-logic QF_BV)
; benchmark generated from python API
(set-info :status unknown)
(declare-fun q0 () (_ BitVec 8))
(declare-fun r0 () (_ BitVec 8))
(declare-fun q1 () (_ BitVec 8))
(declare-fun r1 () (_ BitVec 8))
(declare-fun q2 () (_ BitVec 8))
(declare-fun r2 () (_ BitVec 8))
(declare-fun q3 () (_ BitVec 8))
(declare-fun r3 () (_ BitVec 8))
(declare-fun q4 () (_ BitVec 8))
(declare-fun r4 () (_ BitVec 8))
(declare-fun q5 () (_ BitVec 8))
(declare-fun r5 () (_ BitVec 8))
(declare-fun q6 () (_ BitVec 8))
(declare-fun r6 () (_ BitVec 8))
(declare-fun q7 () (_ BitVec 8))
(declare-fun r7 () (_ BitVec 8))
(declare-fun q8 () (_ BitVec 8))
(declare-fun r8 () (_ BitVec 8))
(declare-fun q9 () (_ BitVec 8))
(declare-fun r9 () (_ BitVec 8))
(declare-fun q10 () (_ BitVec 8))
(declare-fun r10 () (_ BitVec 8))
(declare-fun q11 () (_ BitVec 8))
(declare-fun r11 () (_ BitVec 8))
(declare-fun q12 () (_ BitVec 8))
(declare-fun r12 () (_ BitVec 8))
(declare-fun q13 () (_ BitVec 8))
(declare-fun r13 () (_ BitVec 8))
(declare-fun q14 () (_ BitVec 8))
(declare-fun r14 () (_ BitVec 8))
(declare-fun q15 () (_ BitVec 8))
(declare-fun r15 () (_ BitVec 8))
(declare-fun q16 () (_ BitVec 8))
(declare-fun r16 () (_ BitVec 8))
(declare-fun q17 () (_ BitVec 8))
(declare-fun r17 () (_ BitVec 8))
(declare-fun q18 () (_ BitVec 8))
(declare-fun r18 () (_ BitVec 8))
(declare-fun q19 () (_ BitVec 8))
(declare-fun r19 () (_ BitVec 8))
(declare-fun q20 () (_ BitVec 8))
(declare-fun r20 () (_ BitVec 8))
(declare-fun q21 () (_ BitVec 8))
(declare-fun r21 () (_ BitVec 8))
(declare-fun q22 () (_ BitVec 8))
(declare-fun r22 () (_ BitVec 8))
(declare-fun q23 () (_ BitVec 8))
(declare-fun r23 () (_ BitVec 8))
(declare-fun q24 () (_ BitVec 8))
(declare-fun r24 () (_ BitVec 8))
(declare-fun q25 () (_ BitVec 8))
(declare-fun r25 () (_ BitVec 8))
(declare-fun q26 () (_ BitVec 8))
(declare-fun r26 () (_ BitVec 8))
(declare-fun q27 () (_ BitVec 8))
(declare-fun r27 () (_ BitVec 8))
(declare-fun q28 () (_ BitVec 8))
(declare-fun r28 () (_ BitVec 8))
(declare-fun q29 () (_ BitVec 8))
(declare-fun r29 () (_ BitVec 8))
(declare-fun q30 () (_ BitVec 8))
(declare-fun r30 () (_ BitVec 8))
(declare-fun q31 () (_ BitVec 8))
(declare-fun r31 () (_ BitVec 8))
(declare-fun q32 () (_ BitVec 8))
(declare-fun r32 () (_ BitVec 8))
(assert
 (bvule q0 (_ bv225 8)))
(assert
 (bvule r0 (_ bv225 8)))
(assert
 (bvule q1 (_ bv225 8)))
(assert
 (bvule r1 (_ bv225 8)))
(assert
 (bvule q2 (_ bv225 8)))
(assert
 (bvule r2 (_ bv225 8)))
(assert
 (bvule q3 (_ bv225 8)))
(assert
 (bvule r3 (_ bv225 8)))
(assert
 (bvule q4 (_ bv225 8)))
(assert
 (bvule r4 (_ bv225 8)))
(assert
 (bvule q5 (_ bv225 8)))
(assert
 (bvule r5 (_ bv225 8)))
(assert
 (bvule q6 (_ bv225 8)))
(assert
 (bvule r6 (_ bv225 8)))
(assert
 (bvule q7 (_ bv225 8)))
(assert
 (bvule r7 (_ bv225 8)))
(assert
 (bvule q8 (_ bv225 8)))
(assert
 (bvule r8 (_ bv225 8)))
(assert
 (bvule q9 (_ bv225 8)))
(assert
 (bvule r9 (_ bv225 8)))
(assert
 (bvule q10 (_ bv225 8)))
(assert
 (bvule r10 (_ bv225 8)))
(assert
 (bvule q11 (_ bv225 8)))
(assert
 (bvule r11 (_ bv225 8)))
(assert
 (bvule q12 (_ bv225 8)))
(assert
 (bvule r12 (_ bv225 8)))
(assert
 (bvule q13 (_ bv225 8)))
(assert
 (bvule r13 (_ bv225 8)))
(assert
 (bvule q14 (_ bv225 8)))
(assert
 (bvule r14 (_ bv225 8)))
(assert
 (bvule q15 (_ bv225 8)))
(assert
 (bvule r15 (_ bv225 8)))
(assert
 (bvule q16 (_ bv225 8)))
(assert
 (bvule r16 (_ bv225 8)))
(assert
 (bvule q17 (_ bv225 8)))
(assert
 (bvule r17 (_ bv225 8)))
(assert
 (bvule q18 (_ bv225 8)))
(assert
 (bvule r18 (_ bv225 8)))
(assert
 (bvule q19 (_ bv225 8)))
(assert
 (bvule r19 (_ bv225 8)))
(assert
 (bvule q20 (_ bv225 8)))
(assert
 (bvule r20 (_ bv225 8)))
(assert
 (bvule q21 (_ bv225 8)))
(assert
 (bvule r21 (_ bv225 8)))
(assert
 (bvule q22 (_ bv225 8)))
(assert
 (bvule r22 (_ bv225 8)))
(assert
 (bvule q23 (_ bv225 8)))
(assert
 (bvule r23 (_ bv225 8)))
(assert
 (bvule q24 (_ bv225 8)))
(assert
 (bvule r24 (_ bv225 8)))
(assert
 (bvule q25 (_ bv225 8)))
(assert
 (bvule r25 (_ bv225 8)))
(assert
 (bvule q26 (_ bv225 8)))
(assert
 (bvule r26 (_ bv225 8)))
(assert
 (bvule q27 (_ bv225 8)))
(assert
 (bvule r27 (_ bv225 8)))
(assert
 (bvule q28 (_ bv225 8)))
(assert
 (bvule r28 (_ bv225 8)))
(assert
 (bvule q29 (_ bv225 8)))
(assert
 (bvule r29 (_ bv225 8)))
(assert
 (bvule q30 (_ bv225 8)))
(assert
 (bvule r30 (_ bv225 8)))
(assert
 (bvule q31 (_ bv225 8)))
(assert
 (bvule r31 (_ bv225 8)))
(assert
 (bvule q32 (_ bv225 8)))
(assert
 (bvule r32 (_ bv225 8)))
(assert
 (let ((?x3482 ((_ zero_extend 24) r32)))
 (let ((?x2266 ((_ zero_extend 24) q32)))
 (let ((?x2252 ((_ zero_extend 24) r31)))
 (let ((?x4862 ((_ zero_extend 24) q31)))
 (let ((?x4475 ((_ zero_extend 24) r30)))
 (let ((?x1878 ((_ zero_extend 24) q30)))
 (let ((?x3724 ((_ zero_extend 24) r29)))
 (let ((?x4772 ((_ zero_extend 24) q29)))
 (let ((?x2817 ((_ zero_extend 24) r28)))
 (let ((?x4103 ((_ zero_extend 24) q28)))
 (let ((?x1364 ((_ zero_extend 24) r27)))
 (let ((?x1982 ((_ zero_extend 24) q27)))
 (let ((?x717 ((_ zero_extend 24) r26)))
 (let ((?x4383 ((_ zero_extend 24) q26)))
 (let ((?x4254 ((_ zero_extend 24) r25)))
 (let ((?x3513 ((_ zero_extend 24) q25)))
 (let ((?x2567 ((_ zero_extend 24) r24)))
 (let ((?x2029 ((_ zero_extend 24) q24)))
 (let ((?x2898 ((_ zero_extend 24) r23)))
 (let ((?x570 ((_ zero_extend 24) q23)))
 (let ((?x4205 ((_ zero_extend 24) r22)))
 (let ((?x2295 ((_ zero_extend 24) q22)))
 (let ((?x913 ((_ zero_extend 24) r21)))
 (let ((?x3543 ((_ zero_extend 24) q21)))
 (let ((?x840 ((_ zero_extend 24) r20)))
 (let ((?x4343 ((_ zero_extend 24) q20)))
 (let ((?x2914 ((_ zero_extend 24) r19)))
 (let ((?x4416 ((_ zero_extend 24) q19)))
 (let ((?x3921 ((_ zero_extend 24) r18)))
 (let ((?x4676 ((_ zero_extend 24) q18)))
 (let ((?x2414 ((_ zero_extend 24) r17)))
 (let ((?x1925 ((_ zero_extend 24) q17)))
 (let ((?x2550 ((_ zero_extend 24) r16)))
 (let ((?x3964 ((_ zero_extend 24) q16)))
 (let ((?x5399 ((_ zero_extend 24) r15)))
 (let ((?x1972 ((_ zero_extend 24) q15)))
 (let ((?x2377 ((_ zero_extend 24) r14)))
 (let ((?x129 ((_ zero_extend 24) q14)))
 (let ((?x1203 ((_ zero_extend 24) r13)))
 (let ((?x4488 ((_ zero_extend 24) q13)))
 (let ((?x76 ((_ zero_extend 24) r12)))
 (let ((?x1813 ((_ zero_extend 24) q12)))
 (let ((?x1762 ((_ zero_extend 24) r11)))
 (let ((?x2749 ((_ zero_extend 24) q11)))
 (let ((?x2124 ((_ zero_extend 24) r10)))
 (let ((?x1708 ((_ zero_extend 24) q10)))
 (let ((?x3979 ((_ zero_extend 24) r9)))
 (let ((?x2452 ((_ zero_extend 24) q9)))
 (let ((?x5406 ((_ zero_extend 24) r8)))
 (let ((?x4021 ((_ zero_extend 24) q8)))
 (let ((?x2960 ((_ zero_extend 24) r7)))
 (let ((?x581 ((_ zero_extend 24) q7)))
 (let ((?x3795 ((_ zero_extend 24) r6)))
 (let ((?x2276 ((_ zero_extend 24) q6)))
 (let ((?x3738 ((_ zero_extend 24) r5)))
 (let ((?x2681 ((_ zero_extend 24) q5)))
 (let ((?x167 ((_ zero_extend 24) r4)))
 (let ((?x4049 ((_ zero_extend 24) q4)))
 (let ((?x5514 ((_ zero_extend 24) r3)))
 (let ((?x4732 ((_ zero_extend 24) q3)))
 (let ((?x4285 ((_ zero_extend 24) r2)))
 (let ((?x3385 ((_ zero_extend 24) q2)))
 (let ((?x3301 ((_ zero_extend 24) r1)))
 (let ((?x2639 ((_ zero_extend 24) q1)))
 (let ((?x3394 (bvadd (bvadd (bvadd (bvadd (_ bv0 32) ((_ zero_extend 24) q0)) ((_ zero_extend 24) r0)) ?x2639) ?x3301)))
 (let ((?x1823 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x3394 ?x3385) ?x4285) ?x4732) ?x5514) ?x4049) ?x167)))
 (let ((?x347 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x1823 ?x2681) ?x3738) ?x2276) ?x3795) ?x581) ?x2960)))
 (let ((?x3845 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x347 ?x4021) ?x5406) ?x2452) ?x3979) ?x1708) ?x2124)))
 (let ((?x3568 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x3845 ?x2749) ?x1762) ?x1813) ?x76) ?x4488) ?x1203)))
 (let ((?x2297 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x3568 ?x129) ?x2377) ?x1972) ?x5399) ?x3964) ?x2550)))
 (let ((?x2397 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x2297 ?x1925) ?x2414) ?x4676) ?x3921) ?x4416) ?x2914)))
 (let ((?x241 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x2397 ?x4343) ?x840) ?x3543) ?x913) ?x2295) ?x4205)))
 (let ((?x239 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x241 ?x570) ?x2898) ?x2029) ?x2567) ?x3513) ?x4254)))
 (let ((?x2332 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x239 ?x4383) ?x717) ?x1982) ?x1364) ?x4103) ?x2817)))
 (let ((?x3094 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x2332 ?x4772) ?x3724) ?x1878) ?x4475) ?x4862) ?x2252)))
 (let ((?x660 (bvadd (bvadd ?x3094 ?x2266) ?x3482)))
 (let ((?x4368 (bvadd (bvadd (bvadd (bvadd (_ bv0 32) (_ bv0 32)) ((_ zero_extend 24) q0)) ((_ zero_extend 24) r0)) ?x2639)))
 (let ((?x608 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x4368 ?x3301) ?x3385) ?x4285) ?x4732) ?x5514) ?x4049)))
 (let ((?x657 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x608 ?x167) ?x2681) ?x3738) ?x2276) ?x3795) ?x581)))
 (let ((?x54 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x657 ?x2960) ?x4021) ?x5406) ?x2452) ?x3979) ?x1708)))
 (let ((?x1860 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x54 ?x2124) ?x2749) ?x1762) ?x1813) ?x76) ?x4488)))
 (let ((?x3559 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x1860 ?x1203) ?x129) ?x2377) ?x1972) ?x5399) ?x3964)))
 (let ((?x3677 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x3559 ?x2550) ?x1925) ?x2414) ?x4676) ?x3921) ?x4416)))
 (let ((?x1055 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x3677 ?x2914) ?x4343) ?x840) ?x3543) ?x913) ?x2295)))
 (let ((?x3150 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x1055 ?x4205) ?x570) ?x2898) ?x2029) ?x2567) ?x3513)))
 (let ((?x3720 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x3150 ?x4254) ?x4383) ?x717) ?x1982) ?x1364) ?x4103)))
 (let ((?x1102 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x3720 ?x2817) ?x4772) ?x3724) ?x1878) ?x4475) ?x4862)))
 (let ((?x785 (bvadd (bvadd (bvadd ?x1102 ?x2252) ?x2266) ?x3482)))
 (and (distinct (bvadd ?x785 (_ bv1 32)) (bvadd (bvadd ?x660 (_ bv1 32)) (_ bv1 32))) true))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)