(assert (= x0_minus 0))
(assert (= x0_plus 0))
(assert (= x10_minus 0))
(assert (= x10_plus 1))
(assert (= x11_minus 0))
(assert (= x11_plus 0))
(assert (= x12_minus 0))
(assert (= x12_plus 1))
(assert (= x13_minus 0))
(assert (= x13_plus 4455))
(assert (= x14_minus 3387))
(assert (= x14_plus 0))
(assert (= x15_minus 0))
(assert (= x15_plus 155))
(assert (= x16_minus 5596))
(assert (= x16_plus 0))
(assert (= x17_minus 0))
(assert (= x17_plus 5521))
(assert (= x18_minus 14065))
(assert (= x18_plus 0))
(assert (= x19_minus 6081))
(assert (= x19_plus 0))
(assert (= x1_minus 7483))
(assert (= x1_plus 0))
(assert (= x2_minus 7532))
(assert (= x2_plus 0))
(assert (= x3_minus 4455))
(assert (= x3_plus 0))
(assert (= x4_minus 3715))
(assert (= x4_plus 0))
(assert (= x5_minus 12491))
(assert (= x5_plus 0))
(assert (= x6_minus 0))
(assert (= x6_plus 331))
(assert (= x7_minus 0))
(assert (= x7_plus 4614))
(assert (= x8_minus 0))
(assert (= x8_plus 6113))
(assert (= x9_minus 0))
(assert (= x9_plus 1986))