sat ((((_ to_fp 5 11) RTN (/ 1 1000000)) (fp #b0 #b00000 #b0000010000))) ((((_ to_fp 5 11) RTP (/ 1.2 5)) (fp #b0 #b01100 #b1110101111))) ((((_ to_fp 5 11) RTZ (/ 1.2 3.25)) (fp #b0 #b01101 #b0111101000)))