RUN: $(magic_sequence_sat)