matrix_rank_selected_determinant_empty

Exact expanded first-order arithmetic statement

forall pb pc nb nc w rb rc cb cc. (exists mdr_ub_selected_empty mdr_uc_selected_empty mdr_vb_selected_empty mdr_vc_selected_empty. ((((forall mdr_i_selected_emptymatrixpositive. (exists mdr_gap_selected_emptymatrixpositivebound. mdr_gap_selected_emptymatrixpositivebound + S (mdr_i_selected_emptymatrixpositive) = ((0) * (0))) -> exists mdr_a_selected_emptymatrixpositive. (((exists mdr_r_selected_emptymatrixpositivepoint mdr_s_selected_emptymatrixpositivepoint mdr_u_selected_emptymatrixpositivepoint mdr_v_selected_emptymatrixpositivepoint. ((mdr_i_selected_emptymatrixpositive = (0) * mdr_r_selected_emptymatrixpositivepoint + mdr_s_selected_emptymatrixpositivepoint) /\ ((exists mdr_gap_selected_emptymatrixpositivepointcolumn. mdr_gap_selected_emptymatrixpositivepointcolumn + S (mdr_s_selected_emptymatrixpositivepoint) = (0)) /\ ((((exists ff_h_mdr_selected_emptymatrixpositivepointrow_index. ff_h_mdr_selected_emptymatrixpositivepointrow_index + S (mdr_u_selected_emptymatrixpositivepoint) = S ((S (mdr_r_selected_emptymatrixpositivepoint)) * rc)) /\ exists ff_q_mdr_selected_emptymatrixpositivepointrow_index. rb = ff_q_mdr_selected_emptymatrixpositivepointrow_index * S ((S (mdr_r_selected_emptymatrixpositivepoint)) * rc) + (mdr_u_selected_emptymatrixpositivepoint))) /\ ((((exists ff_h_mdr_selected_emptymatrixpositivepointcolumn_index. ff_h_mdr_selected_emptymatrixpositivepointcolumn_index + S (mdr_v_selected_emptymatrixpositivepoint) = S ((S (mdr_s_selected_emptymatrixpositivepoint)) * cc)) /\ exists ff_q_mdr_selected_emptymatrixpositivepointcolumn_index. cb = ff_q_mdr_selected_emptymatrixpositivepointcolumn_index * S ((S (mdr_s_selected_emptymatrixpositivepoint)) * cc) + (mdr_v_selected_emptymatrixpositivepoint))) /\ (((exists ff_h_mdr_selected_emptymatrixpositivepointsource. ff_h_mdr_selected_emptymatrixpositivepointsource + S (mdr_a_selected_emptymatrixpositive) = S ((S ((mdr_u_selected_emptymatrixpositivepoint) * (w) + (mdr_v_selected_emptymatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_selected_emptymatrixpositivepointsource. pb = ff_q_mdr_selected_emptymatrixpositivepointsource * S ((S ((mdr_u_selected_emptymatrixpositivepoint) * (w) + (mdr_v_selected_emptymatrixpositivepoint))) * pc) + (mdr_a_selected_emptymatrixpositive)))))))) /\ (((exists ff_h_mdr_selected_emptymatrixpositiveoutput. ff_h_mdr_selected_emptymatrixpositiveoutput + S (mdr_a_selected_emptymatrixpositive) = S ((S (mdr_i_selected_emptymatrixpositive)) * mdr_uc_selected_empty)) /\ exists ff_q_mdr_selected_emptymatrixpositiveoutput. mdr_ub_selected_empty = ff_q_mdr_selected_emptymatrixpositiveoutput * S ((S (mdr_i_selected_emptymatrixpositive)) * mdr_uc_selected_empty) + (mdr_a_selected_emptymatrixpositive)))))) /\ (forall mdr_i_selected_emptymatrixnegative. (exists mdr_gap_selected_emptymatrixnegativebound. mdr_gap_selected_emptymatrixnegativebound + S (mdr_i_selected_emptymatrixnegative) = ((0) * (0))) -> exists mdr_a_selected_emptymatrixnegative. (((exists mdr_r_selected_emptymatrixnegativepoint mdr_s_selected_emptymatrixnegativepoint mdr_u_selected_emptymatrixnegativepoint mdr_v_selected_emptymatrixnegativepoint. ((mdr_i_selected_emptymatrixnegative = (0) * mdr_r_selected_emptymatrixnegativepoint + mdr_s_selected_emptymatrixnegativepoint) /\ ((exists mdr_gap_selected_emptymatrixnegativepointcolumn. mdr_gap_selected_emptymatrixnegativepointcolumn + S (mdr_s_selected_emptymatrixnegativepoint) = (0)) /\ ((((exists ff_h_mdr_selected_emptymatrixnegativepointrow_index. ff_h_mdr_selected_emptymatrixnegativepointrow_index + S (mdr_u_selected_emptymatrixnegativepoint) = S ((S (mdr_r_selected_emptymatrixnegativepoint)) * rc)) /\ exists ff_q_mdr_selected_emptymatrixnegativepointrow_index. rb = ff_q_mdr_selected_emptymatrixnegativepointrow_index * S ((S (mdr_r_selected_emptymatrixnegativepoint)) * rc) + (mdr_u_selected_emptymatrixnegativepoint))) /\ ((((exists ff_h_mdr_selected_emptymatrixnegativepointcolumn_index. ff_h_mdr_selected_emptymatrixnegativepointcolumn_index + S (mdr_v_selected_emptymatrixnegativepoint) = S ((S (mdr_s_selected_emptymatrixnegativepoint)) * cc)) /\ exists ff_q_mdr_selected_emptymatrixnegativepointcolumn_index. cb = ff_q_mdr_selected_emptymatrixnegativepointcolumn_index * S ((S (mdr_s_selected_emptymatrixnegativepoint)) * cc) + (mdr_v_selected_emptymatrixnegativepoint))) /\ (((exists ff_h_mdr_selected_emptymatrixnegativepointsource. ff_h_mdr_selected_emptymatrixnegativepointsource + S (mdr_a_selected_emptymatrixnegative) = S ((S ((mdr_u_selected_emptymatrixnegativepoint) * (w) + (mdr_v_selected_emptymatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_selected_emptymatrixnegativepointsource. nb = ff_q_mdr_selected_emptymatrixnegativepointsource * S ((S ((mdr_u_selected_emptymatrixnegativepoint) * (w) + (mdr_v_selected_emptymatrixnegativepoint))) * nc) + (mdr_a_selected_emptymatrixnegative)))))))) /\ (((exists ff_h_mdr_selected_emptymatrixnegativeoutput. ff_h_mdr_selected_emptymatrixnegativeoutput + S (mdr_a_selected_emptymatrixnegative) = S ((S (mdr_i_selected_emptymatrixnegative)) * mdr_vc_selected_empty)) /\ exists ff_q_mdr_selected_emptymatrixnegativeoutput. mdr_vb_selected_empty = ff_q_mdr_selected_emptymatrixnegativeoutput * S ((S (mdr_i_selected_emptymatrixnegative)) * mdr_vc_selected_empty) + (mdr_a_selected_emptymatrixnegative)))))))) /\ (exists mdr_b_selected_emptydeterminant mdr_c_selected_emptydeterminant mdr_l_selected_emptydeterminant mdr_i_selected_emptydeterminant. ((forall mdr_i_selected_emptydeterminanth. (exists mdr_gap_selected_emptydeterminanthi. mdr_gap_selected_emptydeterminanthi + S (mdr_i_selected_emptydeterminanth) = (mdr_l_selected_emptydeterminant)) -> exists mdr_d_selected_emptydeterminanth mdr_pb_selected_emptydeterminanth mdr_pc_selected_emptydeterminanth mdr_nb_selected_emptydeterminanth mdr_nc_selected_emptydeterminanth mdr_p_selected_emptydeterminanth mdr_n_selected_emptydeterminanth. ((exists mdr_z_selected_emptydeterminanthr. ((exists mdr_a_selected_emptydeterminanthrc mdr_b_selected_emptydeterminanthrc mdr_c_selected_emptydeterminanthrc mdr_e_selected_emptydeterminanthrc mdr_f_selected_emptydeterminanthrc. ((mdr_a_selected_emptydeterminanthrc = ((mdr_d_selected_emptydeterminanth) + (mdr_pb_selected_emptydeterminanth)) * S ((mdr_d_selected_emptydeterminanth) + (mdr_pb_selected_emptydeterminanth)) + ((mdr_pb_selected_emptydeterminanth) + (mdr_pb_selected_emptydeterminanth))) /\ ((mdr_b_selected_emptydeterminanthrc = ((mdr_pc_selected_emptydeterminanth) + (mdr_nb_selected_emptydeterminanth)) * S ((mdr_pc_selected_emptydeterminanth) + (mdr_nb_selected_emptydeterminanth)) + ((mdr_nb_selected_emptydeterminanth) + (mdr_nb_selected_emptydeterminanth))) /\ ((mdr_c_selected_emptydeterminanthrc = ((mdr_a_selected_emptydeterminanthrc) + (mdr_b_selected_emptydeterminanthrc)) * S ((mdr_a_selected_emptydeterminanthrc) + (mdr_b_selected_emptydeterminanthrc)) + ((mdr_b_selected_emptydeterminanthrc) + (mdr_b_selected_emptydeterminanthrc))) /\ ((mdr_e_selected_emptydeterminanthrc = ((mdr_p_selected_emptydeterminanth) + (mdr_n_selected_emptydeterminanth)) * S ((mdr_p_selected_emptydeterminanth) + (mdr_n_selected_emptydeterminanth)) + ((mdr_n_selected_emptydeterminanth) + (mdr_n_selected_emptydeterminanth))) /\ ((mdr_f_selected_emptydeterminanthrc = ((mdr_nc_selected_emptydeterminanth) + (mdr_e_selected_emptydeterminanthrc)) * S ((mdr_nc_selected_emptydeterminanth) + (mdr_e_selected_emptydeterminanthrc)) + ((mdr_e_selected_emptydeterminanthrc) + (mdr_e_selected_emptydeterminanthrc))) /\ ((mdr_z_selected_emptydeterminanthr) = ((mdr_c_selected_emptydeterminanthrc) + (mdr_f_selected_emptydeterminanthrc)) * S ((mdr_c_selected_emptydeterminanthrc) + (mdr_f_selected_emptydeterminanthrc)) + ((mdr_f_selected_emptydeterminanthrc) + (mdr_f_selected_emptydeterminanthrc))))))))) /\ (((exists ff_h_mdr_selected_emptydeterminanthrb. ff_h_mdr_selected_emptydeterminanthrb + S (mdr_z_selected_emptydeterminanthr) = S ((S (mdr_i_selected_emptydeterminanth)) * mdr_c_selected_emptydeterminant)) /\ exists ff_q_mdr_selected_emptydeterminanthrb. mdr_b_selected_emptydeterminant = ff_q_mdr_selected_emptydeterminanthrb * S ((S (mdr_i_selected_emptydeterminanth)) * mdr_c_selected_emptydeterminant) + (mdr_z_selected_emptydeterminanthr))))) /\ (((((mdr_d_selected_emptydeterminanth) = 0) /\ (((mdr_p_selected_emptydeterminanth) = 1) /\ ((mdr_n_selected_emptydeterminanth) = 0))) \/ exists mdr_q_selected_emptydeterminanths mdr_eb_selected_emptydeterminanths mdr_ec_selected_emptydeterminanths mdr_fb_selected_emptydeterminanths mdr_fc_selected_emptydeterminanths. (((mdr_d_selected_emptydeterminanth) = S (mdr_q_selected_emptydeterminanths)) /\ ((forall mdr_j_selected_emptydeterminanthsc. (exists mdr_gap_selected_emptydeterminanthscj. mdr_gap_selected_emptydeterminanthscj + S (mdr_j_selected_emptydeterminanthsc) = (S (mdr_q_selected_emptydeterminanths))) -> exists mdr_i_selected_emptydeterminanthsc mdr_up_selected_emptydeterminanthsc mdr_us_selected_emptydeterminanthsc mdr_un_selected_emptydeterminanthsc mdr_ut_selected_emptydeterminanthsc mdr_p_selected_emptydeterminanthsc mdr_n_selected_emptydeterminanthsc. ((exists mdr_gap_selected_emptydeterminanthsci. mdr_gap_selected_emptydeterminanthsci + S (mdr_i_selected_emptydeterminanthsc) = (mdr_i_selected_emptydeterminanth)) /\ ((exists mdr_z_selected_emptydeterminanthscr. ((exists mdr_a_selected_emptydeterminanthscrc mdr_b_selected_emptydeterminanthscrc mdr_c_selected_emptydeterminanthscrc mdr_e_selected_emptydeterminanthscrc mdr_f_selected_emptydeterminanthscrc. ((mdr_a_selected_emptydeterminanthscrc = ((mdr_q_selected_emptydeterminanths) + (mdr_up_selected_emptydeterminanthsc)) * S ((mdr_q_selected_emptydeterminanths) + (mdr_up_selected_emptydeterminanthsc)) + ((mdr_up_selected_emptydeterminanthsc) + (mdr_up_selected_emptydeterminanthsc))) /\ ((mdr_b_selected_emptydeterminanthscrc = ((mdr_us_selected_emptydeterminanthsc) + (mdr_un_selected_emptydeterminanthsc)) * S ((mdr_us_selected_emptydeterminanthsc) + (mdr_un_selected_emptydeterminanthsc)) + ((mdr_un_selected_emptydeterminanthsc) + (mdr_un_selected_emptydeterminanthsc))) /\ ((mdr_c_selected_emptydeterminanthscrc = ((mdr_a_selected_emptydeterminanthscrc) + (mdr_b_selected_emptydeterminanthscrc)) * S ((mdr_a_selected_emptydeterminanthscrc) + (mdr_b_selected_emptydeterminanthscrc)) + ((mdr_b_selected_emptydeterminanthscrc) + (mdr_b_selected_emptydeterminanthscrc))) /\ ((mdr_e_selected_emptydeterminanthscrc = ((mdr_p_selected_emptydeterminanthsc) + (mdr_n_selected_emptydeterminanthsc)) * S ((mdr_p_selected_emptydeterminanthsc) + (mdr_n_selected_emptydeterminanthsc)) + ((mdr_n_selected_emptydeterminanthsc) + (mdr_n_selected_emptydeterminanthsc))) /\ ((mdr_f_selected_emptydeterminanthscrc = ((mdr_ut_selected_emptydeterminanthsc) + (mdr_e_selected_emptydeterminanthscrc)) * S ((mdr_ut_selected_emptydeterminanthsc) + (mdr_e_selected_emptydeterminanthscrc)) + ((mdr_e_selected_emptydeterminanthscrc) + (mdr_e_selected_emptydeterminanthscrc))) /\ ((mdr_z_selected_emptydeterminanthscr) = ((mdr_c_selected_emptydeterminanthscrc) + (mdr_f_selected_emptydeterminanthscrc)) * S ((mdr_c_selected_emptydeterminanthscrc) + (mdr_f_selected_emptydeterminanthscrc)) + ((mdr_f_selected_emptydeterminanthscrc) + (mdr_f_selected_emptydeterminanthscrc))))))))) /\ (((exists ff_h_mdr_selected_emptydeterminanthscrb. ff_h_mdr_selected_emptydeterminanthscrb + S (mdr_z_selected_emptydeterminanthscr) = S ((S (mdr_i_selected_emptydeterminanthsc)) * mdr_c_selected_emptydeterminant)) /\ exists ff_q_mdr_selected_emptydeterminanthscrb. mdr_b_selected_emptydeterminant = ff_q_mdr_selected_emptydeterminanthscrb * S ((S (mdr_i_selected_emptydeterminanthsc)) * mdr_c_selected_emptydeterminant) + (mdr_z_selected_emptydeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_selected_emptydeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_selected_emptydeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_selected_emptydeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_selected_emptydeterminanthscm_positive) = ((mdr_q_selected_emptydeterminanths) * (mdr_q_selected_emptydeterminanths))) -> exists ff_row_mdm_prefix_mdr_selected_emptydeterminanthscm_positive ff_column_mdm_prefix_mdr_selected_emptydeterminanthscm_positive ff_value_mdm_prefix_mdr_selected_emptydeterminanthscm_positive. (ff_index_mdm_prefix_mdr_selected_emptydeterminanthscm_positive = (mdr_q_selected_emptydeterminanths) * ff_row_mdm_prefix_mdr_selected_emptydeterminanthscm_positive + ff_column_mdm_prefix_mdr_selected_emptydeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_selected_emptydeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_selected_emptydeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_selected_emptydeterminanthscm_positive) = (mdr_q_selected_emptydeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_selected_emptydeterminanthscm_positive_cell ff_column_mdm_cell_mdr_selected_emptydeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_selected_emptydeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_selected_emptydeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_selected_emptydeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_selected_emptydeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_selected_emptydeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_selected_emptydeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_selected_emptydeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_selected_emptydeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_selected_emptydeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_selected_emptydeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_selected_emptydeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_selected_emptydeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_selected_emptydeterminanthscm_positive) = (mdr_j_selected_emptydeterminanthsc)) /\ ff_column_mdm_cell_mdr_selected_emptydeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_selected_emptydeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_selected_emptydeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_selected_emptydeterminanthscm_positive_cell_column_after + (mdr_j_selected_emptydeterminanthsc) = (ff_column_mdm_prefix_mdr_selected_emptydeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_selected_emptydeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_selected_emptydeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_selected_emptydeterminanthscm_positive_cell_source. ff_h_mdm_mdr_selected_emptydeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_selected_emptydeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_selected_emptydeterminanthscm_positive_cell) * (S (mdr_q_selected_emptydeterminanths)) + (ff_column_mdm_cell_mdr_selected_emptydeterminanthscm_positive_cell))) * mdr_pc_selected_emptydeterminanth)) /\ exists ff_q_mdm_mdr_selected_emptydeterminanthscm_positive_cell_source. mdr_pb_selected_emptydeterminanth = ff_q_mdm_mdr_selected_emptydeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_selected_emptydeterminanthscm_positive_cell) * (S (mdr_q_selected_emptydeterminanths)) + (ff_column_mdm_cell_mdr_selected_emptydeterminanthscm_positive_cell))) * mdr_pc_selected_emptydeterminanth) + (ff_value_mdm_prefix_mdr_selected_emptydeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_selected_emptydeterminanthscm_positive_target. ff_h_mdm_mdr_selected_emptydeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_selected_emptydeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_selected_emptydeterminanthscm_positive)) * mdr_us_selected_emptydeterminanthsc)) /\ exists ff_q_mdm_mdr_selected_emptydeterminanthscm_positive_target. mdr_up_selected_emptydeterminanthsc = ff_q_mdm_mdr_selected_emptydeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_selected_emptydeterminanthscm_positive)) * mdr_us_selected_emptydeterminanthsc) + (ff_value_mdm_prefix_mdr_selected_emptydeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_selected_emptydeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_selected_emptydeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_selected_emptydeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_selected_emptydeterminanthscm_negative) = ((mdr_q_selected_emptydeterminanths) * (mdr_q_selected_emptydeterminanths))) -> exists ff_row_mdm_prefix_mdr_selected_emptydeterminanthscm_negative ff_column_mdm_prefix_mdr_selected_emptydeterminanthscm_negative ff_value_mdm_prefix_mdr_selected_emptydeterminanthscm_negative. (ff_index_mdm_prefix_mdr_selected_emptydeterminanthscm_negative = (mdr_q_selected_emptydeterminanths) * ff_row_mdm_prefix_mdr_selected_emptydeterminanthscm_negative + ff_column_mdm_prefix_mdr_selected_emptydeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_selected_emptydeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_selected_emptydeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_selected_emptydeterminanthscm_negative) = (mdr_q_selected_emptydeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_selected_emptydeterminanthscm_negative_cell ff_column_mdm_cell_mdr_selected_emptydeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_selected_emptydeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_selected_emptydeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_selected_emptydeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_selected_emptydeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_selected_emptydeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_selected_emptydeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_selected_emptydeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_selected_emptydeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_selected_emptydeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_selected_emptydeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_selected_emptydeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_selected_emptydeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_selected_emptydeterminanthscm_negative) = (mdr_j_selected_emptydeterminanthsc)) /\ ff_column_mdm_cell_mdr_selected_emptydeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_selected_emptydeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_selected_emptydeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_selected_emptydeterminanthscm_negative_cell_column_after + (mdr_j_selected_emptydeterminanthsc) = (ff_column_mdm_prefix_mdr_selected_emptydeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_selected_emptydeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_selected_emptydeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_selected_emptydeterminanthscm_negative_cell_source. ff_h_mdm_mdr_selected_emptydeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_selected_emptydeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_selected_emptydeterminanthscm_negative_cell) * (S (mdr_q_selected_emptydeterminanths)) + (ff_column_mdm_cell_mdr_selected_emptydeterminanthscm_negative_cell))) * mdr_nc_selected_emptydeterminanth)) /\ exists ff_q_mdm_mdr_selected_emptydeterminanthscm_negative_cell_source. mdr_nb_selected_emptydeterminanth = ff_q_mdm_mdr_selected_emptydeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_selected_emptydeterminanthscm_negative_cell) * (S (mdr_q_selected_emptydeterminanths)) + (ff_column_mdm_cell_mdr_selected_emptydeterminanthscm_negative_cell))) * mdr_nc_selected_emptydeterminanth) + (ff_value_mdm_prefix_mdr_selected_emptydeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_selected_emptydeterminanthscm_negative_target. ff_h_mdm_mdr_selected_emptydeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_selected_emptydeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_selected_emptydeterminanthscm_negative)) * mdr_ut_selected_emptydeterminanthsc)) /\ exists ff_q_mdm_mdr_selected_emptydeterminanthscm_negative_target. mdr_un_selected_emptydeterminanthsc = ff_q_mdm_mdr_selected_emptydeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_selected_emptydeterminanthscm_negative)) * mdr_ut_selected_emptydeterminanthsc) + (ff_value_mdm_prefix_mdr_selected_emptydeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_selected_emptydeterminanthscp. ff_h_mdr_selected_emptydeterminanthscp + S (mdr_p_selected_emptydeterminanthsc) = S ((S (mdr_j_selected_emptydeterminanthsc)) * mdr_ec_selected_emptydeterminanths)) /\ exists ff_q_mdr_selected_emptydeterminanthscp. mdr_eb_selected_emptydeterminanths = ff_q_mdr_selected_emptydeterminanthscp * S ((S (mdr_j_selected_emptydeterminanthsc)) * mdr_ec_selected_emptydeterminanths) + (mdr_p_selected_emptydeterminanthsc))) /\ (((exists ff_h_mdr_selected_emptydeterminanthscn. ff_h_mdr_selected_emptydeterminanthscn + S (mdr_n_selected_emptydeterminanthsc) = S ((S (mdr_j_selected_emptydeterminanthsc)) * mdr_fc_selected_emptydeterminanths)) /\ exists ff_q_mdr_selected_emptydeterminanthscn. mdr_fb_selected_emptydeterminanths = ff_q_mdr_selected_emptydeterminanthscn * S ((S (mdr_j_selected_emptydeterminanthsc)) * mdr_fc_selected_emptydeterminanths) + (mdr_n_selected_emptydeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_selected_emptydeterminanthsf ff_uc_mce_fold_mdr_selected_emptydeterminanthsf ff_vb_mce_fold_mdr_selected_emptydeterminanthsf ff_vc_mce_fold_mdr_selected_emptydeterminanthsf. ((forall ff_index_mce_alternating_mdr_selected_emptydeterminanthsf_prefix. (exists ff_gap_mce_mdr_selected_emptydeterminanthsf_prefix_index. ff_gap_mce_mdr_selected_emptydeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_selected_emptydeterminanthsf_prefix) = (S (mdr_q_selected_emptydeterminanths))) -> exists ff_ap_mce_alternating_mdr_selected_emptydeterminanthsf_prefix ff_an_mce_alternating_mdr_selected_emptydeterminanthsf_prefix ff_bp_mce_alternating_mdr_selected_emptydeterminanthsf_prefix ff_bn_mce_alternating_mdr_selected_emptydeterminanthsf_prefix ff_p_mce_alternating_mdr_selected_emptydeterminanthsf_prefix ff_n_mce_alternating_mdr_selected_emptydeterminanthsf_prefix. ((((exists ff_h_mce_mdr_selected_emptydeterminanthsf_prefix_ap. ff_h_mce_mdr_selected_emptydeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_selected_emptydeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_emptydeterminanthsf_prefix)) * mdr_pc_selected_emptydeterminanth)) /\ exists ff_q_mce_mdr_selected_emptydeterminanthsf_prefix_ap. mdr_pb_selected_emptydeterminanth = ff_q_mce_mdr_selected_emptydeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_selected_emptydeterminanthsf_prefix)) * mdr_pc_selected_emptydeterminanth) + (ff_ap_mce_alternating_mdr_selected_emptydeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_emptydeterminanthsf_prefix_an. ff_h_mce_mdr_selected_emptydeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_selected_emptydeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_emptydeterminanthsf_prefix)) * mdr_nc_selected_emptydeterminanth)) /\ exists ff_q_mce_mdr_selected_emptydeterminanthsf_prefix_an. mdr_nb_selected_emptydeterminanth = ff_q_mce_mdr_selected_emptydeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_selected_emptydeterminanthsf_prefix)) * mdr_nc_selected_emptydeterminanth) + (ff_an_mce_alternating_mdr_selected_emptydeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_emptydeterminanthsf_prefix_bp. ff_h_mce_mdr_selected_emptydeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_selected_emptydeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_emptydeterminanthsf_prefix)) * mdr_ec_selected_emptydeterminanths)) /\ exists ff_q_mce_mdr_selected_emptydeterminanthsf_prefix_bp. mdr_eb_selected_emptydeterminanths = ff_q_mce_mdr_selected_emptydeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_selected_emptydeterminanthsf_prefix)) * mdr_ec_selected_emptydeterminanths) + (ff_bp_mce_alternating_mdr_selected_emptydeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_emptydeterminanthsf_prefix_bn. ff_h_mce_mdr_selected_emptydeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_selected_emptydeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_emptydeterminanthsf_prefix)) * mdr_fc_selected_emptydeterminanths)) /\ exists ff_q_mce_mdr_selected_emptydeterminanthsf_prefix_bn. mdr_fb_selected_emptydeterminanths = ff_q_mce_mdr_selected_emptydeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_selected_emptydeterminanthsf_prefix)) * mdr_fc_selected_emptydeterminanths) + (ff_bn_mce_alternating_mdr_selected_emptydeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_emptydeterminanthsf_prefix_positive. ff_h_mce_mdr_selected_emptydeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_selected_emptydeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_emptydeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_selected_emptydeterminanthsf)) /\ exists ff_q_mce_mdr_selected_emptydeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_selected_emptydeterminanthsf = ff_q_mce_mdr_selected_emptydeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_selected_emptydeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_selected_emptydeterminanthsf) + (ff_p_mce_alternating_mdr_selected_emptydeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_emptydeterminanthsf_prefix_negative. ff_h_mce_mdr_selected_emptydeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_selected_emptydeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_emptydeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_selected_emptydeterminanthsf)) /\ exists ff_q_mce_mdr_selected_emptydeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_selected_emptydeterminanthsf = ff_q_mce_mdr_selected_emptydeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_selected_emptydeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_selected_emptydeterminanthsf) + (ff_n_mce_alternating_mdr_selected_emptydeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_selected_emptydeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_selected_emptydeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_selected_emptydeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_selected_emptydeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_selected_emptydeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_selected_emptydeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_selected_emptydeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_selected_emptydeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_selected_emptydeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_selected_emptydeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_selected_emptydeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_selected_emptydeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_selected_emptydeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_selected_emptydeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_selected_emptydeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_selected_emptydeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_selected_emptydeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_selected_emptydeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_selected_emptydeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_selected_emptydeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_selected_emptydeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_selected_emptydeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_selected_emptydeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_selected_emptydeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_selected_emptydeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_selected_emptydeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_selected_emptydeterminanthsf_positive ff_v_mce_mdr_selected_emptydeterminanthsf_positive. ((((exists ff_h_mce_mdr_selected_emptydeterminanthsf_positive_start. ff_h_mce_mdr_selected_emptydeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_selected_emptydeterminanthsf_positive)) /\ exists ff_q_mce_mdr_selected_emptydeterminanthsf_positive_start. ff_u_mce_mdr_selected_emptydeterminanthsf_positive = ff_q_mce_mdr_selected_emptydeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_selected_emptydeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_selected_emptydeterminanthsf_positive_terminal. ff_h_mce_mdr_selected_emptydeterminanthsf_positive_terminal + S (mdr_p_selected_emptydeterminanth) = S ((S ((S (mdr_q_selected_emptydeterminanths)))) * ff_v_mce_mdr_selected_emptydeterminanthsf_positive)) /\ exists ff_q_mce_mdr_selected_emptydeterminanthsf_positive_terminal. ff_u_mce_mdr_selected_emptydeterminanthsf_positive = ff_q_mce_mdr_selected_emptydeterminanthsf_positive_terminal * S ((S ((S (mdr_q_selected_emptydeterminanths)))) * ff_v_mce_mdr_selected_emptydeterminanthsf_positive) + (mdr_p_selected_emptydeterminanth))) /\ forall ff_i_mce_mdr_selected_emptydeterminanthsf_positive. (exists ff_lt_mce_mdr_selected_emptydeterminanthsf_positive_bound. ff_lt_mce_mdr_selected_emptydeterminanthsf_positive_bound + S ff_i_mce_mdr_selected_emptydeterminanthsf_positive = (S (mdr_q_selected_emptydeterminanths))) -> exists ff_a_mce_mdr_selected_emptydeterminanthsf_positive ff_r_mce_mdr_selected_emptydeterminanthsf_positive ff_s_mce_mdr_selected_emptydeterminanthsf_positive. ((((exists ff_h_mce_mdr_selected_emptydeterminanthsf_positive_summand. ff_h_mce_mdr_selected_emptydeterminanthsf_positive_summand + S (ff_a_mce_mdr_selected_emptydeterminanthsf_positive) = S ((S (ff_i_mce_mdr_selected_emptydeterminanthsf_positive)) * ff_uc_mce_fold_mdr_selected_emptydeterminanthsf)) /\ exists ff_q_mce_mdr_selected_emptydeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_selected_emptydeterminanthsf = ff_q_mce_mdr_selected_emptydeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_selected_emptydeterminanthsf_positive)) * ff_uc_mce_fold_mdr_selected_emptydeterminanthsf) + (ff_a_mce_mdr_selected_emptydeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_selected_emptydeterminanthsf_positive_partial. ff_h_mce_mdr_selected_emptydeterminanthsf_positive_partial + S (ff_r_mce_mdr_selected_emptydeterminanthsf_positive) = S ((S (ff_i_mce_mdr_selected_emptydeterminanthsf_positive)) * ff_v_mce_mdr_selected_emptydeterminanthsf_positive)) /\ exists ff_q_mce_mdr_selected_emptydeterminanthsf_positive_partial. ff_u_mce_mdr_selected_emptydeterminanthsf_positive = ff_q_mce_mdr_selected_emptydeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_selected_emptydeterminanthsf_positive)) * ff_v_mce_mdr_selected_emptydeterminanthsf_positive) + (ff_r_mce_mdr_selected_emptydeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_selected_emptydeterminanthsf_positive_successor. ff_h_mce_mdr_selected_emptydeterminanthsf_positive_successor + S (ff_s_mce_mdr_selected_emptydeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_selected_emptydeterminanthsf_positive)) * ff_v_mce_mdr_selected_emptydeterminanthsf_positive)) /\ exists ff_q_mce_mdr_selected_emptydeterminanthsf_positive_successor. ff_u_mce_mdr_selected_emptydeterminanthsf_positive = ff_q_mce_mdr_selected_emptydeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_selected_emptydeterminanthsf_positive)) * ff_v_mce_mdr_selected_emptydeterminanthsf_positive) + (ff_s_mce_mdr_selected_emptydeterminanthsf_positive))) /\ ff_s_mce_mdr_selected_emptydeterminanthsf_positive = ff_r_mce_mdr_selected_emptydeterminanthsf_positive + ff_a_mce_mdr_selected_emptydeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_selected_emptydeterminanthsf_negative ff_v_mce_mdr_selected_emptydeterminanthsf_negative. ((((exists ff_h_mce_mdr_selected_emptydeterminanthsf_negative_start. ff_h_mce_mdr_selected_emptydeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_selected_emptydeterminanthsf_negative)) /\ exists ff_q_mce_mdr_selected_emptydeterminanthsf_negative_start. ff_u_mce_mdr_selected_emptydeterminanthsf_negative = ff_q_mce_mdr_selected_emptydeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_selected_emptydeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_selected_emptydeterminanthsf_negative_terminal. ff_h_mce_mdr_selected_emptydeterminanthsf_negative_terminal + S (mdr_n_selected_emptydeterminanth) = S ((S ((S (mdr_q_selected_emptydeterminanths)))) * ff_v_mce_mdr_selected_emptydeterminanthsf_negative)) /\ exists ff_q_mce_mdr_selected_emptydeterminanthsf_negative_terminal. ff_u_mce_mdr_selected_emptydeterminanthsf_negative = ff_q_mce_mdr_selected_emptydeterminanthsf_negative_terminal * S ((S ((S (mdr_q_selected_emptydeterminanths)))) * ff_v_mce_mdr_selected_emptydeterminanthsf_negative) + (mdr_n_selected_emptydeterminanth))) /\ forall ff_i_mce_mdr_selected_emptydeterminanthsf_negative. (exists ff_lt_mce_mdr_selected_emptydeterminanthsf_negative_bound. ff_lt_mce_mdr_selected_emptydeterminanthsf_negative_bound + S ff_i_mce_mdr_selected_emptydeterminanthsf_negative = (S (mdr_q_selected_emptydeterminanths))) -> exists ff_a_mce_mdr_selected_emptydeterminanthsf_negative ff_r_mce_mdr_selected_emptydeterminanthsf_negative ff_s_mce_mdr_selected_emptydeterminanthsf_negative. ((((exists ff_h_mce_mdr_selected_emptydeterminanthsf_negative_summand. ff_h_mce_mdr_selected_emptydeterminanthsf_negative_summand + S (ff_a_mce_mdr_selected_emptydeterminanthsf_negative) = S ((S (ff_i_mce_mdr_selected_emptydeterminanthsf_negative)) * ff_vc_mce_fold_mdr_selected_emptydeterminanthsf)) /\ exists ff_q_mce_mdr_selected_emptydeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_selected_emptydeterminanthsf = ff_q_mce_mdr_selected_emptydeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_selected_emptydeterminanthsf_negative)) * ff_vc_mce_fold_mdr_selected_emptydeterminanthsf) + (ff_a_mce_mdr_selected_emptydeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_selected_emptydeterminanthsf_negative_partial. ff_h_mce_mdr_selected_emptydeterminanthsf_negative_partial + S (ff_r_mce_mdr_selected_emptydeterminanthsf_negative) = S ((S (ff_i_mce_mdr_selected_emptydeterminanthsf_negative)) * ff_v_mce_mdr_selected_emptydeterminanthsf_negative)) /\ exists ff_q_mce_mdr_selected_emptydeterminanthsf_negative_partial. ff_u_mce_mdr_selected_emptydeterminanthsf_negative = ff_q_mce_mdr_selected_emptydeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_selected_emptydeterminanthsf_negative)) * ff_v_mce_mdr_selected_emptydeterminanthsf_negative) + (ff_r_mce_mdr_selected_emptydeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_selected_emptydeterminanthsf_negative_successor. ff_h_mce_mdr_selected_emptydeterminanthsf_negative_successor + S (ff_s_mce_mdr_selected_emptydeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_selected_emptydeterminanthsf_negative)) * ff_v_mce_mdr_selected_emptydeterminanthsf_negative)) /\ exists ff_q_mce_mdr_selected_emptydeterminanthsf_negative_successor. ff_u_mce_mdr_selected_emptydeterminanthsf_negative = ff_q_mce_mdr_selected_emptydeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_selected_emptydeterminanthsf_negative)) * ff_v_mce_mdr_selected_emptydeterminanthsf_negative) + (ff_s_mce_mdr_selected_emptydeterminanthsf_negative))) /\ ff_s_mce_mdr_selected_emptydeterminanthsf_negative = ff_r_mce_mdr_selected_emptydeterminanthsf_negative + ff_a_mce_mdr_selected_emptydeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_selected_emptydeterminanti. mdr_gap_selected_emptydeterminanti + S (mdr_i_selected_emptydeterminant) = (mdr_l_selected_emptydeterminant)) /\ (exists mdr_z_selected_emptydeterminantr. ((exists mdr_a_selected_emptydeterminantrc mdr_b_selected_emptydeterminantrc mdr_c_selected_emptydeterminantrc mdr_e_selected_emptydeterminantrc mdr_f_selected_emptydeterminantrc. ((mdr_a_selected_emptydeterminantrc = ((0) + (mdr_ub_selected_empty)) * S ((0) + (mdr_ub_selected_empty)) + ((mdr_ub_selected_empty) + (mdr_ub_selected_empty))) /\ ((mdr_b_selected_emptydeterminantrc = ((mdr_uc_selected_empty) + (mdr_vb_selected_empty)) * S ((mdr_uc_selected_empty) + (mdr_vb_selected_empty)) + ((mdr_vb_selected_empty) + (mdr_vb_selected_empty))) /\ ((mdr_c_selected_emptydeterminantrc = ((mdr_a_selected_emptydeterminantrc) + (mdr_b_selected_emptydeterminantrc)) * S ((mdr_a_selected_emptydeterminantrc) + (mdr_b_selected_emptydeterminantrc)) + ((mdr_b_selected_emptydeterminantrc) + (mdr_b_selected_emptydeterminantrc))) /\ ((mdr_e_selected_emptydeterminantrc = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((mdr_f_selected_emptydeterminantrc = ((mdr_vc_selected_empty) + (mdr_e_selected_emptydeterminantrc)) * S ((mdr_vc_selected_empty) + (mdr_e_selected_emptydeterminantrc)) + ((mdr_e_selected_emptydeterminantrc) + (mdr_e_selected_emptydeterminantrc))) /\ ((mdr_z_selected_emptydeterminantr) = ((mdr_c_selected_emptydeterminantrc) + (mdr_f_selected_emptydeterminantrc)) * S ((mdr_c_selected_emptydeterminantrc) + (mdr_f_selected_emptydeterminantrc)) + ((mdr_f_selected_emptydeterminantrc) + (mdr_f_selected_emptydeterminantrc))))))))) /\ (((exists ff_h_mdr_selected_emptydeterminantrb. ff_h_mdr_selected_emptydeterminantrb + S (mdr_z_selected_emptydeterminantr) = S ((S (mdr_i_selected_emptydeterminant)) * mdr_c_selected_emptydeterminant)) /\ exists ff_q_mdr_selected_emptydeterminantrb. mdr_b_selected_emptydeterminant = ff_q_mdr_selected_emptydeterminantrb * S ((S (mdr_i_selected_emptydeterminant)) * mdr_c_selected_emptydeterminant) + (mdr_z_selected_emptydeterminantr))))))))))