(assert (= x0_minus 0))
(assert (= x0_plus 0))
(assert (= x10_minus 0))
(assert (= x10_plus 0))
(assert (= x11_minus 0))
(assert (= x11_plus 0))
(assert (= x12_minus 0))
(assert (= x12_plus 0))
(assert (= x13_minus 0))
(assert (= x13_plus 0))
(assert (= x14_minus 0))
(assert (= x14_plus 0))
(assert (= x15_minus 0))
(assert (= x15_plus 0))
(assert (= x16_minus 0))
(assert (= x16_plus 0))
(assert (= x17_minus 0))
(assert (= x17_plus 0))
(assert (= x18_minus 0))
(assert (= x18_plus 0))
(assert (= x19_minus 0))
(assert (= x19_plus 0))
(assert (= x1_minus 0))
(assert (= x1_plus 0))
(assert (= x20_minus 0))
(assert (= x20_plus 0))
(assert (= x21_minus 0))
(assert (= x21_plus 0))
(assert (= x22_minus 0))
(assert (= x22_plus 0))
(assert (= x23_minus 0))
(assert (= x23_plus 0))
(assert (= x24_minus 0))
(assert (= x24_plus 0))
(assert (= x25_minus 0))
(assert (= x25_plus 0))
(assert (= x26_minus 0))
(assert (= x26_plus 0))
(assert (= x27_minus 0))
(assert (= x27_plus 0))
(assert (= x28_minus 0))
(assert (= x28_plus 0))
(assert (= x29_minus 0))
(assert (= x29_plus 0))
(assert (= x2_minus 0))
(assert (= x2_plus 0))
(assert (= x30_minus 0))
(assert (= x30_plus 0))
(assert (= x31_minus 0))
(assert (= x31_plus 0))
(assert (= x32_minus 0))
(assert (= x32_plus 0))
(assert (= x33_minus 0))
(assert (= x33_plus 0))
(assert (= x34_minus 0))
(assert (= x34_plus 0))
(assert (= x35_minus 0))
(assert (= x35_plus 0))
(assert (= x36_minus 0))
(assert (= x36_plus 0))
(assert (= x37_minus 0))
(assert (= x37_plus 0))
(assert (= x38_minus 0))
(assert (= x38_plus 1))
(assert (= x39_minus 0))
(assert (= x39_plus 0))
(assert (= x3_minus 2))
(assert (= x3_plus 0))
(assert (= x40_minus 5))
(assert (= x40_plus 0))
(assert (= x41_minus 0))
(assert (= x41_plus 2))
(assert (= x42_minus 0))
(assert (= x42_plus 0))
(assert (= x43_minus 0))
(assert (= x43_plus 17))
(assert (= x44_minus 0))
(assert (= x44_plus 12))
(assert (= x4_minus 22))
(assert (= x4_plus 0))
(assert (= x5_minus 0))
(assert (= x5_plus 21))
(assert (= x6_minus 8))
(assert (= x6_plus 0))
(assert (= x7_minus 4))
(assert (= x7_plus 0))
(assert (= x8_minus 0))
(assert (= x8_plus 0))
(assert (= x9_minus 3))
(assert (= x9_plus 0))