(assert (>= |CELL_actual_input_0_0_0| (/ 3152519739159347 4503599627370496)))
(assert (< |CELL_actual_input_0_0_0| (/ 5404319552844595 18014398509481984)))
(assert (>= |CELL_actual_input_0_0_1| (/ 3602879701896397 9007199254740992)))
(assert (< |CELL_actual_input_0_0_1| (/ 1 1)))
(assert (< |CELL_actual_input_0_0_2| (/ 1 4)))
(assert (>= |CELL_actual_input_0_0_2| (/ 0 1)))
(check-sat)
(get-value (|CELL_actual_input_0_0_0|))
(get-value (|CELL_actual_input_0_0_1|))
(get-value (|CELL_actual_input_0_0_2|))
(get-value (|CELL_actual_output_0_0_0|))