positive_determinant_matrix_data_exists_unique

Exact expanded first-order arithmetic statement

forall ab ac bb bc d p n. ~(d = 0) -> (exists mdr_b_unique_data_determinant mdr_c_unique_data_determinant mdr_l_unique_data_determinant mdr_i_unique_data_determinant. ((forall mdr_i_unique_data_determinanth. (exists mdr_gap_unique_data_determinanthi. mdr_gap_unique_data_determinanthi + S (mdr_i_unique_data_determinanth) = (mdr_l_unique_data_determinant)) -> exists mdr_d_unique_data_determinanth mdr_pb_unique_data_determinanth mdr_pc_unique_data_determinanth mdr_nb_unique_data_determinanth mdr_nc_unique_data_determinanth mdr_p_unique_data_determinanth mdr_n_unique_data_determinanth. ((exists mdr_z_unique_data_determinanthr. ((exists mdr_a_unique_data_determinanthrc mdr_b_unique_data_determinanthrc mdr_c_unique_data_determinanthrc mdr_e_unique_data_determinanthrc mdr_f_unique_data_determinanthrc. ((mdr_a_unique_data_determinanthrc = ((mdr_d_unique_data_determinanth) + (mdr_pb_unique_data_determinanth)) * S ((mdr_d_unique_data_determinanth) + (mdr_pb_unique_data_determinanth)) + ((mdr_pb_unique_data_determinanth) + (mdr_pb_unique_data_determinanth))) /\ ((mdr_b_unique_data_determinanthrc = ((mdr_pc_unique_data_determinanth) + (mdr_nb_unique_data_determinanth)) * S ((mdr_pc_unique_data_determinanth) + (mdr_nb_unique_data_determinanth)) + ((mdr_nb_unique_data_determinanth) + (mdr_nb_unique_data_determinanth))) /\ ((mdr_c_unique_data_determinanthrc = ((mdr_a_unique_data_determinanthrc) + (mdr_b_unique_data_determinanthrc)) * S ((mdr_a_unique_data_determinanthrc) + (mdr_b_unique_data_determinanthrc)) + ((mdr_b_unique_data_determinanthrc) + (mdr_b_unique_data_determinanthrc))) /\ ((mdr_e_unique_data_determinanthrc = ((mdr_p_unique_data_determinanth) + (mdr_n_unique_data_determinanth)) * S ((mdr_p_unique_data_determinanth) + (mdr_n_unique_data_determinanth)) + ((mdr_n_unique_data_determinanth) + (mdr_n_unique_data_determinanth))) /\ ((mdr_f_unique_data_determinanthrc = ((mdr_nc_unique_data_determinanth) + (mdr_e_unique_data_determinanthrc)) * S ((mdr_nc_unique_data_determinanth) + (mdr_e_unique_data_determinanthrc)) + ((mdr_e_unique_data_determinanthrc) + (mdr_e_unique_data_determinanthrc))) /\ ((mdr_z_unique_data_determinanthr) = ((mdr_c_unique_data_determinanthrc) + (mdr_f_unique_data_determinanthrc)) * S ((mdr_c_unique_data_determinanthrc) + (mdr_f_unique_data_determinanthrc)) + ((mdr_f_unique_data_determinanthrc) + (mdr_f_unique_data_determinanthrc))))))))) /\ (((exists ff_h_mdr_unique_data_determinanthrb. ff_h_mdr_unique_data_determinanthrb + S (mdr_z_unique_data_determinanthr) = S ((S (mdr_i_unique_data_determinanth)) * mdr_c_unique_data_determinant)) /\ exists ff_q_mdr_unique_data_determinanthrb. mdr_b_unique_data_determinant = ff_q_mdr_unique_data_determinanthrb * S ((S (mdr_i_unique_data_determinanth)) * mdr_c_unique_data_determinant) + (mdr_z_unique_data_determinanthr))))) /\ (((((mdr_d_unique_data_determinanth) = 0) /\ (((mdr_p_unique_data_determinanth) = 1) /\ ((mdr_n_unique_data_determinanth) = 0))) \/ exists mdr_q_unique_data_determinanths mdr_eb_unique_data_determinanths mdr_ec_unique_data_determinanths mdr_fb_unique_data_determinanths mdr_fc_unique_data_determinanths. (((mdr_d_unique_data_determinanth) = S (mdr_q_unique_data_determinanths)) /\ ((forall mdr_j_unique_data_determinanthsc. (exists mdr_gap_unique_data_determinanthscj. mdr_gap_unique_data_determinanthscj + S (mdr_j_unique_data_determinanthsc) = (S (mdr_q_unique_data_determinanths))) -> exists mdr_i_unique_data_determinanthsc mdr_up_unique_data_determinanthsc mdr_us_unique_data_determinanthsc mdr_un_unique_data_determinanthsc mdr_ut_unique_data_determinanthsc mdr_p_unique_data_determinanthsc mdr_n_unique_data_determinanthsc. ((exists mdr_gap_unique_data_determinanthsci. mdr_gap_unique_data_determinanthsci + S (mdr_i_unique_data_determinanthsc) = (mdr_i_unique_data_determinanth)) /\ ((exists mdr_z_unique_data_determinanthscr. ((exists mdr_a_unique_data_determinanthscrc mdr_b_unique_data_determinanthscrc mdr_c_unique_data_determinanthscrc mdr_e_unique_data_determinanthscrc mdr_f_unique_data_determinanthscrc. ((mdr_a_unique_data_determinanthscrc = ((mdr_q_unique_data_determinanths) + (mdr_up_unique_data_determinanthsc)) * S ((mdr_q_unique_data_determinanths) + (mdr_up_unique_data_determinanthsc)) + ((mdr_up_unique_data_determinanthsc) + (mdr_up_unique_data_determinanthsc))) /\ ((mdr_b_unique_data_determinanthscrc = ((mdr_us_unique_data_determinanthsc) + (mdr_un_unique_data_determinanthsc)) * S ((mdr_us_unique_data_determinanthsc) + (mdr_un_unique_data_determinanthsc)) + ((mdr_un_unique_data_determinanthsc) + (mdr_un_unique_data_determinanthsc))) /\ ((mdr_c_unique_data_determinanthscrc = ((mdr_a_unique_data_determinanthscrc) + (mdr_b_unique_data_determinanthscrc)) * S ((mdr_a_unique_data_determinanthscrc) + (mdr_b_unique_data_determinanthscrc)) + ((mdr_b_unique_data_determinanthscrc) + (mdr_b_unique_data_determinanthscrc))) /\ ((mdr_e_unique_data_determinanthscrc = ((mdr_p_unique_data_determinanthsc) + (mdr_n_unique_data_determinanthsc)) * S ((mdr_p_unique_data_determinanthsc) + (mdr_n_unique_data_determinanthsc)) + ((mdr_n_unique_data_determinanthsc) + (mdr_n_unique_data_determinanthsc))) /\ ((mdr_f_unique_data_determinanthscrc = ((mdr_ut_unique_data_determinanthsc) + (mdr_e_unique_data_determinanthscrc)) * S ((mdr_ut_unique_data_determinanthsc) + (mdr_e_unique_data_determinanthscrc)) + ((mdr_e_unique_data_determinanthscrc) + (mdr_e_unique_data_determinanthscrc))) /\ ((mdr_z_unique_data_determinanthscr) = ((mdr_c_unique_data_determinanthscrc) + (mdr_f_unique_data_determinanthscrc)) * S ((mdr_c_unique_data_determinanthscrc) + (mdr_f_unique_data_determinanthscrc)) + ((mdr_f_unique_data_determinanthscrc) + (mdr_f_unique_data_determinanthscrc))))))))) /\ (((exists ff_h_mdr_unique_data_determinanthscrb. ff_h_mdr_unique_data_determinanthscrb + S (mdr_z_unique_data_determinanthscr) = S ((S (mdr_i_unique_data_determinanthsc)) * mdr_c_unique_data_determinant)) /\ exists ff_q_mdr_unique_data_determinanthscrb. mdr_b_unique_data_determinant = ff_q_mdr_unique_data_determinanthscrb * S ((S (mdr_i_unique_data_determinanthsc)) * mdr_c_unique_data_determinant) + (mdr_z_unique_data_determinanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_unique_data_determinanthscm_positive. (exists ff_gap_mdm_lt_mdr_unique_data_determinanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_unique_data_determinanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_unique_data_determinanthscm_positive) = ((mdr_q_unique_data_determinanths) * (mdr_q_unique_data_determinanths))) -> exists ff_row_mdm_prefix_mdr_unique_data_determinanthscm_positive ff_column_mdm_prefix_mdr_unique_data_determinanthscm_positive ff_value_mdm_prefix_mdr_unique_data_determinanthscm_positive. (ff_index_mdm_prefix_mdr_unique_data_determinanthscm_positive = (mdr_q_unique_data_determinanths) * ff_row_mdm_prefix_mdr_unique_data_determinanthscm_positive + ff_column_mdm_prefix_mdr_unique_data_determinanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_unique_data_determinanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_unique_data_determinanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_unique_data_determinanthscm_positive) = (mdr_q_unique_data_determinanths)) /\ ((exists ff_row_mdm_cell_mdr_unique_data_determinanthscm_positive_cell ff_column_mdm_cell_mdr_unique_data_determinanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_unique_data_determinanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_unique_data_determinanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_unique_data_determinanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_unique_data_determinanthscm_positive_cell = ff_row_mdm_prefix_mdr_unique_data_determinanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_unique_data_determinanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_unique_data_determinanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_unique_data_determinanthscm_positive)) /\ ff_row_mdm_cell_mdr_unique_data_determinanthscm_positive_cell = S ff_row_mdm_prefix_mdr_unique_data_determinanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_unique_data_determinanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_unique_data_determinanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_unique_data_determinanthscm_positive) = (mdr_j_unique_data_determinanthsc)) /\ ff_column_mdm_cell_mdr_unique_data_determinanthscm_positive_cell = ff_column_mdm_prefix_mdr_unique_data_determinanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_unique_data_determinanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_unique_data_determinanthscm_positive_cell_column_after + (mdr_j_unique_data_determinanthsc) = (ff_column_mdm_prefix_mdr_unique_data_determinanthscm_positive)) /\ ff_column_mdm_cell_mdr_unique_data_determinanthscm_positive_cell = S ff_column_mdm_prefix_mdr_unique_data_determinanthscm_positive))) /\ (((exists ff_h_mdm_mdr_unique_data_determinanthscm_positive_cell_source. ff_h_mdm_mdr_unique_data_determinanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_unique_data_determinanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_unique_data_determinanthscm_positive_cell) * (S (mdr_q_unique_data_determinanths)) + (ff_column_mdm_cell_mdr_unique_data_determinanthscm_positive_cell))) * mdr_pc_unique_data_determinanth)) /\ exists ff_q_mdm_mdr_unique_data_determinanthscm_positive_cell_source. mdr_pb_unique_data_determinanth = ff_q_mdm_mdr_unique_data_determinanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_unique_data_determinanthscm_positive_cell) * (S (mdr_q_unique_data_determinanths)) + (ff_column_mdm_cell_mdr_unique_data_determinanthscm_positive_cell))) * mdr_pc_unique_data_determinanth) + (ff_value_mdm_prefix_mdr_unique_data_determinanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_unique_data_determinanthscm_positive_target. ff_h_mdm_mdr_unique_data_determinanthscm_positive_target + S (ff_value_mdm_prefix_mdr_unique_data_determinanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_unique_data_determinanthscm_positive)) * mdr_us_unique_data_determinanthsc)) /\ exists ff_q_mdm_mdr_unique_data_determinanthscm_positive_target. mdr_up_unique_data_determinanthsc = ff_q_mdm_mdr_unique_data_determinanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_unique_data_determinanthscm_positive)) * mdr_us_unique_data_determinanthsc) + (ff_value_mdm_prefix_mdr_unique_data_determinanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_unique_data_determinanthscm_negative. (exists ff_gap_mdm_lt_mdr_unique_data_determinanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_unique_data_determinanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_unique_data_determinanthscm_negative) = ((mdr_q_unique_data_determinanths) * (mdr_q_unique_data_determinanths))) -> exists ff_row_mdm_prefix_mdr_unique_data_determinanthscm_negative ff_column_mdm_prefix_mdr_unique_data_determinanthscm_negative ff_value_mdm_prefix_mdr_unique_data_determinanthscm_negative. (ff_index_mdm_prefix_mdr_unique_data_determinanthscm_negative = (mdr_q_unique_data_determinanths) * ff_row_mdm_prefix_mdr_unique_data_determinanthscm_negative + ff_column_mdm_prefix_mdr_unique_data_determinanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_unique_data_determinanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_unique_data_determinanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_unique_data_determinanthscm_negative) = (mdr_q_unique_data_determinanths)) /\ ((exists ff_row_mdm_cell_mdr_unique_data_determinanthscm_negative_cell ff_column_mdm_cell_mdr_unique_data_determinanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_unique_data_determinanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_unique_data_determinanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_unique_data_determinanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_unique_data_determinanthscm_negative_cell = ff_row_mdm_prefix_mdr_unique_data_determinanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_unique_data_determinanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_unique_data_determinanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_unique_data_determinanthscm_negative)) /\ ff_row_mdm_cell_mdr_unique_data_determinanthscm_negative_cell = S ff_row_mdm_prefix_mdr_unique_data_determinanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_unique_data_determinanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_unique_data_determinanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_unique_data_determinanthscm_negative) = (mdr_j_unique_data_determinanthsc)) /\ ff_column_mdm_cell_mdr_unique_data_determinanthscm_negative_cell = ff_column_mdm_prefix_mdr_unique_data_determinanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_unique_data_determinanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_unique_data_determinanthscm_negative_cell_column_after + (mdr_j_unique_data_determinanthsc) = (ff_column_mdm_prefix_mdr_unique_data_determinanthscm_negative)) /\ ff_column_mdm_cell_mdr_unique_data_determinanthscm_negative_cell = S ff_column_mdm_prefix_mdr_unique_data_determinanthscm_negative))) /\ (((exists ff_h_mdm_mdr_unique_data_determinanthscm_negative_cell_source. ff_h_mdm_mdr_unique_data_determinanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_unique_data_determinanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_unique_data_determinanthscm_negative_cell) * (S (mdr_q_unique_data_determinanths)) + (ff_column_mdm_cell_mdr_unique_data_determinanthscm_negative_cell))) * mdr_nc_unique_data_determinanth)) /\ exists ff_q_mdm_mdr_unique_data_determinanthscm_negative_cell_source. mdr_nb_unique_data_determinanth = ff_q_mdm_mdr_unique_data_determinanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_unique_data_determinanthscm_negative_cell) * (S (mdr_q_unique_data_determinanths)) + (ff_column_mdm_cell_mdr_unique_data_determinanthscm_negative_cell))) * mdr_nc_unique_data_determinanth) + (ff_value_mdm_prefix_mdr_unique_data_determinanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_unique_data_determinanthscm_negative_target. ff_h_mdm_mdr_unique_data_determinanthscm_negative_target + S (ff_value_mdm_prefix_mdr_unique_data_determinanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_unique_data_determinanthscm_negative)) * mdr_ut_unique_data_determinanthsc)) /\ exists ff_q_mdm_mdr_unique_data_determinanthscm_negative_target. mdr_un_unique_data_determinanthsc = ff_q_mdm_mdr_unique_data_determinanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_unique_data_determinanthscm_negative)) * mdr_ut_unique_data_determinanthsc) + (ff_value_mdm_prefix_mdr_unique_data_determinanthscm_negative))))))))) /\ ((((exists ff_h_mdr_unique_data_determinanthscp. ff_h_mdr_unique_data_determinanthscp + S (mdr_p_unique_data_determinanthsc) = S ((S (mdr_j_unique_data_determinanthsc)) * mdr_ec_unique_data_determinanths)) /\ exists ff_q_mdr_unique_data_determinanthscp. mdr_eb_unique_data_determinanths = ff_q_mdr_unique_data_determinanthscp * S ((S (mdr_j_unique_data_determinanthsc)) * mdr_ec_unique_data_determinanths) + (mdr_p_unique_data_determinanthsc))) /\ (((exists ff_h_mdr_unique_data_determinanthscn. ff_h_mdr_unique_data_determinanthscn + S (mdr_n_unique_data_determinanthsc) = S ((S (mdr_j_unique_data_determinanthsc)) * mdr_fc_unique_data_determinanths)) /\ exists ff_q_mdr_unique_data_determinanthscn. mdr_fb_unique_data_determinanths = ff_q_mdr_unique_data_determinanthscn * S ((S (mdr_j_unique_data_determinanthsc)) * mdr_fc_unique_data_determinanths) + (mdr_n_unique_data_determinanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_unique_data_determinanthsf ff_uc_mce_fold_mdr_unique_data_determinanthsf ff_vb_mce_fold_mdr_unique_data_determinanthsf ff_vc_mce_fold_mdr_unique_data_determinanthsf. ((forall ff_index_mce_alternating_mdr_unique_data_determinanthsf_prefix. (exists ff_gap_mce_mdr_unique_data_determinanthsf_prefix_index. ff_gap_mce_mdr_unique_data_determinanthsf_prefix_index + S (ff_index_mce_alternating_mdr_unique_data_determinanthsf_prefix) = (S (mdr_q_unique_data_determinanths))) -> exists ff_ap_mce_alternating_mdr_unique_data_determinanthsf_prefix ff_an_mce_alternating_mdr_unique_data_determinanthsf_prefix ff_bp_mce_alternating_mdr_unique_data_determinanthsf_prefix ff_bn_mce_alternating_mdr_unique_data_determinanthsf_prefix ff_p_mce_alternating_mdr_unique_data_determinanthsf_prefix ff_n_mce_alternating_mdr_unique_data_determinanthsf_prefix. ((((exists ff_h_mce_mdr_unique_data_determinanthsf_prefix_ap. ff_h_mce_mdr_unique_data_determinanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_unique_data_determinanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_data_determinanthsf_prefix)) * mdr_pc_unique_data_determinanth)) /\ exists ff_q_mce_mdr_unique_data_determinanthsf_prefix_ap. mdr_pb_unique_data_determinanth = ff_q_mce_mdr_unique_data_determinanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_unique_data_determinanthsf_prefix)) * mdr_pc_unique_data_determinanth) + (ff_ap_mce_alternating_mdr_unique_data_determinanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_data_determinanthsf_prefix_an. ff_h_mce_mdr_unique_data_determinanthsf_prefix_an + S (ff_an_mce_alternating_mdr_unique_data_determinanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_data_determinanthsf_prefix)) * mdr_nc_unique_data_determinanth)) /\ exists ff_q_mce_mdr_unique_data_determinanthsf_prefix_an. mdr_nb_unique_data_determinanth = ff_q_mce_mdr_unique_data_determinanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_unique_data_determinanthsf_prefix)) * mdr_nc_unique_data_determinanth) + (ff_an_mce_alternating_mdr_unique_data_determinanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_data_determinanthsf_prefix_bp. ff_h_mce_mdr_unique_data_determinanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_unique_data_determinanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_data_determinanthsf_prefix)) * mdr_ec_unique_data_determinanths)) /\ exists ff_q_mce_mdr_unique_data_determinanthsf_prefix_bp. mdr_eb_unique_data_determinanths = ff_q_mce_mdr_unique_data_determinanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_unique_data_determinanthsf_prefix)) * mdr_ec_unique_data_determinanths) + (ff_bp_mce_alternating_mdr_unique_data_determinanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_data_determinanthsf_prefix_bn. ff_h_mce_mdr_unique_data_determinanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_unique_data_determinanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_data_determinanthsf_prefix)) * mdr_fc_unique_data_determinanths)) /\ exists ff_q_mce_mdr_unique_data_determinanthsf_prefix_bn. mdr_fb_unique_data_determinanths = ff_q_mce_mdr_unique_data_determinanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_unique_data_determinanthsf_prefix)) * mdr_fc_unique_data_determinanths) + (ff_bn_mce_alternating_mdr_unique_data_determinanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_data_determinanthsf_prefix_positive. ff_h_mce_mdr_unique_data_determinanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_unique_data_determinanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_data_determinanthsf_prefix)) * ff_uc_mce_fold_mdr_unique_data_determinanthsf)) /\ exists ff_q_mce_mdr_unique_data_determinanthsf_prefix_positive. ff_ub_mce_fold_mdr_unique_data_determinanthsf = ff_q_mce_mdr_unique_data_determinanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_unique_data_determinanthsf_prefix)) * ff_uc_mce_fold_mdr_unique_data_determinanthsf) + (ff_p_mce_alternating_mdr_unique_data_determinanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_data_determinanthsf_prefix_negative. ff_h_mce_mdr_unique_data_determinanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_unique_data_determinanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_data_determinanthsf_prefix)) * ff_vc_mce_fold_mdr_unique_data_determinanthsf)) /\ exists ff_q_mce_mdr_unique_data_determinanthsf_prefix_negative. ff_vb_mce_fold_mdr_unique_data_determinanthsf = ff_q_mce_mdr_unique_data_determinanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_unique_data_determinanthsf_prefix)) * ff_vc_mce_fold_mdr_unique_data_determinanthsf) + (ff_n_mce_alternating_mdr_unique_data_determinanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_unique_data_determinanthsf_prefix_term. ff_index_mce_alternating_mdr_unique_data_determinanthsf_prefix = 2 * ff_even_mce_term_mdr_unique_data_determinanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_unique_data_determinanthsf_prefix = (ff_ap_mce_alternating_mdr_unique_data_determinanthsf_prefix) * (ff_bp_mce_alternating_mdr_unique_data_determinanthsf_prefix) + (ff_an_mce_alternating_mdr_unique_data_determinanthsf_prefix) * (ff_bn_mce_alternating_mdr_unique_data_determinanthsf_prefix) /\ ff_n_mce_alternating_mdr_unique_data_determinanthsf_prefix = (ff_ap_mce_alternating_mdr_unique_data_determinanthsf_prefix) * (ff_bn_mce_alternating_mdr_unique_data_determinanthsf_prefix) + (ff_an_mce_alternating_mdr_unique_data_determinanthsf_prefix) * (ff_bp_mce_alternating_mdr_unique_data_determinanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_unique_data_determinanthsf_prefix_term. ff_index_mce_alternating_mdr_unique_data_determinanthsf_prefix = 2 * ff_odd_mce_term_mdr_unique_data_determinanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_unique_data_determinanthsf_prefix = (ff_ap_mce_alternating_mdr_unique_data_determinanthsf_prefix) * (ff_bn_mce_alternating_mdr_unique_data_determinanthsf_prefix) + (ff_an_mce_alternating_mdr_unique_data_determinanthsf_prefix) * (ff_bp_mce_alternating_mdr_unique_data_determinanthsf_prefix) /\ ff_n_mce_alternating_mdr_unique_data_determinanthsf_prefix = (ff_ap_mce_alternating_mdr_unique_data_determinanthsf_prefix) * (ff_bp_mce_alternating_mdr_unique_data_determinanthsf_prefix) + (ff_an_mce_alternating_mdr_unique_data_determinanthsf_prefix) * (ff_bn_mce_alternating_mdr_unique_data_determinanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_unique_data_determinanthsf_positive ff_v_mce_mdr_unique_data_determinanthsf_positive. ((((exists ff_h_mce_mdr_unique_data_determinanthsf_positive_start. ff_h_mce_mdr_unique_data_determinanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_unique_data_determinanthsf_positive)) /\ exists ff_q_mce_mdr_unique_data_determinanthsf_positive_start. ff_u_mce_mdr_unique_data_determinanthsf_positive = ff_q_mce_mdr_unique_data_determinanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_unique_data_determinanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_unique_data_determinanthsf_positive_terminal. ff_h_mce_mdr_unique_data_determinanthsf_positive_terminal + S (mdr_p_unique_data_determinanth) = S ((S ((S (mdr_q_unique_data_determinanths)))) * ff_v_mce_mdr_unique_data_determinanthsf_positive)) /\ exists ff_q_mce_mdr_unique_data_determinanthsf_positive_terminal. ff_u_mce_mdr_unique_data_determinanthsf_positive = ff_q_mce_mdr_unique_data_determinanthsf_positive_terminal * S ((S ((S (mdr_q_unique_data_determinanths)))) * ff_v_mce_mdr_unique_data_determinanthsf_positive) + (mdr_p_unique_data_determinanth))) /\ forall ff_i_mce_mdr_unique_data_determinanthsf_positive. (exists ff_lt_mce_mdr_unique_data_determinanthsf_positive_bound. ff_lt_mce_mdr_unique_data_determinanthsf_positive_bound + S ff_i_mce_mdr_unique_data_determinanthsf_positive = (S (mdr_q_unique_data_determinanths))) -> exists ff_a_mce_mdr_unique_data_determinanthsf_positive ff_r_mce_mdr_unique_data_determinanthsf_positive ff_s_mce_mdr_unique_data_determinanthsf_positive. ((((exists ff_h_mce_mdr_unique_data_determinanthsf_positive_summand. ff_h_mce_mdr_unique_data_determinanthsf_positive_summand + S (ff_a_mce_mdr_unique_data_determinanthsf_positive) = S ((S (ff_i_mce_mdr_unique_data_determinanthsf_positive)) * ff_uc_mce_fold_mdr_unique_data_determinanthsf)) /\ exists ff_q_mce_mdr_unique_data_determinanthsf_positive_summand. ff_ub_mce_fold_mdr_unique_data_determinanthsf = ff_q_mce_mdr_unique_data_determinanthsf_positive_summand * S ((S (ff_i_mce_mdr_unique_data_determinanthsf_positive)) * ff_uc_mce_fold_mdr_unique_data_determinanthsf) + (ff_a_mce_mdr_unique_data_determinanthsf_positive))) /\ ((((exists ff_h_mce_mdr_unique_data_determinanthsf_positive_partial. ff_h_mce_mdr_unique_data_determinanthsf_positive_partial + S (ff_r_mce_mdr_unique_data_determinanthsf_positive) = S ((S (ff_i_mce_mdr_unique_data_determinanthsf_positive)) * ff_v_mce_mdr_unique_data_determinanthsf_positive)) /\ exists ff_q_mce_mdr_unique_data_determinanthsf_positive_partial. ff_u_mce_mdr_unique_data_determinanthsf_positive = ff_q_mce_mdr_unique_data_determinanthsf_positive_partial * S ((S (ff_i_mce_mdr_unique_data_determinanthsf_positive)) * ff_v_mce_mdr_unique_data_determinanthsf_positive) + (ff_r_mce_mdr_unique_data_determinanthsf_positive))) /\ ((((exists ff_h_mce_mdr_unique_data_determinanthsf_positive_successor. ff_h_mce_mdr_unique_data_determinanthsf_positive_successor + S (ff_s_mce_mdr_unique_data_determinanthsf_positive) = S ((S (S ff_i_mce_mdr_unique_data_determinanthsf_positive)) * ff_v_mce_mdr_unique_data_determinanthsf_positive)) /\ exists ff_q_mce_mdr_unique_data_determinanthsf_positive_successor. ff_u_mce_mdr_unique_data_determinanthsf_positive = ff_q_mce_mdr_unique_data_determinanthsf_positive_successor * S ((S (S ff_i_mce_mdr_unique_data_determinanthsf_positive)) * ff_v_mce_mdr_unique_data_determinanthsf_positive) + (ff_s_mce_mdr_unique_data_determinanthsf_positive))) /\ ff_s_mce_mdr_unique_data_determinanthsf_positive = ff_r_mce_mdr_unique_data_determinanthsf_positive + ff_a_mce_mdr_unique_data_determinanthsf_positive)))))) /\ (exists ff_u_mce_mdr_unique_data_determinanthsf_negative ff_v_mce_mdr_unique_data_determinanthsf_negative. ((((exists ff_h_mce_mdr_unique_data_determinanthsf_negative_start. ff_h_mce_mdr_unique_data_determinanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_unique_data_determinanthsf_negative)) /\ exists ff_q_mce_mdr_unique_data_determinanthsf_negative_start. ff_u_mce_mdr_unique_data_determinanthsf_negative = ff_q_mce_mdr_unique_data_determinanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_unique_data_determinanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_unique_data_determinanthsf_negative_terminal. ff_h_mce_mdr_unique_data_determinanthsf_negative_terminal + S (mdr_n_unique_data_determinanth) = S ((S ((S (mdr_q_unique_data_determinanths)))) * ff_v_mce_mdr_unique_data_determinanthsf_negative)) /\ exists ff_q_mce_mdr_unique_data_determinanthsf_negative_terminal. ff_u_mce_mdr_unique_data_determinanthsf_negative = ff_q_mce_mdr_unique_data_determinanthsf_negative_terminal * S ((S ((S (mdr_q_unique_data_determinanths)))) * ff_v_mce_mdr_unique_data_determinanthsf_negative) + (mdr_n_unique_data_determinanth))) /\ forall ff_i_mce_mdr_unique_data_determinanthsf_negative. (exists ff_lt_mce_mdr_unique_data_determinanthsf_negative_bound. ff_lt_mce_mdr_unique_data_determinanthsf_negative_bound + S ff_i_mce_mdr_unique_data_determinanthsf_negative = (S (mdr_q_unique_data_determinanths))) -> exists ff_a_mce_mdr_unique_data_determinanthsf_negative ff_r_mce_mdr_unique_data_determinanthsf_negative ff_s_mce_mdr_unique_data_determinanthsf_negative. ((((exists ff_h_mce_mdr_unique_data_determinanthsf_negative_summand. ff_h_mce_mdr_unique_data_determinanthsf_negative_summand + S (ff_a_mce_mdr_unique_data_determinanthsf_negative) = S ((S (ff_i_mce_mdr_unique_data_determinanthsf_negative)) * ff_vc_mce_fold_mdr_unique_data_determinanthsf)) /\ exists ff_q_mce_mdr_unique_data_determinanthsf_negative_summand. ff_vb_mce_fold_mdr_unique_data_determinanthsf = ff_q_mce_mdr_unique_data_determinanthsf_negative_summand * S ((S (ff_i_mce_mdr_unique_data_determinanthsf_negative)) * ff_vc_mce_fold_mdr_unique_data_determinanthsf) + (ff_a_mce_mdr_unique_data_determinanthsf_negative))) /\ ((((exists ff_h_mce_mdr_unique_data_determinanthsf_negative_partial. ff_h_mce_mdr_unique_data_determinanthsf_negative_partial + S (ff_r_mce_mdr_unique_data_determinanthsf_negative) = S ((S (ff_i_mce_mdr_unique_data_determinanthsf_negative)) * ff_v_mce_mdr_unique_data_determinanthsf_negative)) /\ exists ff_q_mce_mdr_unique_data_determinanthsf_negative_partial. ff_u_mce_mdr_unique_data_determinanthsf_negative = ff_q_mce_mdr_unique_data_determinanthsf_negative_partial * S ((S (ff_i_mce_mdr_unique_data_determinanthsf_negative)) * ff_v_mce_mdr_unique_data_determinanthsf_negative) + (ff_r_mce_mdr_unique_data_determinanthsf_negative))) /\ ((((exists ff_h_mce_mdr_unique_data_determinanthsf_negative_successor. ff_h_mce_mdr_unique_data_determinanthsf_negative_successor + S (ff_s_mce_mdr_unique_data_determinanthsf_negative) = S ((S (S ff_i_mce_mdr_unique_data_determinanthsf_negative)) * ff_v_mce_mdr_unique_data_determinanthsf_negative)) /\ exists ff_q_mce_mdr_unique_data_determinanthsf_negative_successor. ff_u_mce_mdr_unique_data_determinanthsf_negative = ff_q_mce_mdr_unique_data_determinanthsf_negative_successor * S ((S (S ff_i_mce_mdr_unique_data_determinanthsf_negative)) * ff_v_mce_mdr_unique_data_determinanthsf_negative) + (ff_s_mce_mdr_unique_data_determinanthsf_negative))) /\ ff_s_mce_mdr_unique_data_determinanthsf_negative = ff_r_mce_mdr_unique_data_determinanthsf_negative + ff_a_mce_mdr_unique_data_determinanthsf_negative))))))))))))))) /\ ((exists mdr_gap_unique_data_determinanti. mdr_gap_unique_data_determinanti + S (mdr_i_unique_data_determinant) = (mdr_l_unique_data_determinant)) /\ (exists mdr_z_unique_data_determinantr. ((exists mdr_a_unique_data_determinantrc mdr_b_unique_data_determinantrc mdr_c_unique_data_determinantrc mdr_e_unique_data_determinantrc mdr_f_unique_data_determinantrc. ((mdr_a_unique_data_determinantrc = ((d) + (ab)) * S ((d) + (ab)) + ((ab) + (ab))) /\ ((mdr_b_unique_data_determinantrc = ((ac) + (bb)) * S ((ac) + (bb)) + ((bb) + (bb))) /\ ((mdr_c_unique_data_determinantrc = ((mdr_a_unique_data_determinantrc) + (mdr_b_unique_data_determinantrc)) * S ((mdr_a_unique_data_determinantrc) + (mdr_b_unique_data_determinantrc)) + ((mdr_b_unique_data_determinantrc) + (mdr_b_unique_data_determinantrc))) /\ ((mdr_e_unique_data_determinantrc = ((p) + (n)) * S ((p) + (n)) + ((n) + (n))) /\ ((mdr_f_unique_data_determinantrc = ((bc) + (mdr_e_unique_data_determinantrc)) * S ((bc) + (mdr_e_unique_data_determinantrc)) + ((mdr_e_unique_data_determinantrc) + (mdr_e_unique_data_determinantrc))) /\ ((mdr_z_unique_data_determinantr) = ((mdr_c_unique_data_determinantrc) + (mdr_f_unique_data_determinantrc)) * S ((mdr_c_unique_data_determinantrc) + (mdr_f_unique_data_determinantrc)) + ((mdr_f_unique_data_determinantrc) + (mdr_f_unique_data_determinantrc))))))))) /\ (((exists ff_h_mdr_unique_data_determinantrb. ff_h_mdr_unique_data_determinantrb + S (mdr_z_unique_data_determinantr) = S ((S (mdr_i_unique_data_determinant)) * mdr_c_unique_data_determinant)) /\ exists ff_q_mdr_unique_data_determinantrb. mdr_b_unique_data_determinant = ff_q_mdr_unique_data_determinantrb * S ((S (mdr_i_unique_data_determinant)) * mdr_c_unique_data_determinant) + (mdr_z_unique_data_determinantr)))))))) -> ~(p = n) -> exists D. (((((~(d = 0)) /\ ((~(D = 0)) /\ (exists mdr_p_unique_positive_dataabsolute mdr_n_unique_positive_dataabsolute. ((exists mdr_b_unique_positive_dataabsoluteevaluation mdr_c_unique_positive_dataabsoluteevaluation mdr_l_unique_positive_dataabsoluteevaluation mdr_i_unique_positive_dataabsoluteevaluation. ((forall mdr_i_unique_positive_dataabsoluteevaluationh. (exists mdr_gap_unique_positive_dataabsoluteevaluationhi. mdr_gap_unique_positive_dataabsoluteevaluationhi + S (mdr_i_unique_positive_dataabsoluteevaluationh) = (mdr_l_unique_positive_dataabsoluteevaluation)) -> exists mdr_d_unique_positive_dataabsoluteevaluationh mdr_pb_unique_positive_dataabsoluteevaluationh mdr_pc_unique_positive_dataabsoluteevaluationh mdr_nb_unique_positive_dataabsoluteevaluationh mdr_nc_unique_positive_dataabsoluteevaluationh mdr_p_unique_positive_dataabsoluteevaluationh mdr_n_unique_positive_dataabsoluteevaluationh. ((exists mdr_z_unique_positive_dataabsoluteevaluationhr. ((exists mdr_a_unique_positive_dataabsoluteevaluationhrc mdr_b_unique_positive_dataabsoluteevaluationhrc mdr_c_unique_positive_dataabsoluteevaluationhrc mdr_e_unique_positive_dataabsoluteevaluationhrc mdr_f_unique_positive_dataabsoluteevaluationhrc. ((mdr_a_unique_positive_dataabsoluteevaluationhrc = ((mdr_d_unique_positive_dataabsoluteevaluationh) + (mdr_pb_unique_positive_dataabsoluteevaluationh)) * S ((mdr_d_unique_positive_dataabsoluteevaluationh) + (mdr_pb_unique_positive_dataabsoluteevaluationh)) + ((mdr_pb_unique_positive_dataabsoluteevaluationh) + (mdr_pb_unique_positive_dataabsoluteevaluationh))) /\ ((mdr_b_unique_positive_dataabsoluteevaluationhrc = ((mdr_pc_unique_positive_dataabsoluteevaluationh) + (mdr_nb_unique_positive_dataabsoluteevaluationh)) * S ((mdr_pc_unique_positive_dataabsoluteevaluationh) + (mdr_nb_unique_positive_dataabsoluteevaluationh)) + ((mdr_nb_unique_positive_dataabsoluteevaluationh) + (mdr_nb_unique_positive_dataabsoluteevaluationh))) /\ ((mdr_c_unique_positive_dataabsoluteevaluationhrc = ((mdr_a_unique_positive_dataabsoluteevaluationhrc) + (mdr_b_unique_positive_dataabsoluteevaluationhrc)) * S ((mdr_a_unique_positive_dataabsoluteevaluationhrc) + (mdr_b_unique_positive_dataabsoluteevaluationhrc)) + ((mdr_b_unique_positive_dataabsoluteevaluationhrc) + (mdr_b_unique_positive_dataabsoluteevaluationhrc))) /\ ((mdr_e_unique_positive_dataabsoluteevaluationhrc = ((mdr_p_unique_positive_dataabsoluteevaluationh) + (mdr_n_unique_positive_dataabsoluteevaluationh)) * S ((mdr_p_unique_positive_dataabsoluteevaluationh) + (mdr_n_unique_positive_dataabsoluteevaluationh)) + ((mdr_n_unique_positive_dataabsoluteevaluationh) + (mdr_n_unique_positive_dataabsoluteevaluationh))) /\ ((mdr_f_unique_positive_dataabsoluteevaluationhrc = ((mdr_nc_unique_positive_dataabsoluteevaluationh) + (mdr_e_unique_positive_dataabsoluteevaluationhrc)) * S ((mdr_nc_unique_positive_dataabsoluteevaluationh) + (mdr_e_unique_positive_dataabsoluteevaluationhrc)) + ((mdr_e_unique_positive_dataabsoluteevaluationhrc) + (mdr_e_unique_positive_dataabsoluteevaluationhrc))) /\ ((mdr_z_unique_positive_dataabsoluteevaluationhr) = ((mdr_c_unique_positive_dataabsoluteevaluationhrc) + (mdr_f_unique_positive_dataabsoluteevaluationhrc)) * S ((mdr_c_unique_positive_dataabsoluteevaluationhrc) + (mdr_f_unique_positive_dataabsoluteevaluationhrc)) + ((mdr_f_unique_positive_dataabsoluteevaluationhrc) + (mdr_f_unique_positive_dataabsoluteevaluationhrc))))))))) /\ (((exists ff_h_mdr_unique_positive_dataabsoluteevaluationhrb. ff_h_mdr_unique_positive_dataabsoluteevaluationhrb + S (mdr_z_unique_positive_dataabsoluteevaluationhr) = S ((S (mdr_i_unique_positive_dataabsoluteevaluationh)) * mdr_c_unique_positive_dataabsoluteevaluation)) /\ exists ff_q_mdr_unique_positive_dataabsoluteevaluationhrb. mdr_b_unique_positive_dataabsoluteevaluation = ff_q_mdr_unique_positive_dataabsoluteevaluationhrb * S ((S (mdr_i_unique_positive_dataabsoluteevaluationh)) * mdr_c_unique_positive_dataabsoluteevaluation) + (mdr_z_unique_positive_dataabsoluteevaluationhr))))) /\ (((((mdr_d_unique_positive_dataabsoluteevaluationh) = 0) /\ (((mdr_p_unique_positive_dataabsoluteevaluationh) = 1) /\ ((mdr_n_unique_positive_dataabsoluteevaluationh) = 0))) \/ exists mdr_q_unique_positive_dataabsoluteevaluationhs mdr_eb_unique_positive_dataabsoluteevaluationhs mdr_ec_unique_positive_dataabsoluteevaluationhs mdr_fb_unique_positive_dataabsoluteevaluationhs mdr_fc_unique_positive_dataabsoluteevaluationhs. (((mdr_d_unique_positive_dataabsoluteevaluationh) = S (mdr_q_unique_positive_dataabsoluteevaluationhs)) /\ ((forall mdr_j_unique_positive_dataabsoluteevaluationhsc. (exists mdr_gap_unique_positive_dataabsoluteevaluationhscj. mdr_gap_unique_positive_dataabsoluteevaluationhscj + S (mdr_j_unique_positive_dataabsoluteevaluationhsc) = (S (mdr_q_unique_positive_dataabsoluteevaluationhs))) -> exists mdr_i_unique_positive_dataabsoluteevaluationhsc mdr_up_unique_positive_dataabsoluteevaluationhsc mdr_us_unique_positive_dataabsoluteevaluationhsc mdr_un_unique_positive_dataabsoluteevaluationhsc mdr_ut_unique_positive_dataabsoluteevaluationhsc mdr_p_unique_positive_dataabsoluteevaluationhsc mdr_n_unique_positive_dataabsoluteevaluationhsc. ((exists mdr_gap_unique_positive_dataabsoluteevaluationhsci. mdr_gap_unique_positive_dataabsoluteevaluationhsci + S (mdr_i_unique_positive_dataabsoluteevaluationhsc) = (mdr_i_unique_positive_dataabsoluteevaluationh)) /\ ((exists mdr_z_unique_positive_dataabsoluteevaluationhscr. ((exists mdr_a_unique_positive_dataabsoluteevaluationhscrc mdr_b_unique_positive_dataabsoluteevaluationhscrc mdr_c_unique_positive_dataabsoluteevaluationhscrc mdr_e_unique_positive_dataabsoluteevaluationhscrc mdr_f_unique_positive_dataabsoluteevaluationhscrc. ((mdr_a_unique_positive_dataabsoluteevaluationhscrc = ((mdr_q_unique_positive_dataabsoluteevaluationhs) + (mdr_up_unique_positive_dataabsoluteevaluationhsc)) * S ((mdr_q_unique_positive_dataabsoluteevaluationhs) + (mdr_up_unique_positive_dataabsoluteevaluationhsc)) + ((mdr_up_unique_positive_dataabsoluteevaluationhsc) + (mdr_up_unique_positive_dataabsoluteevaluationhsc))) /\ ((mdr_b_unique_positive_dataabsoluteevaluationhscrc = ((mdr_us_unique_positive_dataabsoluteevaluationhsc) + (mdr_un_unique_positive_dataabsoluteevaluationhsc)) * S ((mdr_us_unique_positive_dataabsoluteevaluationhsc) + (mdr_un_unique_positive_dataabsoluteevaluationhsc)) + ((mdr_un_unique_positive_dataabsoluteevaluationhsc) + (mdr_un_unique_positive_dataabsoluteevaluationhsc))) /\ ((mdr_c_unique_positive_dataabsoluteevaluationhscrc = ((mdr_a_unique_positive_dataabsoluteevaluationhscrc) + (mdr_b_unique_positive_dataabsoluteevaluationhscrc)) * S ((mdr_a_unique_positive_dataabsoluteevaluationhscrc) + (mdr_b_unique_positive_dataabsoluteevaluationhscrc)) + ((mdr_b_unique_positive_dataabsoluteevaluationhscrc) + (mdr_b_unique_positive_dataabsoluteevaluationhscrc))) /\ ((mdr_e_unique_positive_dataabsoluteevaluationhscrc = ((mdr_p_unique_positive_dataabsoluteevaluationhsc) + (mdr_n_unique_positive_dataabsoluteevaluationhsc)) * S ((mdr_p_unique_positive_dataabsoluteevaluationhsc) + (mdr_n_unique_positive_dataabsoluteevaluationhsc)) + ((mdr_n_unique_positive_dataabsoluteevaluationhsc) + (mdr_n_unique_positive_dataabsoluteevaluationhsc))) /\ ((mdr_f_unique_positive_dataabsoluteevaluationhscrc = ((mdr_ut_unique_positive_dataabsoluteevaluationhsc) + (mdr_e_unique_positive_dataabsoluteevaluationhscrc)) * S ((mdr_ut_unique_positive_dataabsoluteevaluationhsc) + (mdr_e_unique_positive_dataabsoluteevaluationhscrc)) + ((mdr_e_unique_positive_dataabsoluteevaluationhscrc) + (mdr_e_unique_positive_dataabsoluteevaluationhscrc))) /\ ((mdr_z_unique_positive_dataabsoluteevaluationhscr) = ((mdr_c_unique_positive_dataabsoluteevaluationhscrc) + (mdr_f_unique_positive_dataabsoluteevaluationhscrc)) * S ((mdr_c_unique_positive_dataabsoluteevaluationhscrc) + (mdr_f_unique_positive_dataabsoluteevaluationhscrc)) + ((mdr_f_unique_positive_dataabsoluteevaluationhscrc) + (mdr_f_unique_positive_dataabsoluteevaluationhscrc))))))))) /\ (((exists ff_h_mdr_unique_positive_dataabsoluteevaluationhscrb. ff_h_mdr_unique_positive_dataabsoluteevaluationhscrb + S (mdr_z_unique_positive_dataabsoluteevaluationhscr) = S ((S (mdr_i_unique_positive_dataabsoluteevaluationhsc)) * mdr_c_unique_positive_dataabsoluteevaluation)) /\ exists ff_q_mdr_unique_positive_dataabsoluteevaluationhscrb. mdr_b_unique_positive_dataabsoluteevaluation = ff_q_mdr_unique_positive_dataabsoluteevaluationhscrb * S ((S (mdr_i_unique_positive_dataabsoluteevaluationhsc)) * mdr_c_unique_positive_dataabsoluteevaluation) + (mdr_z_unique_positive_dataabsoluteevaluationhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_positive. (exists ff_gap_mdm_lt_mdr_unique_positive_dataabsoluteevaluationhscm_positive_index_bound. ff_gap_mdm_lt_mdr_unique_positive_dataabsoluteevaluationhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_positive) = ((mdr_q_unique_positive_dataabsoluteevaluationhs) * (mdr_q_unique_positive_dataabsoluteevaluationhs))) -> exists ff_row_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_positive ff_column_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_positive ff_value_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_positive. (ff_index_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_positive = (mdr_q_unique_positive_dataabsoluteevaluationhs) * ff_row_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_positive + ff_column_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_unique_positive_dataabsoluteevaluationhscm_positive_column_bound. ff_gap_mdm_lt_mdr_unique_positive_dataabsoluteevaluationhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_positive) = (mdr_q_unique_positive_dataabsoluteevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_unique_positive_dataabsoluteevaluationhscm_positive_cell ff_column_mdm_cell_mdr_unique_positive_dataabsoluteevaluationhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_unique_positive_dataabsoluteevaluationhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_unique_positive_dataabsoluteevaluationhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_unique_positive_dataabsoluteevaluationhscm_positive_cell = ff_row_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_unique_positive_dataabsoluteevaluationhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_unique_positive_dataabsoluteevaluationhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_positive)) /\ ff_row_mdm_cell_mdr_unique_positive_dataabsoluteevaluationhscm_positive_cell = S ff_row_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_unique_positive_dataabsoluteevaluationhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_unique_positive_dataabsoluteevaluationhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_positive) = (mdr_j_unique_positive_dataabsoluteevaluationhsc)) /\ ff_column_mdm_cell_mdr_unique_positive_dataabsoluteevaluationhscm_positive_cell = ff_column_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_unique_positive_dataabsoluteevaluationhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_unique_positive_dataabsoluteevaluationhscm_positive_cell_column_after + (mdr_j_unique_positive_dataabsoluteevaluationhsc) = (ff_column_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_positive)) /\ ff_column_mdm_cell_mdr_unique_positive_dataabsoluteevaluationhscm_positive_cell = S ff_column_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_positive))) /\ (((exists ff_h_mdm_mdr_unique_positive_dataabsoluteevaluationhscm_positive_cell_source. ff_h_mdm_mdr_unique_positive_dataabsoluteevaluationhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_unique_positive_dataabsoluteevaluationhscm_positive_cell) * (S (mdr_q_unique_positive_dataabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_unique_positive_dataabsoluteevaluationhscm_positive_cell))) * mdr_pc_unique_positive_dataabsoluteevaluationh)) /\ exists ff_q_mdm_mdr_unique_positive_dataabsoluteevaluationhscm_positive_cell_source. mdr_pb_unique_positive_dataabsoluteevaluationh = ff_q_mdm_mdr_unique_positive_dataabsoluteevaluationhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_unique_positive_dataabsoluteevaluationhscm_positive_cell) * (S (mdr_q_unique_positive_dataabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_unique_positive_dataabsoluteevaluationhscm_positive_cell))) * mdr_pc_unique_positive_dataabsoluteevaluationh) + (ff_value_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_unique_positive_dataabsoluteevaluationhscm_positive_target. ff_h_mdm_mdr_unique_positive_dataabsoluteevaluationhscm_positive_target + S (ff_value_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_positive)) * mdr_us_unique_positive_dataabsoluteevaluationhsc)) /\ exists ff_q_mdm_mdr_unique_positive_dataabsoluteevaluationhscm_positive_target. mdr_up_unique_positive_dataabsoluteevaluationhsc = ff_q_mdm_mdr_unique_positive_dataabsoluteevaluationhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_positive)) * mdr_us_unique_positive_dataabsoluteevaluationhsc) + (ff_value_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_negative. (exists ff_gap_mdm_lt_mdr_unique_positive_dataabsoluteevaluationhscm_negative_index_bound. ff_gap_mdm_lt_mdr_unique_positive_dataabsoluteevaluationhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_negative) = ((mdr_q_unique_positive_dataabsoluteevaluationhs) * (mdr_q_unique_positive_dataabsoluteevaluationhs))) -> exists ff_row_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_negative ff_column_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_negative ff_value_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_negative. (ff_index_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_negative = (mdr_q_unique_positive_dataabsoluteevaluationhs) * ff_row_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_negative + ff_column_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_unique_positive_dataabsoluteevaluationhscm_negative_column_bound. ff_gap_mdm_lt_mdr_unique_positive_dataabsoluteevaluationhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_negative) = (mdr_q_unique_positive_dataabsoluteevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_unique_positive_dataabsoluteevaluationhscm_negative_cell ff_column_mdm_cell_mdr_unique_positive_dataabsoluteevaluationhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_unique_positive_dataabsoluteevaluationhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_unique_positive_dataabsoluteevaluationhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_unique_positive_dataabsoluteevaluationhscm_negative_cell = ff_row_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_unique_positive_dataabsoluteevaluationhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_unique_positive_dataabsoluteevaluationhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_negative)) /\ ff_row_mdm_cell_mdr_unique_positive_dataabsoluteevaluationhscm_negative_cell = S ff_row_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_unique_positive_dataabsoluteevaluationhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_unique_positive_dataabsoluteevaluationhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_negative) = (mdr_j_unique_positive_dataabsoluteevaluationhsc)) /\ ff_column_mdm_cell_mdr_unique_positive_dataabsoluteevaluationhscm_negative_cell = ff_column_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_unique_positive_dataabsoluteevaluationhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_unique_positive_dataabsoluteevaluationhscm_negative_cell_column_after + (mdr_j_unique_positive_dataabsoluteevaluationhsc) = (ff_column_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_negative)) /\ ff_column_mdm_cell_mdr_unique_positive_dataabsoluteevaluationhscm_negative_cell = S ff_column_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_negative))) /\ (((exists ff_h_mdm_mdr_unique_positive_dataabsoluteevaluationhscm_negative_cell_source. ff_h_mdm_mdr_unique_positive_dataabsoluteevaluationhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_unique_positive_dataabsoluteevaluationhscm_negative_cell) * (S (mdr_q_unique_positive_dataabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_unique_positive_dataabsoluteevaluationhscm_negative_cell))) * mdr_nc_unique_positive_dataabsoluteevaluationh)) /\ exists ff_q_mdm_mdr_unique_positive_dataabsoluteevaluationhscm_negative_cell_source. mdr_nb_unique_positive_dataabsoluteevaluationh = ff_q_mdm_mdr_unique_positive_dataabsoluteevaluationhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_unique_positive_dataabsoluteevaluationhscm_negative_cell) * (S (mdr_q_unique_positive_dataabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_unique_positive_dataabsoluteevaluationhscm_negative_cell))) * mdr_nc_unique_positive_dataabsoluteevaluationh) + (ff_value_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_unique_positive_dataabsoluteevaluationhscm_negative_target. ff_h_mdm_mdr_unique_positive_dataabsoluteevaluationhscm_negative_target + S (ff_value_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_negative)) * mdr_ut_unique_positive_dataabsoluteevaluationhsc)) /\ exists ff_q_mdm_mdr_unique_positive_dataabsoluteevaluationhscm_negative_target. mdr_un_unique_positive_dataabsoluteevaluationhsc = ff_q_mdm_mdr_unique_positive_dataabsoluteevaluationhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_negative)) * mdr_ut_unique_positive_dataabsoluteevaluationhsc) + (ff_value_mdm_prefix_mdr_unique_positive_dataabsoluteevaluationhscm_negative))))))))) /\ ((((exists ff_h_mdr_unique_positive_dataabsoluteevaluationhscp. ff_h_mdr_unique_positive_dataabsoluteevaluationhscp + S (mdr_p_unique_positive_dataabsoluteevaluationhsc) = S ((S (mdr_j_unique_positive_dataabsoluteevaluationhsc)) * mdr_ec_unique_positive_dataabsoluteevaluationhs)) /\ exists ff_q_mdr_unique_positive_dataabsoluteevaluationhscp. mdr_eb_unique_positive_dataabsoluteevaluationhs = ff_q_mdr_unique_positive_dataabsoluteevaluationhscp * S ((S (mdr_j_unique_positive_dataabsoluteevaluationhsc)) * mdr_ec_unique_positive_dataabsoluteevaluationhs) + (mdr_p_unique_positive_dataabsoluteevaluationhsc))) /\ (((exists ff_h_mdr_unique_positive_dataabsoluteevaluationhscn. ff_h_mdr_unique_positive_dataabsoluteevaluationhscn + S (mdr_n_unique_positive_dataabsoluteevaluationhsc) = S ((S (mdr_j_unique_positive_dataabsoluteevaluationhsc)) * mdr_fc_unique_positive_dataabsoluteevaluationhs)) /\ exists ff_q_mdr_unique_positive_dataabsoluteevaluationhscn. mdr_fb_unique_positive_dataabsoluteevaluationhs = ff_q_mdr_unique_positive_dataabsoluteevaluationhscn * S ((S (mdr_j_unique_positive_dataabsoluteevaluationhsc)) * mdr_fc_unique_positive_dataabsoluteevaluationhs) + (mdr_n_unique_positive_dataabsoluteevaluationhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_unique_positive_dataabsoluteevaluationhsf ff_uc_mce_fold_mdr_unique_positive_dataabsoluteevaluationhsf ff_vb_mce_fold_mdr_unique_positive_dataabsoluteevaluationhsf ff_vc_mce_fold_mdr_unique_positive_dataabsoluteevaluationhsf. ((forall ff_index_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix. (exists ff_gap_mce_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_index. ff_gap_mce_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_index + S (ff_index_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix) = (S (mdr_q_unique_positive_dataabsoluteevaluationhs))) -> exists ff_ap_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix ff_an_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix ff_bp_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix ff_bn_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix ff_p_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix ff_n_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix. ((((exists ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_ap. ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix)) * mdr_pc_unique_positive_dataabsoluteevaluationh)) /\ exists ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_ap. mdr_pb_unique_positive_dataabsoluteevaluationh = ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix)) * mdr_pc_unique_positive_dataabsoluteevaluationh) + (ff_ap_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_an. ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_an + S (ff_an_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix)) * mdr_nc_unique_positive_dataabsoluteevaluationh)) /\ exists ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_an. mdr_nb_unique_positive_dataabsoluteevaluationh = ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix)) * mdr_nc_unique_positive_dataabsoluteevaluationh) + (ff_an_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_bp. ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix)) * mdr_ec_unique_positive_dataabsoluteevaluationhs)) /\ exists ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_bp. mdr_eb_unique_positive_dataabsoluteevaluationhs = ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix)) * mdr_ec_unique_positive_dataabsoluteevaluationhs) + (ff_bp_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_bn. ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix)) * mdr_fc_unique_positive_dataabsoluteevaluationhs)) /\ exists ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_bn. mdr_fb_unique_positive_dataabsoluteevaluationhs = ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix)) * mdr_fc_unique_positive_dataabsoluteevaluationhs) + (ff_bn_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_positive. ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_positive + S (ff_p_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_unique_positive_dataabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_positive. ff_ub_mce_fold_mdr_unique_positive_dataabsoluteevaluationhsf = ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_unique_positive_dataabsoluteevaluationhsf) + (ff_p_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_negative. ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_negative + S (ff_n_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_unique_positive_dataabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_negative. ff_vb_mce_fold_mdr_unique_positive_dataabsoluteevaluationhsf = ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_unique_positive_dataabsoluteevaluationhsf) + (ff_n_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix = 2 * ff_even_mce_term_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix = 2 * ff_odd_mce_term_mdr_unique_positive_dataabsoluteevaluationhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_unique_positive_dataabsoluteevaluationhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive ff_v_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive. ((((exists ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive_start. ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive_start. ff_u_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive = ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive_terminal. ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive_terminal + S (mdr_p_unique_positive_dataabsoluteevaluationh) = S ((S ((S (mdr_q_unique_positive_dataabsoluteevaluationhs)))) * ff_v_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive_terminal. ff_u_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive = ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive_terminal * S ((S ((S (mdr_q_unique_positive_dataabsoluteevaluationhs)))) * ff_v_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive) + (mdr_p_unique_positive_dataabsoluteevaluationh))) /\ forall ff_i_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive. (exists ff_lt_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive_bound. ff_lt_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive_bound + S ff_i_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive = (S (mdr_q_unique_positive_dataabsoluteevaluationhs))) -> exists ff_a_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive ff_r_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive ff_s_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive. ((((exists ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive_summand. ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive_summand + S (ff_a_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive) = S ((S (ff_i_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive)) * ff_uc_mce_fold_mdr_unique_positive_dataabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive_summand. ff_ub_mce_fold_mdr_unique_positive_dataabsoluteevaluationhsf = ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive_summand * S ((S (ff_i_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive)) * ff_uc_mce_fold_mdr_unique_positive_dataabsoluteevaluationhsf) + (ff_a_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive_partial. ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive_partial + S (ff_r_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive) = S ((S (ff_i_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive_partial. ff_u_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive = ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive_partial * S ((S (ff_i_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive) + (ff_r_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive_successor. ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive_successor + S (ff_s_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive) = S ((S (S ff_i_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive_successor. ff_u_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive = ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive_successor * S ((S (S ff_i_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive) + (ff_s_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive))) /\ ff_s_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive = ff_r_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive + ff_a_mce_mdr_unique_positive_dataabsoluteevaluationhsf_positive)))))) /\ (exists ff_u_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative ff_v_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative. ((((exists ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative_start. ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative_start. ff_u_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative = ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative_terminal. ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative_terminal + S (mdr_n_unique_positive_dataabsoluteevaluationh) = S ((S ((S (mdr_q_unique_positive_dataabsoluteevaluationhs)))) * ff_v_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative_terminal. ff_u_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative = ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative_terminal * S ((S ((S (mdr_q_unique_positive_dataabsoluteevaluationhs)))) * ff_v_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative) + (mdr_n_unique_positive_dataabsoluteevaluationh))) /\ forall ff_i_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative. (exists ff_lt_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative_bound. ff_lt_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative_bound + S ff_i_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative = (S (mdr_q_unique_positive_dataabsoluteevaluationhs))) -> exists ff_a_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative ff_r_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative ff_s_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative. ((((exists ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative_summand. ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative_summand + S (ff_a_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative) = S ((S (ff_i_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative)) * ff_vc_mce_fold_mdr_unique_positive_dataabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative_summand. ff_vb_mce_fold_mdr_unique_positive_dataabsoluteevaluationhsf = ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative_summand * S ((S (ff_i_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative)) * ff_vc_mce_fold_mdr_unique_positive_dataabsoluteevaluationhsf) + (ff_a_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative_partial. ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative_partial + S (ff_r_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative) = S ((S (ff_i_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative_partial. ff_u_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative = ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative_partial * S ((S (ff_i_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative) + (ff_r_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative_successor. ff_h_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative_successor + S (ff_s_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative) = S ((S (S ff_i_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative_successor. ff_u_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative = ff_q_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative_successor * S ((S (S ff_i_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative) + (ff_s_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative))) /\ ff_s_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative = ff_r_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative + ff_a_mce_mdr_unique_positive_dataabsoluteevaluationhsf_negative))))))))))))))) /\ ((exists mdr_gap_unique_positive_dataabsoluteevaluationi. mdr_gap_unique_positive_dataabsoluteevaluationi + S (mdr_i_unique_positive_dataabsoluteevaluation) = (mdr_l_unique_positive_dataabsoluteevaluation)) /\ (exists mdr_z_unique_positive_dataabsoluteevaluationr. ((exists mdr_a_unique_positive_dataabsoluteevaluationrc mdr_b_unique_positive_dataabsoluteevaluationrc mdr_c_unique_positive_dataabsoluteevaluationrc mdr_e_unique_positive_dataabsoluteevaluationrc mdr_f_unique_positive_dataabsoluteevaluationrc. ((mdr_a_unique_positive_dataabsoluteevaluationrc = ((d) + (ab)) * S ((d) + (ab)) + ((ab) + (ab))) /\ ((mdr_b_unique_positive_dataabsoluteevaluationrc = ((ac) + (bb)) * S ((ac) + (bb)) + ((bb) + (bb))) /\ ((mdr_c_unique_positive_dataabsoluteevaluationrc = ((mdr_a_unique_positive_dataabsoluteevaluationrc) + (mdr_b_unique_positive_dataabsoluteevaluationrc)) * S ((mdr_a_unique_positive_dataabsoluteevaluationrc) + (mdr_b_unique_positive_dataabsoluteevaluationrc)) + ((mdr_b_unique_positive_dataabsoluteevaluationrc) + (mdr_b_unique_positive_dataabsoluteevaluationrc))) /\ ((mdr_e_unique_positive_dataabsoluteevaluationrc = ((mdr_p_unique_positive_dataabsolute) + (mdr_n_unique_positive_dataabsolute)) * S ((mdr_p_unique_positive_dataabsolute) + (mdr_n_unique_positive_dataabsolute)) + ((mdr_n_unique_positive_dataabsolute) + (mdr_n_unique_positive_dataabsolute))) /\ ((mdr_f_unique_positive_dataabsoluteevaluationrc = ((bc) + (mdr_e_unique_positive_dataabsoluteevaluationrc)) * S ((bc) + (mdr_e_unique_positive_dataabsoluteevaluationrc)) + ((mdr_e_unique_positive_dataabsoluteevaluationrc) + (mdr_e_unique_positive_dataabsoluteevaluationrc))) /\ ((mdr_z_unique_positive_dataabsoluteevaluationr) = ((mdr_c_unique_positive_dataabsoluteevaluationrc) + (mdr_f_unique_positive_dataabsoluteevaluationrc)) * S ((mdr_c_unique_positive_dataabsoluteevaluationrc) + (mdr_f_unique_positive_dataabsoluteevaluationrc)) + ((mdr_f_unique_positive_dataabsoluteevaluationrc) + (mdr_f_unique_positive_dataabsoluteevaluationrc))))))))) /\ (((exists ff_h_mdr_unique_positive_dataabsoluteevaluationrb. ff_h_mdr_unique_positive_dataabsoluteevaluationrb + S (mdr_z_unique_positive_dataabsoluteevaluationr) = S ((S (mdr_i_unique_positive_dataabsoluteevaluation)) * mdr_c_unique_positive_dataabsoluteevaluation)) /\ exists ff_q_mdr_unique_positive_dataabsoluteevaluationrb. mdr_b_unique_positive_dataabsoluteevaluation = ff_q_mdr_unique_positive_dataabsoluteevaluationrb * S ((S (mdr_i_unique_positive_dataabsoluteevaluation)) * mdr_c_unique_positive_dataabsoluteevaluation) + (mdr_z_unique_positive_dataabsoluteevaluationr)))))))) /\ (((mdr_p_unique_positive_dataabsolute) = (mdr_n_unique_positive_dataabsolute) + (D)) \/ ((mdr_n_unique_positive_dataabsolute) = (mdr_p_unique_positive_dataabsolute) + (D)))))))) /\ (forall E. (((~(d = 0)) /\ ((~(E = 0)) /\ (exists mdr_p_other_positive_dataabsolute mdr_n_other_positive_dataabsolute. ((exists mdr_b_other_positive_dataabsoluteevaluation mdr_c_other_positive_dataabsoluteevaluation mdr_l_other_positive_dataabsoluteevaluation mdr_i_other_positive_dataabsoluteevaluation. ((forall mdr_i_other_positive_dataabsoluteevaluationh. (exists mdr_gap_other_positive_dataabsoluteevaluationhi. mdr_gap_other_positive_dataabsoluteevaluationhi + S (mdr_i_other_positive_dataabsoluteevaluationh) = (mdr_l_other_positive_dataabsoluteevaluation)) -> exists mdr_d_other_positive_dataabsoluteevaluationh mdr_pb_other_positive_dataabsoluteevaluationh mdr_pc_other_positive_dataabsoluteevaluationh mdr_nb_other_positive_dataabsoluteevaluationh mdr_nc_other_positive_dataabsoluteevaluationh mdr_p_other_positive_dataabsoluteevaluationh mdr_n_other_positive_dataabsoluteevaluationh. ((exists mdr_z_other_positive_dataabsoluteevaluationhr. ((exists mdr_a_other_positive_dataabsoluteevaluationhrc mdr_b_other_positive_dataabsoluteevaluationhrc mdr_c_other_positive_dataabsoluteevaluationhrc mdr_e_other_positive_dataabsoluteevaluationhrc mdr_f_other_positive_dataabsoluteevaluationhrc. ((mdr_a_other_positive_dataabsoluteevaluationhrc = ((mdr_d_other_positive_dataabsoluteevaluationh) + (mdr_pb_other_positive_dataabsoluteevaluationh)) * S ((mdr_d_other_positive_dataabsoluteevaluationh) + (mdr_pb_other_positive_dataabsoluteevaluationh)) + ((mdr_pb_other_positive_dataabsoluteevaluationh) + (mdr_pb_other_positive_dataabsoluteevaluationh))) /\ ((mdr_b_other_positive_dataabsoluteevaluationhrc = ((mdr_pc_other_positive_dataabsoluteevaluationh) + (mdr_nb_other_positive_dataabsoluteevaluationh)) * S ((mdr_pc_other_positive_dataabsoluteevaluationh) + (mdr_nb_other_positive_dataabsoluteevaluationh)) + ((mdr_nb_other_positive_dataabsoluteevaluationh) + (mdr_nb_other_positive_dataabsoluteevaluationh))) /\ ((mdr_c_other_positive_dataabsoluteevaluationhrc = ((mdr_a_other_positive_dataabsoluteevaluationhrc) + (mdr_b_other_positive_dataabsoluteevaluationhrc)) * S ((mdr_a_other_positive_dataabsoluteevaluationhrc) + (mdr_b_other_positive_dataabsoluteevaluationhrc)) + ((mdr_b_other_positive_dataabsoluteevaluationhrc) + (mdr_b_other_positive_dataabsoluteevaluationhrc))) /\ ((mdr_e_other_positive_dataabsoluteevaluationhrc = ((mdr_p_other_positive_dataabsoluteevaluationh) + (mdr_n_other_positive_dataabsoluteevaluationh)) * S ((mdr_p_other_positive_dataabsoluteevaluationh) + (mdr_n_other_positive_dataabsoluteevaluationh)) + ((mdr_n_other_positive_dataabsoluteevaluationh) + (mdr_n_other_positive_dataabsoluteevaluationh))) /\ ((mdr_f_other_positive_dataabsoluteevaluationhrc = ((mdr_nc_other_positive_dataabsoluteevaluationh) + (mdr_e_other_positive_dataabsoluteevaluationhrc)) * S ((mdr_nc_other_positive_dataabsoluteevaluationh) + (mdr_e_other_positive_dataabsoluteevaluationhrc)) + ((mdr_e_other_positive_dataabsoluteevaluationhrc) + (mdr_e_other_positive_dataabsoluteevaluationhrc))) /\ ((mdr_z_other_positive_dataabsoluteevaluationhr) = ((mdr_c_other_positive_dataabsoluteevaluationhrc) + (mdr_f_other_positive_dataabsoluteevaluationhrc)) * S ((mdr_c_other_positive_dataabsoluteevaluationhrc) + (mdr_f_other_positive_dataabsoluteevaluationhrc)) + ((mdr_f_other_positive_dataabsoluteevaluationhrc) + (mdr_f_other_positive_dataabsoluteevaluationhrc))))))))) /\ (((exists ff_h_mdr_other_positive_dataabsoluteevaluationhrb. ff_h_mdr_other_positive_dataabsoluteevaluationhrb + S (mdr_z_other_positive_dataabsoluteevaluationhr) = S ((S (mdr_i_other_positive_dataabsoluteevaluationh)) * mdr_c_other_positive_dataabsoluteevaluation)) /\ exists ff_q_mdr_other_positive_dataabsoluteevaluationhrb. mdr_b_other_positive_dataabsoluteevaluation = ff_q_mdr_other_positive_dataabsoluteevaluationhrb * S ((S (mdr_i_other_positive_dataabsoluteevaluationh)) * mdr_c_other_positive_dataabsoluteevaluation) + (mdr_z_other_positive_dataabsoluteevaluationhr))))) /\ (((((mdr_d_other_positive_dataabsoluteevaluationh) = 0) /\ (((mdr_p_other_positive_dataabsoluteevaluationh) = 1) /\ ((mdr_n_other_positive_dataabsoluteevaluationh) = 0))) \/ exists mdr_q_other_positive_dataabsoluteevaluationhs mdr_eb_other_positive_dataabsoluteevaluationhs mdr_ec_other_positive_dataabsoluteevaluationhs mdr_fb_other_positive_dataabsoluteevaluationhs mdr_fc_other_positive_dataabsoluteevaluationhs. (((mdr_d_other_positive_dataabsoluteevaluationh) = S (mdr_q_other_positive_dataabsoluteevaluationhs)) /\ ((forall mdr_j_other_positive_dataabsoluteevaluationhsc. (exists mdr_gap_other_positive_dataabsoluteevaluationhscj. mdr_gap_other_positive_dataabsoluteevaluationhscj + S (mdr_j_other_positive_dataabsoluteevaluationhsc) = (S (mdr_q_other_positive_dataabsoluteevaluationhs))) -> exists mdr_i_other_positive_dataabsoluteevaluationhsc mdr_up_other_positive_dataabsoluteevaluationhsc mdr_us_other_positive_dataabsoluteevaluationhsc mdr_un_other_positive_dataabsoluteevaluationhsc mdr_ut_other_positive_dataabsoluteevaluationhsc mdr_p_other_positive_dataabsoluteevaluationhsc mdr_n_other_positive_dataabsoluteevaluationhsc. ((exists mdr_gap_other_positive_dataabsoluteevaluationhsci. mdr_gap_other_positive_dataabsoluteevaluationhsci + S (mdr_i_other_positive_dataabsoluteevaluationhsc) = (mdr_i_other_positive_dataabsoluteevaluationh)) /\ ((exists mdr_z_other_positive_dataabsoluteevaluationhscr. ((exists mdr_a_other_positive_dataabsoluteevaluationhscrc mdr_b_other_positive_dataabsoluteevaluationhscrc mdr_c_other_positive_dataabsoluteevaluationhscrc mdr_e_other_positive_dataabsoluteevaluationhscrc mdr_f_other_positive_dataabsoluteevaluationhscrc. ((mdr_a_other_positive_dataabsoluteevaluationhscrc = ((mdr_q_other_positive_dataabsoluteevaluationhs) + (mdr_up_other_positive_dataabsoluteevaluationhsc)) * S ((mdr_q_other_positive_dataabsoluteevaluationhs) + (mdr_up_other_positive_dataabsoluteevaluationhsc)) + ((mdr_up_other_positive_dataabsoluteevaluationhsc) + (mdr_up_other_positive_dataabsoluteevaluationhsc))) /\ ((mdr_b_other_positive_dataabsoluteevaluationhscrc = ((mdr_us_other_positive_dataabsoluteevaluationhsc) + (mdr_un_other_positive_dataabsoluteevaluationhsc)) * S ((mdr_us_other_positive_dataabsoluteevaluationhsc) + (mdr_un_other_positive_dataabsoluteevaluationhsc)) + ((mdr_un_other_positive_dataabsoluteevaluationhsc) + (mdr_un_other_positive_dataabsoluteevaluationhsc))) /\ ((mdr_c_other_positive_dataabsoluteevaluationhscrc = ((mdr_a_other_positive_dataabsoluteevaluationhscrc) + (mdr_b_other_positive_dataabsoluteevaluationhscrc)) * S ((mdr_a_other_positive_dataabsoluteevaluationhscrc) + (mdr_b_other_positive_dataabsoluteevaluationhscrc)) + ((mdr_b_other_positive_dataabsoluteevaluationhscrc) + (mdr_b_other_positive_dataabsoluteevaluationhscrc))) /\ ((mdr_e_other_positive_dataabsoluteevaluationhscrc = ((mdr_p_other_positive_dataabsoluteevaluationhsc) + (mdr_n_other_positive_dataabsoluteevaluationhsc)) * S ((mdr_p_other_positive_dataabsoluteevaluationhsc) + (mdr_n_other_positive_dataabsoluteevaluationhsc)) + ((mdr_n_other_positive_dataabsoluteevaluationhsc) + (mdr_n_other_positive_dataabsoluteevaluationhsc))) /\ ((mdr_f_other_positive_dataabsoluteevaluationhscrc = ((mdr_ut_other_positive_dataabsoluteevaluationhsc) + (mdr_e_other_positive_dataabsoluteevaluationhscrc)) * S ((mdr_ut_other_positive_dataabsoluteevaluationhsc) + (mdr_e_other_positive_dataabsoluteevaluationhscrc)) + ((mdr_e_other_positive_dataabsoluteevaluationhscrc) + (mdr_e_other_positive_dataabsoluteevaluationhscrc))) /\ ((mdr_z_other_positive_dataabsoluteevaluationhscr) = ((mdr_c_other_positive_dataabsoluteevaluationhscrc) + (mdr_f_other_positive_dataabsoluteevaluationhscrc)) * S ((mdr_c_other_positive_dataabsoluteevaluationhscrc) + (mdr_f_other_positive_dataabsoluteevaluationhscrc)) + ((mdr_f_other_positive_dataabsoluteevaluationhscrc) + (mdr_f_other_positive_dataabsoluteevaluationhscrc))))))))) /\ (((exists ff_h_mdr_other_positive_dataabsoluteevaluationhscrb. ff_h_mdr_other_positive_dataabsoluteevaluationhscrb + S (mdr_z_other_positive_dataabsoluteevaluationhscr) = S ((S (mdr_i_other_positive_dataabsoluteevaluationhsc)) * mdr_c_other_positive_dataabsoluteevaluation)) /\ exists ff_q_mdr_other_positive_dataabsoluteevaluationhscrb. mdr_b_other_positive_dataabsoluteevaluation = ff_q_mdr_other_positive_dataabsoluteevaluationhscrb * S ((S (mdr_i_other_positive_dataabsoluteevaluationhsc)) * mdr_c_other_positive_dataabsoluteevaluation) + (mdr_z_other_positive_dataabsoluteevaluationhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_positive. (exists ff_gap_mdm_lt_mdr_other_positive_dataabsoluteevaluationhscm_positive_index_bound. ff_gap_mdm_lt_mdr_other_positive_dataabsoluteevaluationhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_positive) = ((mdr_q_other_positive_dataabsoluteevaluationhs) * (mdr_q_other_positive_dataabsoluteevaluationhs))) -> exists ff_row_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_positive ff_column_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_positive ff_value_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_positive. (ff_index_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_positive = (mdr_q_other_positive_dataabsoluteevaluationhs) * ff_row_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_positive + ff_column_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_other_positive_dataabsoluteevaluationhscm_positive_column_bound. ff_gap_mdm_lt_mdr_other_positive_dataabsoluteevaluationhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_positive) = (mdr_q_other_positive_dataabsoluteevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_other_positive_dataabsoluteevaluationhscm_positive_cell ff_column_mdm_cell_mdr_other_positive_dataabsoluteevaluationhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_other_positive_dataabsoluteevaluationhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_other_positive_dataabsoluteevaluationhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_other_positive_dataabsoluteevaluationhscm_positive_cell = ff_row_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_other_positive_dataabsoluteevaluationhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_other_positive_dataabsoluteevaluationhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_positive)) /\ ff_row_mdm_cell_mdr_other_positive_dataabsoluteevaluationhscm_positive_cell = S ff_row_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_other_positive_dataabsoluteevaluationhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_other_positive_dataabsoluteevaluationhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_positive) = (mdr_j_other_positive_dataabsoluteevaluationhsc)) /\ ff_column_mdm_cell_mdr_other_positive_dataabsoluteevaluationhscm_positive_cell = ff_column_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_other_positive_dataabsoluteevaluationhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_other_positive_dataabsoluteevaluationhscm_positive_cell_column_after + (mdr_j_other_positive_dataabsoluteevaluationhsc) = (ff_column_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_positive)) /\ ff_column_mdm_cell_mdr_other_positive_dataabsoluteevaluationhscm_positive_cell = S ff_column_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_positive))) /\ (((exists ff_h_mdm_mdr_other_positive_dataabsoluteevaluationhscm_positive_cell_source. ff_h_mdm_mdr_other_positive_dataabsoluteevaluationhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_other_positive_dataabsoluteevaluationhscm_positive_cell) * (S (mdr_q_other_positive_dataabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_other_positive_dataabsoluteevaluationhscm_positive_cell))) * mdr_pc_other_positive_dataabsoluteevaluationh)) /\ exists ff_q_mdm_mdr_other_positive_dataabsoluteevaluationhscm_positive_cell_source. mdr_pb_other_positive_dataabsoluteevaluationh = ff_q_mdm_mdr_other_positive_dataabsoluteevaluationhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_other_positive_dataabsoluteevaluationhscm_positive_cell) * (S (mdr_q_other_positive_dataabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_other_positive_dataabsoluteevaluationhscm_positive_cell))) * mdr_pc_other_positive_dataabsoluteevaluationh) + (ff_value_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_other_positive_dataabsoluteevaluationhscm_positive_target. ff_h_mdm_mdr_other_positive_dataabsoluteevaluationhscm_positive_target + S (ff_value_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_positive)) * mdr_us_other_positive_dataabsoluteevaluationhsc)) /\ exists ff_q_mdm_mdr_other_positive_dataabsoluteevaluationhscm_positive_target. mdr_up_other_positive_dataabsoluteevaluationhsc = ff_q_mdm_mdr_other_positive_dataabsoluteevaluationhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_positive)) * mdr_us_other_positive_dataabsoluteevaluationhsc) + (ff_value_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_negative. (exists ff_gap_mdm_lt_mdr_other_positive_dataabsoluteevaluationhscm_negative_index_bound. ff_gap_mdm_lt_mdr_other_positive_dataabsoluteevaluationhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_negative) = ((mdr_q_other_positive_dataabsoluteevaluationhs) * (mdr_q_other_positive_dataabsoluteevaluationhs))) -> exists ff_row_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_negative ff_column_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_negative ff_value_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_negative. (ff_index_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_negative = (mdr_q_other_positive_dataabsoluteevaluationhs) * ff_row_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_negative + ff_column_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_other_positive_dataabsoluteevaluationhscm_negative_column_bound. ff_gap_mdm_lt_mdr_other_positive_dataabsoluteevaluationhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_negative) = (mdr_q_other_positive_dataabsoluteevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_other_positive_dataabsoluteevaluationhscm_negative_cell ff_column_mdm_cell_mdr_other_positive_dataabsoluteevaluationhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_other_positive_dataabsoluteevaluationhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_other_positive_dataabsoluteevaluationhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_other_positive_dataabsoluteevaluationhscm_negative_cell = ff_row_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_other_positive_dataabsoluteevaluationhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_other_positive_dataabsoluteevaluationhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_negative)) /\ ff_row_mdm_cell_mdr_other_positive_dataabsoluteevaluationhscm_negative_cell = S ff_row_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_other_positive_dataabsoluteevaluationhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_other_positive_dataabsoluteevaluationhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_negative) = (mdr_j_other_positive_dataabsoluteevaluationhsc)) /\ ff_column_mdm_cell_mdr_other_positive_dataabsoluteevaluationhscm_negative_cell = ff_column_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_other_positive_dataabsoluteevaluationhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_other_positive_dataabsoluteevaluationhscm_negative_cell_column_after + (mdr_j_other_positive_dataabsoluteevaluationhsc) = (ff_column_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_negative)) /\ ff_column_mdm_cell_mdr_other_positive_dataabsoluteevaluationhscm_negative_cell = S ff_column_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_negative))) /\ (((exists ff_h_mdm_mdr_other_positive_dataabsoluteevaluationhscm_negative_cell_source. ff_h_mdm_mdr_other_positive_dataabsoluteevaluationhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_other_positive_dataabsoluteevaluationhscm_negative_cell) * (S (mdr_q_other_positive_dataabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_other_positive_dataabsoluteevaluationhscm_negative_cell))) * mdr_nc_other_positive_dataabsoluteevaluationh)) /\ exists ff_q_mdm_mdr_other_positive_dataabsoluteevaluationhscm_negative_cell_source. mdr_nb_other_positive_dataabsoluteevaluationh = ff_q_mdm_mdr_other_positive_dataabsoluteevaluationhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_other_positive_dataabsoluteevaluationhscm_negative_cell) * (S (mdr_q_other_positive_dataabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_other_positive_dataabsoluteevaluationhscm_negative_cell))) * mdr_nc_other_positive_dataabsoluteevaluationh) + (ff_value_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_other_positive_dataabsoluteevaluationhscm_negative_target. ff_h_mdm_mdr_other_positive_dataabsoluteevaluationhscm_negative_target + S (ff_value_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_negative)) * mdr_ut_other_positive_dataabsoluteevaluationhsc)) /\ exists ff_q_mdm_mdr_other_positive_dataabsoluteevaluationhscm_negative_target. mdr_un_other_positive_dataabsoluteevaluationhsc = ff_q_mdm_mdr_other_positive_dataabsoluteevaluationhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_negative)) * mdr_ut_other_positive_dataabsoluteevaluationhsc) + (ff_value_mdm_prefix_mdr_other_positive_dataabsoluteevaluationhscm_negative))))))))) /\ ((((exists ff_h_mdr_other_positive_dataabsoluteevaluationhscp. ff_h_mdr_other_positive_dataabsoluteevaluationhscp + S (mdr_p_other_positive_dataabsoluteevaluationhsc) = S ((S (mdr_j_other_positive_dataabsoluteevaluationhsc)) * mdr_ec_other_positive_dataabsoluteevaluationhs)) /\ exists ff_q_mdr_other_positive_dataabsoluteevaluationhscp. mdr_eb_other_positive_dataabsoluteevaluationhs = ff_q_mdr_other_positive_dataabsoluteevaluationhscp * S ((S (mdr_j_other_positive_dataabsoluteevaluationhsc)) * mdr_ec_other_positive_dataabsoluteevaluationhs) + (mdr_p_other_positive_dataabsoluteevaluationhsc))) /\ (((exists ff_h_mdr_other_positive_dataabsoluteevaluationhscn. ff_h_mdr_other_positive_dataabsoluteevaluationhscn + S (mdr_n_other_positive_dataabsoluteevaluationhsc) = S ((S (mdr_j_other_positive_dataabsoluteevaluationhsc)) * mdr_fc_other_positive_dataabsoluteevaluationhs)) /\ exists ff_q_mdr_other_positive_dataabsoluteevaluationhscn. mdr_fb_other_positive_dataabsoluteevaluationhs = ff_q_mdr_other_positive_dataabsoluteevaluationhscn * S ((S (mdr_j_other_positive_dataabsoluteevaluationhsc)) * mdr_fc_other_positive_dataabsoluteevaluationhs) + (mdr_n_other_positive_dataabsoluteevaluationhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_other_positive_dataabsoluteevaluationhsf ff_uc_mce_fold_mdr_other_positive_dataabsoluteevaluationhsf ff_vb_mce_fold_mdr_other_positive_dataabsoluteevaluationhsf ff_vc_mce_fold_mdr_other_positive_dataabsoluteevaluationhsf. ((forall ff_index_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix. (exists ff_gap_mce_mdr_other_positive_dataabsoluteevaluationhsf_prefix_index. ff_gap_mce_mdr_other_positive_dataabsoluteevaluationhsf_prefix_index + S (ff_index_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix) = (S (mdr_q_other_positive_dataabsoluteevaluationhs))) -> exists ff_ap_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix ff_an_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix ff_bp_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix ff_bn_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix ff_p_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix ff_n_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix. ((((exists ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_prefix_ap. ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix)) * mdr_pc_other_positive_dataabsoluteevaluationh)) /\ exists ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_prefix_ap. mdr_pb_other_positive_dataabsoluteevaluationh = ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix)) * mdr_pc_other_positive_dataabsoluteevaluationh) + (ff_ap_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_prefix_an. ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_prefix_an + S (ff_an_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix)) * mdr_nc_other_positive_dataabsoluteevaluationh)) /\ exists ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_prefix_an. mdr_nb_other_positive_dataabsoluteevaluationh = ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix)) * mdr_nc_other_positive_dataabsoluteevaluationh) + (ff_an_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_prefix_bp. ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix)) * mdr_ec_other_positive_dataabsoluteevaluationhs)) /\ exists ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_prefix_bp. mdr_eb_other_positive_dataabsoluteevaluationhs = ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix)) * mdr_ec_other_positive_dataabsoluteevaluationhs) + (ff_bp_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_prefix_bn. ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix)) * mdr_fc_other_positive_dataabsoluteevaluationhs)) /\ exists ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_prefix_bn. mdr_fb_other_positive_dataabsoluteevaluationhs = ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix)) * mdr_fc_other_positive_dataabsoluteevaluationhs) + (ff_bn_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_prefix_positive. ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_prefix_positive + S (ff_p_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_other_positive_dataabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_prefix_positive. ff_ub_mce_fold_mdr_other_positive_dataabsoluteevaluationhsf = ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_other_positive_dataabsoluteevaluationhsf) + (ff_p_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_prefix_negative. ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_prefix_negative + S (ff_n_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_other_positive_dataabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_prefix_negative. ff_vb_mce_fold_mdr_other_positive_dataabsoluteevaluationhsf = ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_other_positive_dataabsoluteevaluationhsf) + (ff_n_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_other_positive_dataabsoluteevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix = 2 * ff_even_mce_term_mdr_other_positive_dataabsoluteevaluationhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_other_positive_dataabsoluteevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix = 2 * ff_odd_mce_term_mdr_other_positive_dataabsoluteevaluationhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_other_positive_dataabsoluteevaluationhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive ff_v_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive. ((((exists ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive_start. ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive_start. ff_u_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive = ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive_terminal. ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive_terminal + S (mdr_p_other_positive_dataabsoluteevaluationh) = S ((S ((S (mdr_q_other_positive_dataabsoluteevaluationhs)))) * ff_v_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive_terminal. ff_u_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive = ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive_terminal * S ((S ((S (mdr_q_other_positive_dataabsoluteevaluationhs)))) * ff_v_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive) + (mdr_p_other_positive_dataabsoluteevaluationh))) /\ forall ff_i_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive. (exists ff_lt_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive_bound. ff_lt_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive_bound + S ff_i_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive = (S (mdr_q_other_positive_dataabsoluteevaluationhs))) -> exists ff_a_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive ff_r_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive ff_s_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive. ((((exists ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive_summand. ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive_summand + S (ff_a_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive) = S ((S (ff_i_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive)) * ff_uc_mce_fold_mdr_other_positive_dataabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive_summand. ff_ub_mce_fold_mdr_other_positive_dataabsoluteevaluationhsf = ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive_summand * S ((S (ff_i_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive)) * ff_uc_mce_fold_mdr_other_positive_dataabsoluteevaluationhsf) + (ff_a_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive_partial. ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive_partial + S (ff_r_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive) = S ((S (ff_i_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive_partial. ff_u_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive = ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive_partial * S ((S (ff_i_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive) + (ff_r_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive_successor. ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive_successor + S (ff_s_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive) = S ((S (S ff_i_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive_successor. ff_u_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive = ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive_successor * S ((S (S ff_i_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive) + (ff_s_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive))) /\ ff_s_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive = ff_r_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive + ff_a_mce_mdr_other_positive_dataabsoluteevaluationhsf_positive)))))) /\ (exists ff_u_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative ff_v_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative. ((((exists ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative_start. ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative_start. ff_u_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative = ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative_terminal. ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative_terminal + S (mdr_n_other_positive_dataabsoluteevaluationh) = S ((S ((S (mdr_q_other_positive_dataabsoluteevaluationhs)))) * ff_v_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative_terminal. ff_u_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative = ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative_terminal * S ((S ((S (mdr_q_other_positive_dataabsoluteevaluationhs)))) * ff_v_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative) + (mdr_n_other_positive_dataabsoluteevaluationh))) /\ forall ff_i_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative. (exists ff_lt_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative_bound. ff_lt_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative_bound + S ff_i_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative = (S (mdr_q_other_positive_dataabsoluteevaluationhs))) -> exists ff_a_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative ff_r_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative ff_s_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative. ((((exists ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative_summand. ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative_summand + S (ff_a_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative) = S ((S (ff_i_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative)) * ff_vc_mce_fold_mdr_other_positive_dataabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative_summand. ff_vb_mce_fold_mdr_other_positive_dataabsoluteevaluationhsf = ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative_summand * S ((S (ff_i_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative)) * ff_vc_mce_fold_mdr_other_positive_dataabsoluteevaluationhsf) + (ff_a_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative_partial. ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative_partial + S (ff_r_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative) = S ((S (ff_i_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative_partial. ff_u_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative = ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative_partial * S ((S (ff_i_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative) + (ff_r_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative_successor. ff_h_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative_successor + S (ff_s_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative) = S ((S (S ff_i_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative_successor. ff_u_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative = ff_q_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative_successor * S ((S (S ff_i_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative) + (ff_s_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative))) /\ ff_s_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative = ff_r_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative + ff_a_mce_mdr_other_positive_dataabsoluteevaluationhsf_negative))))))))))))))) /\ ((exists mdr_gap_other_positive_dataabsoluteevaluationi. mdr_gap_other_positive_dataabsoluteevaluationi + S (mdr_i_other_positive_dataabsoluteevaluation) = (mdr_l_other_positive_dataabsoluteevaluation)) /\ (exists mdr_z_other_positive_dataabsoluteevaluationr. ((exists mdr_a_other_positive_dataabsoluteevaluationrc mdr_b_other_positive_dataabsoluteevaluationrc mdr_c_other_positive_dataabsoluteevaluationrc mdr_e_other_positive_dataabsoluteevaluationrc mdr_f_other_positive_dataabsoluteevaluationrc. ((mdr_a_other_positive_dataabsoluteevaluationrc = ((d) + (ab)) * S ((d) + (ab)) + ((ab) + (ab))) /\ ((mdr_b_other_positive_dataabsoluteevaluationrc = ((ac) + (bb)) * S ((ac) + (bb)) + ((bb) + (bb))) /\ ((mdr_c_other_positive_dataabsoluteevaluationrc = ((mdr_a_other_positive_dataabsoluteevaluationrc) + (mdr_b_other_positive_dataabsoluteevaluationrc)) * S ((mdr_a_other_positive_dataabsoluteevaluationrc) + (mdr_b_other_positive_dataabsoluteevaluationrc)) + ((mdr_b_other_positive_dataabsoluteevaluationrc) + (mdr_b_other_positive_dataabsoluteevaluationrc))) /\ ((mdr_e_other_positive_dataabsoluteevaluationrc = ((mdr_p_other_positive_dataabsolute) + (mdr_n_other_positive_dataabsolute)) * S ((mdr_p_other_positive_dataabsolute) + (mdr_n_other_positive_dataabsolute)) + ((mdr_n_other_positive_dataabsolute) + (mdr_n_other_positive_dataabsolute))) /\ ((mdr_f_other_positive_dataabsoluteevaluationrc = ((bc) + (mdr_e_other_positive_dataabsoluteevaluationrc)) * S ((bc) + (mdr_e_other_positive_dataabsoluteevaluationrc)) + ((mdr_e_other_positive_dataabsoluteevaluationrc) + (mdr_e_other_positive_dataabsoluteevaluationrc))) /\ ((mdr_z_other_positive_dataabsoluteevaluationr) = ((mdr_c_other_positive_dataabsoluteevaluationrc) + (mdr_f_other_positive_dataabsoluteevaluationrc)) * S ((mdr_c_other_positive_dataabsoluteevaluationrc) + (mdr_f_other_positive_dataabsoluteevaluationrc)) + ((mdr_f_other_positive_dataabsoluteevaluationrc) + (mdr_f_other_positive_dataabsoluteevaluationrc))))))))) /\ (((exists ff_h_mdr_other_positive_dataabsoluteevaluationrb. ff_h_mdr_other_positive_dataabsoluteevaluationrb + S (mdr_z_other_positive_dataabsoluteevaluationr) = S ((S (mdr_i_other_positive_dataabsoluteevaluation)) * mdr_c_other_positive_dataabsoluteevaluation)) /\ exists ff_q_mdr_other_positive_dataabsoluteevaluationrb. mdr_b_other_positive_dataabsoluteevaluation = ff_q_mdr_other_positive_dataabsoluteevaluationrb * S ((S (mdr_i_other_positive_dataabsoluteevaluation)) * mdr_c_other_positive_dataabsoluteevaluation) + (mdr_z_other_positive_dataabsoluteevaluationr)))))))) /\ (((mdr_p_other_positive_dataabsolute) = (mdr_n_other_positive_dataabsolute) + (E)) \/ ((mdr_n_other_positive_dataabsolute) = (mdr_p_other_positive_dataabsolute) + (E)))))))) -> E = D)))