positive_determinant_matrix_data_full_rank

forall ab ac bb bc d D. (((~(d = 0)) /\ ((~(D = 0)) /\ (exists mdr_p_full_rank_dataabsolute mdr_n_full_rank_dataabsolute. ((exists mdr_b_full_rank_dataabsoluteevaluation mdr_c_full_rank_dataabsoluteevaluation mdr_l_full_rank_dataabsoluteevaluation mdr_i_full_rank_dataabsoluteevaluation. ((forall mdr_i_full_rank_dataabsoluteevaluationh. (exists mdr_gap_full_rank_dataabsoluteevaluationhi. mdr_gap_full_rank_dataabsoluteevaluationhi + S (mdr_i_full_rank_dataabsoluteevaluationh) = (mdr_l_full_rank_dataabsoluteevaluation)) -> exists mdr_d_full_rank_dataabsoluteevaluationh mdr_pb_full_rank_dataabsoluteevaluationh mdr_pc_full_rank_dataabsoluteevaluationh mdr_nb_full_rank_dataabsoluteevaluationh mdr_nc_full_rank_dataabsoluteevaluationh mdr_p_full_rank_dataabsoluteevaluationh mdr_n_full_rank_dataabsoluteevaluationh. ((exists mdr_z_full_rank_dataabsoluteevaluationhr. ((exists mdr_a_full_rank_dataabsoluteevaluationhrc mdr_b_full_rank_dataabsoluteevaluationhrc mdr_c_full_rank_dataabsoluteevaluationhrc mdr_e_full_rank_dataabsoluteevaluationhrc mdr_f_full_rank_dataabsoluteevaluationhrc. ((mdr_a_full_rank_dataabsoluteevaluationhrc = ((mdr_d_full_rank_dataabsoluteevaluationh) + (mdr_pb_full_rank_dataabsoluteevaluationh)) * S ((mdr_d_full_rank_dataabsoluteevaluationh) + (mdr_pb_full_rank_dataabsoluteevaluationh)) + ((mdr_pb_full_rank_dataabsoluteevaluationh) + (mdr_pb_full_rank_dataabsoluteevaluationh))) /\ ((mdr_b_full_rank_dataabsoluteevaluationhrc = ((mdr_pc_full_rank_dataabsoluteevaluationh) + (mdr_nb_full_rank_dataabsoluteevaluationh)) * S ((mdr_pc_full_rank_dataabsoluteevaluationh) + (mdr_nb_full_rank_dataabsoluteevaluationh)) + ((mdr_nb_full_rank_dataabsoluteevaluationh) + (mdr_nb_full_rank_dataabsoluteevaluationh))) /\ ((mdr_c_full_rank_dataabsoluteevaluationhrc = ((mdr_a_full_rank_dataabsoluteevaluationhrc) + (mdr_b_full_rank_dataabsoluteevaluationhrc)) * S ((mdr_a_full_rank_dataabsoluteevaluationhrc) + (mdr_b_full_rank_dataabsoluteevaluationhrc)) + ((mdr_b_full_rank_dataabsoluteevaluationhrc) + (mdr_b_full_rank_dataabsoluteevaluationhrc))) /\ ((mdr_e_full_rank_dataabsoluteevaluationhrc = ((mdr_p_full_rank_dataabsoluteevaluationh) + (mdr_n_full_rank_dataabsoluteevaluationh)) * S ((mdr_p_full_rank_dataabsoluteevaluationh) + (mdr_n_full_rank_dataabsoluteevaluationh)) + ((mdr_n_full_rank_dataabsoluteevaluationh) + (mdr_n_full_rank_dataabsoluteevaluationh))) /\ ((mdr_f_full_rank_dataabsoluteevaluationhrc = ((mdr_nc_full_rank_dataabsoluteevaluationh) + (mdr_e_full_rank_dataabsoluteevaluationhrc)) * S ((mdr_nc_full_rank_dataabsoluteevaluationh) + (mdr_e_full_rank_dataabsoluteevaluationhrc)) + ((mdr_e_full_rank_dataabsoluteevaluationhrc) + (mdr_e_full_rank_dataabsoluteevaluationhrc))) /\ ((mdr_z_full_rank_dataabsoluteevaluationhr) = ((mdr_c_full_rank_dataabsoluteevaluationhrc) + (mdr_f_full_rank_dataabsoluteevaluationhrc)) * S ((mdr_c_full_rank_dataabsoluteevaluationhrc) + (mdr_f_full_rank_dataabsoluteevaluationhrc)) + ((mdr_f_full_rank_dataabsoluteevaluationhrc) + (mdr_f_full_rank_dataabsoluteevaluationhrc))))))))) /\ (((exists ff_h_mdr_full_rank_dataabsoluteevaluationhrb. ff_h_mdr_full_rank_dataabsoluteevaluationhrb + S (mdr_z_full_rank_dataabsoluteevaluationhr) = S ((S (mdr_i_full_rank_dataabsoluteevaluationh)) * mdr_c_full_rank_dataabsoluteevaluation)) /\ exists ff_q_mdr_full_rank_dataabsoluteevaluationhrb. mdr_b_full_rank_dataabsoluteevaluation = ff_q_mdr_full_rank_dataabsoluteevaluationhrb * S ((S (mdr_i_full_rank_dataabsoluteevaluationh)) * mdr_c_full_rank_dataabsoluteevaluation) + (mdr_z_full_rank_dataabsoluteevaluationhr))))) /\ (((((mdr_d_full_rank_dataabsoluteevaluationh) = 0) /\ (((mdr_p_full_rank_dataabsoluteevaluationh) = 1) /\ ((mdr_n_full_rank_dataabsoluteevaluationh) = 0))) \/ exists mdr_q_full_rank_dataabsoluteevaluationhs mdr_eb_full_rank_dataabsoluteevaluationhs mdr_ec_full_rank_dataabsoluteevaluationhs mdr_fb_full_rank_dataabsoluteevaluationhs mdr_fc_full_rank_dataabsoluteevaluationhs. (((mdr_d_full_rank_dataabsoluteevaluationh) = S (mdr_q_full_rank_dataabsoluteevaluationhs)) /\ ((forall mdr_j_full_rank_dataabsoluteevaluationhsc. (exists mdr_gap_full_rank_dataabsoluteevaluationhscj. mdr_gap_full_rank_dataabsoluteevaluationhscj + S (mdr_j_full_rank_dataabsoluteevaluationhsc) = (S (mdr_q_full_rank_dataabsoluteevaluationhs))) -> exists mdr_i_full_rank_dataabsoluteevaluationhsc mdr_up_full_rank_dataabsoluteevaluationhsc mdr_us_full_rank_dataabsoluteevaluationhsc mdr_un_full_rank_dataabsoluteevaluationhsc mdr_ut_full_rank_dataabsoluteevaluationhsc mdr_p_full_rank_dataabsoluteevaluationhsc mdr_n_full_rank_dataabsoluteevaluationhsc. ((exists mdr_gap_full_rank_dataabsoluteevaluationhsci. mdr_gap_full_rank_dataabsoluteevaluationhsci + S (mdr_i_full_rank_dataabsoluteevaluationhsc) = (mdr_i_full_rank_dataabsoluteevaluationh)) /\ ((exists mdr_z_full_rank_dataabsoluteevaluationhscr. ((exists mdr_a_full_rank_dataabsoluteevaluationhscrc mdr_b_full_rank_dataabsoluteevaluationhscrc mdr_c_full_rank_dataabsoluteevaluationhscrc mdr_e_full_rank_dataabsoluteevaluationhscrc mdr_f_full_rank_dataabsoluteevaluationhscrc. ((mdr_a_full_rank_dataabsoluteevaluationhscrc = ((mdr_q_full_rank_dataabsoluteevaluationhs) + (mdr_up_full_rank_dataabsoluteevaluationhsc)) * S ((mdr_q_full_rank_dataabsoluteevaluationhs) + (mdr_up_full_rank_dataabsoluteevaluationhsc)) + ((mdr_up_full_rank_dataabsoluteevaluationhsc) + (mdr_up_full_rank_dataabsoluteevaluationhsc))) /\ ((mdr_b_full_rank_dataabsoluteevaluationhscrc = ((mdr_us_full_rank_dataabsoluteevaluationhsc) + (mdr_un_full_rank_dataabsoluteevaluationhsc)) * S ((mdr_us_full_rank_dataabsoluteevaluationhsc) + (mdr_un_full_rank_dataabsoluteevaluationhsc)) + ((mdr_un_full_rank_dataabsoluteevaluationhsc) + (mdr_un_full_rank_dataabsoluteevaluationhsc))) /\ ((mdr_c_full_rank_dataabsoluteevaluationhscrc = ((mdr_a_full_rank_dataabsoluteevaluationhscrc) + (mdr_b_full_rank_dataabsoluteevaluationhscrc)) * S ((mdr_a_full_rank_dataabsoluteevaluationhscrc) + (mdr_b_full_rank_dataabsoluteevaluationhscrc)) + ((mdr_b_full_rank_dataabsoluteevaluationhscrc) + (mdr_b_full_rank_dataabsoluteevaluationhscrc))) /\ ((mdr_e_full_rank_dataabsoluteevaluationhscrc = ((mdr_p_full_rank_dataabsoluteevaluationhsc) + (mdr_n_full_rank_dataabsoluteevaluationhsc)) * S ((mdr_p_full_rank_dataabsoluteevaluationhsc) + (mdr_n_full_rank_dataabsoluteevaluationhsc)) + ((mdr_n_full_rank_dataabsoluteevaluationhsc) + (mdr_n_full_rank_dataabsoluteevaluationhsc))) /\ ((mdr_f_full_rank_dataabsoluteevaluationhscrc = ((mdr_ut_full_rank_dataabsoluteevaluationhsc) + (mdr_e_full_rank_dataabsoluteevaluationhscrc)) * S ((mdr_ut_full_rank_dataabsoluteevaluationhsc) + (mdr_e_full_rank_dataabsoluteevaluationhscrc)) + ((mdr_e_full_rank_dataabsoluteevaluationhscrc) + (mdr_e_full_rank_dataabsoluteevaluationhscrc))) /\ ((mdr_z_full_rank_dataabsoluteevaluationhscr) = ((mdr_c_full_rank_dataabsoluteevaluationhscrc) + (mdr_f_full_rank_dataabsoluteevaluationhscrc)) * S ((mdr_c_full_rank_dataabsoluteevaluationhscrc) + (mdr_f_full_rank_dataabsoluteevaluationhscrc)) + ((mdr_f_full_rank_dataabsoluteevaluationhscrc) + (mdr_f_full_rank_dataabsoluteevaluationhscrc))))))))) /\ (((exists ff_h_mdr_full_rank_dataabsoluteevaluationhscrb. ff_h_mdr_full_rank_dataabsoluteevaluationhscrb + S (mdr_z_full_rank_dataabsoluteevaluationhscr) = S ((S (mdr_i_full_rank_dataabsoluteevaluationhsc)) * mdr_c_full_rank_dataabsoluteevaluation)) /\ exists ff_q_mdr_full_rank_dataabsoluteevaluationhscrb. mdr_b_full_rank_dataabsoluteevaluation = ff_q_mdr_full_rank_dataabsoluteevaluationhscrb * S ((S (mdr_i_full_rank_dataabsoluteevaluationhsc)) * mdr_c_full_rank_dataabsoluteevaluation) + (mdr_z_full_rank_dataabsoluteevaluationhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_positive. (exists ff_gap_mdm_lt_mdr_full_rank_dataabsoluteevaluationhscm_positive_index_bound. ff_gap_mdm_lt_mdr_full_rank_dataabsoluteevaluationhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_positive) = ((mdr_q_full_rank_dataabsoluteevaluationhs) * (mdr_q_full_rank_dataabsoluteevaluationhs))) -> exists ff_row_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_positive ff_column_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_positive ff_value_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_positive. (ff_index_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_positive = (mdr_q_full_rank_dataabsoluteevaluationhs) * ff_row_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_positive + ff_column_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_full_rank_dataabsoluteevaluationhscm_positive_column_bound. ff_gap_mdm_lt_mdr_full_rank_dataabsoluteevaluationhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_positive) = (mdr_q_full_rank_dataabsoluteevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_full_rank_dataabsoluteevaluationhscm_positive_cell ff_column_mdm_cell_mdr_full_rank_dataabsoluteevaluationhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_full_rank_dataabsoluteevaluationhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_full_rank_dataabsoluteevaluationhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_full_rank_dataabsoluteevaluationhscm_positive_cell = ff_row_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_full_rank_dataabsoluteevaluationhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_full_rank_dataabsoluteevaluationhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_positive)) /\ ff_row_mdm_cell_mdr_full_rank_dataabsoluteevaluationhscm_positive_cell = S ff_row_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_full_rank_dataabsoluteevaluationhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_full_rank_dataabsoluteevaluationhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_positive) = (mdr_j_full_rank_dataabsoluteevaluationhsc)) /\ ff_column_mdm_cell_mdr_full_rank_dataabsoluteevaluationhscm_positive_cell = ff_column_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_full_rank_dataabsoluteevaluationhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_full_rank_dataabsoluteevaluationhscm_positive_cell_column_after + (mdr_j_full_rank_dataabsoluteevaluationhsc) = (ff_column_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_positive)) /\ ff_column_mdm_cell_mdr_full_rank_dataabsoluteevaluationhscm_positive_cell = S ff_column_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_positive))) /\ (((exists ff_h_mdm_mdr_full_rank_dataabsoluteevaluationhscm_positive_cell_source. ff_h_mdm_mdr_full_rank_dataabsoluteevaluationhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_full_rank_dataabsoluteevaluationhscm_positive_cell) * (S (mdr_q_full_rank_dataabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_full_rank_dataabsoluteevaluationhscm_positive_cell))) * mdr_pc_full_rank_dataabsoluteevaluationh)) /\ exists ff_q_mdm_mdr_full_rank_dataabsoluteevaluationhscm_positive_cell_source. mdr_pb_full_rank_dataabsoluteevaluationh = ff_q_mdm_mdr_full_rank_dataabsoluteevaluationhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_full_rank_dataabsoluteevaluationhscm_positive_cell) * (S (mdr_q_full_rank_dataabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_full_rank_dataabsoluteevaluationhscm_positive_cell))) * mdr_pc_full_rank_dataabsoluteevaluationh) + (ff_value_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_full_rank_dataabsoluteevaluationhscm_positive_target. ff_h_mdm_mdr_full_rank_dataabsoluteevaluationhscm_positive_target + S (ff_value_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_positive)) * mdr_us_full_rank_dataabsoluteevaluationhsc)) /\ exists ff_q_mdm_mdr_full_rank_dataabsoluteevaluationhscm_positive_target. mdr_up_full_rank_dataabsoluteevaluationhsc = ff_q_mdm_mdr_full_rank_dataabsoluteevaluationhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_positive)) * mdr_us_full_rank_dataabsoluteevaluationhsc) + (ff_value_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_negative. (exists ff_gap_mdm_lt_mdr_full_rank_dataabsoluteevaluationhscm_negative_index_bound. ff_gap_mdm_lt_mdr_full_rank_dataabsoluteevaluationhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_negative) = ((mdr_q_full_rank_dataabsoluteevaluationhs) * (mdr_q_full_rank_dataabsoluteevaluationhs))) -> exists ff_row_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_negative ff_column_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_negative ff_value_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_negative. (ff_index_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_negative = (mdr_q_full_rank_dataabsoluteevaluationhs) * ff_row_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_negative + ff_column_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_full_rank_dataabsoluteevaluationhscm_negative_column_bound. ff_gap_mdm_lt_mdr_full_rank_dataabsoluteevaluationhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_negative) = (mdr_q_full_rank_dataabsoluteevaluationhs)) /\ ((exists ff_row_mdm_cell_mdr_full_rank_dataabsoluteevaluationhscm_negative_cell ff_column_mdm_cell_mdr_full_rank_dataabsoluteevaluationhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_full_rank_dataabsoluteevaluationhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_full_rank_dataabsoluteevaluationhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_full_rank_dataabsoluteevaluationhscm_negative_cell = ff_row_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_full_rank_dataabsoluteevaluationhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_full_rank_dataabsoluteevaluationhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_negative)) /\ ff_row_mdm_cell_mdr_full_rank_dataabsoluteevaluationhscm_negative_cell = S ff_row_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_full_rank_dataabsoluteevaluationhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_full_rank_dataabsoluteevaluationhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_negative) = (mdr_j_full_rank_dataabsoluteevaluationhsc)) /\ ff_column_mdm_cell_mdr_full_rank_dataabsoluteevaluationhscm_negative_cell = ff_column_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_full_rank_dataabsoluteevaluationhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_full_rank_dataabsoluteevaluationhscm_negative_cell_column_after + (mdr_j_full_rank_dataabsoluteevaluationhsc) = (ff_column_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_negative)) /\ ff_column_mdm_cell_mdr_full_rank_dataabsoluteevaluationhscm_negative_cell = S ff_column_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_negative))) /\ (((exists ff_h_mdm_mdr_full_rank_dataabsoluteevaluationhscm_negative_cell_source. ff_h_mdm_mdr_full_rank_dataabsoluteevaluationhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_full_rank_dataabsoluteevaluationhscm_negative_cell) * (S (mdr_q_full_rank_dataabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_full_rank_dataabsoluteevaluationhscm_negative_cell))) * mdr_nc_full_rank_dataabsoluteevaluationh)) /\ exists ff_q_mdm_mdr_full_rank_dataabsoluteevaluationhscm_negative_cell_source. mdr_nb_full_rank_dataabsoluteevaluationh = ff_q_mdm_mdr_full_rank_dataabsoluteevaluationhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_full_rank_dataabsoluteevaluationhscm_negative_cell) * (S (mdr_q_full_rank_dataabsoluteevaluationhs)) + (ff_column_mdm_cell_mdr_full_rank_dataabsoluteevaluationhscm_negative_cell))) * mdr_nc_full_rank_dataabsoluteevaluationh) + (ff_value_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_full_rank_dataabsoluteevaluationhscm_negative_target. ff_h_mdm_mdr_full_rank_dataabsoluteevaluationhscm_negative_target + S (ff_value_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_negative)) * mdr_ut_full_rank_dataabsoluteevaluationhsc)) /\ exists ff_q_mdm_mdr_full_rank_dataabsoluteevaluationhscm_negative_target. mdr_un_full_rank_dataabsoluteevaluationhsc = ff_q_mdm_mdr_full_rank_dataabsoluteevaluationhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_negative)) * mdr_ut_full_rank_dataabsoluteevaluationhsc) + (ff_value_mdm_prefix_mdr_full_rank_dataabsoluteevaluationhscm_negative))))))))) /\ ((((exists ff_h_mdr_full_rank_dataabsoluteevaluationhscp. ff_h_mdr_full_rank_dataabsoluteevaluationhscp + S (mdr_p_full_rank_dataabsoluteevaluationhsc) = S ((S (mdr_j_full_rank_dataabsoluteevaluationhsc)) * mdr_ec_full_rank_dataabsoluteevaluationhs)) /\ exists ff_q_mdr_full_rank_dataabsoluteevaluationhscp. mdr_eb_full_rank_dataabsoluteevaluationhs = ff_q_mdr_full_rank_dataabsoluteevaluationhscp * S ((S (mdr_j_full_rank_dataabsoluteevaluationhsc)) * mdr_ec_full_rank_dataabsoluteevaluationhs) + (mdr_p_full_rank_dataabsoluteevaluationhsc))) /\ (((exists ff_h_mdr_full_rank_dataabsoluteevaluationhscn. ff_h_mdr_full_rank_dataabsoluteevaluationhscn + S (mdr_n_full_rank_dataabsoluteevaluationhsc) = S ((S (mdr_j_full_rank_dataabsoluteevaluationhsc)) * mdr_fc_full_rank_dataabsoluteevaluationhs)) /\ exists ff_q_mdr_full_rank_dataabsoluteevaluationhscn. mdr_fb_full_rank_dataabsoluteevaluationhs = ff_q_mdr_full_rank_dataabsoluteevaluationhscn * S ((S (mdr_j_full_rank_dataabsoluteevaluationhsc)) * mdr_fc_full_rank_dataabsoluteevaluationhs) + (mdr_n_full_rank_dataabsoluteevaluationhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_full_rank_dataabsoluteevaluationhsf ff_uc_mce_fold_mdr_full_rank_dataabsoluteevaluationhsf ff_vb_mce_fold_mdr_full_rank_dataabsoluteevaluationhsf ff_vc_mce_fold_mdr_full_rank_dataabsoluteevaluationhsf. ((forall ff_index_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix. (exists ff_gap_mce_mdr_full_rank_dataabsoluteevaluationhsf_prefix_index. ff_gap_mce_mdr_full_rank_dataabsoluteevaluationhsf_prefix_index + S (ff_index_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix) = (S (mdr_q_full_rank_dataabsoluteevaluationhs))) -> exists ff_ap_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix ff_an_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix ff_bp_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix ff_bn_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix ff_p_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix ff_n_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix. ((((exists ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_prefix_ap. ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix)) * mdr_pc_full_rank_dataabsoluteevaluationh)) /\ exists ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_prefix_ap. mdr_pb_full_rank_dataabsoluteevaluationh = ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix)) * mdr_pc_full_rank_dataabsoluteevaluationh) + (ff_ap_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_prefix_an. ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_prefix_an + S (ff_an_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix)) * mdr_nc_full_rank_dataabsoluteevaluationh)) /\ exists ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_prefix_an. mdr_nb_full_rank_dataabsoluteevaluationh = ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix)) * mdr_nc_full_rank_dataabsoluteevaluationh) + (ff_an_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_prefix_bp. ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix)) * mdr_ec_full_rank_dataabsoluteevaluationhs)) /\ exists ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_prefix_bp. mdr_eb_full_rank_dataabsoluteevaluationhs = ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix)) * mdr_ec_full_rank_dataabsoluteevaluationhs) + (ff_bp_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_prefix_bn. ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix)) * mdr_fc_full_rank_dataabsoluteevaluationhs)) /\ exists ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_prefix_bn. mdr_fb_full_rank_dataabsoluteevaluationhs = ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix)) * mdr_fc_full_rank_dataabsoluteevaluationhs) + (ff_bn_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_prefix_positive. ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_prefix_positive + S (ff_p_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_full_rank_dataabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_prefix_positive. ff_ub_mce_fold_mdr_full_rank_dataabsoluteevaluationhsf = ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix)) * ff_uc_mce_fold_mdr_full_rank_dataabsoluteevaluationhsf) + (ff_p_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix))) /\ ((((exists ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_prefix_negative. ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_prefix_negative + S (ff_n_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_full_rank_dataabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_prefix_negative. ff_vb_mce_fold_mdr_full_rank_dataabsoluteevaluationhsf = ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix)) * ff_vc_mce_fold_mdr_full_rank_dataabsoluteevaluationhsf) + (ff_n_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_full_rank_dataabsoluteevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix = 2 * ff_even_mce_term_mdr_full_rank_dataabsoluteevaluationhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_full_rank_dataabsoluteevaluationhsf_prefix_term. ff_index_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix = 2 * ff_odd_mce_term_mdr_full_rank_dataabsoluteevaluationhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix) /\ ff_n_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix = (ff_ap_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix) * (ff_bp_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix) + (ff_an_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix) * (ff_bn_mce_alternating_mdr_full_rank_dataabsoluteevaluationhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive ff_v_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive. ((((exists ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive_start. ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive_start. ff_u_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive = ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive_terminal. ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive_terminal + S (mdr_p_full_rank_dataabsoluteevaluationh) = S ((S ((S (mdr_q_full_rank_dataabsoluteevaluationhs)))) * ff_v_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive_terminal. ff_u_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive = ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive_terminal * S ((S ((S (mdr_q_full_rank_dataabsoluteevaluationhs)))) * ff_v_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive) + (mdr_p_full_rank_dataabsoluteevaluationh))) /\ forall ff_i_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive. (exists ff_lt_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive_bound. ff_lt_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive_bound + S ff_i_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive = (S (mdr_q_full_rank_dataabsoluteevaluationhs))) -> exists ff_a_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive ff_r_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive ff_s_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive. ((((exists ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive_summand. ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive_summand + S (ff_a_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive) = S ((S (ff_i_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive)) * ff_uc_mce_fold_mdr_full_rank_dataabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive_summand. ff_ub_mce_fold_mdr_full_rank_dataabsoluteevaluationhsf = ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive_summand * S ((S (ff_i_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive)) * ff_uc_mce_fold_mdr_full_rank_dataabsoluteevaluationhsf) + (ff_a_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive_partial. ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive_partial + S (ff_r_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive) = S ((S (ff_i_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive_partial. ff_u_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive = ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive_partial * S ((S (ff_i_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive) + (ff_r_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive))) /\ ((((exists ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive_successor. ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive_successor + S (ff_s_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive) = S ((S (S ff_i_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive)) /\ exists ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive_successor. ff_u_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive = ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive_successor * S ((S (S ff_i_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive)) * ff_v_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive) + (ff_s_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive))) /\ ff_s_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive = ff_r_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive + ff_a_mce_mdr_full_rank_dataabsoluteevaluationhsf_positive)))))) /\ (exists ff_u_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative ff_v_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative. ((((exists ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative_start. ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative_start. ff_u_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative = ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative_terminal. ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative_terminal + S (mdr_n_full_rank_dataabsoluteevaluationh) = S ((S ((S (mdr_q_full_rank_dataabsoluteevaluationhs)))) * ff_v_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative_terminal. ff_u_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative = ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative_terminal * S ((S ((S (mdr_q_full_rank_dataabsoluteevaluationhs)))) * ff_v_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative) + (mdr_n_full_rank_dataabsoluteevaluationh))) /\ forall ff_i_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative. (exists ff_lt_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative_bound. ff_lt_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative_bound + S ff_i_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative = (S (mdr_q_full_rank_dataabsoluteevaluationhs))) -> exists ff_a_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative ff_r_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative ff_s_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative. ((((exists ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative_summand. ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative_summand + S (ff_a_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative) = S ((S (ff_i_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative)) * ff_vc_mce_fold_mdr_full_rank_dataabsoluteevaluationhsf)) /\ exists ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative_summand. ff_vb_mce_fold_mdr_full_rank_dataabsoluteevaluationhsf = ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative_summand * S ((S (ff_i_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative)) * ff_vc_mce_fold_mdr_full_rank_dataabsoluteevaluationhsf) + (ff_a_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative_partial. ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative_partial + S (ff_r_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative) = S ((S (ff_i_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative_partial. ff_u_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative = ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative_partial * S ((S (ff_i_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative) + (ff_r_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative))) /\ ((((exists ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative_successor. ff_h_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative_successor + S (ff_s_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative) = S ((S (S ff_i_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative)) /\ exists ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative_successor. ff_u_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative = ff_q_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative_successor * S ((S (S ff_i_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative)) * ff_v_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative) + (ff_s_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative))) /\ ff_s_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative = ff_r_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative + ff_a_mce_mdr_full_rank_dataabsoluteevaluationhsf_negative))))))))))))))) /\ ((exists mdr_gap_full_rank_dataabsoluteevaluationi. mdr_gap_full_rank_dataabsoluteevaluationi + S (mdr_i_full_rank_dataabsoluteevaluation) = (mdr_l_full_rank_dataabsoluteevaluation)) /\ (exists mdr_z_full_rank_dataabsoluteevaluationr. ((exists mdr_a_full_rank_dataabsoluteevaluationrc mdr_b_full_rank_dataabsoluteevaluationrc mdr_c_full_rank_dataabsoluteevaluationrc mdr_e_full_rank_dataabsoluteevaluationrc mdr_f_full_rank_dataabsoluteevaluationrc. ((mdr_a_full_rank_dataabsoluteevaluationrc = ((d) + (ab)) * S ((d) + (ab)) + ((ab) + (ab))) /\ ((mdr_b_full_rank_dataabsoluteevaluationrc = ((ac) + (bb)) * S ((ac) + (bb)) + ((bb) + (bb))) /\ ((mdr_c_full_rank_dataabsoluteevaluationrc = ((mdr_a_full_rank_dataabsoluteevaluationrc) + (mdr_b_full_rank_dataabsoluteevaluationrc)) * S ((mdr_a_full_rank_dataabsoluteevaluationrc) + (mdr_b_full_rank_dataabsoluteevaluationrc)) + ((mdr_b_full_rank_dataabsoluteevaluationrc) + (mdr_b_full_rank_dataabsoluteevaluationrc))) /\ ((mdr_e_full_rank_dataabsoluteevaluationrc = ((mdr_p_full_rank_dataabsolute) + (mdr_n_full_rank_dataabsolute)) * S ((mdr_p_full_rank_dataabsolute) + (mdr_n_full_rank_dataabsolute)) + ((mdr_n_full_rank_dataabsolute) + (mdr_n_full_rank_dataabsolute))) /\ ((mdr_f_full_rank_dataabsoluteevaluationrc = ((bc) + (mdr_e_full_rank_dataabsoluteevaluationrc)) * S ((bc) + (mdr_e_full_rank_dataabsoluteevaluationrc)) + ((mdr_e_full_rank_dataabsoluteevaluationrc) + (mdr_e_full_rank_dataabsoluteevaluationrc))) /\ ((mdr_z_full_rank_dataabsoluteevaluationr) = ((mdr_c_full_rank_dataabsoluteevaluationrc) + (mdr_f_full_rank_dataabsoluteevaluationrc)) * S ((mdr_c_full_rank_dataabsoluteevaluationrc) + (mdr_f_full_rank_dataabsoluteevaluationrc)) + ((mdr_f_full_rank_dataabsoluteevaluationrc) + (mdr_f_full_rank_dataabsoluteevaluationrc))))))))) /\ (((exists ff_h_mdr_full_rank_dataabsoluteevaluationrb. ff_h_mdr_full_rank_dataabsoluteevaluationrb + S (mdr_z_full_rank_dataabsoluteevaluationr) = S ((S (mdr_i_full_rank_dataabsoluteevaluation)) * mdr_c_full_rank_dataabsoluteevaluation)) /\ exists ff_q_mdr_full_rank_dataabsoluteevaluationrb. mdr_b_full_rank_dataabsoluteevaluation = ff_q_mdr_full_rank_dataabsoluteevaluationrb * S ((S (mdr_i_full_rank_dataabsoluteevaluation)) * mdr_c_full_rank_dataabsoluteevaluation) + (mdr_z_full_rank_dataabsoluteevaluationr)))))))) /\ (((mdr_p_full_rank_dataabsolute) = (mdr_n_full_rank_dataabsolute) + (D)) \/ ((mdr_n_full_rank_dataabsolute) = (mdr_p_full_rank_dataabsolute) + (D)))))))) -> (((exists mdr_gap_data_full_rankrows_bound. mdr_gap_data_full_rankrows_bound + (d) = (d)) /\ ((exists mdr_gap_data_full_rankcolumns_bound. mdr_gap_data_full_rankcolumns_bound + (d) = (d)) /\ ((exists mdr_rb_data_full_rankwitness mdr_rc_data_full_rankwitness mdr_cb_data_full_rankwitness mdr_cc_data_full_rankwitness. (((((forall fom_index_mrf_data_full_rankwitnessminorrowsbound. (exists fom_gap_mrf_data_full_rankwitnessminorrowsbound_index_bound. fom_gap_mrf_data_full_rankwitnessminorrowsbound_index_bound + S (fom_index_mrf_data_full_rankwitnessminorrowsbound) = d) -> exists fom_value_mrf_data_full_rankwitnessminorrowsbound. ((((exists fom_beta_height_mrf_data_full_rankwitnessminorrowsbound_entry. fom_beta_height_mrf_data_full_rankwitnessminorrowsbound_entry + S (fom_value_mrf_data_full_rankwitnessminorrowsbound) = S ((S (fom_index_mrf_data_full_rankwitnessminorrowsbound)) * mdr_rc_data_full_rankwitness)) /\ exists fom_beta_quotient_mrf_data_full_rankwitnessminorrowsbound_entry. mdr_rb_data_full_rankwitness = fom_beta_quotient_mrf_data_full_rankwitnessminorrowsbound_entry * S ((S (fom_index_mrf_data_full_rankwitnessminorrowsbound)) * mdr_rc_data_full_rankwitness) + (fom_value_mrf_data_full_rankwitnessminorrowsbound))) /\ (exists fom_gap_mrf_data_full_rankwitnessminorrowsbound_value_bound. fom_gap_mrf_data_full_rankwitnessminorrowsbound_value_bound + S (fom_value_mrf_data_full_rankwitnessminorrowsbound) = d))) /\ (forall mdr_i_data_full_rankwitnessminorrowsdistinct mdr_j_data_full_rankwitnessminorrowsdistinct mdr_a_data_full_rankwitnessminorrowsdistinct. (exists mdr_gap_data_full_rankwitnessminorrowsdistincti. mdr_gap_data_full_rankwitnessminorrowsdistincti + S (mdr_i_data_full_rankwitnessminorrowsdistinct) = (d)) -> (exists mdr_gap_data_full_rankwitnessminorrowsdistinctj. mdr_gap_data_full_rankwitnessminorrowsdistinctj + S (mdr_j_data_full_rankwitnessminorrowsdistinct) = (d)) -> (((exists ff_h_mdr_data_full_rankwitnessminorrowsdistinctfirst. ff_h_mdr_data_full_rankwitnessminorrowsdistinctfirst + S (mdr_a_data_full_rankwitnessminorrowsdistinct) = S ((S (mdr_i_data_full_rankwitnessminorrowsdistinct)) * mdr_rc_data_full_rankwitness)) /\ exists ff_q_mdr_data_full_rankwitnessminorrowsdistinctfirst. mdr_rb_data_full_rankwitness = ff_q_mdr_data_full_rankwitnessminorrowsdistinctfirst * S ((S (mdr_i_data_full_rankwitnessminorrowsdistinct)) * mdr_rc_data_full_rankwitness) + (mdr_a_data_full_rankwitnessminorrowsdistinct))) -> (((exists ff_h_mdr_data_full_rankwitnessminorrowsdistinctsecond. ff_h_mdr_data_full_rankwitnessminorrowsdistinctsecond + S (mdr_a_data_full_rankwitnessminorrowsdistinct) = S ((S (mdr_j_data_full_rankwitnessminorrowsdistinct)) * mdr_rc_data_full_rankwitness)) /\ exists ff_q_mdr_data_full_rankwitnessminorrowsdistinctsecond. mdr_rb_data_full_rankwitness = ff_q_mdr_data_full_rankwitnessminorrowsdistinctsecond * S ((S (mdr_j_data_full_rankwitnessminorrowsdistinct)) * mdr_rc_data_full_rankwitness) + (mdr_a_data_full_rankwitnessminorrowsdistinct))) -> mdr_i_data_full_rankwitnessminorrowsdistinct = mdr_j_data_full_rankwitnessminorrowsdistinct))) /\ ((((forall fom_index_mrf_data_full_rankwitnessminorcolumnsbound. (exists fom_gap_mrf_data_full_rankwitnessminorcolumnsbound_index_bound. fom_gap_mrf_data_full_rankwitnessminorcolumnsbound_index_bound + S (fom_index_mrf_data_full_rankwitnessminorcolumnsbound) = d) -> exists fom_value_mrf_data_full_rankwitnessminorcolumnsbound. ((((exists fom_beta_height_mrf_data_full_rankwitnessminorcolumnsbound_entry. fom_beta_height_mrf_data_full_rankwitnessminorcolumnsbound_entry + S (fom_value_mrf_data_full_rankwitnessminorcolumnsbound) = S ((S (fom_index_mrf_data_full_rankwitnessminorcolumnsbound)) * mdr_cc_data_full_rankwitness)) /\ exists fom_beta_quotient_mrf_data_full_rankwitnessminorcolumnsbound_entry. mdr_cb_data_full_rankwitness = fom_beta_quotient_mrf_data_full_rankwitnessminorcolumnsbound_entry * S ((S (fom_index_mrf_data_full_rankwitnessminorcolumnsbound)) * mdr_cc_data_full_rankwitness) + (fom_value_mrf_data_full_rankwitnessminorcolumnsbound))) /\ (exists fom_gap_mrf_data_full_rankwitnessminorcolumnsbound_value_bound. fom_gap_mrf_data_full_rankwitnessminorcolumnsbound_value_bound + S (fom_value_mrf_data_full_rankwitnessminorcolumnsbound) = d))) /\ (forall mdr_i_data_full_rankwitnessminorcolumnsdistinct mdr_j_data_full_rankwitnessminorcolumnsdistinct mdr_a_data_full_rankwitnessminorcolumnsdistinct. (exists mdr_gap_data_full_rankwitnessminorcolumnsdistincti. mdr_gap_data_full_rankwitnessminorcolumnsdistincti + S (mdr_i_data_full_rankwitnessminorcolumnsdistinct) = (d)) -> (exists mdr_gap_data_full_rankwitnessminorcolumnsdistinctj. mdr_gap_data_full_rankwitnessminorcolumnsdistinctj + S (mdr_j_data_full_rankwitnessminorcolumnsdistinct) = (d)) -> (((exists ff_h_mdr_data_full_rankwitnessminorcolumnsdistinctfirst. ff_h_mdr_data_full_rankwitnessminorcolumnsdistinctfirst + S (mdr_a_data_full_rankwitnessminorcolumnsdistinct) = S ((S (mdr_i_data_full_rankwitnessminorcolumnsdistinct)) * mdr_cc_data_full_rankwitness)) /\ exists ff_q_mdr_data_full_rankwitnessminorcolumnsdistinctfirst. mdr_cb_data_full_rankwitness = ff_q_mdr_data_full_rankwitnessminorcolumnsdistinctfirst * S ((S (mdr_i_data_full_rankwitnessminorcolumnsdistinct)) * mdr_cc_data_full_rankwitness) + (mdr_a_data_full_rankwitnessminorcolumnsdistinct))) -> (((exists ff_h_mdr_data_full_rankwitnessminorcolumnsdistinctsecond. ff_h_mdr_data_full_rankwitnessminorcolumnsdistinctsecond + S (mdr_a_data_full_rankwitnessminorcolumnsdistinct) = S ((S (mdr_j_data_full_rankwitnessminorcolumnsdistinct)) * mdr_cc_data_full_rankwitness)) /\ exists ff_q_mdr_data_full_rankwitnessminorcolumnsdistinctsecond. mdr_cb_data_full_rankwitness = ff_q_mdr_data_full_rankwitnessminorcolumnsdistinctsecond * S ((S (mdr_j_data_full_rankwitnessminorcolumnsdistinct)) * mdr_cc_data_full_rankwitness) + (mdr_a_data_full_rankwitnessminorcolumnsdistinct))) -> mdr_i_data_full_rankwitnessminorcolumnsdistinct = mdr_j_data_full_rankwitnessminorcolumnsdistinct))) /\ (exists mdr_p_data_full_rankwitnessminornonzero mdr_n_data_full_rankwitnessminornonzero. ((exists mdr_ub_data_full_rankwitnessminornonzeroevaluation mdr_uc_data_full_rankwitnessminornonzeroevaluation mdr_vb_data_full_rankwitnessminornonzeroevaluation mdr_vc_data_full_rankwitnessminornonzeroevaluation. ((((forall mdr_i_data_full_rankwitnessminornonzeroevaluationmatrixpositive. (exists mdr_gap_data_full_rankwitnessminornonzeroevaluationmatrixpositivebound. mdr_gap_data_full_rankwitnessminornonzeroevaluationmatrixpositivebound + S (mdr_i_data_full_rankwitnessminornonzeroevaluationmatrixpositive) = ((d) * (d))) -> exists mdr_a_data_full_rankwitnessminornonzeroevaluationmatrixpositive. (((exists mdr_r_data_full_rankwitnessminornonzeroevaluationmatrixpositivepoint mdr_s_data_full_rankwitnessminornonzeroevaluationmatrixpositivepoint mdr_u_data_full_rankwitnessminornonzeroevaluationmatrixpositivepoint mdr_v_data_full_rankwitnessminornonzeroevaluationmatrixpositivepoint. ((mdr_i_data_full_rankwitnessminornonzeroevaluationmatrixpositive = (d) * mdr_r_data_full_rankwitnessminornonzeroevaluationmatrixpositivepoint + mdr_s_data_full_rankwitnessminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_data_full_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_data_full_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_data_full_rankwitnessminornonzeroevaluationmatrixpositivepoint) = (d)) /\ ((((exists ff_h_mdr_data_full_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_data_full_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_data_full_rankwitnessminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_data_full_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_data_full_rankwitness)) /\ exists ff_q_mdr_data_full_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index. mdr_rb_data_full_rankwitness = ff_q_mdr_data_full_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_data_full_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_data_full_rankwitness) + (mdr_u_data_full_rankwitnessminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_data_full_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_data_full_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_data_full_rankwitnessminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_data_full_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_data_full_rankwitness)) /\ exists ff_q_mdr_data_full_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_data_full_rankwitness = ff_q_mdr_data_full_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_data_full_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_data_full_rankwitness) + (mdr_v_data_full_rankwitnessminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_data_full_rankwitnessminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_data_full_rankwitnessminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_data_full_rankwitnessminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_data_full_rankwitnessminornonzeroevaluationmatrixpositivepoint) * (d) + (mdr_v_data_full_rankwitnessminornonzeroevaluationmatrixpositivepoint))) * ac)) /\ exists ff_q_mdr_data_full_rankwitnessminornonzeroevaluationmatrixpositivepointsource. ab = ff_q_mdr_data_full_rankwitnessminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_data_full_rankwitnessminornonzeroevaluationmatrixpositivepoint) * (d) + (mdr_v_data_full_rankwitnessminornonzeroevaluationmatrixpositivepoint))) * ac) + (mdr_a_data_full_rankwitnessminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_data_full_rankwitnessminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_data_full_rankwitnessminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_data_full_rankwitnessminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_data_full_rankwitnessminornonzeroevaluationmatrixpositive)) * mdr_uc_data_full_rankwitnessminornonzeroevaluation)) /\ exists ff_q_mdr_data_full_rankwitnessminornonzeroevaluationmatrixpositiveoutput. mdr_ub_data_full_rankwitnessminornonzeroevaluation = ff_q_mdr_data_full_rankwitnessminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_data_full_rankwitnessminornonzeroevaluationmatrixpositive)) * mdr_uc_data_full_rankwitnessminornonzeroevaluation) + (mdr_a_data_full_rankwitnessminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_data_full_rankwitnessminornonzeroevaluationmatrixnegative. (exists mdr_gap_data_full_rankwitnessminornonzeroevaluationmatrixnegativebound. mdr_gap_data_full_rankwitnessminornonzeroevaluationmatrixnegativebound + S (mdr_i_data_full_rankwitnessminornonzeroevaluationmatrixnegative) = ((d) * (d))) -> exists mdr_a_data_full_rankwitnessminornonzeroevaluationmatrixnegative. (((exists mdr_r_data_full_rankwitnessminornonzeroevaluationmatrixnegativepoint mdr_s_data_full_rankwitnessminornonzeroevaluationmatrixnegativepoint mdr_u_data_full_rankwitnessminornonzeroevaluationmatrixnegativepoint mdr_v_data_full_rankwitnessminornonzeroevaluationmatrixnegativepoint. ((mdr_i_data_full_rankwitnessminornonzeroevaluationmatrixnegative = (d) * mdr_r_data_full_rankwitnessminornonzeroevaluationmatrixnegativepoint + mdr_s_data_full_rankwitnessminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_data_full_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_data_full_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_data_full_rankwitnessminornonzeroevaluationmatrixnegativepoint) = (d)) /\ ((((exists ff_h_mdr_data_full_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_data_full_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_data_full_rankwitnessminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_data_full_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_data_full_rankwitness)) /\ exists ff_q_mdr_data_full_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index. mdr_rb_data_full_rankwitness = ff_q_mdr_data_full_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_data_full_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_data_full_rankwitness) + (mdr_u_data_full_rankwitnessminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_data_full_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_data_full_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_data_full_rankwitnessminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_data_full_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_data_full_rankwitness)) /\ exists ff_q_mdr_data_full_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_data_full_rankwitness = ff_q_mdr_data_full_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_data_full_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_data_full_rankwitness) + (mdr_v_data_full_rankwitnessminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_data_full_rankwitnessminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_data_full_rankwitnessminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_data_full_rankwitnessminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_data_full_rankwitnessminornonzeroevaluationmatrixnegativepoint) * (d) + (mdr_v_data_full_rankwitnessminornonzeroevaluationmatrixnegativepoint))) * bc)) /\ exists ff_q_mdr_data_full_rankwitnessminornonzeroevaluationmatrixnegativepointsource. bb = ff_q_mdr_data_full_rankwitnessminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_data_full_rankwitnessminornonzeroevaluationmatrixnegativepoint) * (d) + (mdr_v_data_full_rankwitnessminornonzeroevaluationmatrixnegativepoint))) * bc) + (mdr_a_data_full_rankwitnessminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_data_full_rankwitnessminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_data_full_rankwitnessminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_data_full_rankwitnessminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_data_full_rankwitnessminornonzeroevaluationmatrixnegative)) * mdr_vc_data_full_rankwitnessminornonzeroevaluation)) /\ exists ff_q_mdr_data_full_rankwitnessminornonzeroevaluationmatrixnegativeoutput. mdr_vb_data_full_rankwitnessminornonzeroevaluation = ff_q_mdr_data_full_rankwitnessminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_data_full_rankwitnessminornonzeroevaluationmatrixnegative)) * mdr_vc_data_full_rankwitnessminornonzeroevaluation) + (mdr_a_data_full_rankwitnessminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_data_full_rankwitnessminornonzeroevaluationdeterminant mdr_c_data_full_rankwitnessminornonzeroevaluationdeterminant mdr_l_data_full_rankwitnessminornonzeroevaluationdeterminant mdr_i_data_full_rankwitnessminornonzeroevaluationdeterminant. ((forall mdr_i_data_full_rankwitnessminornonzeroevaluationdeterminanth. (exists mdr_gap_data_full_rankwitnessminornonzeroevaluationdeterminanthi. mdr_gap_data_full_rankwitnessminornonzeroevaluationdeterminanthi + S (mdr_i_data_full_rankwitnessminornonzeroevaluationdeterminanth) = (mdr_l_data_full_rankwitnessminornonzeroevaluationdeterminant)) -> exists mdr_d_data_full_rankwitnessminornonzeroevaluationdeterminanth mdr_pb_data_full_rankwitnessminornonzeroevaluationdeterminanth mdr_pc_data_full_rankwitnessminornonzeroevaluationdeterminanth mdr_nb_data_full_rankwitnessminornonzeroevaluationdeterminanth mdr_nc_data_full_rankwitnessminornonzeroevaluationdeterminanth mdr_p_data_full_rankwitnessminornonzeroevaluationdeterminanth mdr_n_data_full_rankwitnessminornonzeroevaluationdeterminanth. ((exists mdr_z_data_full_rankwitnessminornonzeroevaluationdeterminanthr. ((exists mdr_a_data_full_rankwitnessminornonzeroevaluationdeterminanthrc mdr_b_data_full_rankwitnessminornonzeroevaluationdeterminanthrc mdr_c_data_full_rankwitnessminornonzeroevaluationdeterminanthrc mdr_e_data_full_rankwitnessminornonzeroevaluationdeterminanthrc mdr_f_data_full_rankwitnessminornonzeroevaluationdeterminanthrc. ((mdr_a_data_full_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_d_data_full_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_data_full_rankwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_d_data_full_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_data_full_rankwitnessminornonzeroevaluationdeterminanth)) + ((mdr_pb_data_full_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_data_full_rankwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_b_data_full_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_pc_data_full_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_data_full_rankwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_pc_data_full_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_data_full_rankwitnessminornonzeroevaluationdeterminanth)) + ((mdr_nb_data_full_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_data_full_rankwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_c_data_full_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_a_data_full_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_data_full_rankwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_data_full_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_data_full_rankwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_b_data_full_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_data_full_rankwitnessminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_data_full_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_p_data_full_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_n_data_full_rankwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_p_data_full_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_n_data_full_rankwitnessminornonzeroevaluationdeterminanth)) + ((mdr_n_data_full_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_n_data_full_rankwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_f_data_full_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_nc_data_full_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_e_data_full_rankwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_data_full_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_e_data_full_rankwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_e_data_full_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_e_data_full_rankwitnessminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_data_full_rankwitnessminornonzeroevaluationdeterminanthr) = ((mdr_c_data_full_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_data_full_rankwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_data_full_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_data_full_rankwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_f_data_full_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_data_full_rankwitnessminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthrb. ff_h_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthrb + S (mdr_z_data_full_rankwitnessminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_data_full_rankwitnessminornonzeroevaluationdeterminanth)) * mdr_c_data_full_rankwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthrb. mdr_b_data_full_rankwitnessminornonzeroevaluationdeterminant = ff_q_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_data_full_rankwitnessminornonzeroevaluationdeterminanth)) * mdr_c_data_full_rankwitnessminornonzeroevaluationdeterminant) + (mdr_z_data_full_rankwitnessminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_data_full_rankwitnessminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_data_full_rankwitnessminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_data_full_rankwitnessminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_data_full_rankwitnessminornonzeroevaluationdeterminanths mdr_eb_data_full_rankwitnessminornonzeroevaluationdeterminanths mdr_ec_data_full_rankwitnessminornonzeroevaluationdeterminanths mdr_fb_data_full_rankwitnessminornonzeroevaluationdeterminanths mdr_fc_data_full_rankwitnessminornonzeroevaluationdeterminanths. (((mdr_d_data_full_rankwitnessminornonzeroevaluationdeterminanth) = S (mdr_q_data_full_rankwitnessminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_data_full_rankwitnessminornonzeroevaluationdeterminanthsc. (exists mdr_gap_data_full_rankwitnessminornonzeroevaluationdeterminanthscj. mdr_gap_data_full_rankwitnessminornonzeroevaluationdeterminanthscj + S (mdr_j_data_full_rankwitnessminornonzeroevaluationdeterminanthsc) = (S (mdr_q_data_full_rankwitnessminornonzeroevaluationdeterminanths))) -> exists mdr_i_data_full_rankwitnessminornonzeroevaluationdeterminanthsc mdr_up_data_full_rankwitnessminornonzeroevaluationdeterminanthsc mdr_us_data_full_rankwitnessminornonzeroevaluationdeterminanthsc mdr_un_data_full_rankwitnessminornonzeroevaluationdeterminanthsc mdr_ut_data_full_rankwitnessminornonzeroevaluationdeterminanthsc mdr_p_data_full_rankwitnessminornonzeroevaluationdeterminanthsc mdr_n_data_full_rankwitnessminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_data_full_rankwitnessminornonzeroevaluationdeterminanthsci. mdr_gap_data_full_rankwitnessminornonzeroevaluationdeterminanthsci + S (mdr_i_data_full_rankwitnessminornonzeroevaluationdeterminanthsc) = (mdr_i_data_full_rankwitnessminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_data_full_rankwitnessminornonzeroevaluationdeterminanthscr. ((exists mdr_a_data_full_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_b_data_full_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_c_data_full_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_e_data_full_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_f_data_full_rankwitnessminornonzeroevaluationdeterminanthscrc. ((mdr_a_data_full_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_q_data_full_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_up_data_full_rankwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_data_full_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_up_data_full_rankwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_up_data_full_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_up_data_full_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_data_full_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_us_data_full_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_data_full_rankwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_data_full_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_data_full_rankwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_un_data_full_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_data_full_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_data_full_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_a_data_full_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_data_full_rankwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_data_full_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_data_full_rankwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_data_full_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_data_full_rankwitnessminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_data_full_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_p_data_full_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_data_full_rankwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_data_full_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_data_full_rankwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_n_data_full_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_data_full_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_data_full_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_ut_data_full_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_e_data_full_rankwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_data_full_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_e_data_full_rankwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_data_full_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_e_data_full_rankwitnessminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_data_full_rankwitnessminornonzeroevaluationdeterminanthscr) = ((mdr_c_data_full_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_data_full_rankwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_data_full_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_data_full_rankwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_data_full_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_data_full_rankwitnessminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscrb. ff_h_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscrb + S (mdr_z_data_full_rankwitnessminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_data_full_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_c_data_full_rankwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscrb. mdr_b_data_full_rankwitnessminornonzeroevaluationdeterminant = ff_q_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_data_full_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_c_data_full_rankwitnessminornonzeroevaluationdeterminant) + (mdr_z_data_full_rankwitnessminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_data_full_rankwitnessminornonzeroevaluationdeterminanths) * (mdr_q_data_full_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive = (mdr_q_data_full_rankwitnessminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_data_full_rankwitnessminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_data_full_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_data_full_rankwitnessminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_data_full_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_data_full_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_data_full_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_data_full_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_data_full_rankwitnessminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_data_full_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_data_full_rankwitnessminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_data_full_rankwitnessminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_data_full_rankwitnessminornonzeroevaluationdeterminanths) * (mdr_q_data_full_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative = (mdr_q_data_full_rankwitnessminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_data_full_rankwitnessminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_data_full_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_data_full_rankwitnessminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_data_full_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_data_full_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_data_full_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_data_full_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_data_full_rankwitnessminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_data_full_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_data_full_rankwitnessminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_data_full_rankwitnessminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscp. ff_h_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscp + S (mdr_p_data_full_rankwitnessminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_data_full_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_ec_data_full_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscp. mdr_eb_data_full_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_data_full_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_ec_data_full_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_p_data_full_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscn. ff_h_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscn + S (mdr_n_data_full_rankwitnessminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_data_full_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_fc_data_full_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscn. mdr_fb_data_full_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_data_full_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_fc_data_full_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_n_data_full_rankwitnessminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_data_full_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_data_full_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_data_full_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_data_full_rankwitnessminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_data_full_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_data_full_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_data_full_rankwitnessminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_data_full_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_data_full_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_data_full_rankwitnessminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_data_full_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_data_full_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_data_full_rankwitnessminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_data_full_rankwitnessminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_data_full_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_data_full_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_data_full_rankwitnessminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_data_full_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_data_full_rankwitnessminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_data_full_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_data_full_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_data_full_rankwitnessminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_data_full_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_data_full_rankwitnessminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_data_full_rankwitnessminornonzeroevaluationdeterminanti. mdr_gap_data_full_rankwitnessminornonzeroevaluationdeterminanti + S (mdr_i_data_full_rankwitnessminornonzeroevaluationdeterminant) = (mdr_l_data_full_rankwitnessminornonzeroevaluationdeterminant)) /\ (exists mdr_z_data_full_rankwitnessminornonzeroevaluationdeterminantr. ((exists mdr_a_data_full_rankwitnessminornonzeroevaluationdeterminantrc mdr_b_data_full_rankwitnessminornonzeroevaluationdeterminantrc mdr_c_data_full_rankwitnessminornonzeroevaluationdeterminantrc mdr_e_data_full_rankwitnessminornonzeroevaluationdeterminantrc mdr_f_data_full_rankwitnessminornonzeroevaluationdeterminantrc. ((mdr_a_data_full_rankwitnessminornonzeroevaluationdeterminantrc = ((d) + (mdr_ub_data_full_rankwitnessminornonzeroevaluation)) * S ((d) + (mdr_ub_data_full_rankwitnessminornonzeroevaluation)) + ((mdr_ub_data_full_rankwitnessminornonzeroevaluation) + (mdr_ub_data_full_rankwitnessminornonzeroevaluation))) /\ ((mdr_b_data_full_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_uc_data_full_rankwitnessminornonzeroevaluation) + (mdr_vb_data_full_rankwitnessminornonzeroevaluation)) * S ((mdr_uc_data_full_rankwitnessminornonzeroevaluation) + (mdr_vb_data_full_rankwitnessminornonzeroevaluation)) + ((mdr_vb_data_full_rankwitnessminornonzeroevaluation) + (mdr_vb_data_full_rankwitnessminornonzeroevaluation))) /\ ((mdr_c_data_full_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_a_data_full_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_data_full_rankwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_a_data_full_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_data_full_rankwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_b_data_full_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_data_full_rankwitnessminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_data_full_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_p_data_full_rankwitnessminornonzero) + (mdr_n_data_full_rankwitnessminornonzero)) * S ((mdr_p_data_full_rankwitnessminornonzero) + (mdr_n_data_full_rankwitnessminornonzero)) + ((mdr_n_data_full_rankwitnessminornonzero) + (mdr_n_data_full_rankwitnessminornonzero))) /\ ((mdr_f_data_full_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_vc_data_full_rankwitnessminornonzeroevaluation) + (mdr_e_data_full_rankwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_data_full_rankwitnessminornonzeroevaluation) + (mdr_e_data_full_rankwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_e_data_full_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_e_data_full_rankwitnessminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_data_full_rankwitnessminornonzeroevaluationdeterminantr) = ((mdr_c_data_full_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_data_full_rankwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_c_data_full_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_data_full_rankwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_f_data_full_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_data_full_rankwitnessminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_data_full_rankwitnessminornonzeroevaluationdeterminantrb. ff_h_mdr_data_full_rankwitnessminornonzeroevaluationdeterminantrb + S (mdr_z_data_full_rankwitnessminornonzeroevaluationdeterminantr) = S ((S (mdr_i_data_full_rankwitnessminornonzeroevaluationdeterminant)) * mdr_c_data_full_rankwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_data_full_rankwitnessminornonzeroevaluationdeterminantrb. mdr_b_data_full_rankwitnessminornonzeroevaluationdeterminant = ff_q_mdr_data_full_rankwitnessminornonzeroevaluationdeterminantrb * S ((S (mdr_i_data_full_rankwitnessminornonzeroevaluationdeterminant)) * mdr_c_data_full_rankwitnessminornonzeroevaluationdeterminant) + (mdr_z_data_full_rankwitnessminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_data_full_rankwitnessminornonzero = mdr_n_data_full_rankwitnessminornonzero)))))))) /\ (forall mdr_q_data_full_rank. (exists mdr_gap_data_full_rankhigher. mdr_gap_data_full_rankhigher + S (d) = (mdr_q_data_full_rank)) -> (forall mdr_rb_data_full_rankzero mdr_rc_data_full_rankzero mdr_cb_data_full_rankzero mdr_cc_data_full_rankzero mdr_p_data_full_rankzero mdr_n_data_full_rankzero. (((forall fom_index_mrf_data_full_rankzerorowsbound. (exists fom_gap_mrf_data_full_rankzerorowsbound_index_bound. fom_gap_mrf_data_full_rankzerorowsbound_index_bound + S (fom_index_mrf_data_full_rankzerorowsbound) = mdr_q_data_full_rank) -> exists fom_value_mrf_data_full_rankzerorowsbound. ((((exists fom_beta_height_mrf_data_full_rankzerorowsbound_entry. fom_beta_height_mrf_data_full_rankzerorowsbound_entry + S (fom_value_mrf_data_full_rankzerorowsbound) = S ((S (fom_index_mrf_data_full_rankzerorowsbound)) * mdr_rc_data_full_rankzero)) /\ exists fom_beta_quotient_mrf_data_full_rankzerorowsbound_entry. mdr_rb_data_full_rankzero = fom_beta_quotient_mrf_data_full_rankzerorowsbound_entry * S ((S (fom_index_mrf_data_full_rankzerorowsbound)) * mdr_rc_data_full_rankzero) + (fom_value_mrf_data_full_rankzerorowsbound))) /\ (exists fom_gap_mrf_data_full_rankzerorowsbound_value_bound. fom_gap_mrf_data_full_rankzerorowsbound_value_bound + S (fom_value_mrf_data_full_rankzerorowsbound) = d))) /\ (forall mdr_i_data_full_rankzerorowsdistinct mdr_j_data_full_rankzerorowsdistinct mdr_a_data_full_rankzerorowsdistinct. (exists mdr_gap_data_full_rankzerorowsdistincti. mdr_gap_data_full_rankzerorowsdistincti + S (mdr_i_data_full_rankzerorowsdistinct) = (mdr_q_data_full_rank)) -> (exists mdr_gap_data_full_rankzerorowsdistinctj. mdr_gap_data_full_rankzerorowsdistinctj + S (mdr_j_data_full_rankzerorowsdistinct) = (mdr_q_data_full_rank)) -> (((exists ff_h_mdr_data_full_rankzerorowsdistinctfirst. ff_h_mdr_data_full_rankzerorowsdistinctfirst + S (mdr_a_data_full_rankzerorowsdistinct) = S ((S (mdr_i_data_full_rankzerorowsdistinct)) * mdr_rc_data_full_rankzero)) /\ exists ff_q_mdr_data_full_rankzerorowsdistinctfirst. mdr_rb_data_full_rankzero = ff_q_mdr_data_full_rankzerorowsdistinctfirst * S ((S (mdr_i_data_full_rankzerorowsdistinct)) * mdr_rc_data_full_rankzero) + (mdr_a_data_full_rankzerorowsdistinct))) -> (((exists ff_h_mdr_data_full_rankzerorowsdistinctsecond. ff_h_mdr_data_full_rankzerorowsdistinctsecond + S (mdr_a_data_full_rankzerorowsdistinct) = S ((S (mdr_j_data_full_rankzerorowsdistinct)) * mdr_rc_data_full_rankzero)) /\ exists ff_q_mdr_data_full_rankzerorowsdistinctsecond. mdr_rb_data_full_rankzero = ff_q_mdr_data_full_rankzerorowsdistinctsecond * S ((S (mdr_j_data_full_rankzerorowsdistinct)) * mdr_rc_data_full_rankzero) + (mdr_a_data_full_rankzerorowsdistinct))) -> mdr_i_data_full_rankzerorowsdistinct = mdr_j_data_full_rankzerorowsdistinct))) -> (((forall fom_index_mrf_data_full_rankzerocolumnsbound. (exists fom_gap_mrf_data_full_rankzerocolumnsbound_index_bound. fom_gap_mrf_data_full_rankzerocolumnsbound_index_bound + S (fom_index_mrf_data_full_rankzerocolumnsbound) = mdr_q_data_full_rank) -> exists fom_value_mrf_data_full_rankzerocolumnsbound. ((((exists fom_beta_height_mrf_data_full_rankzerocolumnsbound_entry. fom_beta_height_mrf_data_full_rankzerocolumnsbound_entry + S (fom_value_mrf_data_full_rankzerocolumnsbound) = S ((S (fom_index_mrf_data_full_rankzerocolumnsbound)) * mdr_cc_data_full_rankzero)) /\ exists fom_beta_quotient_mrf_data_full_rankzerocolumnsbound_entry. mdr_cb_data_full_rankzero = fom_beta_quotient_mrf_data_full_rankzerocolumnsbound_entry * S ((S (fom_index_mrf_data_full_rankzerocolumnsbound)) * mdr_cc_data_full_rankzero) + (fom_value_mrf_data_full_rankzerocolumnsbound))) /\ (exists fom_gap_mrf_data_full_rankzerocolumnsbound_value_bound. fom_gap_mrf_data_full_rankzerocolumnsbound_value_bound + S (fom_value_mrf_data_full_rankzerocolumnsbound) = d))) /\ (forall mdr_i_data_full_rankzerocolumnsdistinct mdr_j_data_full_rankzerocolumnsdistinct mdr_a_data_full_rankzerocolumnsdistinct. (exists mdr_gap_data_full_rankzerocolumnsdistincti. mdr_gap_data_full_rankzerocolumnsdistincti + S (mdr_i_data_full_rankzerocolumnsdistinct) = (mdr_q_data_full_rank)) -> (exists mdr_gap_data_full_rankzerocolumnsdistinctj. mdr_gap_data_full_rankzerocolumnsdistinctj + S (mdr_j_data_full_rankzerocolumnsdistinct) = (mdr_q_data_full_rank)) -> (((exists ff_h_mdr_data_full_rankzerocolumnsdistinctfirst. ff_h_mdr_data_full_rankzerocolumnsdistinctfirst + S (mdr_a_data_full_rankzerocolumnsdistinct) = S ((S (mdr_i_data_full_rankzerocolumnsdistinct)) * mdr_cc_data_full_rankzero)) /\ exists ff_q_mdr_data_full_rankzerocolumnsdistinctfirst. mdr_cb_data_full_rankzero = ff_q_mdr_data_full_rankzerocolumnsdistinctfirst * S ((S (mdr_i_data_full_rankzerocolumnsdistinct)) * mdr_cc_data_full_rankzero) + (mdr_a_data_full_rankzerocolumnsdistinct))) -> (((exists ff_h_mdr_data_full_rankzerocolumnsdistinctsecond. ff_h_mdr_data_full_rankzerocolumnsdistinctsecond + S (mdr_a_data_full_rankzerocolumnsdistinct) = S ((S (mdr_j_data_full_rankzerocolumnsdistinct)) * mdr_cc_data_full_rankzero)) /\ exists ff_q_mdr_data_full_rankzerocolumnsdistinctsecond. mdr_cb_data_full_rankzero = ff_q_mdr_data_full_rankzerocolumnsdistinctsecond * S ((S (mdr_j_data_full_rankzerocolumnsdistinct)) * mdr_cc_data_full_rankzero) + (mdr_a_data_full_rankzerocolumnsdistinct))) -> mdr_i_data_full_rankzerocolumnsdistinct = mdr_j_data_full_rankzerocolumnsdistinct))) -> (exists mdr_ub_data_full_rankzeroevaluation mdr_uc_data_full_rankzeroevaluation mdr_vb_data_full_rankzeroevaluation mdr_vc_data_full_rankzeroevaluation. ((((forall mdr_i_data_full_rankzeroevaluationmatrixpositive. (exists mdr_gap_data_full_rankzeroevaluationmatrixpositivebound. mdr_gap_data_full_rankzeroevaluationmatrixpositivebound + S (mdr_i_data_full_rankzeroevaluationmatrixpositive) = ((mdr_q_data_full_rank) * (mdr_q_data_full_rank))) -> exists mdr_a_data_full_rankzeroevaluationmatrixpositive. (((exists mdr_r_data_full_rankzeroevaluationmatrixpositivepoint mdr_s_data_full_rankzeroevaluationmatrixpositivepoint mdr_u_data_full_rankzeroevaluationmatrixpositivepoint mdr_v_data_full_rankzeroevaluationmatrixpositivepoint. ((mdr_i_data_full_rankzeroevaluationmatrixpositive = (mdr_q_data_full_rank) * mdr_r_data_full_rankzeroevaluationmatrixpositivepoint + mdr_s_data_full_rankzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_data_full_rankzeroevaluationmatrixpositivepointcolumn. mdr_gap_data_full_rankzeroevaluationmatrixpositivepointcolumn + S (mdr_s_data_full_rankzeroevaluationmatrixpositivepoint) = (mdr_q_data_full_rank)) /\ ((((exists ff_h_mdr_data_full_rankzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_data_full_rankzeroevaluationmatrixpositivepointrow_index + S (mdr_u_data_full_rankzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_data_full_rankzeroevaluationmatrixpositivepoint)) * mdr_rc_data_full_rankzero)) /\ exists ff_q_mdr_data_full_rankzeroevaluationmatrixpositivepointrow_index. mdr_rb_data_full_rankzero = ff_q_mdr_data_full_rankzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_data_full_rankzeroevaluationmatrixpositivepoint)) * mdr_rc_data_full_rankzero) + (mdr_u_data_full_rankzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_data_full_rankzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_data_full_rankzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_data_full_rankzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_data_full_rankzeroevaluationmatrixpositivepoint)) * mdr_cc_data_full_rankzero)) /\ exists ff_q_mdr_data_full_rankzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_data_full_rankzero = ff_q_mdr_data_full_rankzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_data_full_rankzeroevaluationmatrixpositivepoint)) * mdr_cc_data_full_rankzero) + (mdr_v_data_full_rankzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_data_full_rankzeroevaluationmatrixpositivepointsource. ff_h_mdr_data_full_rankzeroevaluationmatrixpositivepointsource + S (mdr_a_data_full_rankzeroevaluationmatrixpositive) = S ((S ((mdr_u_data_full_rankzeroevaluationmatrixpositivepoint) * (d) + (mdr_v_data_full_rankzeroevaluationmatrixpositivepoint))) * ac)) /\ exists ff_q_mdr_data_full_rankzeroevaluationmatrixpositivepointsource. ab = ff_q_mdr_data_full_rankzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_data_full_rankzeroevaluationmatrixpositivepoint) * (d) + (mdr_v_data_full_rankzeroevaluationmatrixpositivepoint))) * ac) + (mdr_a_data_full_rankzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_data_full_rankzeroevaluationmatrixpositiveoutput. ff_h_mdr_data_full_rankzeroevaluationmatrixpositiveoutput + S (mdr_a_data_full_rankzeroevaluationmatrixpositive) = S ((S (mdr_i_data_full_rankzeroevaluationmatrixpositive)) * mdr_uc_data_full_rankzeroevaluation)) /\ exists ff_q_mdr_data_full_rankzeroevaluationmatrixpositiveoutput. mdr_ub_data_full_rankzeroevaluation = ff_q_mdr_data_full_rankzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_data_full_rankzeroevaluationmatrixpositive)) * mdr_uc_data_full_rankzeroevaluation) + (mdr_a_data_full_rankzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_data_full_rankzeroevaluationmatrixnegative. (exists mdr_gap_data_full_rankzeroevaluationmatrixnegativebound. mdr_gap_data_full_rankzeroevaluationmatrixnegativebound + S (mdr_i_data_full_rankzeroevaluationmatrixnegative) = ((mdr_q_data_full_rank) * (mdr_q_data_full_rank))) -> exists mdr_a_data_full_rankzeroevaluationmatrixnegative. (((exists mdr_r_data_full_rankzeroevaluationmatrixnegativepoint mdr_s_data_full_rankzeroevaluationmatrixnegativepoint mdr_u_data_full_rankzeroevaluationmatrixnegativepoint mdr_v_data_full_rankzeroevaluationmatrixnegativepoint. ((mdr_i_data_full_rankzeroevaluationmatrixnegative = (mdr_q_data_full_rank) * mdr_r_data_full_rankzeroevaluationmatrixnegativepoint + mdr_s_data_full_rankzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_data_full_rankzeroevaluationmatrixnegativepointcolumn. mdr_gap_data_full_rankzeroevaluationmatrixnegativepointcolumn + S (mdr_s_data_full_rankzeroevaluationmatrixnegativepoint) = (mdr_q_data_full_rank)) /\ ((((exists ff_h_mdr_data_full_rankzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_data_full_rankzeroevaluationmatrixnegativepointrow_index + S (mdr_u_data_full_rankzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_data_full_rankzeroevaluationmatrixnegativepoint)) * mdr_rc_data_full_rankzero)) /\ exists ff_q_mdr_data_full_rankzeroevaluationmatrixnegativepointrow_index. mdr_rb_data_full_rankzero = ff_q_mdr_data_full_rankzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_data_full_rankzeroevaluationmatrixnegativepoint)) * mdr_rc_data_full_rankzero) + (mdr_u_data_full_rankzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_data_full_rankzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_data_full_rankzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_data_full_rankzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_data_full_rankzeroevaluationmatrixnegativepoint)) * mdr_cc_data_full_rankzero)) /\ exists ff_q_mdr_data_full_rankzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_data_full_rankzero = ff_q_mdr_data_full_rankzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_data_full_rankzeroevaluationmatrixnegativepoint)) * mdr_cc_data_full_rankzero) + (mdr_v_data_full_rankzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_data_full_rankzeroevaluationmatrixnegativepointsource. ff_h_mdr_data_full_rankzeroevaluationmatrixnegativepointsource + S (mdr_a_data_full_rankzeroevaluationmatrixnegative) = S ((S ((mdr_u_data_full_rankzeroevaluationmatrixnegativepoint) * (d) + (mdr_v_data_full_rankzeroevaluationmatrixnegativepoint))) * bc)) /\ exists ff_q_mdr_data_full_rankzeroevaluationmatrixnegativepointsource. bb = ff_q_mdr_data_full_rankzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_data_full_rankzeroevaluationmatrixnegativepoint) * (d) + (mdr_v_data_full_rankzeroevaluationmatrixnegativepoint))) * bc) + (mdr_a_data_full_rankzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_data_full_rankzeroevaluationmatrixnegativeoutput. ff_h_mdr_data_full_rankzeroevaluationmatrixnegativeoutput + S (mdr_a_data_full_rankzeroevaluationmatrixnegative) = S ((S (mdr_i_data_full_rankzeroevaluationmatrixnegative)) * mdr_vc_data_full_rankzeroevaluation)) /\ exists ff_q_mdr_data_full_rankzeroevaluationmatrixnegativeoutput. mdr_vb_data_full_rankzeroevaluation = ff_q_mdr_data_full_rankzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_data_full_rankzeroevaluationmatrixnegative)) * mdr_vc_data_full_rankzeroevaluation) + (mdr_a_data_full_rankzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_data_full_rankzeroevaluationdeterminant mdr_c_data_full_rankzeroevaluationdeterminant mdr_l_data_full_rankzeroevaluationdeterminant mdr_i_data_full_rankzeroevaluationdeterminant. ((forall mdr_i_data_full_rankzeroevaluationdeterminanth. (exists mdr_gap_data_full_rankzeroevaluationdeterminanthi. mdr_gap_data_full_rankzeroevaluationdeterminanthi + S (mdr_i_data_full_rankzeroevaluationdeterminanth) = (mdr_l_data_full_rankzeroevaluationdeterminant)) -> exists mdr_d_data_full_rankzeroevaluationdeterminanth mdr_pb_data_full_rankzeroevaluationdeterminanth mdr_pc_data_full_rankzeroevaluationdeterminanth mdr_nb_data_full_rankzeroevaluationdeterminanth mdr_nc_data_full_rankzeroevaluationdeterminanth mdr_p_data_full_rankzeroevaluationdeterminanth mdr_n_data_full_rankzeroevaluationdeterminanth. ((exists mdr_z_data_full_rankzeroevaluationdeterminanthr. ((exists mdr_a_data_full_rankzeroevaluationdeterminanthrc mdr_b_data_full_rankzeroevaluationdeterminanthrc mdr_c_data_full_rankzeroevaluationdeterminanthrc mdr_e_data_full_rankzeroevaluationdeterminanthrc mdr_f_data_full_rankzeroevaluationdeterminanthrc. ((mdr_a_data_full_rankzeroevaluationdeterminanthrc = ((mdr_d_data_full_rankzeroevaluationdeterminanth) + (mdr_pb_data_full_rankzeroevaluationdeterminanth)) * S ((mdr_d_data_full_rankzeroevaluationdeterminanth) + (mdr_pb_data_full_rankzeroevaluationdeterminanth)) + ((mdr_pb_data_full_rankzeroevaluationdeterminanth) + (mdr_pb_data_full_rankzeroevaluationdeterminanth))) /\ ((mdr_b_data_full_rankzeroevaluationdeterminanthrc = ((mdr_pc_data_full_rankzeroevaluationdeterminanth) + (mdr_nb_data_full_rankzeroevaluationdeterminanth)) * S ((mdr_pc_data_full_rankzeroevaluationdeterminanth) + (mdr_nb_data_full_rankzeroevaluationdeterminanth)) + ((mdr_nb_data_full_rankzeroevaluationdeterminanth) + (mdr_nb_data_full_rankzeroevaluationdeterminanth))) /\ ((mdr_c_data_full_rankzeroevaluationdeterminanthrc = ((mdr_a_data_full_rankzeroevaluationdeterminanthrc) + (mdr_b_data_full_rankzeroevaluationdeterminanthrc)) * S ((mdr_a_data_full_rankzeroevaluationdeterminanthrc) + (mdr_b_data_full_rankzeroevaluationdeterminanthrc)) + ((mdr_b_data_full_rankzeroevaluationdeterminanthrc) + (mdr_b_data_full_rankzeroevaluationdeterminanthrc))) /\ ((mdr_e_data_full_rankzeroevaluationdeterminanthrc = ((mdr_p_data_full_rankzeroevaluationdeterminanth) + (mdr_n_data_full_rankzeroevaluationdeterminanth)) * S ((mdr_p_data_full_rankzeroevaluationdeterminanth) + (mdr_n_data_full_rankzeroevaluationdeterminanth)) + ((mdr_n_data_full_rankzeroevaluationdeterminanth) + (mdr_n_data_full_rankzeroevaluationdeterminanth))) /\ ((mdr_f_data_full_rankzeroevaluationdeterminanthrc = ((mdr_nc_data_full_rankzeroevaluationdeterminanth) + (mdr_e_data_full_rankzeroevaluationdeterminanthrc)) * S ((mdr_nc_data_full_rankzeroevaluationdeterminanth) + (mdr_e_data_full_rankzeroevaluationdeterminanthrc)) + ((mdr_e_data_full_rankzeroevaluationdeterminanthrc) + (mdr_e_data_full_rankzeroevaluationdeterminanthrc))) /\ ((mdr_z_data_full_rankzeroevaluationdeterminanthr) = ((mdr_c_data_full_rankzeroevaluationdeterminanthrc) + (mdr_f_data_full_rankzeroevaluationdeterminanthrc)) * S ((mdr_c_data_full_rankzeroevaluationdeterminanthrc) + (mdr_f_data_full_rankzeroevaluationdeterminanthrc)) + ((mdr_f_data_full_rankzeroevaluationdeterminanthrc) + (mdr_f_data_full_rankzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_data_full_rankzeroevaluationdeterminanthrb. ff_h_mdr_data_full_rankzeroevaluationdeterminanthrb + S (mdr_z_data_full_rankzeroevaluationdeterminanthr) = S ((S (mdr_i_data_full_rankzeroevaluationdeterminanth)) * mdr_c_data_full_rankzeroevaluationdeterminant)) /\ exists ff_q_mdr_data_full_rankzeroevaluationdeterminanthrb. mdr_b_data_full_rankzeroevaluationdeterminant = ff_q_mdr_data_full_rankzeroevaluationdeterminanthrb * S ((S (mdr_i_data_full_rankzeroevaluationdeterminanth)) * mdr_c_data_full_rankzeroevaluationdeterminant) + (mdr_z_data_full_rankzeroevaluationdeterminanthr))))) /\ (((((mdr_d_data_full_rankzeroevaluationdeterminanth) = 0) /\ (((mdr_p_data_full_rankzeroevaluationdeterminanth) = 1) /\ ((mdr_n_data_full_rankzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_data_full_rankzeroevaluationdeterminanths mdr_eb_data_full_rankzeroevaluationdeterminanths mdr_ec_data_full_rankzeroevaluationdeterminanths mdr_fb_data_full_rankzeroevaluationdeterminanths mdr_fc_data_full_rankzeroevaluationdeterminanths. (((mdr_d_data_full_rankzeroevaluationdeterminanth) = S (mdr_q_data_full_rankzeroevaluationdeterminanths)) /\ ((forall mdr_j_data_full_rankzeroevaluationdeterminanthsc. (exists mdr_gap_data_full_rankzeroevaluationdeterminanthscj. mdr_gap_data_full_rankzeroevaluationdeterminanthscj + S (mdr_j_data_full_rankzeroevaluationdeterminanthsc) = (S (mdr_q_data_full_rankzeroevaluationdeterminanths))) -> exists mdr_i_data_full_rankzeroevaluationdeterminanthsc mdr_up_data_full_rankzeroevaluationdeterminanthsc mdr_us_data_full_rankzeroevaluationdeterminanthsc mdr_un_data_full_rankzeroevaluationdeterminanthsc mdr_ut_data_full_rankzeroevaluationdeterminanthsc mdr_p_data_full_rankzeroevaluationdeterminanthsc mdr_n_data_full_rankzeroevaluationdeterminanthsc. ((exists mdr_gap_data_full_rankzeroevaluationdeterminanthsci. mdr_gap_data_full_rankzeroevaluationdeterminanthsci + S (mdr_i_data_full_rankzeroevaluationdeterminanthsc) = (mdr_i_data_full_rankzeroevaluationdeterminanth)) /\ ((exists mdr_z_data_full_rankzeroevaluationdeterminanthscr. ((exists mdr_a_data_full_rankzeroevaluationdeterminanthscrc mdr_b_data_full_rankzeroevaluationdeterminanthscrc mdr_c_data_full_rankzeroevaluationdeterminanthscrc mdr_e_data_full_rankzeroevaluationdeterminanthscrc mdr_f_data_full_rankzeroevaluationdeterminanthscrc. ((mdr_a_data_full_rankzeroevaluationdeterminanthscrc = ((mdr_q_data_full_rankzeroevaluationdeterminanths) + (mdr_up_data_full_rankzeroevaluationdeterminanthsc)) * S ((mdr_q_data_full_rankzeroevaluationdeterminanths) + (mdr_up_data_full_rankzeroevaluationdeterminanthsc)) + ((mdr_up_data_full_rankzeroevaluationdeterminanthsc) + (mdr_up_data_full_rankzeroevaluationdeterminanthsc))) /\ ((mdr_b_data_full_rankzeroevaluationdeterminanthscrc = ((mdr_us_data_full_rankzeroevaluationdeterminanthsc) + (mdr_un_data_full_rankzeroevaluationdeterminanthsc)) * S ((mdr_us_data_full_rankzeroevaluationdeterminanthsc) + (mdr_un_data_full_rankzeroevaluationdeterminanthsc)) + ((mdr_un_data_full_rankzeroevaluationdeterminanthsc) + (mdr_un_data_full_rankzeroevaluationdeterminanthsc))) /\ ((mdr_c_data_full_rankzeroevaluationdeterminanthscrc = ((mdr_a_data_full_rankzeroevaluationdeterminanthscrc) + (mdr_b_data_full_rankzeroevaluationdeterminanthscrc)) * S ((mdr_a_data_full_rankzeroevaluationdeterminanthscrc) + (mdr_b_data_full_rankzeroevaluationdeterminanthscrc)) + ((mdr_b_data_full_rankzeroevaluationdeterminanthscrc) + (mdr_b_data_full_rankzeroevaluationdeterminanthscrc))) /\ ((mdr_e_data_full_rankzeroevaluationdeterminanthscrc = ((mdr_p_data_full_rankzeroevaluationdeterminanthsc) + (mdr_n_data_full_rankzeroevaluationdeterminanthsc)) * S ((mdr_p_data_full_rankzeroevaluationdeterminanthsc) + (mdr_n_data_full_rankzeroevaluationdeterminanthsc)) + ((mdr_n_data_full_rankzeroevaluationdeterminanthsc) + (mdr_n_data_full_rankzeroevaluationdeterminanthsc))) /\ ((mdr_f_data_full_rankzeroevaluationdeterminanthscrc = ((mdr_ut_data_full_rankzeroevaluationdeterminanthsc) + (mdr_e_data_full_rankzeroevaluationdeterminanthscrc)) * S ((mdr_ut_data_full_rankzeroevaluationdeterminanthsc) + (mdr_e_data_full_rankzeroevaluationdeterminanthscrc)) + ((mdr_e_data_full_rankzeroevaluationdeterminanthscrc) + (mdr_e_data_full_rankzeroevaluationdeterminanthscrc))) /\ ((mdr_z_data_full_rankzeroevaluationdeterminanthscr) = ((mdr_c_data_full_rankzeroevaluationdeterminanthscrc) + (mdr_f_data_full_rankzeroevaluationdeterminanthscrc)) * S ((mdr_c_data_full_rankzeroevaluationdeterminanthscrc) + (mdr_f_data_full_rankzeroevaluationdeterminanthscrc)) + ((mdr_f_data_full_rankzeroevaluationdeterminanthscrc) + (mdr_f_data_full_rankzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_data_full_rankzeroevaluationdeterminanthscrb. ff_h_mdr_data_full_rankzeroevaluationdeterminanthscrb + S (mdr_z_data_full_rankzeroevaluationdeterminanthscr) = S ((S (mdr_i_data_full_rankzeroevaluationdeterminanthsc)) * mdr_c_data_full_rankzeroevaluationdeterminant)) /\ exists ff_q_mdr_data_full_rankzeroevaluationdeterminanthscrb. mdr_b_data_full_rankzeroevaluationdeterminant = ff_q_mdr_data_full_rankzeroevaluationdeterminanthscrb * S ((S (mdr_i_data_full_rankzeroevaluationdeterminanthsc)) * mdr_c_data_full_rankzeroevaluationdeterminant) + (mdr_z_data_full_rankzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_positive) = ((mdr_q_data_full_rankzeroevaluationdeterminanths) * (mdr_q_data_full_rankzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_positive = (mdr_q_data_full_rankzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_positive) = (mdr_q_data_full_rankzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_positive) = (mdr_j_data_full_rankzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_data_full_rankzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_data_full_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_data_full_rankzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_data_full_rankzeroevaluationdeterminanth = ff_q_mdm_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_data_full_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_data_full_rankzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_positive)) * mdr_us_data_full_rankzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_target. mdr_up_data_full_rankzeroevaluationdeterminanthsc = ff_q_mdm_mdr_data_full_rankzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_positive)) * mdr_us_data_full_rankzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_negative) = ((mdr_q_data_full_rankzeroevaluationdeterminanths) * (mdr_q_data_full_rankzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_negative = (mdr_q_data_full_rankzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_negative) = (mdr_q_data_full_rankzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_negative) = (mdr_j_data_full_rankzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_data_full_rankzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_data_full_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_data_full_rankzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_data_full_rankzeroevaluationdeterminanth = ff_q_mdm_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_data_full_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_data_full_rankzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_negative)) * mdr_ut_data_full_rankzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_target. mdr_un_data_full_rankzeroevaluationdeterminanthsc = ff_q_mdm_mdr_data_full_rankzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_negative)) * mdr_ut_data_full_rankzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_data_full_rankzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_data_full_rankzeroevaluationdeterminanthscp. ff_h_mdr_data_full_rankzeroevaluationdeterminanthscp + S (mdr_p_data_full_rankzeroevaluationdeterminanthsc) = S ((S (mdr_j_data_full_rankzeroevaluationdeterminanthsc)) * mdr_ec_data_full_rankzeroevaluationdeterminanths)) /\ exists ff_q_mdr_data_full_rankzeroevaluationdeterminanthscp. mdr_eb_data_full_rankzeroevaluationdeterminanths = ff_q_mdr_data_full_rankzeroevaluationdeterminanthscp * S ((S (mdr_j_data_full_rankzeroevaluationdeterminanthsc)) * mdr_ec_data_full_rankzeroevaluationdeterminanths) + (mdr_p_data_full_rankzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_data_full_rankzeroevaluationdeterminanthscn. ff_h_mdr_data_full_rankzeroevaluationdeterminanthscn + S (mdr_n_data_full_rankzeroevaluationdeterminanthsc) = S ((S (mdr_j_data_full_rankzeroevaluationdeterminanthsc)) * mdr_fc_data_full_rankzeroevaluationdeterminanths)) /\ exists ff_q_mdr_data_full_rankzeroevaluationdeterminanthscn. mdr_fb_data_full_rankzeroevaluationdeterminanths = ff_q_mdr_data_full_rankzeroevaluationdeterminanthscn * S ((S (mdr_j_data_full_rankzeroevaluationdeterminanthsc)) * mdr_fc_data_full_rankzeroevaluationdeterminanths) + (mdr_n_data_full_rankzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_data_full_rankzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_data_full_rankzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_data_full_rankzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_data_full_rankzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_data_full_rankzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix)) * mdr_pc_data_full_rankzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_data_full_rankzeroevaluationdeterminanth = ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix)) * mdr_pc_data_full_rankzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix)) * mdr_nc_data_full_rankzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_an. mdr_nb_data_full_rankzeroevaluationdeterminanth = ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix)) * mdr_nc_data_full_rankzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix)) * mdr_ec_data_full_rankzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_data_full_rankzeroevaluationdeterminanths = ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix)) * mdr_ec_data_full_rankzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix)) * mdr_fc_data_full_rankzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_data_full_rankzeroevaluationdeterminanths = ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix)) * mdr_fc_data_full_rankzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_data_full_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_data_full_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_data_full_rankzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_data_full_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_data_full_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_data_full_rankzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_data_full_rankzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_data_full_rankzeroevaluationdeterminanth) = S ((S ((S (mdr_q_data_full_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_data_full_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive) + (mdr_p_data_full_rankzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive = (S (mdr_q_data_full_rankzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_data_full_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_data_full_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_data_full_rankzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_data_full_rankzeroevaluationdeterminanth) = S ((S ((S (mdr_q_data_full_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_data_full_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative) + (mdr_n_data_full_rankzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative = (S (mdr_q_data_full_rankzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_data_full_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_data_full_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_data_full_rankzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_data_full_rankzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_data_full_rankzeroevaluationdeterminanti. mdr_gap_data_full_rankzeroevaluationdeterminanti + S (mdr_i_data_full_rankzeroevaluationdeterminant) = (mdr_l_data_full_rankzeroevaluationdeterminant)) /\ (exists mdr_z_data_full_rankzeroevaluationdeterminantr. ((exists mdr_a_data_full_rankzeroevaluationdeterminantrc mdr_b_data_full_rankzeroevaluationdeterminantrc mdr_c_data_full_rankzeroevaluationdeterminantrc mdr_e_data_full_rankzeroevaluationdeterminantrc mdr_f_data_full_rankzeroevaluationdeterminantrc. ((mdr_a_data_full_rankzeroevaluationdeterminantrc = ((mdr_q_data_full_rank) + (mdr_ub_data_full_rankzeroevaluation)) * S ((mdr_q_data_full_rank) + (mdr_ub_data_full_rankzeroevaluation)) + ((mdr_ub_data_full_rankzeroevaluation) + (mdr_ub_data_full_rankzeroevaluation))) /\ ((mdr_b_data_full_rankzeroevaluationdeterminantrc = ((mdr_uc_data_full_rankzeroevaluation) + (mdr_vb_data_full_rankzeroevaluation)) * S ((mdr_uc_data_full_rankzeroevaluation) + (mdr_vb_data_full_rankzeroevaluation)) + ((mdr_vb_data_full_rankzeroevaluation) + (mdr_vb_data_full_rankzeroevaluation))) /\ ((mdr_c_data_full_rankzeroevaluationdeterminantrc = ((mdr_a_data_full_rankzeroevaluationdeterminantrc) + (mdr_b_data_full_rankzeroevaluationdeterminantrc)) * S ((mdr_a_data_full_rankzeroevaluationdeterminantrc) + (mdr_b_data_full_rankzeroevaluationdeterminantrc)) + ((mdr_b_data_full_rankzeroevaluationdeterminantrc) + (mdr_b_data_full_rankzeroevaluationdeterminantrc))) /\ ((mdr_e_data_full_rankzeroevaluationdeterminantrc = ((mdr_p_data_full_rankzero) + (mdr_n_data_full_rankzero)) * S ((mdr_p_data_full_rankzero) + (mdr_n_data_full_rankzero)) + ((mdr_n_data_full_rankzero) + (mdr_n_data_full_rankzero))) /\ ((mdr_f_data_full_rankzeroevaluationdeterminantrc = ((mdr_vc_data_full_rankzeroevaluation) + (mdr_e_data_full_rankzeroevaluationdeterminantrc)) * S ((mdr_vc_data_full_rankzeroevaluation) + (mdr_e_data_full_rankzeroevaluationdeterminantrc)) + ((mdr_e_data_full_rankzeroevaluationdeterminantrc) + (mdr_e_data_full_rankzeroevaluationdeterminantrc))) /\ ((mdr_z_data_full_rankzeroevaluationdeterminantr) = ((mdr_c_data_full_rankzeroevaluationdeterminantrc) + (mdr_f_data_full_rankzeroevaluationdeterminantrc)) * S ((mdr_c_data_full_rankzeroevaluationdeterminantrc) + (mdr_f_data_full_rankzeroevaluationdeterminantrc)) + ((mdr_f_data_full_rankzeroevaluationdeterminantrc) + (mdr_f_data_full_rankzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_data_full_rankzeroevaluationdeterminantrb. ff_h_mdr_data_full_rankzeroevaluationdeterminantrb + S (mdr_z_data_full_rankzeroevaluationdeterminantr) = S ((S (mdr_i_data_full_rankzeroevaluationdeterminant)) * mdr_c_data_full_rankzeroevaluationdeterminant)) /\ exists ff_q_mdr_data_full_rankzeroevaluationdeterminantrb. mdr_b_data_full_rankzeroevaluationdeterminant = ff_q_mdr_data_full_rankzeroevaluationdeterminantrb * S ((S (mdr_i_data_full_rankzeroevaluationdeterminant)) * mdr_c_data_full_rankzeroevaluationdeterminant) + (mdr_z_data_full_rankzeroevaluationdeterminantr)))))))))) -> mdr_p_data_full_rankzero = mdr_n_data_full_rankzero))))))