(set-logic ALL) (declare-const ui_1 Int) (assert ( exists ((iuqv0 Int)) ( forall ((ieqv0 Int)) ( <= (div (+ iuqv0 109) (div ieqv0 (- 446))) (mod (mod 65308 ui_1) 24) )) )) (check-sat)