(assert (= x19_plus 0))
(assert (= x19_minus 0))
(assert (= x18_plus 0))
(assert (= x18_minus 0))
(assert (= x17_plus 0))
(assert (= x17_minus 0))
(assert (= x16_plus 1))
(assert (= x16_minus 0))
(assert (= x12_plus 0))
(assert (= x12_minus 10))
(assert (= x8_plus 0))
(assert (= x8_minus 0))
(assert (= x7_plus 13))
(assert (= x7_minus 0))
(assert (= x4_plus 0))
(assert (= x4_minus 32))
(assert (= x3_plus 28))
(assert (= x3_minus 0))
(assert (= x2_plus 0))
(assert (= x2_minus 36))
(assert (= x13_plus 0))
(assert (= x13_minus 30))
(assert (= x11_plus 0))
(assert (= x11_minus 4))
(assert (= x10_plus 0))
(assert (= x10_minus 0))
(assert (= x9_plus 0))
(assert (= x9_minus 8))
(assert (= x6_plus 0))
(assert (= x6_minus 18))
(assert (= x15_plus 40))
(assert (= x15_minus 0))
(assert (= x1_plus 0))
(assert (= x1_minus 3))
(assert (= x5_plus 33))
(assert (= x5_minus 0))
(assert (= x0_plus 0))
(assert (= x0_minus 24))
(assert (= x14_plus 0))
(assert (= x14_minus 6))