(assert (= x0_minus 0))
(assert (= x0_plus 0))
(assert (= x10_minus 43))
(assert (= x10_plus 0))
(assert (= x11_minus 54))
(assert (= x11_plus 0))
(assert (= x12_minus 47))
(assert (= x12_plus 0))
(assert (= x13_minus 0))
(assert (= x13_plus 44))
(assert (= x14_minus 0))
(assert (= x14_plus 17))
(assert (= x1_minus 36))
(assert (= x1_plus 0))
(assert (= x2_minus 0))
(assert (= x2_plus 44))
(assert (= x3_minus 41))
(assert (= x3_plus 0))
(assert (= x4_minus 0))
(assert (= x4_plus 20))
(assert (= x5_minus 31))
(assert (= x5_plus 0))
(assert (= x6_minus 19))
(assert (= x6_plus 0))
(assert (= x7_minus 61))
(assert (= x7_plus 0))
(assert (= x8_minus 23))
(assert (= x8_plus 0))
(assert (= x9_minus 0))
(assert (= x9_plus 12))