opd 2221230822094041230a4142
(((= (sha256 x0) x1)) (reduce x1 x2))
