(assert (= x17_plus 0)) (assert (= x17_minus 0)) (assert (= x16_plus 0)) (assert (= x16_minus 0)) (assert (= x13_plus 0)) (assert (= x13_minus 0)) (assert (= x11_plus 0)) (assert (= x11_minus 12)) (assert (= x9_plus 0)) (assert (= x9_minus 2)) (assert (= x7_plus 0)) (assert (= x7_minus 14)) (assert (= x6_plus 42)) (assert (= x6_minus 0)) (assert (= x1_plus 20)) (assert (= x1_minus 0)) (assert (= x19_plus 3)) (assert (= x19_minus 0)) (assert (= x12_plus 0)) (assert (= x12_minus 32)) (assert (= x4_plus 0)) (assert (= x4_minus 18)) (assert (= x2_plus 45)) (assert (= x2_minus 0)) (assert (= x0_plus 33)) (assert (= x0_minus 0)) (assert (= x15_plus 36)) (assert (= x15_minus 0)) (assert (= x8_plus 0)) (assert (= x8_minus 22)) (assert (= x14_plus 0)) (assert (= x14_minus 10)) (assert (= x18_plus 5)) (assert (= x18_minus 0)) (assert (= x5_plus 29)) (assert (= x5_minus 0)) (assert (= x3_plus 6)) (assert (= x3_minus 0)) (assert (= x10_plus 0)) (assert (= x10_minus 4))