(set-info :status sat)
(set-option :global-declarations true)
(set-option :pp-variable-subst-norm-bv-ineq true)
(set-option :rewrite-level 0)
(declare-const _x0 (_ BitVec 56))
(check-sat-assuming ( (bvsle #b01111111111111111111111111111111111111111111111111111111 _x0) (bvsle #b01111111111111111111111111111111111111111111111111111111 _x0) (bvsle #b01111111111111111111111111111111111111111111111111111111 _x0) (bvsle #b01111111111111111111111111111111111111111111111111111111 _x0)))