My did my numbers wrong. 0b1111 is definitely not 13. Not under normal encodings, not with the -1 OP_RUN bias. Bro what.