positive_determinant_matrix_data_integer_transport

forall ab ac bb bc eb ec fb fc d D. (forall ics_index_data_integer_equal ics_value0_data_integer_equal ics_value1_data_integer_equal ics_value2_data_integer_equal ics_value3_data_integer_equal. (exists ics_gap_data_integer_equal_bound. ics_gap_data_integer_equal_bound + S (ics_index_data_integer_equal) = ((d) * (d))) -> (((exists fs_h_ics_data_integer_equal_at0. fs_h_ics_data_integer_equal_at0 + S (ics_value0_data_integer_equal) = S ((S (ics_index_data_integer_equal)) * ac)) /\ exists fs_q_ics_data_integer_equal_at0. ab = fs_q_ics_data_integer_equal_at0 * S ((S (ics_index_data_integer_equal)) * ac) + (ics_value0_data_integer_equal))) -> (((exists fs_h_ics_data_integer_equal_at1. fs_h_ics_data_integer_equal_at1 + S (ics_value1_data_integer_equal) = S ((S (ics_index_data_integer_equal)) * bc)) /\ exists fs_q_ics_data_integer_equal_at1. bb = fs_q_ics_data_integer_equal_at1 * S ((S (ics_index_data_integer_equal)) * bc) + (ics_value1_data_integer_equal))) -> (((exists fs_h_ics_data_integer_equal_at2. fs_h_ics_data_integer_equal_at2 + S (ics_value2_data_integer_equal) = S ((S (ics_index_data_integer_equal)) * ec)) /\ exists fs_q_ics_data_integer_equal_at2. eb = fs_q_ics_data_integer_equal_at2 * S ((S (ics_index_data_integer_equal)) * ec) + (ics_value2_data_integer_equal))) -> (((exists fs_h_ics_data_integer_equal_at3. fs_h_ics_data_integer_equal_at3 + S (ics_value3_data_integer_equal) = S ((S (ics_index_data_integer_equal)) * fc)) /\ exists fs_q_ics_data_integer_equal_at3. fb = fs_q_ics_data_integer_equal_at3 * S ((S (ics_index_data_integer_equal)) * fc) + (ics_value3_data_integer_equal))) -> ics_value0_data_integer_equal + ics_value3_data_integer_equal = ics_value2_data_integer_equal + ics_value1_data_integer_equal) -> (((~(d = 0)) /\ ((~(D = 0)) /\ (exists mdr_p_data_integer_firstabsolute mdr_n_data_integer_firstabsolute. ((exists mdr_b_data_integer_firstabsoluteevaluation mdr_c_data_integer_firstabsoluteevaluation mdr_l_data_integer_firstabsoluteevaluation mdr_i_data_integer_firstabsoluteevaluation. ((forall mdr_i_data_integer_firstabsoluteevaluationh. (exists mdr_gap_data_integer_firstabsoluteevaluationhi. mdr_gap_data_integer_firstabsoluteevaluationhi + S (mdr_i_data_integer_firstabsoluteevaluationh) = (mdr_l_data_integer_firstabsoluteevaluation)) -> exists mdr_d_data_integer_firstabsoluteevaluationh mdr_pb_data_integer_firstabsoluteevaluationh mdr_pc_data_integer_firstabsoluteevaluationh mdr_nb_data_integer_firstabsoluteevaluationh mdr_nc_data_integer_firstabsoluteevaluationh mdr_p_data_integer_firstabsoluteevaluationh mdr_n_data_integer_firstabsoluteevaluationh. ((exists mdr_z_data_integer_firstabsoluteevaluationhr. ((exists mdr_a_data_integer_firstabsoluteevaluationhrc mdr_b_data_integer_firstabsoluteevaluationhrc mdr_c_data_integer_firstabsoluteevaluationhrc mdr_e_data_integer_firstabsoluteevaluationhrc mdr_f_data_integer_firstabsoluteevaluationhrc. ((mdr_a_data_integer_firstabsoluteevaluationhrc = ((mdr_d_data_integer_firstabsoluteevaluationh) + (mdr_pb_data_integer_firstabsoluteevaluationh)) * S ((mdr_d_data_integer_firstabsoluteevaluationh) + (mdr_pb_data_integer_firstabsoluteevaluationh)) + ((mdr_pb_data_integer_firstabsoluteevaluationh) + (mdr_pb_data_integer_firstabsoluteevaluationh))) /\ ((mdr_b_data_integer_firstabsoluteevaluationhrc = ((mdr_pc_data_integer_firstabsoluteevaluationh) + (mdr_nb_data_integer_firstabsoluteevaluationh)) * S ((mdr_pc_data_integer_firstabsoluteevaluationh) + (mdr_nb_data_integer_firstabsoluteevaluationh)) + ((mdr_nb_data_integer_firstabsoluteevaluationh) + (mdr_nb_data_integer_firstabsoluteevaluationh))) /\ ((mdr_c_data_integer_firstabsoluteevaluationhrc = ((mdr_a_data_integer_firstabsoluteevaluationhrc) + (mdr_b_data_integer_firstabsoluteevaluationhrc)) * S ((mdr_a_data_integer_firstabsoluteevaluationhrc) + (mdr_b_data_integer_firstabsoluteevaluationhrc)) + ((mdr_b_data_integer_firstabsoluteevaluationhrc) + (mdr_b_data_integer_firstabsoluteevaluationhrc))) /\ ((mdr_e_data_integer_firstabsoluteevaluationhrc = ((mdr_p_data_integer_firstabsoluteevaluationh) + (mdr_n_data_integer_firstabsoluteevaluationh)) * S ((mdr_p_data_integer_firstabsoluteevaluationh) + (mdr_n_data_integer_firstabsoluteevaluationh)) + ((mdr_n_data_integer_firstabsoluteevaluationh) + (mdr_n_data_integer_firstabsoluteevaluationh))) /\ ((mdr_f_data_integer_firstabsoluteevaluationhrc = ((mdr_nc_data_integer_firstabsoluteevaluationh) + (mdr_e_data_integer_firstabsoluteevaluationhrc)) * S ((mdr_nc_data_integer_firstabsoluteevaluationh) + (mdr_e_data_integer_firstabsoluteevaluationhrc)) + ((mdr_e_data_integer_firstabsoluteevaluationhrc) + (mdr_e_data_integer_firstabsoluteevaluationhrc))) /\ ((mdr_z_data_integer_firstabsoluteevaluationhr) = ((mdr_c_data_integer_firstabsoluteevaluationhrc) + (mdr_f_data_integer_firstabsoluteevaluationhrc)) * S ((mdr_c_data_integer_firstabsoluteevaluationhrc) + (mdr_f_data_integer_firstabsoluteevaluationhrc)) + ((mdr_f_data_integer_firstabsoluteevaluationhrc) + (mdr_f_data_integer_firstabsoluteevaluationhrc))))))))) /\ (((exists ff_h_mdr_data_integer_firstabsoluteevaluationhrb. ff_h_mdr_data_integer_firstabsoluteevaluationhrb + S (mdr_z_data_integer_firstabsoluteevaluationhr) = S ((S (mdr_i_data_integer_firstabsoluteevaluationh)) * mdr_c_data_integer_firstabsoluteevaluation)) /\ exists ff_q_mdr_data_integer_firstabsoluteevaluationhrb. mdr_b_data_integer_firstabsoluteevaluation = ff_q_mdr_data_integer_firstabsoluteevaluationhrb * S ((S (mdr_i_data_integer_firstabsoluteevaluationh)) * mdr_c_data_integer_firstabsoluteevaluation) + (mdr_z_data_integer_firstabsoluteevaluationhr))))) /\ (((((mdr_d_data_integer_firstabsoluteevaluationh) = 0) /\ (((mdr_p_data_integer_firstabsoluteevaluationh) = 1) /\ ((mdr_n_data_integer_firstabsoluteevaluationh) = 0))) \/ exists mdr_q_data_integer_firstabsoluteevaluationhs mdr_eb_data_integer_firstabsoluteevaluationhs mdr_ec_data_integer_firstabsoluteevaluationhs mdr_fb_data_integer_firstabsoluteevaluationhs mdr_fc_data_integer_firstabsoluteevaluationhs. (((mdr_d_data_integer_firstabsoluteevaluationh) = S (mdr_q_data_integer_firstabsoluteevaluationhs)) /\ ((forall mdr_j_data_integer_firstabsoluteevaluationhsc. (exists mdr_gap_data_integer_firstabsoluteevaluationhscj. mdr_gap_data_integer_firstabsoluteevaluationhscj + S (mdr_j_data_integer_firstabsoluteevaluationhsc) = (S (mdr_q_data_integer_firstabsoluteevaluationhs))) -> exists mdr_i_data_integer_firstabsoluteevaluationhsc mdr_up_data_integer_firstabsoluteevaluationhsc mdr_us_data_integer_firstabsoluteevaluationhsc mdr_un_data_integer_firstabsoluteevaluationhsc mdr_ut_data_integer_firstabsoluteevaluationhsc mdr_p_data_integer_firstabsoluteevaluationhsc mdr_n_data_integer_firstabsoluteevaluationhsc. ((exists mdr_gap_data_integer_firstabsoluteevaluationhsci. mdr_gap_data_integer_firstabsoluteevaluationhsci + S (mdr_i_data_integer_firstabsoluteevaluationhsc) = (mdr_i_data_integer_firstabsoluteevaluationh)) /\ ((exists mdr_z_data_integer_firstabsoluteevaluationhscr. ((exists mdr_a_data_integer_firstabsoluteevaluationhscrc mdr_b_data_integer_firstabsoluteevaluationhscrc mdr_c_data_integer_firstabsoluteevaluationhscrc mdr_e_data_integer_firstabsoluteevaluationhscrc mdr_f_data_integer_firstabsoluteevaluationhscrc. ((mdr_a_data_integer_firstabsoluteevaluationhscrc = ((mdr_q_data_integer_firstabsoluteevaluationhs) + (mdr_up_data_integer_firstabsoluteevaluationhsc)) * S ((mdr_q_data_integer_firstabsoluteevaluationhs) + (mdr_up_data_integer_firstabsoluteevaluationhsc)) + ((mdr_up_data_integer_firstabsoluteevaluationhsc) + (mdr_up_data_integer_firstabsoluteevaluationhsc))) /\ ((mdr_b_data_integer_firstabsoluteevaluationhscrc = ((mdr_us_data_integer_firstabsoluteevaluationhsc) + (mdr_un_data_integer_firstabsoluteevaluationhsc)) * S ((mdr_us_data_integer_firstabsoluteevaluationhsc) + (mdr_un_data_integer_firstabsoluteevaluationhsc)) + ((mdr_un_data_integer_firstabsoluteevaluationhsc) + (mdr_un_data_integer_firstabsoluteevaluationhsc))) /\ ((mdr_c_data_integer_firstabsoluteevaluationhscrc = ((mdr_a_data_integer_firstabsoluteevaluationhscrc) + (mdr_b_data_integer_firstabsoluteevaluationhscrc)) * S ((mdr_a_data_integer_firstabsoluteevaluationhscrc) + (mdr_b_data_integer_firstabsoluteevaluationhscrc)) + ((mdr_b_data_integer_firstabsoluteevaluationhscrc) + (mdr_b_data_integer_firstabsoluteevaluationhscrc))) /\ ((mdr_e_data_integer_firstabsoluteevaluationhscrc = ((mdr_p_data_integer_firstabsoluteevaluationhsc) + (mdr_n_data_integer_firstabsoluteevaluationhsc)) * S ((mdr_p_data_integer_firstabsoluteevaluationhsc) + (mdr_n_data_integer_firstabsoluteevaluationhsc)) + ((mdr_n_data_integer_firstabsoluteevaluationhsc) + (mdr_n_data_integer_firstabsoluteevaluationhsc))) /\ ((mdr_f_data_integer_firstabsoluteevaluationhscrc = ((mdr_ut_data_integer_firstabsoluteevaluationhsc) + (mdr_e_data_integer_firstabsoluteevaluationhscrc)) * S ((mdr_ut_data_integer_firstabsoluteevaluationhsc) + (mdr_e_data_integer_firstabsoluteevaluationhscrc)) + ((mdr_e_data_integer_firstabsoluteevaluationhscrc) + (mdr_e_data_integer_firstabsoluteevaluationhscrc))) /\ ((mdr_z_data_integer_firstabsoluteevaluationhscr) = ((mdr_c_data_integer_firstabsoluteevaluationhscrc) + (mdr_f_data_integer_firstabsoluteevaluationhscrc)) * S ((mdr_c_data_integer_firstabsoluteevaluationhscrc) + (mdr_f_data_integer_firstabsoluteevaluationhscrc)) + ((mdr_f_data_integer_firstabsoluteevaluationhscrc) + (mdr_f_data_integer_firstabsoluteevaluationhscrc))))))))) /\ (((exists ff_h_mdr_data_integer_firstabsoluteevaluationhscrb. ff_h_mdr_data_integer_firstabsoluteevaluationhscrb + S (mdr_z_data_integer_firstabsoluteevaluationhscr) = S ((S (mdr_i_data_integer_firstabsoluteevaluationhsc)) * mdr_c_data_integer_firstabsoluteevaluation)) /\ exists ff_q_mdr_data_integer_firstabsoluteevaluationhscrb. mdr_b_data_integer_firstabsoluteevaluation = ff_q_mdr_data_integer_firstabsoluteevaluationhscrb * S ((S (mdr_i_data_integer_firstabsoluteevaluationhsc)) * mdr_c_data_integer_firstabsoluteevaluation) + (mdr_z_data_integer_firstabsoluteevaluationhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive. (exists ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_positive_index_bound. ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive) = ((mdr_q_data_integer_firstabsoluteevaluationhs) * (mdr_q_data_integer_firstabsoluteevaluationhs))) -> exists ff_row_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive ff_column_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive ff_value_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive. (ff_index_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive = (mdr_q_data_integer_firstabsoluteevaluationhs) * ff_row_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive + ff_column_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_positive_column_bound. ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive) = (mdr_q_data_integer_firstabsoluteevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell ff_column_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell = ff_row_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive)) /\ ff_row_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell = S ff_row_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive) = (mdr_j_data_integer_firstabsoluteevaluationhsc)) /\ ff_column_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell = ff_column_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell_column_after + (mdr_j_data_integer_firstabsoluteevaluationhsc) = (ff_column_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive)) /\ ff_column_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell = S ff_column_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive))) /\ (((exists ff_h_mdm_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell_source. ff_h_mdm_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell) * (S (mdr_q_data_integer_firstabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell))) * mdr_pc_data_integer_firstabsoluteevaluationh)) /\ exists ff_q_mdm_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell_source. mdr_pb_data_integer_firstabsoluteevaluationh = ff_q_mdm_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell) * (S (mdr_q_data_integer_firstabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_positive_cell))) * mdr_pc_data_integer_firstabsoluteevaluationh) + (ff_value_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_data_integer_firstabsoluteevaluationhscm_positive_target. ff_h_mdm_mdr_data_integer_firstabsoluteevaluationhscm_positive_target + S (ff_value_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive)) * mdr_us_data_integer_firstabsoluteevaluationhsc)) /\ exists ff_q_mdm_mdr_data_integer_firstabsoluteevaluationhscm_positive_target. mdr_up_data_integer_firstabsoluteevaluationhsc = ff_q_mdm_mdr_data_integer_firstabsoluteevaluationhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive)) * mdr_us_data_integer_firstabsoluteevaluationhsc) + (ff_value_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative. (exists ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_negative_index_bound. ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative) = ((mdr_q_data_integer_firstabsoluteevaluationhs) * (mdr_q_data_integer_firstabsoluteevaluationhs))) -> exists ff_row_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative ff_column_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative ff_value_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative. (ff_index_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative = (mdr_q_data_integer_firstabsoluteevaluationhs) * ff_row_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative + ff_column_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_negative_column_bound. ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative) = (mdr_q_data_integer_firstabsoluteevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell ff_column_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell = ff_row_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative)) /\ ff_row_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell = S ff_row_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative) = (mdr_j_data_integer_firstabsoluteevaluationhsc)) /\ ff_column_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell = ff_column_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell_column_after + (mdr_j_data_integer_firstabsoluteevaluationhsc) = (ff_column_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative)) /\ ff_column_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell = S ff_column_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative))) /\ (((exists ff_h_mdm_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell_source. ff_h_mdm_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell) * (S (mdr_q_data_integer_firstabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell))) * mdr_nc_data_integer_firstabsoluteevaluationh)) /\ exists ff_q_mdm_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell_source. mdr_nb_data_integer_firstabsoluteevaluationh = ff_q_mdm_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell) * (S (mdr_q_data_integer_firstabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_data_integer_firstabsoluteevaluationhscm_negative_cell))) * mdr_nc_data_integer_firstabsoluteevaluationh) + (ff_value_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_data_integer_firstabsoluteevaluationhscm_negative_target. ff_h_mdm_mdr_data_integer_firstabsoluteevaluationhscm_negative_target + S (ff_value_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative)) * mdr_ut_data_integer_firstabsoluteevaluationhsc)) /\ exists ff_q_mdm_mdr_data_integer_firstabsoluteevaluationhscm_negative_target. mdr_un_data_integer_firstabsoluteevaluationhsc = ff_q_mdm_mdr_data_integer_firstabsoluteevaluationhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative)) * mdr_ut_data_integer_firstabsoluteevaluationhsc) + (ff_value_mdm_prefix_mdr_data_integer_firstabsoluteevaluationhscm_negative))))))))) /\ ((((exists ff_h_mdr_data_integer_firstabsoluteevaluationhscp. ff_h_mdr_data_integer_firstabsoluteevaluationhscp + S (mdr_p_data_integer_firstabsoluteevaluationhsc) = S ((S (mdr_j_data_integer_firstabsoluteevaluationhsc)) * mdr_ec_data_integer_firstabsoluteevaluationhs)) /\ exists ff_q_mdr_data_integer_firstabsoluteevaluationhscp. mdr_eb_data_integer_firstabsoluteevaluationhs = ff_q_mdr_data_integer_firstabsoluteevaluationhscp * S ((S (mdr_j_data_integer_firstabsoluteevaluationhsc)) * mdr_ec_data_integer_firstabsoluteevaluationhs) + (mdr_p_data_integer_firstabsoluteevaluationhsc))) /\ (((exists ff_h_mdr_data_integer_firstabsoluteevaluationhscn. ff_h_mdr_data_integer_firstabsoluteevaluationhscn + S (mdr_n_data_integer_firstabsoluteevaluationhsc) = S ((S (mdr_j_data_integer_firstabsoluteevaluationhsc)) * mdr_fc_data_integer_firstabsoluteevaluationhs)) /\ exists ff_q_mdr_data_integer_firstabsoluteevaluationhscn. mdr_fb_data_integer_firstabsoluteevaluationhs = ff_q_mdr_data_integer_firstabsoluteevaluationhscn * S ((S (mdr_j_data_integer_firstabsoluteevaluationhsc)) * mdr_fc_data_integer_firstabsoluteevaluationhs) + (mdr_n_data_integer_firstabsoluteevaluationhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf ff_uc_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf ff_vb_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf ff_vc_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf. ((forall ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix. (exists ff_gap_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_index. ff_gap_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_index + S (ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) = (S (mdr_q_data_integer_firstabsoluteevaluationhs))) -> exists ff_ap_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix ff_an_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix ff_bp_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix ff_bn_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix ff_p_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix ff_n_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix. ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_ap. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix)) * mdr_pc_data_integer_firstabsoluteevaluationh)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_ap. mdr_pb_data_integer_firstabsoluteevaluationh = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix)) * mdr_pc_data_integer_firstabsoluteevaluationh) + (ff_ap_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_an. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_an + S (ff_an_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix)) * mdr_nc_data_integer_firstabsoluteevaluationh)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_an. mdr_nb_data_integer_firstabsoluteevaluationh = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix)) * mdr_nc_data_integer_firstabsoluteevaluationh) + (ff_an_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_bp. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix)) * mdr_ec_data_integer_firstabsoluteevaluationhs)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_bp. mdr_eb_data_integer_firstabsoluteevaluationhs = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix)) * mdr_ec_data_integer_firstabsoluteevaluationhs) + (ff_bp_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_bn. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix)) * mdr_fc_data_integer_firstabsoluteevaluationhs)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_bn. mdr_fb_data_integer_firstabsoluteevaluationhs = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix)) * mdr_fc_data_integer_firstabsoluteevaluationhs) + (ff_bn_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_positive. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_positive + S (ff_p_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_positive. ff_ub_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf) + (ff_p_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_negative. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_negative + S (ff_n_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_negative. ff_vb_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf) + (ff_n_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_data_integer_firstabsoluteevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix = 2 * ff_even_mce_term_mdr_data_integer_firstabsoluteevaluationhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_data_integer_firstabsoluteevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix = 2 * ff_odd_mce_term_mdr_data_integer_firstabsoluteevaluationhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_data_integer_firstabsoluteevaluationhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive. ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_start. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_start. ff_u_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_terminal. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_terminal + S (mdr_p_data_integer_firstabsoluteevaluationh) = S ((S ((S (mdr_q_data_integer_firstabsoluteevaluationhs)))) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_terminal. ff_u_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_terminal * S ((S ((S (mdr_q_data_integer_firstabsoluteevaluationhs)))) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive) + (mdr_p_data_integer_firstabsoluteevaluationh))) /\ forall ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive. (exists ff_lt_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_bound. ff_lt_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_bound + S ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive = (S (mdr_q_data_integer_firstabsoluteevaluationhs))) -> exists ff_a_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive ff_r_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive ff_s_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive. ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_summand. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_summand + S (ff_a_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive) = S ((S (ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive)) * ff_uc_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_summand. ff_ub_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_summand * S ((S (ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive)) * ff_uc_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf) + (ff_a_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_partial. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_partial + S (ff_r_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive) = S ((S (ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_partial. ff_u_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_partial * S ((S (ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive) + (ff_r_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_successor. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_successor + S (ff_s_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive) = S ((S (S ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_successor. ff_u_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive_successor * S ((S (S ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive) + (ff_s_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive))) /\ ff_s_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive = ff_r_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive + ff_a_mce_mdr_data_integer_firstabsoluteevaluationhsf_positive)))))) /\ (exists ff_u_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative. ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_start. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_start. ff_u_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_terminal. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_terminal + S (mdr_n_data_integer_firstabsoluteevaluationh) = S ((S ((S (mdr_q_data_integer_firstabsoluteevaluationhs)))) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_terminal. ff_u_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_terminal * S ((S ((S (mdr_q_data_integer_firstabsoluteevaluationhs)))) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative) + (mdr_n_data_integer_firstabsoluteevaluationh))) /\ forall ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative. (exists ff_lt_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_bound. ff_lt_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_bound + S ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative = (S (mdr_q_data_integer_firstabsoluteevaluationhs))) -> exists ff_a_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative ff_r_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative ff_s_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative. ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_summand. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_summand + S (ff_a_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative) = S ((S (ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative)) * ff_vc_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_summand. ff_vb_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_summand * S ((S (ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative)) * ff_vc_mce_fold_mdr_data_integer_firstabsoluteevaluationhsf) + (ff_a_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_partial. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_partial + S (ff_r_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative) = S ((S (ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_partial. ff_u_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_partial * S ((S (ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative) + (ff_r_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_successor. ff_h_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_successor + S (ff_s_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative) = S ((S (S ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_successor. ff_u_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative = ff_q_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative_successor * S ((S (S ff_i_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative) + (ff_s_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative))) /\ ff_s_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative = ff_r_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative + ff_a_mce_mdr_data_integer_firstabsoluteevaluationhsf_negative))))))))))))))) /\ ((exists mdr_gap_data_integer_firstabsoluteevaluationi. mdr_gap_data_integer_firstabsoluteevaluationi + S (mdr_i_data_integer_firstabsoluteevaluation) = (mdr_l_data_integer_firstabsoluteevaluation)) /\ (exists mdr_z_data_integer_firstabsoluteevaluationr. ((exists mdr_a_data_integer_firstabsoluteevaluationrc mdr_b_data_integer_firstabsoluteevaluationrc mdr_c_data_integer_firstabsoluteevaluationrc mdr_e_data_integer_firstabsoluteevaluationrc mdr_f_data_integer_firstabsoluteevaluationrc. ((mdr_a_data_integer_firstabsoluteevaluationrc = ((d) + (ab)) * S ((d) + (ab)) + ((ab) + (ab))) /\ ((mdr_b_data_integer_firstabsoluteevaluationrc = ((ac) + (bb)) * S ((ac) + (bb)) + ((bb) + (bb))) /\ ((mdr_c_data_integer_firstabsoluteevaluationrc = ((mdr_a_data_integer_firstabsoluteevaluationrc) + (mdr_b_data_integer_firstabsoluteevaluationrc)) * S ((mdr_a_data_integer_firstabsoluteevaluationrc) + (mdr_b_data_integer_firstabsoluteevaluationrc)) + ((mdr_b_data_integer_firstabsoluteevaluationrc) + (mdr_b_data_integer_firstabsoluteevaluationrc))) /\ ((mdr_e_data_integer_firstabsoluteevaluationrc = ((mdr_p_data_integer_firstabsolute) + (mdr_n_data_integer_firstabsolute)) * S ((mdr_p_data_integer_firstabsolute) + (mdr_n_data_integer_firstabsolute)) + ((mdr_n_data_integer_firstabsolute) + (mdr_n_data_integer_firstabsolute))) /\ ((mdr_f_data_integer_firstabsoluteevaluationrc = ((bc) + (mdr_e_data_integer_firstabsoluteevaluationrc)) * S ((bc) + (mdr_e_data_integer_firstabsoluteevaluationrc)) + ((mdr_e_data_integer_firstabsoluteevaluationrc) + (mdr_e_data_integer_firstabsoluteevaluationrc))) /\ ((mdr_z_data_integer_firstabsoluteevaluationr) = ((mdr_c_data_integer_firstabsoluteevaluationrc) + (mdr_f_data_integer_firstabsoluteevaluationrc)) * S ((mdr_c_data_integer_firstabsoluteevaluationrc) + (mdr_f_data_integer_firstabsoluteevaluationrc)) + ((mdr_f_data_integer_firstabsoluteevaluationrc) + (mdr_f_data_integer_firstabsoluteevaluationrc))))))))) /\ (((exists ff_h_mdr_data_integer_firstabsoluteevaluationrb. ff_h_mdr_data_integer_firstabsoluteevaluationrb + S (mdr_z_data_integer_firstabsoluteevaluationr) = S ((S (mdr_i_data_integer_firstabsoluteevaluation)) * mdr_c_data_integer_firstabsoluteevaluation)) /\ exists ff_q_mdr_data_integer_firstabsoluteevaluationrb. mdr_b_data_integer_firstabsoluteevaluation = ff_q_mdr_data_integer_firstabsoluteevaluationrb * S ((S (mdr_i_data_integer_firstabsoluteevaluation)) * mdr_c_data_integer_firstabsoluteevaluation) + (mdr_z_data_integer_firstabsoluteevaluationr)))))))) /\ (((mdr_p_data_integer_firstabsolute) = (mdr_n_data_integer_firstabsolute) + (D)) \/ ((mdr_n_data_integer_firstabsolute) = (mdr_p_data_integer_firstabsolute) + (D)))))))) -> (((~(d = 0)) /\ ((~(D = 0)) /\ (exists mdr_p_data_integer_secondabsolute mdr_n_data_integer_secondabsolute. ((exists mdr_b_data_integer_secondabsoluteevaluation mdr_c_data_integer_secondabsoluteevaluation mdr_l_data_integer_secondabsoluteevaluation mdr_i_data_integer_secondabsoluteevaluation. ((forall mdr_i_data_integer_secondabsoluteevaluationh. (exists mdr_gap_data_integer_secondabsoluteevaluationhi. mdr_gap_data_integer_secondabsoluteevaluationhi + S (mdr_i_data_integer_secondabsoluteevaluationh) = (mdr_l_data_integer_secondabsoluteevaluation)) -> exists mdr_d_data_integer_secondabsoluteevaluationh mdr_pb_data_integer_secondabsoluteevaluationh mdr_pc_data_integer_secondabsoluteevaluationh mdr_nb_data_integer_secondabsoluteevaluationh mdr_nc_data_integer_secondabsoluteevaluationh mdr_p_data_integer_secondabsoluteevaluationh mdr_n_data_integer_secondabsoluteevaluationh. ((exists mdr_z_data_integer_secondabsoluteevaluationhr. ((exists mdr_a_data_integer_secondabsoluteevaluationhrc mdr_b_data_integer_secondabsoluteevaluationhrc mdr_c_data_integer_secondabsoluteevaluationhrc mdr_e_data_integer_secondabsoluteevaluationhrc mdr_f_data_integer_secondabsoluteevaluationhrc. ((mdr_a_data_integer_secondabsoluteevaluationhrc = ((mdr_d_data_integer_secondabsoluteevaluationh) + (mdr_pb_data_integer_secondabsoluteevaluationh)) * S ((mdr_d_data_integer_secondabsoluteevaluationh) + (mdr_pb_data_integer_secondabsoluteevaluationh)) + ((mdr_pb_data_integer_secondabsoluteevaluationh) + (mdr_pb_data_integer_secondabsoluteevaluationh))) /\ ((mdr_b_data_integer_secondabsoluteevaluationhrc = ((mdr_pc_data_integer_secondabsoluteevaluationh) + (mdr_nb_data_integer_secondabsoluteevaluationh)) * S ((mdr_pc_data_integer_secondabsoluteevaluationh) + (mdr_nb_data_integer_secondabsoluteevaluationh)) + ((mdr_nb_data_integer_secondabsoluteevaluationh) + (mdr_nb_data_integer_secondabsoluteevaluationh))) /\ ((mdr_c_data_integer_secondabsoluteevaluationhrc = ((mdr_a_data_integer_secondabsoluteevaluationhrc) + (mdr_b_data_integer_secondabsoluteevaluationhrc)) * S ((mdr_a_data_integer_secondabsoluteevaluationhrc) + (mdr_b_data_integer_secondabsoluteevaluationhrc)) + ((mdr_b_data_integer_secondabsoluteevaluationhrc) + (mdr_b_data_integer_secondabsoluteevaluationhrc))) /\ ((mdr_e_data_integer_secondabsoluteevaluationhrc = ((mdr_p_data_integer_secondabsoluteevaluationh) + (mdr_n_data_integer_secondabsoluteevaluationh)) * S ((mdr_p_data_integer_secondabsoluteevaluationh) + (mdr_n_data_integer_secondabsoluteevaluationh)) + ((mdr_n_data_integer_secondabsoluteevaluationh) + (mdr_n_data_integer_secondabsoluteevaluationh))) /\ ((mdr_f_data_integer_secondabsoluteevaluationhrc = ((mdr_nc_data_integer_secondabsoluteevaluationh) + (mdr_e_data_integer_secondabsoluteevaluationhrc)) * S ((mdr_nc_data_integer_secondabsoluteevaluationh) + (mdr_e_data_integer_secondabsoluteevaluationhrc)) + ((mdr_e_data_integer_secondabsoluteevaluationhrc) + (mdr_e_data_integer_secondabsoluteevaluationhrc))) /\ ((mdr_z_data_integer_secondabsoluteevaluationhr) = ((mdr_c_data_integer_secondabsoluteevaluationhrc) + (mdr_f_data_integer_secondabsoluteevaluationhrc)) * S ((mdr_c_data_integer_secondabsoluteevaluationhrc) + (mdr_f_data_integer_secondabsoluteevaluationhrc)) + ((mdr_f_data_integer_secondabsoluteevaluationhrc) + (mdr_f_data_integer_secondabsoluteevaluationhrc))))))))) /\ (((exists ff_h_mdr_data_integer_secondabsoluteevaluationhrb. ff_h_mdr_data_integer_secondabsoluteevaluationhrb + S (mdr_z_data_integer_secondabsoluteevaluationhr) = S ((S (mdr_i_data_integer_secondabsoluteevaluationh)) * mdr_c_data_integer_secondabsoluteevaluation)) /\ exists ff_q_mdr_data_integer_secondabsoluteevaluationhrb. mdr_b_data_integer_secondabsoluteevaluation = ff_q_mdr_data_integer_secondabsoluteevaluationhrb * S ((S (mdr_i_data_integer_secondabsoluteevaluationh)) * mdr_c_data_integer_secondabsoluteevaluation) + (mdr_z_data_integer_secondabsoluteevaluationhr))))) /\ (((((mdr_d_data_integer_secondabsoluteevaluationh) = 0) /\ (((mdr_p_data_integer_secondabsoluteevaluationh) = 1) /\ ((mdr_n_data_integer_secondabsoluteevaluationh) = 0))) \/ exists mdr_q_data_integer_secondabsoluteevaluationhs mdr_eb_data_integer_secondabsoluteevaluationhs mdr_ec_data_integer_secondabsoluteevaluationhs mdr_fb_data_integer_secondabsoluteevaluationhs mdr_fc_data_integer_secondabsoluteevaluationhs. (((mdr_d_data_integer_secondabsoluteevaluationh) = S (mdr_q_data_integer_secondabsoluteevaluationhs)) /\ ((forall mdr_j_data_integer_secondabsoluteevaluationhsc. (exists mdr_gap_data_integer_secondabsoluteevaluationhscj. mdr_gap_data_integer_secondabsoluteevaluationhscj + S (mdr_j_data_integer_secondabsoluteevaluationhsc) = (S (mdr_q_data_integer_secondabsoluteevaluationhs))) -> exists mdr_i_data_integer_secondabsoluteevaluationhsc mdr_up_data_integer_secondabsoluteevaluationhsc mdr_us_data_integer_secondabsoluteevaluationhsc mdr_un_data_integer_secondabsoluteevaluationhsc mdr_ut_data_integer_secondabsoluteevaluationhsc mdr_p_data_integer_secondabsoluteevaluationhsc mdr_n_data_integer_secondabsoluteevaluationhsc. ((exists mdr_gap_data_integer_secondabsoluteevaluationhsci. mdr_gap_data_integer_secondabsoluteevaluationhsci + S (mdr_i_data_integer_secondabsoluteevaluationhsc) = (mdr_i_data_integer_secondabsoluteevaluationh)) /\ ((exists mdr_z_data_integer_secondabsoluteevaluationhscr. ((exists mdr_a_data_integer_secondabsoluteevaluationhscrc mdr_b_data_integer_secondabsoluteevaluationhscrc mdr_c_data_integer_secondabsoluteevaluationhscrc mdr_e_data_integer_secondabsoluteevaluationhscrc mdr_f_data_integer_secondabsoluteevaluationhscrc. ((mdr_a_data_integer_secondabsoluteevaluationhscrc = ((mdr_q_data_integer_secondabsoluteevaluationhs) + (mdr_up_data_integer_secondabsoluteevaluationhsc)) * S ((mdr_q_data_integer_secondabsoluteevaluationhs) + (mdr_up_data_integer_secondabsoluteevaluationhsc)) + ((mdr_up_data_integer_secondabsoluteevaluationhsc) + (mdr_up_data_integer_secondabsoluteevaluationhsc))) /\ ((mdr_b_data_integer_secondabsoluteevaluationhscrc = ((mdr_us_data_integer_secondabsoluteevaluationhsc) + (mdr_un_data_integer_secondabsoluteevaluationhsc)) * S ((mdr_us_data_integer_secondabsoluteevaluationhsc) + (mdr_un_data_integer_secondabsoluteevaluationhsc)) + ((mdr_un_data_integer_secondabsoluteevaluationhsc) + (mdr_un_data_integer_secondabsoluteevaluationhsc))) /\ ((mdr_c_data_integer_secondabsoluteevaluationhscrc = ((mdr_a_data_integer_secondabsoluteevaluationhscrc) + (mdr_b_data_integer_secondabsoluteevaluationhscrc)) * S ((mdr_a_data_integer_secondabsoluteevaluationhscrc) + (mdr_b_data_integer_secondabsoluteevaluationhscrc)) + ((mdr_b_data_integer_secondabsoluteevaluationhscrc) + (mdr_b_data_integer_secondabsoluteevaluationhscrc))) /\ ((mdr_e_data_integer_secondabsoluteevaluationhscrc = ((mdr_p_data_integer_secondabsoluteevaluationhsc) + (mdr_n_data_integer_secondabsoluteevaluationhsc)) * S ((mdr_p_data_integer_secondabsoluteevaluationhsc) + (mdr_n_data_integer_secondabsoluteevaluationhsc)) + ((mdr_n_data_integer_secondabsoluteevaluationhsc) + (mdr_n_data_integer_secondabsoluteevaluationhsc))) /\ ((mdr_f_data_integer_secondabsoluteevaluationhscrc = ((mdr_ut_data_integer_secondabsoluteevaluationhsc) + (mdr_e_data_integer_secondabsoluteevaluationhscrc)) * S ((mdr_ut_data_integer_secondabsoluteevaluationhsc) + (mdr_e_data_integer_secondabsoluteevaluationhscrc)) + ((mdr_e_data_integer_secondabsoluteevaluationhscrc) + (mdr_e_data_integer_secondabsoluteevaluationhscrc))) /\ ((mdr_z_data_integer_secondabsoluteevaluationhscr) = ((mdr_c_data_integer_secondabsoluteevaluationhscrc) + (mdr_f_data_integer_secondabsoluteevaluationhscrc)) * S ((mdr_c_data_integer_secondabsoluteevaluationhscrc) + (mdr_f_data_integer_secondabsoluteevaluationhscrc)) + ((mdr_f_data_integer_secondabsoluteevaluationhscrc) + (mdr_f_data_integer_secondabsoluteevaluationhscrc))))))))) /\ (((exists ff_h_mdr_data_integer_secondabsoluteevaluationhscrb. ff_h_mdr_data_integer_secondabsoluteevaluationhscrb + S (mdr_z_data_integer_secondabsoluteevaluationhscr) = S ((S (mdr_i_data_integer_secondabsoluteevaluationhsc)) * mdr_c_data_integer_secondabsoluteevaluation)) /\ exists ff_q_mdr_data_integer_secondabsoluteevaluationhscrb. mdr_b_data_integer_secondabsoluteevaluation = ff_q_mdr_data_integer_secondabsoluteevaluationhscrb * S ((S (mdr_i_data_integer_secondabsoluteevaluationhsc)) * mdr_c_data_integer_secondabsoluteevaluation) + (mdr_z_data_integer_secondabsoluteevaluationhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive. (exists ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_positive_index_bound. ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive) = ((mdr_q_data_integer_secondabsoluteevaluationhs) * (mdr_q_data_integer_secondabsoluteevaluationhs))) -> exists ff_row_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive ff_column_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive ff_value_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive. (ff_index_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive = (mdr_q_data_integer_secondabsoluteevaluationhs) * ff_row_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive + ff_column_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_positive_column_bound. ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive) = (mdr_q_data_integer_secondabsoluteevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell ff_column_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell = ff_row_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive)) /\ ff_row_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell = S ff_row_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive) = (mdr_j_data_integer_secondabsoluteevaluationhsc)) /\ ff_column_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell = ff_column_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell_column_after + (mdr_j_data_integer_secondabsoluteevaluationhsc) = (ff_column_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive)) /\ ff_column_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell = S ff_column_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive))) /\ (((exists ff_h_mdm_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell_source. ff_h_mdm_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell) * (S (mdr_q_data_integer_secondabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell))) * mdr_pc_data_integer_secondabsoluteevaluationh)) /\ exists ff_q_mdm_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell_source. mdr_pb_data_integer_secondabsoluteevaluationh = ff_q_mdm_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell) * (S (mdr_q_data_integer_secondabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_positive_cell))) * mdr_pc_data_integer_secondabsoluteevaluationh) + (ff_value_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_data_integer_secondabsoluteevaluationhscm_positive_target. ff_h_mdm_mdr_data_integer_secondabsoluteevaluationhscm_positive_target + S (ff_value_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive)) * mdr_us_data_integer_secondabsoluteevaluationhsc)) /\ exists ff_q_mdm_mdr_data_integer_secondabsoluteevaluationhscm_positive_target. mdr_up_data_integer_secondabsoluteevaluationhsc = ff_q_mdm_mdr_data_integer_secondabsoluteevaluationhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive)) * mdr_us_data_integer_secondabsoluteevaluationhsc) + (ff_value_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative. (exists ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_negative_index_bound. ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative) = ((mdr_q_data_integer_secondabsoluteevaluationhs) * (mdr_q_data_integer_secondabsoluteevaluationhs))) -> exists ff_row_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative ff_column_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative ff_value_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative. (ff_index_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative = (mdr_q_data_integer_secondabsoluteevaluationhs) * ff_row_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative + ff_column_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_negative_column_bound. ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative) = (mdr_q_data_integer_secondabsoluteevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell ff_column_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell = ff_row_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative)) /\ ff_row_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell = S ff_row_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative) = (mdr_j_data_integer_secondabsoluteevaluationhsc)) /\ ff_column_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell = ff_column_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell_column_after + (mdr_j_data_integer_secondabsoluteevaluationhsc) = (ff_column_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative)) /\ ff_column_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell = S ff_column_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative))) /\ (((exists ff_h_mdm_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell_source. ff_h_mdm_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell) * (S (mdr_q_data_integer_secondabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell))) * mdr_nc_data_integer_secondabsoluteevaluationh)) /\ exists ff_q_mdm_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell_source. mdr_nb_data_integer_secondabsoluteevaluationh = ff_q_mdm_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell) * (S (mdr_q_data_integer_secondabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_data_integer_secondabsoluteevaluationhscm_negative_cell))) * mdr_nc_data_integer_secondabsoluteevaluationh) + (ff_value_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_data_integer_secondabsoluteevaluationhscm_negative_target. ff_h_mdm_mdr_data_integer_secondabsoluteevaluationhscm_negative_target + S (ff_value_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative)) * mdr_ut_data_integer_secondabsoluteevaluationhsc)) /\ exists ff_q_mdm_mdr_data_integer_secondabsoluteevaluationhscm_negative_target. mdr_un_data_integer_secondabsoluteevaluationhsc = ff_q_mdm_mdr_data_integer_secondabsoluteevaluationhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative)) * mdr_ut_data_integer_secondabsoluteevaluationhsc) + (ff_value_mdm_prefix_mdr_data_integer_secondabsoluteevaluationhscm_negative))))))))) /\ ((((exists ff_h_mdr_data_integer_secondabsoluteevaluationhscp. ff_h_mdr_data_integer_secondabsoluteevaluationhscp + S (mdr_p_data_integer_secondabsoluteevaluationhsc) = S ((S (mdr_j_data_integer_secondabsoluteevaluationhsc)) * mdr_ec_data_integer_secondabsoluteevaluationhs)) /\ exists ff_q_mdr_data_integer_secondabsoluteevaluationhscp. mdr_eb_data_integer_secondabsoluteevaluationhs = ff_q_mdr_data_integer_secondabsoluteevaluationhscp * S ((S (mdr_j_data_integer_secondabsoluteevaluationhsc)) * mdr_ec_data_integer_secondabsoluteevaluationhs) + (mdr_p_data_integer_secondabsoluteevaluationhsc))) /\ (((exists ff_h_mdr_data_integer_secondabsoluteevaluationhscn. ff_h_mdr_data_integer_secondabsoluteevaluationhscn + S (mdr_n_data_integer_secondabsoluteevaluationhsc) = S ((S (mdr_j_data_integer_secondabsoluteevaluationhsc)) * mdr_fc_data_integer_secondabsoluteevaluationhs)) /\ exists ff_q_mdr_data_integer_secondabsoluteevaluationhscn. mdr_fb_data_integer_secondabsoluteevaluationhs = ff_q_mdr_data_integer_secondabsoluteevaluationhscn * S ((S (mdr_j_data_integer_secondabsoluteevaluationhsc)) * mdr_fc_data_integer_secondabsoluteevaluationhs) + (mdr_n_data_integer_secondabsoluteevaluationhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf ff_uc_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf ff_vb_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf ff_vc_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf. ((forall ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix. (exists ff_gap_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_index. ff_gap_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_index + S (ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) = (S (mdr_q_data_integer_secondabsoluteevaluationhs))) -> exists ff_ap_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix ff_an_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix ff_bp_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix ff_bn_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix ff_p_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix ff_n_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix. ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_ap. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix)) * mdr_pc_data_integer_secondabsoluteevaluationh)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_ap. mdr_pb_data_integer_secondabsoluteevaluationh = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix)) * mdr_pc_data_integer_secondabsoluteevaluationh) + (ff_ap_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_an. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_an + S (ff_an_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix)) * mdr_nc_data_integer_secondabsoluteevaluationh)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_an. mdr_nb_data_integer_secondabsoluteevaluationh = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix)) * mdr_nc_data_integer_secondabsoluteevaluationh) + (ff_an_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_bp. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix)) * mdr_ec_data_integer_secondabsoluteevaluationhs)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_bp. mdr_eb_data_integer_secondabsoluteevaluationhs = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix)) * mdr_ec_data_integer_secondabsoluteevaluationhs) + (ff_bp_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_bn. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix)) * mdr_fc_data_integer_secondabsoluteevaluationhs)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_bn. mdr_fb_data_integer_secondabsoluteevaluationhs = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix)) * mdr_fc_data_integer_secondabsoluteevaluationhs) + (ff_bn_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_positive. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_positive + S (ff_p_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_positive. ff_ub_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf) + (ff_p_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_negative. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_negative + S (ff_n_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_negative. ff_vb_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf) + (ff_n_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_data_integer_secondabsoluteevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix = 2 * ff_even_mce_term_mdr_data_integer_secondabsoluteevaluationhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_data_integer_secondabsoluteevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix = 2 * ff_odd_mce_term_mdr_data_integer_secondabsoluteevaluationhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_data_integer_secondabsoluteevaluationhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive. ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_start. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_start. ff_u_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_terminal. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_terminal + S (mdr_p_data_integer_secondabsoluteevaluationh) = S ((S ((S (mdr_q_data_integer_secondabsoluteevaluationhs)))) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_terminal. ff_u_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_terminal * S ((S ((S (mdr_q_data_integer_secondabsoluteevaluationhs)))) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive) + (mdr_p_data_integer_secondabsoluteevaluationh))) /\ forall ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive. (exists ff_lt_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_bound. ff_lt_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_bound + S ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive = (S (mdr_q_data_integer_secondabsoluteevaluationhs))) -> exists ff_a_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive ff_r_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive ff_s_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive. ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_summand. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_summand + S (ff_a_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive) = S ((S (ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive)) * ff_uc_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_summand. ff_ub_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_summand * S ((S (ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive)) * ff_uc_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf) + (ff_a_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_partial. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_partial + S (ff_r_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive) = S ((S (ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_partial. ff_u_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_partial * S ((S (ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive) + (ff_r_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_successor. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_successor + S (ff_s_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive) = S ((S (S ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_successor. ff_u_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive_successor * S ((S (S ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive) + (ff_s_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive))) /\ ff_s_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive = ff_r_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive + ff_a_mce_mdr_data_integer_secondabsoluteevaluationhsf_positive)))))) /\ (exists ff_u_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative. ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_start. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_start. ff_u_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_terminal. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_terminal + S (mdr_n_data_integer_secondabsoluteevaluationh) = S ((S ((S (mdr_q_data_integer_secondabsoluteevaluationhs)))) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_terminal. ff_u_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_terminal * S ((S ((S (mdr_q_data_integer_secondabsoluteevaluationhs)))) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative) + (mdr_n_data_integer_secondabsoluteevaluationh))) /\ forall ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative. (exists ff_lt_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_bound. ff_lt_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_bound + S ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative = (S (mdr_q_data_integer_secondabsoluteevaluationhs))) -> exists ff_a_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative ff_r_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative ff_s_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative. ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_summand. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_summand + S (ff_a_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative) = S ((S (ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative)) * ff_vc_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_summand. ff_vb_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_summand * S ((S (ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative)) * ff_vc_mce_fold_mdr_data_integer_secondabsoluteevaluationhsf) + (ff_a_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_partial. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_partial + S (ff_r_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative) = S ((S (ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_partial. ff_u_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_partial * S ((S (ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative) + (ff_r_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_successor. ff_h_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_successor + S (ff_s_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative) = S ((S (S ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_successor. ff_u_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative = ff_q_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative_successor * S ((S (S ff_i_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative) + (ff_s_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative))) /\ ff_s_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative = ff_r_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative + ff_a_mce_mdr_data_integer_secondabsoluteevaluationhsf_negative))))))))))))))) /\ ((exists mdr_gap_data_integer_secondabsoluteevaluationi. mdr_gap_data_integer_secondabsoluteevaluationi + S (mdr_i_data_integer_secondabsoluteevaluation) = (mdr_l_data_integer_secondabsoluteevaluation)) /\ (exists mdr_z_data_integer_secondabsoluteevaluationr. ((exists mdr_a_data_integer_secondabsoluteevaluationrc mdr_b_data_integer_secondabsoluteevaluationrc mdr_c_data_integer_secondabsoluteevaluationrc mdr_e_data_integer_secondabsoluteevaluationrc mdr_f_data_integer_secondabsoluteevaluationrc. ((mdr_a_data_integer_secondabsoluteevaluationrc = ((d) + (eb)) * S ((d) + (eb)) + ((eb) + (eb))) /\ ((mdr_b_data_integer_secondabsoluteevaluationrc = ((ec) + (fb)) * S ((ec) + (fb)) + ((fb) + (fb))) /\ ((mdr_c_data_integer_secondabsoluteevaluationrc = ((mdr_a_data_integer_secondabsoluteevaluationrc) + (mdr_b_data_integer_secondabsoluteevaluationrc)) * S ((mdr_a_data_integer_secondabsoluteevaluationrc) + (mdr_b_data_integer_secondabsoluteevaluationrc)) + ((mdr_b_data_integer_secondabsoluteevaluationrc) + (mdr_b_data_integer_secondabsoluteevaluationrc))) /\ ((mdr_e_data_integer_secondabsoluteevaluationrc = ((mdr_p_data_integer_secondabsolute) + (mdr_n_data_integer_secondabsolute)) * S ((mdr_p_data_integer_secondabsolute) + (mdr_n_data_integer_secondabsolute)) + ((mdr_n_data_integer_secondabsolute) + (mdr_n_data_integer_secondabsolute))) /\ ((mdr_f_data_integer_secondabsoluteevaluationrc = ((fc) + (mdr_e_data_integer_secondabsoluteevaluationrc)) * S ((fc) + (mdr_e_data_integer_secondabsoluteevaluationrc)) + ((mdr_e_data_integer_secondabsoluteevaluationrc) + (mdr_e_data_integer_secondabsoluteevaluationrc))) /\ ((mdr_z_data_integer_secondabsoluteevaluationr) = ((mdr_c_data_integer_secondabsoluteevaluationrc) + (mdr_f_data_integer_secondabsoluteevaluationrc)) * S ((mdr_c_data_integer_secondabsoluteevaluationrc) + (mdr_f_data_integer_secondabsoluteevaluationrc)) + ((mdr_f_data_integer_secondabsoluteevaluationrc) + (mdr_f_data_integer_secondabsoluteevaluationrc))))))))) /\ (((exists ff_h_mdr_data_integer_secondabsoluteevaluationrb. ff_h_mdr_data_integer_secondabsoluteevaluationrb + S (mdr_z_data_integer_secondabsoluteevaluationr) = S ((S (mdr_i_data_integer_secondabsoluteevaluation)) * mdr_c_data_integer_secondabsoluteevaluation)) /\ exists ff_q_mdr_data_integer_secondabsoluteevaluationrb. mdr_b_data_integer_secondabsoluteevaluation = ff_q_mdr_data_integer_secondabsoluteevaluationrb * S ((S (mdr_i_data_integer_secondabsoluteevaluation)) * mdr_c_data_integer_secondabsoluteevaluation) + (mdr_z_data_integer_secondabsoluteevaluationr)))))))) /\ (((mdr_p_data_integer_secondabsolute) = (mdr_n_data_integer_secondabsolute) + (D)) \/ ((mdr_n_data_integer_secondabsolute) = (mdr_p_data_integer_secondabsolute) + (D))))))))