(set-logic ALL)(declare-fun QFYTjoo_new () Int)(declare-fun DlqpfIW_new () Int)(declare-fun IcTSpor_new () Int)(declare-fun pclIuXt_new () Int)(declare-fun NEXCQtF_new () Int)(declare-fun xnbQxWN_new () Int)(declare-fun IrJEuXI_new () Int)(declare-fun nNChjFs_new () Int)(declare-fun puEBwYN_new () Int)(declare-fun QWjBzHC_new () Int)(declare-fun sopWFKn_new () Int)(declare-fun vEEUsHa_new () Int)(declare-fun kAdFbmi_new () Int)(declare-fun VOlcMOP_new () Int)(declare-fun BueQASA_new () Int)(declare-fun ndfZUwN_new () Int)(declare-fun obWVHpT_new () Int)(declare-fun UVgkblP_new () Int)(declare-fun nAGYFTC_new () Int)(declare-fun gZwKvSn_new () Int)(declare-fun lRzOrzO_new () Int)(declare-fun DBItqbo_new () Int)(declare-fun shifted1_P_2 () Bool)(declare-fun shifted1_P_3 () Bool)(declare-fun shifted1_P_4 () Bool)(declare-fun shifted1_P_5 () Bool)(declare-fun shifted1_P_6 () Bool)(declare-fun shifted1_P_7 () Bool)(declare-fun shifted1_P_8 () Bool)(declare-fun shifted1_P_9 () Bool)(declare-fun shifted1_P_10 () Bool)(declare-fun shifted1_P_11 () Bool)(declare-fun shifted1_P_12 () Bool)(declare-fun shifted1_P_13 () Bool)(declare-fun shifted1_P_14 () Bool)(declare-fun shifted1_P_15 () Int)(declare-fun shifted1_P_16 () Int)(declare-fun shifted1_P_17 () Bool)(declare-fun shifted1_P_18 () Bool)(declare-fun shifted1_P_19 () Int)(declare-fun shifted1_P_20 () Int)(declare-fun shifted1_P_21 () Bool)(declare-fun shifted1_P_22 () Bool)(declare-fun shifted1_P_23 () Int)(declare-fun shifted1_P_24 () Int)(declare-fun shifted1_P_25 () Bool)(declare-fun shifted1_P_26 () Bool)(declare-fun shifted1_P_27 () Bool)(declare-fun shifted1_P_28 () Bool)(declare-fun shifted1_P_29 () Bool)(declare-fun shifted1_P_30 () Bool)(declare-fun shifted1_P_31 () Bool)(declare-fun shifted1_P_32 () Int)(declare-fun shifted1_P_33 () Int)(declare-fun shifted1_P_34 () Int)(declare-fun shifted1_P_35 () Bool)(declare-fun shifted1_P_36 () Int)(declare-fun shifted1_P_37 () Int)(declare-fun shifted1_P_38 () Int)(declare-fun shifted1_P_39 () Int)(declare-fun shifted1_P_40 () Bool)(declare-fun shifted1_P_41 () Bool)(declare-fun shifted1_P_42 () Int)(declare-fun shifted1_P_43 () Int)(declare-fun shifted1_P_44 () Bool)(declare-fun shifted1_P_45 () Bool)(declare-fun shifted1_P_46 () Int)(declare-fun shifted1_P_47 () Int)(declare-fun shifted1_P_48 () Int)(declare-fun shifted1_P_49 () Bool)(declare-fun shifted1_P_50 () Int)(declare-fun shifted1_P_51 () Int)(declare-fun shifted1_P_63 () Int)(declare-fun shifted1_dz () Int)(declare-fun shifted1_rz () Bool)(declare-fun shifted2_x38_plus () Int)(declare-fun shifted2_x38_minus () Int)(declare-fun shifted2_x36_plus () Int)(declare-fun shifted2_x36_minus () Int)(declare-fun shifted2_x31_plus () Int)(declare-fun shifted2_x31_minus () Int)(declare-fun shifted2_x30_plus () Int)(declare-fun shifted2_x30_minus () Int)(declare-fun shifted2_x26_plus () Int)(declare-fun shifted2_x26_minus () Int)(declare-fun shifted2_x22_plus () Int)(declare-fun shifted2_x22_minus () Int)(declare-fun shifted2_x20_plus () Int)(declare-fun shifted2_x20_minus () Int)(declare-fun shifted2_x18_plus () Int)(declare-fun shifted2_x18_minus () Int)(declare-fun shifted2_x17_plus () Int)(declare-fun shifted2_x17_minus () Int)(declare-fun shifted2_x15_plus () Int)(declare-fun shifted2_x15_minus () Int)(declare-fun shifted2_x14_plus () Int)(declare-fun shifted2_x14_minus () Int)(declare-fun shifted2_x13_plus () Int)(declare-fun shifted2_x13_minus () Int)(declare-fun shifted2_x10_plus () Int)(declare-fun shifted2_x10_minus () Int)(declare-fun shifted2_x9_plus () Int)(declare-fun shifted2_x9_minus () Int)(declare-fun shifted2_x8_plus () Int)(declare-fun shifted2_x8_minus () Int)(declare-fun shifted2_x6_plus () Int)(declare-fun shifted2_x6_minus () Int)(declare-fun shifted2_x4_plus () Int)(declare-fun shifted2_x4_minus () Int)(declare-fun shifted2_x3_plus () Int)(declare-fun shifted2_x3_minus () Int)(declare-fun shifted2_x39_plus () Int)(declare-fun shifted2_x39_minus () Int)(declare-fun shifted2_x37_plus () Int)(declare-fun shifted2_x37_minus () Int)(declare-fun shifted2_x33_plus () Int)(declare-fun shifted2_x33_minus () Int)(declare-fun shifted2_x32_plus () Int)(declare-fun shifted2_x32_minus () Int)(declare-fun shifted2_x29_plus () Int)(declare-fun shifted2_x29_minus () Int)(declare-fun shifted2_x28_plus () Int)(declare-fun shifted2_x28_minus () Int)(declare-fun shifted2_x27_plus () Int)(declare-fun shifted2_x27_minus () Int)(declare-fun shifted2_x25_plus () Int)(declare-fun shifted2_x25_minus () Int)(declare-fun shifted2_x12_plus () Int)(declare-fun shifted2_x12_minus () Int)(declare-fun shifted2_x11_plus () Int)(declare-fun shifted2_x11_minus () Int)(declare-fun shifted2_x5_plus () Int)(declare-fun shifted2_x5_minus () Int)(declare-fun shifted2_x2_plus () Int)(declare-fun shifted2_x2_minus () Int)(declare-fun shifted2_x1_plus () Int)(declare-fun shifted2_x1_minus () Int)(declare-fun shifted2_x23_plus () Int)(declare-fun shifted2_x23_minus () Int)(declare-fun shifted2_x19_plus () Int)(declare-fun shifted2_x19_minus () Int)(declare-fun shifted2_x0_plus () Int)(declare-fun shifted2_x0_minus () Int)(declare-fun shifted2_x35_plus () Int)(declare-fun shifted2_x35_minus () Int)(declare-fun shifted2_x34_plus () Int)(declare-fun shifted2_x34_minus () Int)(declare-fun shifted2_x24_plus () Int)(declare-fun shifted2_x24_minus () Int)(declare-fun shifted2_x21_plus () Int)(declare-fun shifted2_x21_minus () Int)(declare-fun shifted2_x7_plus () Int)(declare-fun shifted2_x7_minus () Int)(declare-fun shifted2_x16_plus () Int)(declare-fun shifted2_x16_minus () Int)(assert (<= (- 4) (- QFYTjoo_new shifted2_x0_plus)))(assert (<= (- QFYTjoo_new shifted2_x0_plus) 3))(assert (<= (- 2) (- DlqpfIW_new shifted2_x3_minus)))(assert (<= (- DlqpfIW_new shifted2_x3_minus) 1))(assert (<= (- 4) (- (- IcTSpor_new (- 169)) shifted2_x35_minus)))(assert (<= (- (- IcTSpor_new (- 169)) shifted2_x35_minus) 3))(assert (<= (- 2) (- pclIuXt_new shifted2_x21_plus)))(assert (<= (- pclIuXt_new shifted2_x21_plus) 1))(assert (<= (- 4) (- NEXCQtF_new shifted2_x31_plus)))(assert (<= (- NEXCQtF_new shifted2_x31_plus) 3))(assert (<= (- 2) (div xnbQxWN_new shifted2_x36_minus)))(assert (<= (div xnbQxWN_new shifted2_x36_minus) 1))(assert (<= 0 shifted1_P_32))(assert (<= (div IrJEuXI_new shifted2_x10_plus) 7))(assert (<= 0 (- (- nNChjFs_new (- 542)) shifted2_x20_plus)))(assert (<= (- (- nNChjFs_new (- 542)) shifted2_x20_plus) 7))(assert (<= 0 shifted1_P_34))(assert (<= (div puEBwYN_new shifted2_x17_plus) 7))(assert (<= 0 shifted1_P_36))(assert (<= (- QWjBzHC_new shifted2_x35_minus) 7))(assert (<= 0 (- (- sopWFKn_new (- 756)) shifted2_x2_plus)))(assert (<= shifted1_P_37 7))(assert (<= 0 (- (- vEEUsHa_new (- 786)) shifted2_x25_minus)))(assert (<= shifted1_P_38 7))(assert (<= 0 shifted1_P_39))(assert (<= shifted1_P_39 7))(assert (<= 0 shifted1_P_42))(assert (<= (div VOlcMOP_new shifted2_x12_minus) 7))(assert (<= 0 shifted1_P_43))(assert (<= (- (- BueQASA_new 883) shifted2_x1_plus) 7))(assert (<= 0 (div ndfZUwN_new shifted2_x36_plus)))(assert (<= (div ndfZUwN_new shifted2_x36_plus) 7))(assert (<= 0 shifted1_P_47))(assert (<= (- obWVHpT_new shifted2_x9_minus) 7))(assert (<= 0 shifted1_P_48))(assert (<= (div UVgkblP_new shifted2_x14_plus) 7))(assert (<= 0 shifted1_P_50))(assert (<= shifted1_P_50 7))(assert (<= (- 32) (- gZwKvSn_new shifted2_x12_minus)))(assert (<= (- gZwKvSn_new shifted2_x12_minus) 31))(assert (<= (- 32) (- (- lRzOrzO_new 626) shifted2_x10_minus)))(assert (<= (- (- lRzOrzO_new 626) shifted2_x10_minus) 31))(assert (let ((?v_0 (not shifted1_P_3)) (?v_3 (not shifted1_P_9))) (let ((?v_2 (not (ite ?v_0 false (ite (not shifted1_P_4) (or (or shifted1_P_5 shifted1_P_6) shifted1_P_7) false)))) (?v_1 (not (not shifted1_P_2))) (?v_5 (not shifted1_P_31)) (?v_4 (not shifted1_P_30))) (let ((?v_7 (ite ?v_4 0 (ite ?v_5 shifted1_P_32 shifted1_P_33))) (?v_6 (not (not shifted1_P_29)))) (let ((?v_10 (ite ?v_6 ?v_7 (ite ?v_4 0 (ite ?v_5 shifted1_P_33 (div puEBwYN_new shifted2_x17_plus))))) (?v_8 (ite (not (not shifted1_P_35)) ?v_7 (ite ?v_4 0 (ite ?v_5 (- QWjBzHC_new shifted2_x35_minus) (- (- sopWFKn_new (- 756)) shifted2_x2_plus))))) (?v_9 (not (not shifted1_P_41)))) (let ((?v_11 (ite ?v_9 ?v_7 (ite ?v_4 0 (ite ?v_5 (div VOlcMOP_new shifted2_x12_minus) shifted1_P_32)))) (?v_12 (ite (not (not shifted1_P_45)) ?v_7 (ite ?v_4 0 (ite ?v_5 (div ndfZUwN_new shifted2_x36_plus) shifted1_P_47))))) (let ((?v_14 (= (+ (ite (> (ite (not (not shifted1_P_28)) ?v_10 (ite ?v_6 ?v_8 (ite ?v_4 0 (ite ?v_5 shifted1_P_37 (- (- vEEUsHa_new (- 786)) shifted2_x25_minus))))) shifted1_P_39) 256 0) (+ (ite (> ?v_8 (- kAdFbmi_new shifted2_x25_minus)) 128 0) (+ (ite (> (ite (not (not shifted1_P_40)) ?v_11 (ite ?v_9 ?v_8 (ite ?v_4 0 (ite ?v_5 shifted1_P_43 shifted1_P_36)))) (- kAdFbmi_new shifted2_x25_minus)) 64 0) (+ (ite (> ?v_10 (- kAdFbmi_new shifted2_x25_minus)) 32 0) (+ (ite (> ?v_7 (- kAdFbmi_new shifted2_x25_minus)) 16 0) (+ (ite (> ?v_11 shifted1_P_39) 8 0) (+ (ite (> (ite (not (not shifted1_P_44)) ?v_10 (ite ?v_6 ?v_12 (ite ?v_4 0 (ite ?v_5 (- obWVHpT_new shifted2_x9_minus) shifted1_P_48)))) shifted1_P_39) 4 0) (+ (ite (> ?v_12 (- kAdFbmi_new shifted2_x25_minus)) 2 0) (ite (> (ite (not (not shifted1_P_49)) ?v_11 (ite ?v_9 ?v_12 (ite ?v_4 0 (ite ?v_5 shifted1_P_50 shifted1_P_46)))) shifted1_P_39) 1 0))))))))) 401)) (?v_13 (not (not (or (not (ite ?v_1 (ite ?v_2 (ite ?v_0 shifted1_P_8 (ite ?v_3 shifted1_P_10 shifted1_P_8)) shifted1_P_8) false)) (not (ite ?v_1 (ite ?v_2 (ite ?v_0 shifted1_P_11 (ite ?v_3 (not (= (ite (not (not shifted1_P_12)) 0 (+ (+ (+ (+ (+ (+ (+ (+ (ite (and (and shifted1_P_13 shifted1_P_14) (< shifted1_P_15 0)) 1 0) (ite (and shifted1_P_13 (< (- DlqpfIW_new shifted2_x3_minus) 0)) 1 0)) (ite (and (and shifted1_P_13 shifted1_P_17) shifted1_P_18) 1 0)) (ite (and shifted1_P_14 (< shifted1_P_19 0)) 1 0)) (ite (< (- pclIuXt_new shifted2_x21_plus) 0) 1 0)) (ite (and shifted1_P_17 shifted1_P_21) 1 0)) (ite (and (and shifted1_P_22 shifted1_P_14) (< (- NEXCQtF_new shifted2_x31_plus) 0)) 1 0)) (ite (and shifted1_P_22 (< (div xnbQxWN_new shifted2_x36_minus) 0)) 1 0)) (ite (and (and shifted1_P_22 shifted1_P_17) shifted1_P_25) 1 0))) 0)) shifted1_P_11)) shifted1_P_11) false)))))) (?v_15 (ite (not (not (or (not shifted1_P_8) (not shifted1_P_11)))) shifted1_P_26 shifted1_P_27))) (= (+ (* 2 shifted1_dz) 1) (- (ite (ite ?v_13 false (ite ?v_1 (ite ?v_2 (ite ?v_0 shifted1_P_27 (ite ?v_3 (and ?v_14 (< shifted1_P_63 0)) shifted1_P_27)) shifted1_P_27) false)) 1 0) (ite (ite ?v_13 false (ite ?v_1 (ite ?v_2 (ite ?v_0 ?v_15 (ite ?v_3 (and ?v_14 (< shifted1_P_51 0)) ?v_15)) ?v_15) false)) 1 0))))))))))(assert (>= shifted2_x38_plus 0))(assert (>= shifted2_x38_minus 0))(assert (>= (div ndfZUwN_new shifted1_P_46) 0))(assert (>= (div xnbQxWN_new shifted1_P_24) 0))(assert (>= (- NEXCQtF_new shifted1_P_23) 0))(assert (>= shifted2_x31_minus 0))(assert (>= shifted2_x30_plus 0))(assert (>= shifted2_x30_minus 0))(assert (>= shifted2_x26_plus 0))(assert (>= shifted2_x26_minus 0))(assert (>= shifted2_x22_plus 0))(assert (>= shifted2_x22_minus 0))(assert (>= (- (- nNChjFs_new (- 542)) shifted1_P_33) 0))(assert (>= shifted2_x20_minus 0))(assert (>= shifted2_x18_plus 0))(assert (>= shifted2_x18_minus 0))(assert (>= shifted2_x17_plus 0))(assert (>= shifted2_x17_minus 0))(assert (>= shifted2_x15_plus 0))(assert (>= shifted2_x15_minus 0))(assert (>= (div UVgkblP_new shifted1_P_48) 0))(assert (>= shifted2_x14_minus 0))(assert (>= shifted2_x13_plus 0))(assert (>= shifted2_x13_minus 0))(assert (>= (div IrJEuXI_new shifted1_P_32) 0))(assert (>= (- (- lRzOrzO_new 626) shifted1_P_63) 0))(assert (>= shifted2_x9_plus 0))(assert (>= (- obWVHpT_new shifted1_P_47) 0))(assert (>= shifted2_x8_plus 0))(assert (>= shifted2_x8_minus 0))(assert (>= shifted2_x6_plus 0))(assert (>= shifted2_x6_minus 0))(assert (>= shifted2_x4_plus 0))(assert (>= shifted2_x4_minus 0))(assert (>= shifted2_x3_plus 0))(assert (>= (- DlqpfIW_new shifted1_P_16) 0))(assert (>= shifted2_x39_plus 0))(assert (>= shifted2_x39_minus 0))(assert (>= shifted2_x37_plus 0))(assert (>= shifted2_x37_minus 0))(assert (>= shifted2_x33_plus 0))(assert (>= shifted2_x33_minus 0))(assert (>= shifted2_x32_plus 0))(assert (>= shifted2_x32_minus 0))(assert (>= shifted2_x29_plus 0))(assert (>= shifted2_x29_minus 0))(assert (>= shifted2_x28_plus 0))(assert (>= shifted2_x28_minus 0))(assert (>= shifted2_x27_plus 0))(assert (>= shifted2_x27_minus 0))(assert (>= shifted2_x25_plus 0))(assert (>= (- kAdFbmi_new shifted1_P_39) 0))(assert (>= shifted2_x12_plus 0))(assert (>= (div VOlcMOP_new shifted1_P_42) 0))(assert (>= shifted2_x11_plus 0))(assert (>= shifted2_x11_minus 0))(assert (>= shifted2_x5_plus 0))(assert (>= shifted2_x5_minus 0))(assert (>= (- DBItqbo_new shifted1_dz) 0))(assert (>= shifted2_x2_minus 0))(assert (>= (- (- BueQASA_new 883) shifted1_P_43) 0))(assert (>= shifted2_x1_minus 0))(assert (>= shifted2_x23_plus 0))(assert (>= shifted2_x23_minus 0))(assert (>= shifted2_x19_plus 0))(assert (>= shifted2_x19_minus 0))(assert (>= shifted2_x0_plus 0))(assert (>= shifted2_x0_minus 0))(assert (>= shifted2_x35_plus 0))(assert (>= (- (- IcTSpor_new (- 169)) shifted1_P_19) 0))(assert (>= shifted2_x34_plus 0))(assert (>= shifted2_x34_minus 0))(assert (>= shifted2_x24_plus 0))(assert (>= shifted2_x24_minus 0))(assert (>= (- pclIuXt_new shifted1_P_20) 0))(assert (>= shifted2_x21_minus 0))(assert (>= shifted2_x7_plus 0))(assert (>= shifted2_x7_minus 0))(assert (>= shifted2_x16_plus 0))(assert (>= shifted2_x16_minus 0))(assert (<= (+ shifted2_x38_plus (* (- 1) shifted2_x38_minus) (* (- 1) (div ndfZUwN_new shifted1_P_46)) (div xnbQxWN_new shifted1_P_24) (- NEXCQtF_new shifted1_P_23) (* (- 1) shifted2_x31_minus) shifted2_x30_plus (* (- 1) shifted2_x30_minus) (* (- 1) shifted2_x26_plus) shifted2_x26_minus (* (- 1) shifted2_x22_plus) shifted2_x22_minus (* (- 1) (- (- nNChjFs_new (- 542)) shifted1_P_33)) shifted2_x20_minus (* (- 1) shifted2_x18_plus) shifted2_x18_minus (* (- 1) (div puEBwYN_new shifted1_P_34)) shifted2_x17_minus shifted2_x15_plus (* (- 1) shifted2_x15_minus) shifted2_x14_plus (* (- 1) shifted2_x14_minus) (* (- 1) shifted2_x13_plus) shifted2_x13_minus shifted2_x10_plus (* (- 1) (- (- lRzOrzO_new 626) shifted1_P_63)) (* (- 1) shifted2_x9_plus) (- obWVHpT_new shifted1_P_47) (* (- 1) shifted2_x8_plus) shifted2_x8_minus (* 2 shifted2_x6_plus) (* (- 2) shifted2_x6_minus) (* (- 1) shifted2_x4_plus) shifted2_x4_minus shifted2_x3_plus (* (- 1) shifted2_x3_minus) ) (- 1) ) )(assert (<= (+ shifted2_x39_plus (* (- 1) shifted2_x39_minus) (* (- 1) shifted2_x37_plus) shifted2_x37_minus (div ndfZUwN_new shifted1_P_46) (* (- 1) (div xnbQxWN_new shifted1_P_24)) shifted2_x33_plus (* (- 1) shifted2_x33_minus) shifted2_x32_plus (* (- 1) shifted2_x32_minus) shifted2_x29_plus (* (- 1) shifted2_x29_minus) (* (- 1) shifted2_x28_plus) shifted2_x28_minus (* (- 1) shifted2_x27_plus) shifted2_x27_minus shifted2_x25_plus (* (- 1) (- (- vEEUsHa_new (- 786)) shifted1_P_38)) (* (- 1) shifted2_x22_plus) shifted2_x22_minus (* (- 1) shifted2_x15_plus) shifted2_x15_minus shifted2_x13_plus (* (- 1) shifted2_x13_minus) (* 2 shifted2_x12_plus) (* (- 2) (div VOlcMOP_new shifted1_P_42)) (* (- 1) shifted2_x11_plus) shifted2_x11_minus (* (- 1) shifted2_x10_plus) (- (- lRzOrzO_new 626) shifted1_P_63) (* (- 1) shifted2_x5_plus) shifted2_x5_minus (- DBItqbo_new shifted1_dz) (* (- 1) shifted2_x2_minus) shifted2_x1_plus (* (- 1) shifted2_x1_minus) ) 1 ) )(assert (<= (+ shifted2_x39_plus (* (- 1) shifted2_x39_minus) (* (- 1) shifted2_x37_plus) shifted2_x37_minus (* 2 shifted2_x33_plus) (* (- 2) shifted2_x33_minus) (* (- 1) (- NEXCQtF_new shifted1_P_23)) shifted2_x31_minus (* (- 1) shifted2_x30_plus) shifted2_x30_minus shifted2_x28_plus (* (- 1) shifted2_x28_minus) (* (- 1) shifted2_x27_plus) shifted2_x27_minus shifted2_x26_plus (* (- 1) shifted2_x26_minus) (* (- 1) shifted2_x23_plus) shifted2_x23_minus (* (- 1) shifted2_x22_plus) shifted2_x22_minus shifted2_x19_plus (* (- 1) shifted2_x19_minus) (* (- 1) shifted2_x18_plus) shifted2_x18_minus shifted2_x8_plus (* (- 1) shifted2_x8_minus) shifted2_x6_plus (* (- 1) shifted2_x6_minus) shifted2_x5_plus (* (- 1) shifted2_x5_minus) (* (- 1) shifted2_x3_plus) shifted2_x3_minus (* (- 1) shifted2_x1_plus) shifted2_x1_minus (* 2 (- QFYTjoo_new shifted1_P_15)) (* (- 2) shifted2_x0_minus) ) (- 1) ) )(assert (<= (+ shifted2_x39_plus (* (- 1) shifted2_x39_minus) (* (- 1) (div ndfZUwN_new shifted1_P_46)) shifted2_x36_minus (* (- 1) shifted2_x35_plus) (- QWjBzHC_new shifted1_P_36) shifted2_x34_plus (* (- 1) shifted2_x34_minus) shifted2_x32_plus (* (- 1) shifted2_x32_minus) shifted2_x26_plus (* (- 1) shifted2_x26_minus) (* (- 1) shifted2_x24_plus) shifted2_x24_minus shifted2_x20_plus (* (- 1) shifted2_x20_minus) (* (- 2) shifted2_x17_plus) (* 2 shifted2_x17_minus) (* (- 1) (div UVgkblP_new shifted1_P_48)) shifted2_x14_minus (* (- 1) shifted2_x13_plus) shifted2_x13_minus (* (- 1) shifted2_x11_plus) shifted2_x11_minus (* (- 1) shifted2_x8_plus) shifted2_x8_minus (* (- 1) shifted2_x6_plus) shifted2_x6_minus shifted2_x5_plus (* (- 1) shifted2_x5_minus) shifted2_x1_plus (* (- 1) shifted2_x1_minus) ) 1 ) )(assert (<= (+ shifted2_x37_plus (* (- 1) shifted2_x37_minus) shifted2_x36_plus (* (- 1) shifted2_x36_minus) shifted2_x33_plus (* (- 1) shifted2_x33_minus) shifted2_x32_plus (* (- 1) shifted2_x32_minus) shifted2_x29_plus (* (- 1) shifted2_x29_minus) (* 2 (- nAGYFTC_new shifted1_P_50)) (* (- 2) shifted2_x27_minus) shifted2_x25_plus (* (- 1) (- (- vEEUsHa_new (- 786)) shifted1_P_38)) shifted2_x24_plus (* (- 1) shifted2_x24_minus) shifted2_x18_plus (* (- 1) shifted2_x18_minus) (* (- 1) shifted2_x15_plus) shifted2_x15_minus (* (- 1) shifted2_x12_plus) (div VOlcMOP_new shifted1_P_42) (* (- 1) shifted2_x11_plus) shifted2_x11_minus shifted2_x8_plus (* (- 1) shifted2_x8_minus) shifted2_x4_plus (* (- 1) shifted2_x4_minus) (* (- 2) (- (- sopWFKn_new (- 756)) shifted1_P_37)) (* 2 shifted2_x2_minus) (- (- BueQASA_new 883) shifted1_P_43) (* (- 1) shifted2_x1_minus) ) (- 1) ) )(assert (<= (+ shifted2_x36_plus (* (- 1) (div xnbQxWN_new shifted1_P_24)) (* (- 1) shifted2_x34_plus) shifted2_x34_minus (* (- 1) shifted2_x30_plus) shifted2_x30_minus (* (- 1) shifted2_x29_plus) shifted2_x29_minus shifted2_x27_plus (* (- 1) shifted2_x27_minus) (* (- 1) shifted2_x22_plus) shifted2_x22_minus (* (- 1) shifted2_x21_plus) shifted2_x21_minus (* (- 2) (- (- nNChjFs_new (- 542)) shifted1_P_33)) (* 2 shifted2_x20_minus) (* (- 1) shifted2_x17_plus) shifted2_x17_minus (* (- 1) shifted2_x11_plus) shifted2_x11_minus shifted2_x10_plus (* (- 1) (- (- lRzOrzO_new 626) shifted1_P_63)) shifted2_x8_plus (* (- 1) shifted2_x8_minus) shifted2_x7_plus (* (- 1) shifted2_x7_minus) shifted2_x4_plus (* (- 1) shifted2_x4_minus) (- (- sopWFKn_new (- 756)) shifted1_P_37) (* (- 1) shifted2_x2_minus) (- QFYTjoo_new shifted1_P_15) (* (- 1) shifted2_x0_minus) ) 0 ) )(assert (<= (+ shifted2_x39_plus (* (- 1) shifted2_x39_minus) shifted2_x37_plus (* (- 1) shifted2_x37_minus) (* (- 1) shifted2_x35_plus) shifted2_x35_minus (* (- 1) shifted2_x34_plus) shifted2_x34_minus (* (- 2) shifted2_x31_plus) (* 2 shifted2_x31_minus) (- nAGYFTC_new shifted1_P_50) (* (- 1) shifted2_x27_minus) shifted2_x25_plus (* (- 1) shifted2_x25_minus) shifted2_x21_plus (* (- 1) shifted2_x21_minus) shifted2_x18_plus (* (- 1) shifted2_x18_minus) (* (- 1) shifted2_x16_plus) shifted2_x16_minus (* (- 1) shifted2_x10_plus) shifted2_x10_minus shifted2_x8_plus (* (- 1) shifted2_x8_minus) shifted2_x7_plus (* (- 1) shifted2_x7_minus) (* (- 2) shifted2_x6_plus) (* 2 shifted2_x6_minus) shifted2_x5_plus (* (- 1) shifted2_x5_minus) shifted2_x1_plus (* (- 1) shifted2_x1_minus) ) 0 ) )(assert (<= (+ shifted2_x39_plus (* (- 1) shifted2_x39_minus) (* (- 1) shifted2_x35_plus) shifted2_x35_minus (* (- 1) shifted2_x34_plus) shifted2_x34_minus (* (- 1) shifted2_x33_plus) shifted2_x33_minus shifted2_x30_plus (* (- 1) shifted2_x30_minus) shifted2_x26_plus (* (- 1) shifted2_x26_minus) (* (- 1) shifted2_x25_plus) shifted2_x25_minus shifted2_x24_plus (* (- 1) shifted2_x24_minus) shifted2_x22_plus (* (- 1) shifted2_x22_minus) (* (- 1) (- pclIuXt_new shifted1_P_20)) shifted2_x21_minus (* (- 1) shifted2_x18_plus) shifted2_x18_minus shifted2_x15_plus (* (- 1) shifted2_x15_minus) (* (- 1) shifted2_x7_plus) shifted2_x7_minus (* (- 1) shifted2_x5_plus) shifted2_x5_minus (* (- 1) shifted2_x0_plus) shifted2_x0_minus ) 0 ) )(assert (<= (+ shifted2_x38_plus (* (- 1) shifted2_x38_minus) (* (- 1) shifted2_x32_plus) shifted2_x32_minus (* (- 2) (- NEXCQtF_new shifted1_P_23)) (* 2 shifted2_x31_minus) (* (- 1) shifted2_x30_plus) shifted2_x30_minus (* 2 shifted2_x25_plus) (* (- 2) (- kAdFbmi_new shifted1_P_39)) shifted2_x24_plus (* (- 1) shifted2_x24_minus) (* (- 1) (- (- nNChjFs_new (- 542)) shifted1_P_33)) shifted2_x20_minus (div puEBwYN_new shifted1_P_34) (* (- 1) shifted2_x17_minus) (div UVgkblP_new shifted1_P_48) (* (- 1) shifted2_x14_minus) (div IrJEuXI_new shifted1_P_32) (* (- 1) (- (- lRzOrzO_new 626) shifted1_P_63)) (* 2 shifted2_x5_plus) (* (- 2) shifted2_x5_minus) (* (- 1) shifted2_x4_plus) shifted2_x4_minus (* (- 1) (- (- sopWFKn_new (- 756)) shifted1_P_37)) shifted2_x2_minus (* (- 1) (- (- BueQASA_new 883) shifted1_P_43)) shifted2_x1_minus (* (- 1) shifted2_x0_plus) shifted2_x0_minus ) 0 ) )(assert (<= (+ shifted2_x38_plus (* (- 1) shifted2_x38_minus) (* (- 1) shifted2_x34_plus) shifted2_x34_minus (* (- 2) shifted2_x31_plus) (* 2 shifted2_x31_minus) (* (- 2) shifted2_x22_plus) (* 2 shifted2_x22_minus) (* (- 1) (- pclIuXt_new shifted1_P_20)) shifted2_x21_minus shifted2_x19_plus (* (- 1) shifted2_x19_minus) shifted2_x16_plus (* (- 1) shifted2_x16_minus) (* (- 1) shifted2_x15_plus) shifted2_x15_minus shifted2_x13_plus (* (- 1) shifted2_x13_minus) (* (- 1) shifted2_x11_plus) shifted2_x11_minus shifted2_x10_plus (* (- 1) (- (- lRzOrzO_new 626) shifted1_P_63)) (* (- 1) shifted2_x6_plus) shifted2_x6_minus shifted2_x5_plus (* (- 1) shifted2_x5_minus) (* (- 1) shifted2_x3_plus) (- DlqpfIW_new shifted1_P_16) (* (- 1) (- (- BueQASA_new 883) shifted1_P_43)) shifted2_x1_minus ) 1 ) )(assert (<= (+ shifted2_x39_plus (* (- 1) shifted2_x39_minus) (* (- 1) shifted2_x35_plus) (- (- IcTSpor_new (- 169)) shifted1_P_19) (* (- 1) shifted2_x33_plus) shifted2_x33_minus (- NEXCQtF_new shifted1_P_23) (* (- 1) shifted2_x31_minus) shifted2_x30_plus (* (- 1) shifted2_x30_minus) shifted2_x26_plus (* (- 1) shifted2_x26_minus) (* 2 shifted2_x25_plus) (* (- 2) (- (- vEEUsHa_new (- 786)) shifted1_P_38)) (* 3 shifted2_x23_plus) (* (- 3) shifted2_x23_minus) (* (- 1) shifted2_x22_plus) shifted2_x22_minus (- (- nNChjFs_new (- 542)) shifted1_P_33) (* (- 1) shifted2_x20_minus) (* (- 1) shifted2_x19_plus) shifted2_x19_minus (* (- 1) shifted2_x12_plus) (- gZwKvSn_new shifted1_P_51) (* (- 2) shifted2_x7_plus) (* 2 shifted2_x7_minus) shifted2_x5_plus (* (- 1) shifted2_x5_minus) shifted2_x2_plus (* (- 1) shifted2_x2_minus) ) 1 ) )(assert (<= (+ shifted2_x37_plus (* (- 1) shifted2_x37_minus) (- NEXCQtF_new shifted1_P_23) (* (- 1) shifted2_x31_minus) (* (- 1) (- nAGYFTC_new shifted1_P_50)) shifted2_x27_minus shifted2_x26_plus (* (- 1) shifted2_x26_minus) (* 2 shifted2_x24_plus) (* (- 2) shifted2_x24_minus) shifted2_x22_plus (* (- 1) shifted2_x22_minus) (* (- 1) shifted2_x21_plus) shifted2_x21_minus (- (- nNChjFs_new (- 542)) shifted1_P_33) (* (- 1) shifted2_x20_minus) (* (- 1) shifted2_x19_plus) shifted2_x19_minus shifted2_x18_plus (* (- 1) shifted2_x18_minus) (* (- 2) (div puEBwYN_new shifted1_P_34)) (* 2 shifted2_x17_minus) shifted2_x12_plus (* (- 1) shifted2_x12_minus) shifted2_x10_plus (* (- 1) shifted2_x10_minus) (* (- 1) shifted2_x7_plus) shifted2_x7_minus ) 1 ) )(assert (<= (+ shifted2_x39_plus (* (- 1) shifted2_x39_minus) (* (- 2) shifted2_x38_plus) (* 2 shifted2_x38_minus) (* (- 1) shifted2_x37_plus) shifted2_x37_minus (* (- 1) shifted2_x34_plus) shifted2_x34_minus (* (- 1) shifted2_x24_plus) shifted2_x24_minus (* (- 1) (- pclIuXt_new shifted1_P_20)) shifted2_x21_minus shifted2_x19_plus (* (- 1) shifted2_x19_minus) shifted2_x17_plus (* (- 1) shifted2_x17_minus) shifted2_x13_plus (* (- 1) shifted2_x13_minus) (* (- 1) shifted2_x12_plus) (div VOlcMOP_new shifted1_P_42) (* (- 1) shifted2_x8_plus) shifted2_x8_minus (* (- 1) shifted2_x3_plus) (- DlqpfIW_new shifted1_P_16) (* (- 1) shifted2_x2_plus) shifted2_x2_minus (- QFYTjoo_new shifted1_P_15) (* (- 1) shifted2_x0_minus) ) 0 ) )(assert (<= (+ shifted2_x38_plus (* (- 1) shifted2_x38_minus) shifted2_x34_plus (* (- 1) shifted2_x34_minus) (* (- 1) shifted2_x32_plus) shifted2_x32_minus shifted2_x28_plus (* (- 1) shifted2_x28_minus) shifted2_x27_plus (* (- 1) shifted2_x27_minus) shifted2_x25_plus (* (- 1) (- kAdFbmi_new shifted1_P_39)) (* (- 2) shifted2_x24_plus) (* 2 shifted2_x24_minus) shifted2_x23_plus (* (- 1) shifted2_x23_minus) shifted2_x19_plus (* (- 1) shifted2_x19_minus) (* (- 1) shifted2_x13_plus) shifted2_x13_minus (* (- 1) shifted2_x6_plus) shifted2_x6_minus shifted2_x4_plus (* (- 1) shifted2_x4_minus) shifted2_x1_plus (* (- 1) shifted2_x1_minus) (* (- 1) shifted2_x0_plus) shifted2_x0_minus ) 1 ) )(assert (<= (+ (* 2 shifted2_x38_plus) (* (- 2) shifted2_x38_minus) (* 2 (div ndfZUwN_new shifted1_P_46)) (* (- 2) shifted2_x36_minus) shifted2_x33_plus (* (- 1) shifted2_x33_minus) (* (- 1) shifted2_x29_plus) shifted2_x29_minus (* (- 1) shifted2_x28_plus) shifted2_x28_minus (* (- 2) shifted2_x25_plus) (* 2 (- kAdFbmi_new shifted1_P_39)) shifted2_x22_plus (* (- 1) shifted2_x22_minus) (* (- 2) (- (- nNChjFs_new (- 542)) shifted1_P_33)) (* 2 shifted2_x20_minus) (* (- 1) shifted2_x18_plus) shifted2_x18_minus (div puEBwYN_new shifted1_P_34) (* (- 1) shifted2_x17_minus) shifted2_x11_plus (* (- 1) shifted2_x11_minus) shifted2_x9_plus (* (- 1) (- obWVHpT_new shifted1_P_47)) shifted2_x2_plus (* (- 1) shifted2_x2_minus) (* (- 1) shifted2_x1_plus) shifted2_x1_minus ) (- 1) ) )(assert (<= (+ shifted2_x39_plus (* (- 1) shifted2_x39_minus) (* (- 2) shifted2_x37_plus) (* 2 shifted2_x37_minus) (div ndfZUwN_new shifted1_P_46) (* (- 1) (div xnbQxWN_new shifted1_P_24)) (* (- 1) shifted2_x35_plus) (- (- IcTSpor_new (- 169)) shifted1_P_19) shifted2_x31_plus (* (- 1) shifted2_x31_minus) shifted2_x22_plus (* (- 1) shifted2_x22_minus) shifted2_x21_plus (* (- 1) shifted2_x21_minus) (- (- nNChjFs_new (- 542)) shifted1_P_33) (* (- 1) shifted2_x20_minus) shifted2_x19_plus (* (- 1) shifted2_x19_minus) shifted2_x16_plus (* (- 1) shifted2_x16_minus) (* (- 2) shifted2_x15_plus) (* 2 shifted2_x15_minus) shifted2_x10_plus (* (- 1) shifted2_x10_minus) (* (- 1) shifted2_x8_plus) shifted2_x8_minus (- DBItqbo_new shifted1_dz) (* (- 1) shifted2_x2_minus) ) 0 ) )(assert (<= (+ shifted2_x37_plus (* (- 1) shifted2_x37_minus) (div ndfZUwN_new shifted1_P_46) (* (- 1) shifted2_x36_minus) (* 2 shifted2_x35_plus) (* (- 2) (- (- IcTSpor_new (- 169)) shifted1_P_19)) (* 2 shifted2_x33_plus) (* (- 2) shifted2_x33_minus) shifted2_x32_plus (* (- 1) shifted2_x32_minus) (* (- 1) (- NEXCQtF_new shifted1_P_23)) shifted2_x31_minus (* (- 1) shifted2_x30_plus) shifted2_x30_minus shifted2_x28_plus (* (- 1) shifted2_x28_minus) (* (- 1) shifted2_x26_plus) shifted2_x26_minus (* 2 shifted2_x23_plus) (* (- 2) shifted2_x23_minus) (* (- 2) shifted2_x19_plus) (* 2 shifted2_x19_minus) shifted2_x18_plus (* (- 1) shifted2_x18_minus) shifted2_x8_plus (* (- 1) shifted2_x8_minus) ) 0 ) )(assert (<= (+ shifted2_x39_plus (* (- 1) shifted2_x39_minus) shifted2_x38_plus (* (- 1) shifted2_x38_minus) shifted2_x37_plus (* (- 1) shifted2_x37_minus) shifted2_x26_plus (* (- 1) shifted2_x26_minus) (* (- 1) shifted2_x23_plus) shifted2_x23_minus shifted2_x22_plus (* (- 1) shifted2_x22_minus) (* (- 1) shifted2_x14_plus) shifted2_x14_minus (* (- 1) shifted2_x13_plus) shifted2_x13_minus (* (- 1) shifted2_x11_plus) shifted2_x11_minus shifted2_x7_plus (* (- 1) shifted2_x7_minus) shifted2_x4_plus (* (- 1) shifted2_x4_minus) (* (- 1) (- (- sopWFKn_new (- 756)) shifted1_P_37)) shifted2_x2_minus (* (- 2) (- QFYTjoo_new shifted1_P_15)) (* 2 shifted2_x0_minus) ) (- 1) ) )(assert (<= (+ shifted2_x38_plus (* (- 1) shifted2_x38_minus) (* (- 1) shifted2_x37_plus) shifted2_x37_minus shifted2_x34_plus (* (- 1) shifted2_x34_minus) shifted2_x33_plus (* (- 1) shifted2_x33_minus) shifted2_x32_plus (* (- 1) shifted2_x32_minus) (* (- 1) shifted2_x31_plus) shifted2_x31_minus shifted2_x30_plus (* (- 1) shifted2_x30_minus) shifted2_x25_plus (* (- 1) (- kAdFbmi_new shifted1_P_39)) shifted2_x22_plus (* (- 1) shifted2_x22_minus) (* (- 1) shifted2_x15_plus) shifted2_x15_minus (* (- 1) shifted2_x9_plus) (- obWVHpT_new shifted1_P_47) (* (- 1) shifted2_x7_plus) shifted2_x7_minus (* (- 1) (- (- sopWFKn_new (- 756)) shifted1_P_37)) shifted2_x2_minus ) 0 ) )(assert (<= (+ shifted2_x39_plus (* (- 1) shifted2_x39_minus) (* (- 1) shifted2_x37_plus) shifted2_x37_minus (* (- 1) shifted2_x35_plus) (- (- IcTSpor_new (- 169)) shifted1_P_19) shifted2_x32_plus (* (- 1) shifted2_x32_minus) shifted2_x28_plus (* (- 1) shifted2_x28_minus) (* (- 1) shifted2_x26_plus) shifted2_x26_minus shifted2_x22_plus (* (- 1) shifted2_x22_minus) (* (- 1) (- pclIuXt_new shifted1_P_20)) shifted2_x21_minus (* 2 shifted2_x7_plus) (* (- 2) shifted2_x7_minus) (* (- 1) shifted2_x6_plus) shifted2_x6_minus (* (- 1) shifted2_x4_plus) shifted2_x4_minus shifted2_x3_plus (* (- 1) (- DlqpfIW_new shifted1_P_16)) (* (- 1) (- (- BueQASA_new 883) shifted1_P_43)) shifted2_x1_minus ) (- 1) ) )(assert (<= (+ shifted2_x38_plus (* (- 1) shifted2_x38_minus) (* (- 1) shifted2_x37_plus) shifted2_x37_minus (div ndfZUwN_new shifted1_P_46) (* (- 1) (div xnbQxWN_new shifted1_P_24)) (* (- 1) shifted2_x34_plus) shifted2_x34_minus (* (- 1) shifted2_x32_plus) shifted2_x32_minus shifted2_x26_plus (* (- 1) shifted2_x26_minus) (* (- 1) shifted2_x25_plus) (- (- vEEUsHa_new (- 786)) shifted1_P_38) (* (- 2) shifted2_x22_plus) (* 2 shifted2_x22_minus) (* (- 1) shifted2_x19_plus) shifted2_x19_minus (* (- 1) shifted2_x15_plus) shifted2_x15_minus (* (- 1) shifted2_x14_plus) shifted2_x14_minus shifted2_x13_plus (* (- 1) shifted2_x13_minus) (* (- 1) shifted2_x11_plus) shifted2_x11_minus ) 0 ) )(assert (<= (+ shifted2_x39_plus (* (- 1) shifted2_x39_minus) shifted2_x37_plus (* (- 1) shifted2_x37_minus) shifted2_x33_plus (* (- 1) shifted2_x33_minus) (* (- 1) (- NEXCQtF_new shifted1_P_23)) shifted2_x31_minus shifted2_x30_plus (* (- 1) shifted2_x30_minus) shifted2_x29_plus (* (- 1) shifted2_x29_minus) shifted2_x27_plus (* (- 1) shifted2_x27_minus) (* (- 1) shifted2_x26_plus) shifted2_x26_minus shifted2_x22_plus (* (- 1) shifted2_x22_minus) (- pclIuXt_new shifted1_P_20) (* (- 1) shifted2_x21_minus) (* (- 1) shifted2_x20_plus) shifted2_x20_minus (div IrJEuXI_new shifted1_P_32) (* (- 1) (- (- lRzOrzO_new 626) shifted1_P_63)) shifted2_x3_plus (* (- 1) (- DlqpfIW_new shifted1_P_16)) ) (- 1) ) )(assert (<= (+ shifted2_x39_plus (* (- 1) shifted2_x39_minus) (* (- 2) shifted2_x37_plus) (* 2 shifted2_x37_minus) (* (- 1) shifted2_x35_plus) (- QWjBzHC_new shifted1_P_36) shifted2_x30_plus (* (- 1) shifted2_x30_minus) (* (- 2) shifted2_x27_plus) (* 2 shifted2_x27_minus) shifted2_x23_plus (* (- 1) shifted2_x23_minus) (- (- nNChjFs_new (- 542)) shifted1_P_33) (* (- 1) shifted2_x20_minus) (* (- 1) shifted2_x16_plus) shifted2_x16_minus shifted2_x13_plus (* (- 1) shifted2_x13_minus) (* (- 1) shifted2_x11_plus) shifted2_x11_minus (* (- 1) shifted2_x8_plus) shifted2_x8_minus ) (- 1) ) )(assert (<= (+ shifted2_x33_plus (* (- 1) shifted2_x33_minus) (* (- 1) shifted2_x29_plus) shifted2_x29_minus (* (- 1) shifted2_x26_plus) shifted2_x26_minus (* (- 1) shifted2_x25_plus) shifted2_x25_minus (* (- 2) shifted2_x23_plus) (* 2 shifted2_x23_minus) (- pclIuXt_new shifted1_P_20) (* (- 1) shifted2_x21_minus) (* (- 1) shifted2_x15_plus) shifted2_x15_minus (* (- 1) shifted2_x11_plus) shifted2_x11_minus (* 2 shifted2_x9_plus) (* (- 2) shifted2_x9_minus) (* (- 2) shifted2_x4_plus) (* 2 shifted2_x4_minus) (* (- 1) (- (- BueQASA_new 883) shifted1_P_43)) shifted2_x1_minus ) (- 1) ) )(assert (<= (+ shifted2_x32_plus (* (- 1) shifted2_x32_minus) shifted2_x29_plus (* (- 1) shifted2_x29_minus) (* (- 2) shifted2_x26_plus) (* 2 shifted2_x26_minus) (* (- 1) shifted2_x22_plus) shifted2_x22_minus (* 2 shifted2_x21_plus) (* (- 2) shifted2_x21_minus) (* (- 1) shifted2_x19_plus) shifted2_x19_minus shifted2_x15_plus (* (- 1) shifted2_x15_minus) (div IrJEuXI_new shifted1_P_32) (* (- 1) shifted2_x10_minus) (* (- 3) shifted2_x7_plus) (* 3 shifted2_x7_minus) shifted2_x6_plus (* (- 1) shifted2_x6_minus) (* (- 1) shifted2_x1_plus) shifted2_x1_minus ) 1 ) )(assert (>= (+ shifted2_x38_plus (* (- 1) shifted2_x38_minus) shifted2_x35_plus (* (- 1) (- (- IcTSpor_new (- 169)) shifted1_P_19)) shifted2_x33_plus (* (- 1) shifted2_x33_minus) (* (- 1) shifted2_x30_plus) shifted2_x30_minus (* (- 1) shifted2_x29_plus) shifted2_x29_minus (* (- 2) shifted2_x28_plus) (* 2 shifted2_x28_minus) (* (- 2) shifted2_x27_plus) (* 2 shifted2_x27_minus) (* (- 1) shifted2_x26_plus) shifted2_x26_minus (- (- nNChjFs_new (- 542)) shifted1_P_33) (* (- 1) shifted2_x20_minus) (* (- 1) shifted2_x18_plus) shifted2_x18_minus (div puEBwYN_new shifted1_P_34) (* (- 1) shifted2_x17_minus) shifted2_x16_plus (* (- 1) shifted2_x16_minus) (* (- 1) shifted2_x14_plus) shifted2_x14_minus (* (- 1) shifted2_x13_plus) shifted2_x13_minus (* (- 1) shifted2_x11_plus) shifted2_x11_minus (* (- 1) (div IrJEuXI_new shifted1_P_32)) shifted2_x10_minus shifted2_x8_plus (* (- 1) shifted2_x8_minus) (- (- sopWFKn_new (- 756)) shifted1_P_37) (* (- 1) shifted2_x2_minus) shifted2_x1_plus (* (- 1) shifted2_x1_minus) (- QFYTjoo_new shifted1_P_15) (* (- 1) shifted2_x0_minus) ) (- 1) ) )(assert (>= (+ shifted2_x39_plus (* (- 1) shifted2_x39_minus) shifted2_x38_plus (* (- 1) shifted2_x38_minus) shifted2_x37_plus (* (- 1) shifted2_x37_minus) (* (- 1) shifted2_x34_plus) shifted2_x34_minus shifted2_x31_plus (* (- 1) shifted2_x31_minus) (* (- 1) shifted2_x27_plus) shifted2_x27_minus (* (- 1) shifted2_x25_plus) shifted2_x25_minus (* (- 1) shifted2_x24_plus) shifted2_x24_minus (* (- 1) shifted2_x21_plus) shifted2_x21_minus (* (- 1) (- (- nNChjFs_new (- 542)) shifted1_P_33)) shifted2_x20_minus (* (- 1) shifted2_x19_plus) shifted2_x19_minus shifted2_x17_plus (* (- 1) shifted2_x17_minus) (* (- 1) shifted2_x15_plus) shifted2_x15_minus shifted2_x12_plus (* (- 1) (div VOlcMOP_new shifted1_P_42)) (* (- 1) shifted2_x11_plus) shifted2_x11_minus shifted2_x8_plus (* (- 1) shifted2_x8_minus) (* (- 1) shifted2_x6_plus) shifted2_x6_minus (* (- 1) shifted2_x3_plus) (- DlqpfIW_new shifted1_P_16) (* (- 1) (- (- sopWFKn_new (- 756)) shifted1_P_37)) shifted2_x2_minus (* 2 (- (- BueQASA_new 883) shifted1_P_43)) (* (- 2) shifted2_x1_minus) ) 1 ) )(assert (>= (+ shifted2_x34_plus (* (- 1) shifted2_x34_minus) shifted2_x33_plus (* (- 1) shifted2_x33_minus) shifted2_x32_plus (* (- 1) shifted2_x32_minus) (* (- 1) shifted2_x28_plus) shifted2_x28_minus (* (- 1) shifted2_x26_plus) shifted2_x26_minus (* 2 shifted2_x24_plus) (* (- 2) shifted2_x24_minus) (* (- 1) shifted2_x22_plus) shifted2_x22_minus shifted2_x21_plus (* (- 1) shifted2_x21_minus) (- (- nNChjFs_new (- 542)) shifted1_P_33) (* (- 1) shifted2_x20_minus) (* 2 shifted2_x19_plus) (* (- 2) shifted2_x19_minus) (* (- 1) shifted2_x13_plus) shifted2_x13_minus shifted2_x12_plus (* (- 1) (div VOlcMOP_new shifted1_P_42)) shifted2_x9_plus (* (- 1) shifted2_x9_minus) (* (- 1) shifted2_x7_plus) shifted2_x7_minus shifted2_x5_plus (* (- 1) shifted2_x5_minus) shifted2_x4_plus (* (- 1) shifted2_x4_minus) (* (- 1) shifted2_x3_plus) shifted2_x3_minus (* (- 1) (- DBItqbo_new shifted1_dz)) shifted2_x2_minus (- QFYTjoo_new shifted1_P_15) (* (- 1) shifted2_x0_minus) ) 0 ) )(assert (>= (+ shifted2_x39_plus (* (- 1) shifted2_x39_minus) shifted2_x38_plus (* (- 1) shifted2_x38_minus) (* (- 1) shifted2_x37_plus) shifted2_x37_minus (* (- 1) shifted2_x34_plus) shifted2_x34_minus (* (- 2) shifted2_x33_plus) (* 2 shifted2_x33_minus) (* (- 1) shifted2_x31_plus) shifted2_x31_minus shifted2_x29_plus (* (- 1) shifted2_x29_minus) (* (- 1) shifted2_x26_plus) shifted2_x26_minus (* (- 1) shifted2_x23_plus) shifted2_x23_minus shifted2_x15_plus (* (- 1) shifted2_x15_minus) shifted2_x13_plus (* (- 1) shifted2_x13_minus) (* (- 1) shifted2_x12_plus) (div VOlcMOP_new shifted1_P_42) shifted2_x11_plus (* (- 1) shifted2_x11_minus) shifted2_x7_plus (* (- 1) shifted2_x7_minus) (* (- 1) shifted2_x5_plus) shifted2_x5_minus (* (- 1) shifted2_x4_plus) shifted2_x4_minus (* 3 shifted2_x3_plus) (* (- 3) shifted2_x3_minus) ) (- 1) ) )(assert (>= (+ shifted2_x37_plus (* (- 1) shifted2_x37_minus) shifted2_x35_plus (* (- 1) (- QWjBzHC_new shifted1_P_36)) shifted2_x34_plus (* (- 1) shifted2_x34_minus) (* (- 2) (- nAGYFTC_new shifted1_P_50)) (* 2 shifted2_x27_minus) (* (- 1) shifted2_x26_plus) shifted2_x26_minus (* (- 1) shifted2_x24_plus) shifted2_x24_minus shifted2_x23_plus (* (- 1) shifted2_x23_minus) shifted2_x21_plus (* (- 1) shifted2_x21_minus) (* (- 1) (- (- nNChjFs_new (- 542)) shifted1_P_33)) shifted2_x20_minus shifted2_x19_plus (* (- 1) shifted2_x19_minus) (* (- 1) shifted2_x18_plus) shifted2_x18_minus shifted2_x15_plus (* (- 1) shifted2_x15_minus) (* (- 1) shifted2_x7_plus) shifted2_x7_minus (* (- 2) shifted2_x4_plus) (* 2 shifted2_x4_minus) shifted2_x3_plus (* (- 1) (- DlqpfIW_new shifted1_P_16)) (- (- BueQASA_new 883) shifted1_P_43) (* (- 1) shifted2_x1_minus) ) 0 ) )(assert (>= (+ shifted2_x35_plus (* (- 1) (- QWjBzHC_new shifted1_P_36)) (* (- 2) shifted2_x33_plus) (* 2 shifted2_x33_minus) (- NEXCQtF_new shifted1_P_23) (* (- 1) shifted2_x31_minus) (* (- 2) shifted2_x30_plus) (* 2 shifted2_x30_minus) (* (- 2) shifted2_x29_plus) (* 2 shifted2_x29_minus) (* (- 1) shifted2_x28_plus) shifted2_x28_minus shifted2_x27_plus (* (- 1) shifted2_x27_minus) (* (- 1) shifted2_x22_plus) shifted2_x22_minus (* (- 1) (- (- nNChjFs_new (- 542)) shifted1_P_33)) shifted2_x20_minus (* (- 1) (div puEBwYN_new shifted1_P_34)) shifted2_x17_minus shifted2_x12_plus (* (- 1) (div VOlcMOP_new shifted1_P_42)) shifted2_x11_plus (* (- 1) shifted2_x11_minus) (* (- 1) shifted2_x8_plus) shifted2_x8_minus shifted2_x7_plus (* (- 1) shifted2_x7_minus) (* (- 1) shifted2_x5_plus) shifted2_x5_minus shifted2_x4_plus (* (- 1) shifted2_x4_minus) ) 0 ) )(assert (>= (+ shifted2_x38_plus (* (- 1) shifted2_x38_minus) shifted2_x32_plus (* (- 1) shifted2_x32_minus) (* (- 1) (- NEXCQtF_new shifted1_P_23)) shifted2_x31_minus (* (- 2) shifted2_x26_plus) (* 2 shifted2_x26_minus) (* (- 1) shifted2_x25_plus) (- (- vEEUsHa_new (- 786)) shifted1_P_38) shifted2_x23_plus (* (- 1) shifted2_x23_minus) shifted2_x22_plus (* (- 1) shifted2_x22_minus) (* (- 1) shifted2_x21_plus) shifted2_x21_minus (* (- 1) shifted2_x19_plus) shifted2_x19_minus (* (- 1) shifted2_x18_plus) shifted2_x18_minus shifted2_x10_plus (* (- 1) shifted2_x10_minus) (* (- 1) shifted2_x9_plus) (- obWVHpT_new shifted1_P_47) (* (- 2) shifted2_x7_plus) (* 2 shifted2_x7_minus) (* (- 1) shifted2_x6_plus) shifted2_x6_minus (* (- 1) shifted2_x5_plus) shifted2_x5_minus (* (- 1) shifted2_x4_plus) shifted2_x4_minus ) 0 ) )(assert (>= (+ shifted2_x39_plus (* (- 1) shifted2_x39_minus) (* (- 1) shifted2_x37_plus) shifted2_x37_minus (* 2 shifted2_x33_plus) (* (- 2) shifted2_x33_minus) (* (- 1) shifted2_x32_plus) shifted2_x32_minus (* (- 2) shifted2_x24_plus) (* 2 shifted2_x24_minus) shifted2_x23_plus (* (- 1) shifted2_x23_minus) (* (- 1) (- pclIuXt_new shifted1_P_20)) shifted2_x21_minus shifted2_x18_plus (* (- 1) shifted2_x18_minus) (div puEBwYN_new shifted1_P_34) (* (- 1) shifted2_x17_minus) (* (- 1) shifted2_x12_plus) (- gZwKvSn_new shifted1_P_51) shifted2_x11_plus (* (- 1) shifted2_x11_minus) (* (- 1) shifted2_x7_plus) shifted2_x7_minus (* (- 1) shifted2_x6_plus) shifted2_x6_minus shifted2_x3_plus (* (- 1) (- DlqpfIW_new shifted1_P_16)) (- (- sopWFKn_new (- 756)) shifted1_P_37) (* (- 1) shifted2_x2_minus) (- (- BueQASA_new 883) shifted1_P_43) (* (- 1) shifted2_x1_minus) ) 0 ) )(assert (>= (+ (* 2 shifted2_x39_plus) (* (- 2) shifted2_x39_minus) shifted2_x34_plus (* (- 1) shifted2_x34_minus) (* (- 1) shifted2_x33_plus) shifted2_x33_minus shifted2_x32_plus (* (- 1) shifted2_x32_minus) (* 2 shifted2_x27_plus) (* (- 2) shifted2_x27_minus) (* (- 1) shifted2_x26_plus) shifted2_x26_minus (* (- 1) shifted2_x22_plus) shifted2_x22_minus shifted2_x20_plus (* (- 1) shifted2_x20_minus) shifted2_x19_plus (* (- 1) shifted2_x19_minus) (* (- 1) shifted2_x15_plus) shifted2_x15_minus (* (- 1) (div UVgkblP_new shifted1_P_48)) shifted2_x14_minus shifted2_x9_plus (* (- 1) shifted2_x9_minus) shifted2_x7_plus (* (- 1) shifted2_x7_minus) shifted2_x6_plus (* (- 1) shifted2_x6_minus) (* (- 1) shifted2_x4_plus) shifted2_x4_minus ) 0 ) )(assert (>= (+ shifted2_x38_plus (* (- 1) shifted2_x38_minus) (* (- 1) shifted2_x37_plus) shifted2_x37_minus shifted2_x36_plus (* (- 1) (div xnbQxWN_new shifted1_P_24)) shifted2_x33_plus (* (- 1) shifted2_x33_minus) (* (- 1) shifted2_x30_plus) shifted2_x30_minus shifted2_x29_plus (* (- 1) shifted2_x29_minus) (* (- 1) shifted2_x28_plus) shifted2_x28_minus (* (- 1) (- nAGYFTC_new shifted1_P_50)) shifted2_x27_minus shifted2_x22_plus (* (- 1) shifted2_x22_minus) (* (- 1) (- pclIuXt_new shifted1_P_20)) shifted2_x21_minus (* 2 (- (- nNChjFs_new (- 542)) shifted1_P_33)) (* (- 2) shifted2_x20_minus) (* (- 1) shifted2_x18_plus) shifted2_x18_minus (* (- 1) shifted2_x17_plus) shifted2_x17_minus shifted2_x3_plus (* (- 1) shifted2_x3_minus) (- (- BueQASA_new 883) shifted1_P_43) (* (- 1) shifted2_x1_minus) ) 1 ) )(assert (>= (+ (* 3 shifted2_x36_plus) (* (- 3) (div xnbQxWN_new shifted1_P_24)) (* (- 1) shifted2_x33_plus) shifted2_x33_minus (* (- 1) shifted2_x32_plus) shifted2_x32_minus shifted2_x26_plus (* (- 1) shifted2_x26_minus) (* (- 2) shifted2_x25_plus) (* 2 (- (- vEEUsHa_new (- 786)) shifted1_P_38)) (* (- 1) shifted2_x23_plus) shifted2_x23_minus (* (- 1) shifted2_x19_plus) shifted2_x19_minus shifted2_x18_plus (* (- 1) shifted2_x18_minus) (* (- 1) shifted2_x12_plus) (div VOlcMOP_new shifted1_P_42) shifted2_x11_plus (* (- 1) shifted2_x11_minus) shifted2_x9_plus (* (- 1) (- obWVHpT_new shifted1_P_47)) shifted2_x6_plus (* (- 1) shifted2_x6_minus) (* (- 1) shifted2_x3_plus) (- DlqpfIW_new shifted1_P_16) (* 2 (- (- sopWFKn_new (- 756)) shifted1_P_37)) (* (- 2) shifted2_x2_minus) (- (- BueQASA_new 883) shifted1_P_43) (* (- 1) shifted2_x1_minus) ) 1 ) )(assert (>= (+ shifted2_x39_plus (* (- 1) shifted2_x39_minus) shifted2_x38_plus (* (- 1) shifted2_x38_minus) (* (- 1) (- NEXCQtF_new shifted1_P_23)) shifted2_x31_minus shifted2_x30_plus (* (- 1) shifted2_x30_minus) shifted2_x29_plus (* (- 1) shifted2_x29_minus) shifted2_x26_plus (* (- 1) shifted2_x26_minus) (* (- 1) shifted2_x19_plus) shifted2_x19_minus shifted2_x17_plus (* (- 1) shifted2_x17_minus) shifted2_x16_plus (* (- 1) shifted2_x16_minus) shifted2_x13_plus (* (- 1) shifted2_x13_minus) (* (- 1) shifted2_x8_plus) shifted2_x8_minus shifted2_x6_plus (* (- 1) shifted2_x6_minus) (* (- 1) shifted2_x5_plus) shifted2_x5_minus shifted2_x4_plus (* (- 1) shifted2_x4_minus) (* 2 shifted2_x0_plus) (* (- 2) shifted2_x0_minus) ) 0 ) )(assert (>= (+ shifted2_x37_plus (* (- 1) shifted2_x37_minus) shifted2_x35_plus (* (- 1) (- QWjBzHC_new shifted1_P_36)) shifted2_x34_plus (* (- 1) shifted2_x34_minus) (- NEXCQtF_new shifted1_P_23) (* (- 1) shifted2_x31_minus) (* (- 1) shifted2_x28_plus) shifted2_x28_minus (* (- 1) shifted2_x26_plus) shifted2_x26_minus shifted2_x24_plus (* (- 1) shifted2_x24_minus) (* (- 1) shifted2_x22_plus) shifted2_x22_minus shifted2_x15_plus (* (- 1) shifted2_x15_minus) shifted2_x12_plus (* (- 1) (div VOlcMOP_new shifted1_P_42)) shifted2_x10_plus (* (- 1) shifted2_x10_minus) (* (- 1) shifted2_x9_plus) shifted2_x9_minus shifted2_x6_plus (* (- 1) shifted2_x6_minus) (* (- 1) shifted2_x5_plus) shifted2_x5_minus (* (- 1) shifted2_x4_plus) shifted2_x4_minus ) 0 ) )(assert (>= (+ shifted2_x36_plus (* (- 1) shifted2_x36_minus) shifted2_x34_plus (* (- 1) shifted2_x34_minus) (* (- 1) shifted2_x32_plus) shifted2_x32_minus (- NEXCQtF_new shifted1_P_23) (* (- 1) shifted2_x31_minus) (* (- 1) shifted2_x29_plus) shifted2_x29_minus shifted2_x27_plus (* (- 1) shifted2_x27_minus) shifted2_x24_plus (* (- 1) shifted2_x24_minus) (* (- 1) shifted2_x23_plus) shifted2_x23_minus (* (- 1) shifted2_x22_plus) shifted2_x22_minus (* (- 1) shifted2_x21_plus) shifted2_x21_minus (* (- 1) shifted2_x19_plus) shifted2_x19_minus shifted2_x18_plus (* (- 1) shifted2_x18_minus) (div UVgkblP_new shifted1_P_48) (* (- 1) shifted2_x14_minus) (* (- 1) shifted2_x9_plus) (- obWVHpT_new shifted1_P_47) (* (- 1) shifted2_x6_plus) shifted2_x6_minus ) (- 1) ) )(assert (>= (+ shifted2_x38_plus (* (- 1) shifted2_x38_minus) (* (- 1) (div ndfZUwN_new shifted1_P_46)) (div xnbQxWN_new shifted1_P_24) (* (- 1) shifted2_x35_plus) shifted2_x35_minus (* (- 1) shifted2_x34_plus) shifted2_x34_minus (* 2 shifted2_x33_plus) (* (- 2) shifted2_x33_minus) (* (- 1) shifted2_x27_plus) shifted2_x27_minus shifted2_x24_plus (* (- 1) shifted2_x24_minus) shifted2_x22_plus (* (- 1) shifted2_x22_minus) shifted2_x20_plus (* (- 1) shifted2_x20_minus) shifted2_x19_plus (* (- 1) shifted2_x19_minus) (* (- 2) shifted2_x13_plus) (* 2 shifted2_x13_minus) (* (- 1) shifted2_x8_plus) shifted2_x8_minus (* (- 1) shifted2_x7_plus) shifted2_x7_minus (* (- 1) shifted2_x5_plus) shifted2_x5_minus (* (- 1) (- (- BueQASA_new 883) shifted1_P_43)) shifted2_x1_minus ) 1 ) )(assert (>= (+ shifted2_x38_plus (* (- 1) shifted2_x38_minus) (* (- 1) shifted2_x35_plus) shifted2_x35_minus (* (- 1) shifted2_x31_plus) shifted2_x31_minus (* (- 2) shifted2_x27_plus) (* 2 shifted2_x27_minus) (* (- 1) shifted2_x23_plus) shifted2_x23_minus shifted2_x22_plus (* (- 1) shifted2_x22_minus) shifted2_x19_plus (* (- 1) shifted2_x19_minus) (* 4 shifted2_x18_plus) (* (- 4) shifted2_x18_minus) shifted2_x17_plus (* (- 1) shifted2_x17_minus) (* 2 (div UVgkblP_new shifted1_P_48)) (* (- 2) shifted2_x14_minus) (* (- 1) shifted2_x12_plus) (- gZwKvSn_new shifted1_P_51) shifted2_x11_plus (* (- 1) shifted2_x11_minus) shifted2_x6_plus (* (- 1) shifted2_x6_minus) (* (- 1) (- QFYTjoo_new shifted1_P_15)) shifted2_x0_minus ) 1 ) )(assert (>= (+ shifted2_x38_plus (* (- 1) shifted2_x38_minus) (* (- 1) shifted2_x37_plus) shifted2_x37_minus (* 2 shifted2_x30_plus) (* (- 2) shifted2_x30_minus) (* (- 1) shifted2_x23_plus) shifted2_x23_minus shifted2_x19_plus (* (- 1) shifted2_x19_minus) (* (- 1) shifted2_x17_plus) shifted2_x17_minus (* (- 1) shifted2_x16_plus) shifted2_x16_minus (* (- 2) shifted2_x11_plus) (* 2 shifted2_x11_minus) shifted2_x9_plus (* (- 1) (- obWVHpT_new shifted1_P_47)) (* (- 1) (- (- sopWFKn_new (- 756)) shifted1_P_37)) shifted2_x2_minus (* (- 1) shifted2_x0_plus) shifted2_x0_minus ) 0 ) )(assert (>= (+ shifted2_x39_plus (* (- 1) shifted2_x39_minus) (* (- 1) shifted2_x38_plus) shifted2_x38_minus shifted2_x33_plus (* (- 1) shifted2_x33_minus) (* (- 1) shifted2_x23_plus) shifted2_x23_minus shifted2_x22_plus (* (- 1) shifted2_x22_minus) shifted2_x19_plus (* (- 1) shifted2_x19_minus) shifted2_x17_plus (* (- 1) shifted2_x17_minus) shifted2_x10_plus (* (- 1) (- (- lRzOrzO_new 626) shifted1_P_63)) shifted2_x9_plus (* (- 1) shifted2_x9_minus) (* (- 1) shifted2_x7_plus) shifted2_x7_minus (* (- 1) shifted2_x6_plus) shifted2_x6_minus ) 0 ) )(assert (>= (+ shifted2_x39_plus (* (- 1) shifted2_x39_minus) (* (- 1) shifted2_x38_plus) shifted2_x38_minus (* (- 1) shifted2_x36_plus) shifted2_x36_minus (* (- 1) shifted2_x33_plus) shifted2_x33_minus shifted2_x32_plus (* (- 1) shifted2_x32_minus) (* (- 1) shifted2_x27_plus) shifted2_x27_minus (* 2 shifted2_x19_plus) (* (- 2) shifted2_x19_minus) shifted2_x11_plus (* (- 1) shifted2_x11_minus) (* (- 1) shifted2_x3_plus) (- DlqpfIW_new shifted1_P_16) (* (- 1) shifted2_x0_plus) shifted2_x0_minus ) (- 1) ) )(assert (>= (+ shifted2_x38_plus (* (- 1) shifted2_x38_minus) shifted2_x30_plus (* (- 1) shifted2_x30_minus) shifted2_x26_plus (* (- 1) shifted2_x26_minus) (* (- 1) shifted2_x23_plus) shifted2_x23_minus (div puEBwYN_new shifted1_P_34) (* (- 1) shifted2_x17_minus) shifted2_x16_plus (* (- 1) shifted2_x16_minus) shifted2_x7_plus (* (- 1) shifted2_x7_minus) shifted2_x6_plus (* (- 1) shifted2_x6_minus) (* (- 1) shifted2_x5_plus) shifted2_x5_minus (* 3 (- QFYTjoo_new shifted1_P_15)) (* (- 3) shifted2_x0_minus) ) 0 ) )(check-sat)(exit)

ASSERTION VIOLATION
File: ../src/smt/theory_arith_inv.h
Line: 197
!below_lower(v)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB