(assert (= x32_plus 0)) (assert (= x32_minus 0)) (assert (= x31_plus 0)) (assert (= x31_minus 0)) (assert (= x30_plus 0)) (assert (= x30_minus 0)) (assert (= x27_plus 0)) (assert (= x27_minus 0)) (assert (= x24_plus 0)) (assert (= x24_minus 0)) (assert (= x22_plus 0)) (assert (= x22_minus 0)) (assert (= x19_plus 0)) (assert (= x19_minus 0)) (assert (= x16_plus 0)) (assert (= x16_minus 0)) (assert (= x13_plus 0)) (assert (= x13_minus 0)) (assert (= x12_plus 0)) (assert (= x12_minus 0)) (assert (= x6_plus 0)) (assert (= x6_minus 0)) (assert (= x4_plus 0)) (assert (= x4_minus 0)) (assert (= x3_plus 0)) (assert (= x3_minus 0)) (assert (= x2_plus 798)) (assert (= x2_minus 0)) (assert (= x1_plus 361)) (assert (= x1_minus 0)) (assert (= x0_plus 436)) (assert (= x0_minus 0)) (assert (= x34_plus 15)) (assert (= x34_minus 38)) (assert (= x33_plus 716)) (assert (= x33_minus 0)) (assert (= x29_plus 0)) (assert (= x29_minus 730)) (assert (= x28_plus 51)) (assert (= x28_minus 0)) (assert (= x25_plus 835)) (assert (= x25_minus 0)) (assert (= x21_plus 0)) (assert (= x21_minus 1355)) (assert (= x20_plus 0)) (assert (= x20_minus 172)) (assert (= x18_plus 0)) (assert (= x18_minus 569)) (assert (= x17_plus 184)) (assert (= x17_minus 0)) (assert (= x7_plus 0)) (assert (= x7_minus 731)) (assert (= x14_plus 26)) (assert (= x14_minus 0)) (assert (= x11_plus 0)) (assert (= x11_minus 947)) (assert (= x10_plus 0)) (assert (= x10_minus 393)) (assert (= x9_plus 495)) (assert (= x9_minus 0)) (assert (= x8_plus 278)) (assert (= x8_minus 0)) (assert (= x5_plus 0)) (assert (= x5_minus 687)) (assert (= x23_plus 991)) (assert (= x23_minus 0)) (assert (= x26_plus 287)) (assert (= x26_minus 0)) (assert (= x15_plus 0)) (assert (= x15_minus 723))