matrix_rank_selected_determinant_exists

forall pb pc nb nc w rb rc cb cc q. exists p n. (exists mdr_ub_selected_det_exists mdr_uc_selected_det_exists mdr_vb_selected_det_exists mdr_vc_selected_det_exists. ((((forall mdr_i_selected_det_existsmatrixpositive. (exists mdr_gap_selected_det_existsmatrixpositivebound. mdr_gap_selected_det_existsmatrixpositivebound + S (mdr_i_selected_det_existsmatrixpositive) = ((q) * (q))) -> exists mdr_a_selected_det_existsmatrixpositive. (((exists mdr_r_selected_det_existsmatrixpositivepoint mdr_s_selected_det_existsmatrixpositivepoint mdr_u_selected_det_existsmatrixpositivepoint mdr_v_selected_det_existsmatrixpositivepoint. ((mdr_i_selected_det_existsmatrixpositive = (q) * mdr_r_selected_det_existsmatrixpositivepoint + mdr_s_selected_det_existsmatrixpositivepoint) /\ ((exists mdr_gap_selected_det_existsmatrixpositivepointcolumn. mdr_gap_selected_det_existsmatrixpositivepointcolumn + S (mdr_s_selected_det_existsmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_selected_det_existsmatrixpositivepointrow_index. ff_h_mdr_selected_det_existsmatrixpositivepointrow_index + S (mdr_u_selected_det_existsmatrixpositivepoint) = S ((S (mdr_r_selected_det_existsmatrixpositivepoint)) * rc)) /\ exists ff_q_mdr_selected_det_existsmatrixpositivepointrow_index. rb = ff_q_mdr_selected_det_existsmatrixpositivepointrow_index * S ((S (mdr_r_selected_det_existsmatrixpositivepoint)) * rc) + (mdr_u_selected_det_existsmatrixpositivepoint))) /\ ((((exists ff_h_mdr_selected_det_existsmatrixpositivepointcolumn_index. ff_h_mdr_selected_det_existsmatrixpositivepointcolumn_index + S (mdr_v_selected_det_existsmatrixpositivepoint) = S ((S (mdr_s_selected_det_existsmatrixpositivepoint)) * cc)) /\ exists ff_q_mdr_selected_det_existsmatrixpositivepointcolumn_index. cb = ff_q_mdr_selected_det_existsmatrixpositivepointcolumn_index * S ((S (mdr_s_selected_det_existsmatrixpositivepoint)) * cc) + (mdr_v_selected_det_existsmatrixpositivepoint))) /\ (((exists ff_h_mdr_selected_det_existsmatrixpositivepointsource. ff_h_mdr_selected_det_existsmatrixpositivepointsource + S (mdr_a_selected_det_existsmatrixpositive) = S ((S ((mdr_u_selected_det_existsmatrixpositivepoint) * (w) + (mdr_v_selected_det_existsmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_selected_det_existsmatrixpositivepointsource. pb = ff_q_mdr_selected_det_existsmatrixpositivepointsource * S ((S ((mdr_u_selected_det_existsmatrixpositivepoint) * (w) + (mdr_v_selected_det_existsmatrixpositivepoint))) * pc) + (mdr_a_selected_det_existsmatrixpositive)))))))) /\ (((exists ff_h_mdr_selected_det_existsmatrixpositiveoutput. ff_h_mdr_selected_det_existsmatrixpositiveoutput + S (mdr_a_selected_det_existsmatrixpositive) = S ((S (mdr_i_selected_det_existsmatrixpositive)) * mdr_uc_selected_det_exists)) /\ exists ff_q_mdr_selected_det_existsmatrixpositiveoutput. mdr_ub_selected_det_exists = ff_q_mdr_selected_det_existsmatrixpositiveoutput * S ((S (mdr_i_selected_det_existsmatrixpositive)) * mdr_uc_selected_det_exists) + (mdr_a_selected_det_existsmatrixpositive)))))) /\ (forall mdr_i_selected_det_existsmatrixnegative. (exists mdr_gap_selected_det_existsmatrixnegativebound. mdr_gap_selected_det_existsmatrixnegativebound + S (mdr_i_selected_det_existsmatrixnegative) = ((q) * (q))) -> exists mdr_a_selected_det_existsmatrixnegative. (((exists mdr_r_selected_det_existsmatrixnegativepoint mdr_s_selected_det_existsmatrixnegativepoint mdr_u_selected_det_existsmatrixnegativepoint mdr_v_selected_det_existsmatrixnegativepoint. ((mdr_i_selected_det_existsmatrixnegative = (q) * mdr_r_selected_det_existsmatrixnegativepoint + mdr_s_selected_det_existsmatrixnegativepoint) /\ ((exists mdr_gap_selected_det_existsmatrixnegativepointcolumn. mdr_gap_selected_det_existsmatrixnegativepointcolumn + S (mdr_s_selected_det_existsmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_selected_det_existsmatrixnegativepointrow_index. ff_h_mdr_selected_det_existsmatrixnegativepointrow_index + S (mdr_u_selected_det_existsmatrixnegativepoint) = S ((S (mdr_r_selected_det_existsmatrixnegativepoint)) * rc)) /\ exists ff_q_mdr_selected_det_existsmatrixnegativepointrow_index. rb = ff_q_mdr_selected_det_existsmatrixnegativepointrow_index * S ((S (mdr_r_selected_det_existsmatrixnegativepoint)) * rc) + (mdr_u_selected_det_existsmatrixnegativepoint))) /\ ((((exists ff_h_mdr_selected_det_existsmatrixnegativepointcolumn_index. ff_h_mdr_selected_det_existsmatrixnegativepointcolumn_index + S (mdr_v_selected_det_existsmatrixnegativepoint) = S ((S (mdr_s_selected_det_existsmatrixnegativepoint)) * cc)) /\ exists ff_q_mdr_selected_det_existsmatrixnegativepointcolumn_index. cb = ff_q_mdr_selected_det_existsmatrixnegativepointcolumn_index * S ((S (mdr_s_selected_det_existsmatrixnegativepoint)) * cc) + (mdr_v_selected_det_existsmatrixnegativepoint))) /\ (((exists ff_h_mdr_selected_det_existsmatrixnegativepointsource. ff_h_mdr_selected_det_existsmatrixnegativepointsource + S (mdr_a_selected_det_existsmatrixnegative) = S ((S ((mdr_u_selected_det_existsmatrixnegativepoint) * (w) + (mdr_v_selected_det_existsmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_selected_det_existsmatrixnegativepointsource. nb = ff_q_mdr_selected_det_existsmatrixnegativepointsource * S ((S ((mdr_u_selected_det_existsmatrixnegativepoint) * (w) + (mdr_v_selected_det_existsmatrixnegativepoint))) * nc) + (mdr_a_selected_det_existsmatrixnegative)))))))) /\ (((exists ff_h_mdr_selected_det_existsmatrixnegativeoutput. ff_h_mdr_selected_det_existsmatrixnegativeoutput + S (mdr_a_selected_det_existsmatrixnegative) = S ((S (mdr_i_selected_det_existsmatrixnegative)) * mdr_vc_selected_det_exists)) /\ exists ff_q_mdr_selected_det_existsmatrixnegativeoutput. mdr_vb_selected_det_exists = ff_q_mdr_selected_det_existsmatrixnegativeoutput * S ((S (mdr_i_selected_det_existsmatrixnegative)) * mdr_vc_selected_det_exists) + (mdr_a_selected_det_existsmatrixnegative)))))))) /\ (exists mdr_b_selected_det_existsdeterminant mdr_c_selected_det_existsdeterminant mdr_l_selected_det_existsdeterminant mdr_i_selected_det_existsdeterminant. ((forall mdr_i_selected_det_existsdeterminanth. (exists mdr_gap_selected_det_existsdeterminanthi. mdr_gap_selected_det_existsdeterminanthi + S (mdr_i_selected_det_existsdeterminanth) = (mdr_l_selected_det_existsdeterminant)) -> exists mdr_d_selected_det_existsdeterminanth mdr_pb_selected_det_existsdeterminanth mdr_pc_selected_det_existsdeterminanth mdr_nb_selected_det_existsdeterminanth mdr_nc_selected_det_existsdeterminanth mdr_p_selected_det_existsdeterminanth mdr_n_selected_det_existsdeterminanth. ((exists mdr_z_selected_det_existsdeterminanthr. ((exists mdr_a_selected_det_existsdeterminanthrc mdr_b_selected_det_existsdeterminanthrc mdr_c_selected_det_existsdeterminanthrc mdr_e_selected_det_existsdeterminanthrc mdr_f_selected_det_existsdeterminanthrc. ((mdr_a_selected_det_existsdeterminanthrc = ((mdr_d_selected_det_existsdeterminanth) + (mdr_pb_selected_det_existsdeterminanth)) * S ((mdr_d_selected_det_existsdeterminanth) + (mdr_pb_selected_det_existsdeterminanth)) + ((mdr_pb_selected_det_existsdeterminanth) + (mdr_pb_selected_det_existsdeterminanth))) /\ ((mdr_b_selected_det_existsdeterminanthrc = ((mdr_pc_selected_det_existsdeterminanth) + (mdr_nb_selected_det_existsdeterminanth)) * S ((mdr_pc_selected_det_existsdeterminanth) + (mdr_nb_selected_det_existsdeterminanth)) + ((mdr_nb_selected_det_existsdeterminanth) + (mdr_nb_selected_det_existsdeterminanth))) /\ ((mdr_c_selected_det_existsdeterminanthrc = ((mdr_a_selected_det_existsdeterminanthrc) + (mdr_b_selected_det_existsdeterminanthrc)) * S ((mdr_a_selected_det_existsdeterminanthrc) + (mdr_b_selected_det_existsdeterminanthrc)) + ((mdr_b_selected_det_existsdeterminanthrc) + (mdr_b_selected_det_existsdeterminanthrc))) /\ ((mdr_e_selected_det_existsdeterminanthrc = ((mdr_p_selected_det_existsdeterminanth) + (mdr_n_selected_det_existsdeterminanth)) * S ((mdr_p_selected_det_existsdeterminanth) + (mdr_n_selected_det_existsdeterminanth)) + ((mdr_n_selected_det_existsdeterminanth) + (mdr_n_selected_det_existsdeterminanth))) /\ ((mdr_f_selected_det_existsdeterminanthrc = ((mdr_nc_selected_det_existsdeterminanth) + (mdr_e_selected_det_existsdeterminanthrc)) * S ((mdr_nc_selected_det_existsdeterminanth) + (mdr_e_selected_det_existsdeterminanthrc)) + ((mdr_e_selected_det_existsdeterminanthrc) + (mdr_e_selected_det_existsdeterminanthrc))) /\ ((mdr_z_selected_det_existsdeterminanthr) = ((mdr_c_selected_det_existsdeterminanthrc) + (mdr_f_selected_det_existsdeterminanthrc)) * S ((mdr_c_selected_det_existsdeterminanthrc) + (mdr_f_selected_det_existsdeterminanthrc)) + ((mdr_f_selected_det_existsdeterminanthrc) + (mdr_f_selected_det_existsdeterminanthrc))))))))) /\ (((exists ff_h_mdr_selected_det_existsdeterminanthrb. ff_h_mdr_selected_det_existsdeterminanthrb + S (mdr_z_selected_det_existsdeterminanthr) = S ((S (mdr_i_selected_det_existsdeterminanth)) * mdr_c_selected_det_existsdeterminant)) /\ exists ff_q_mdr_selected_det_existsdeterminanthrb. mdr_b_selected_det_existsdeterminant = ff_q_mdr_selected_det_existsdeterminanthrb * S ((S (mdr_i_selected_det_existsdeterminanth)) * mdr_c_selected_det_existsdeterminant) + (mdr_z_selected_det_existsdeterminanthr))))) /\ (((((mdr_d_selected_det_existsdeterminanth) = 0) /\ (((mdr_p_selected_det_existsdeterminanth) = 1) /\ ((mdr_n_selected_det_existsdeterminanth) = 0))) \/ exists mdr_q_selected_det_existsdeterminanths mdr_eb_selected_det_existsdeterminanths mdr_ec_selected_det_existsdeterminanths mdr_fb_selected_det_existsdeterminanths mdr_fc_selected_det_existsdeterminanths. (((mdr_d_selected_det_existsdeterminanth) = S (mdr_q_selected_det_existsdeterminanths)) /\ ((forall mdr_j_selected_det_existsdeterminanthsc. (exists mdr_gap_selected_det_existsdeterminanthscj. mdr_gap_selected_det_existsdeterminanthscj + S (mdr_j_selected_det_existsdeterminanthsc) = (S (mdr_q_selected_det_existsdeterminanths))) -> exists mdr_i_selected_det_existsdeterminanthsc mdr_up_selected_det_existsdeterminanthsc mdr_us_selected_det_existsdeterminanthsc mdr_un_selected_det_existsdeterminanthsc mdr_ut_selected_det_existsdeterminanthsc mdr_p_selected_det_existsdeterminanthsc mdr_n_selected_det_existsdeterminanthsc. ((exists mdr_gap_selected_det_existsdeterminanthsci. mdr_gap_selected_det_existsdeterminanthsci + S (mdr_i_selected_det_existsdeterminanthsc) = (mdr_i_selected_det_existsdeterminanth)) /\ ((exists mdr_z_selected_det_existsdeterminanthscr. ((exists mdr_a_selected_det_existsdeterminanthscrc mdr_b_selected_det_existsdeterminanthscrc mdr_c_selected_det_existsdeterminanthscrc mdr_e_selected_det_existsdeterminanthscrc mdr_f_selected_det_existsdeterminanthscrc. ((mdr_a_selected_det_existsdeterminanthscrc = ((mdr_q_selected_det_existsdeterminanths) + (mdr_up_selected_det_existsdeterminanthsc)) * S ((mdr_q_selected_det_existsdeterminanths) + (mdr_up_selected_det_existsdeterminanthsc)) + ((mdr_up_selected_det_existsdeterminanthsc) + (mdr_up_selected_det_existsdeterminanthsc))) /\ ((mdr_b_selected_det_existsdeterminanthscrc = ((mdr_us_selected_det_existsdeterminanthsc) + (mdr_un_selected_det_existsdeterminanthsc)) * S ((mdr_us_selected_det_existsdeterminanthsc) + (mdr_un_selected_det_existsdeterminanthsc)) + ((mdr_un_selected_det_existsdeterminanthsc) + (mdr_un_selected_det_existsdeterminanthsc))) /\ ((mdr_c_selected_det_existsdeterminanthscrc = ((mdr_a_selected_det_existsdeterminanthscrc) + (mdr_b_selected_det_existsdeterminanthscrc)) * S ((mdr_a_selected_det_existsdeterminanthscrc) + (mdr_b_selected_det_existsdeterminanthscrc)) + ((mdr_b_selected_det_existsdeterminanthscrc) + (mdr_b_selected_det_existsdeterminanthscrc))) /\ ((mdr_e_selected_det_existsdeterminanthscrc = ((mdr_p_selected_det_existsdeterminanthsc) + (mdr_n_selected_det_existsdeterminanthsc)) * S ((mdr_p_selected_det_existsdeterminanthsc) + (mdr_n_selected_det_existsdeterminanthsc)) + ((mdr_n_selected_det_existsdeterminanthsc) + (mdr_n_selected_det_existsdeterminanthsc))) /\ ((mdr_f_selected_det_existsdeterminanthscrc = ((mdr_ut_selected_det_existsdeterminanthsc) + (mdr_e_selected_det_existsdeterminanthscrc)) * S ((mdr_ut_selected_det_existsdeterminanthsc) + (mdr_e_selected_det_existsdeterminanthscrc)) + ((mdr_e_selected_det_existsdeterminanthscrc) + (mdr_e_selected_det_existsdeterminanthscrc))) /\ ((mdr_z_selected_det_existsdeterminanthscr) = ((mdr_c_selected_det_existsdeterminanthscrc) + (mdr_f_selected_det_existsdeterminanthscrc)) * S ((mdr_c_selected_det_existsdeterminanthscrc) + (mdr_f_selected_det_existsdeterminanthscrc)) + ((mdr_f_selected_det_existsdeterminanthscrc) + (mdr_f_selected_det_existsdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_selected_det_existsdeterminanthscrb. ff_h_mdr_selected_det_existsdeterminanthscrb + S (mdr_z_selected_det_existsdeterminanthscr) = S ((S (mdr_i_selected_det_existsdeterminanthsc)) * mdr_c_selected_det_existsdeterminant)) /\ exists ff_q_mdr_selected_det_existsdeterminanthscrb. mdr_b_selected_det_existsdeterminant = ff_q_mdr_selected_det_existsdeterminanthscrb * S ((S (mdr_i_selected_det_existsdeterminanthsc)) * mdr_c_selected_det_existsdeterminant) + (mdr_z_selected_det_existsdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_selected_det_existsdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_selected_det_existsdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_selected_det_existsdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_selected_det_existsdeterminanthscm_positive) = ((mdr_q_selected_det_existsdeterminanths) * (mdr_q_selected_det_existsdeterminanths))) -> exists ff_row_mdm_prefix_mdr_selected_det_existsdeterminanthscm_positive ff_column_mdm_prefix_mdr_selected_det_existsdeterminanthscm_positive ff_value_mdm_prefix_mdr_selected_det_existsdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_selected_det_existsdeterminanthscm_positive = (mdr_q_selected_det_existsdeterminanths) * ff_row_mdm_prefix_mdr_selected_det_existsdeterminanthscm_positive + ff_column_mdm_prefix_mdr_selected_det_existsdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_selected_det_existsdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_selected_det_existsdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_selected_det_existsdeterminanthscm_positive) = (mdr_q_selected_det_existsdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_selected_det_existsdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_selected_det_existsdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_selected_det_existsdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_selected_det_existsdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_selected_det_existsdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_selected_det_existsdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_selected_det_existsdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_selected_det_existsdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_selected_det_existsdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_selected_det_existsdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_selected_det_existsdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_selected_det_existsdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_selected_det_existsdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_selected_det_existsdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_selected_det_existsdeterminanthscm_positive) = (mdr_j_selected_det_existsdeterminanthsc)) /\ ff_column_mdm_cell_mdr_selected_det_existsdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_selected_det_existsdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_selected_det_existsdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_selected_det_existsdeterminanthscm_positive_cell_column_after + (mdr_j_selected_det_existsdeterminanthsc) = (ff_column_mdm_prefix_mdr_selected_det_existsdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_selected_det_existsdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_selected_det_existsdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_selected_det_existsdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_selected_det_existsdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_selected_det_existsdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_selected_det_existsdeterminanthscm_positive_cell) * (S (mdr_q_selected_det_existsdeterminanths)) + (ff_column_mdm_cell_mdr_selected_det_existsdeterminanthscm_positive_cell))) * mdr_pc_selected_det_existsdeterminanth)) /\ exists ff_q_mdm_mdr_selected_det_existsdeterminanthscm_positive_cell_source. mdr_pb_selected_det_existsdeterminanth = ff_q_mdm_mdr_selected_det_existsdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_selected_det_existsdeterminanthscm_positive_cell) * (S (mdr_q_selected_det_existsdeterminanths)) + (ff_column_mdm_cell_mdr_selected_det_existsdeterminanthscm_positive_cell))) * mdr_pc_selected_det_existsdeterminanth) + (ff_value_mdm_prefix_mdr_selected_det_existsdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_selected_det_existsdeterminanthscm_positive_target. ff_h_mdm_mdr_selected_det_existsdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_selected_det_existsdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_selected_det_existsdeterminanthscm_positive)) * mdr_us_selected_det_existsdeterminanthsc)) /\ exists ff_q_mdm_mdr_selected_det_existsdeterminanthscm_positive_target. mdr_up_selected_det_existsdeterminanthsc = ff_q_mdm_mdr_selected_det_existsdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_selected_det_existsdeterminanthscm_positive)) * mdr_us_selected_det_existsdeterminanthsc) + (ff_value_mdm_prefix_mdr_selected_det_existsdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_selected_det_existsdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_selected_det_existsdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_selected_det_existsdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_selected_det_existsdeterminanthscm_negative) = ((mdr_q_selected_det_existsdeterminanths) * (mdr_q_selected_det_existsdeterminanths))) -> exists ff_row_mdm_prefix_mdr_selected_det_existsdeterminanthscm_negative ff_column_mdm_prefix_mdr_selected_det_existsdeterminanthscm_negative ff_value_mdm_prefix_mdr_selected_det_existsdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_selected_det_existsdeterminanthscm_negative = (mdr_q_selected_det_existsdeterminanths) * ff_row_mdm_prefix_mdr_selected_det_existsdeterminanthscm_negative + ff_column_mdm_prefix_mdr_selected_det_existsdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_selected_det_existsdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_selected_det_existsdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_selected_det_existsdeterminanthscm_negative) = (mdr_q_selected_det_existsdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_selected_det_existsdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_selected_det_existsdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_selected_det_existsdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_selected_det_existsdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_selected_det_existsdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_selected_det_existsdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_selected_det_existsdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_selected_det_existsdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_selected_det_existsdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_selected_det_existsdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_selected_det_existsdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_selected_det_existsdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_selected_det_existsdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_selected_det_existsdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_selected_det_existsdeterminanthscm_negative) = (mdr_j_selected_det_existsdeterminanthsc)) /\ ff_column_mdm_cell_mdr_selected_det_existsdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_selected_det_existsdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_selected_det_existsdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_selected_det_existsdeterminanthscm_negative_cell_column_after + (mdr_j_selected_det_existsdeterminanthsc) = (ff_column_mdm_prefix_mdr_selected_det_existsdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_selected_det_existsdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_selected_det_existsdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_selected_det_existsdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_selected_det_existsdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_selected_det_existsdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_selected_det_existsdeterminanthscm_negative_cell) * (S (mdr_q_selected_det_existsdeterminanths)) + (ff_column_mdm_cell_mdr_selected_det_existsdeterminanthscm_negative_cell))) * mdr_nc_selected_det_existsdeterminanth)) /\ exists ff_q_mdm_mdr_selected_det_existsdeterminanthscm_negative_cell_source. mdr_nb_selected_det_existsdeterminanth = ff_q_mdm_mdr_selected_det_existsdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_selected_det_existsdeterminanthscm_negative_cell) * (S (mdr_q_selected_det_existsdeterminanths)) + (ff_column_mdm_cell_mdr_selected_det_existsdeterminanthscm_negative_cell))) * mdr_nc_selected_det_existsdeterminanth) + (ff_value_mdm_prefix_mdr_selected_det_existsdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_selected_det_existsdeterminanthscm_negative_target. ff_h_mdm_mdr_selected_det_existsdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_selected_det_existsdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_selected_det_existsdeterminanthscm_negative)) * mdr_ut_selected_det_existsdeterminanthsc)) /\ exists ff_q_mdm_mdr_selected_det_existsdeterminanthscm_negative_target. mdr_un_selected_det_existsdeterminanthsc = ff_q_mdm_mdr_selected_det_existsdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_selected_det_existsdeterminanthscm_negative)) * mdr_ut_selected_det_existsdeterminanthsc) + (ff_value_mdm_prefix_mdr_selected_det_existsdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_selected_det_existsdeterminanthscp. ff_h_mdr_selected_det_existsdeterminanthscp + S (mdr_p_selected_det_existsdeterminanthsc) = S ((S (mdr_j_selected_det_existsdeterminanthsc)) * mdr_ec_selected_det_existsdeterminanths)) /\ exists ff_q_mdr_selected_det_existsdeterminanthscp. mdr_eb_selected_det_existsdeterminanths = ff_q_mdr_selected_det_existsdeterminanthscp * S ((S (mdr_j_selected_det_existsdeterminanthsc)) * mdr_ec_selected_det_existsdeterminanths) + (mdr_p_selected_det_existsdeterminanthsc))) /\ (((exists ff_h_mdr_selected_det_existsdeterminanthscn. ff_h_mdr_selected_det_existsdeterminanthscn + S (mdr_n_selected_det_existsdeterminanthsc) = S ((S (mdr_j_selected_det_existsdeterminanthsc)) * mdr_fc_selected_det_existsdeterminanths)) /\ exists ff_q_mdr_selected_det_existsdeterminanthscn. mdr_fb_selected_det_existsdeterminanths = ff_q_mdr_selected_det_existsdeterminanthscn * S ((S (mdr_j_selected_det_existsdeterminanthsc)) * mdr_fc_selected_det_existsdeterminanths) + (mdr_n_selected_det_existsdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_selected_det_existsdeterminanthsf ff_uc_mce_fold_mdr_selected_det_existsdeterminanthsf ff_vb_mce_fold_mdr_selected_det_existsdeterminanthsf ff_vc_mce_fold_mdr_selected_det_existsdeterminanthsf. ((forall ff_index_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix. (exists ff_gap_mce_mdr_selected_det_existsdeterminanthsf_prefix_index. ff_gap_mce_mdr_selected_det_existsdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix) = (S (mdr_q_selected_det_existsdeterminanths))) -> exists ff_ap_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix ff_an_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix ff_bp_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix ff_bn_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix ff_p_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix ff_n_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_selected_det_existsdeterminanthsf_prefix_ap. ff_h_mce_mdr_selected_det_existsdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix)) * mdr_pc_selected_det_existsdeterminanth)) /\ exists ff_q_mce_mdr_selected_det_existsdeterminanthsf_prefix_ap. mdr_pb_selected_det_existsdeterminanth = ff_q_mce_mdr_selected_det_existsdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix)) * mdr_pc_selected_det_existsdeterminanth) + (ff_ap_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_det_existsdeterminanthsf_prefix_an. ff_h_mce_mdr_selected_det_existsdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix)) * mdr_nc_selected_det_existsdeterminanth)) /\ exists ff_q_mce_mdr_selected_det_existsdeterminanthsf_prefix_an. mdr_nb_selected_det_existsdeterminanth = ff_q_mce_mdr_selected_det_existsdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix)) * mdr_nc_selected_det_existsdeterminanth) + (ff_an_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_det_existsdeterminanthsf_prefix_bp. ff_h_mce_mdr_selected_det_existsdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix)) * mdr_ec_selected_det_existsdeterminanths)) /\ exists ff_q_mce_mdr_selected_det_existsdeterminanthsf_prefix_bp. mdr_eb_selected_det_existsdeterminanths = ff_q_mce_mdr_selected_det_existsdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix)) * mdr_ec_selected_det_existsdeterminanths) + (ff_bp_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_det_existsdeterminanthsf_prefix_bn. ff_h_mce_mdr_selected_det_existsdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix)) * mdr_fc_selected_det_existsdeterminanths)) /\ exists ff_q_mce_mdr_selected_det_existsdeterminanthsf_prefix_bn. mdr_fb_selected_det_existsdeterminanths = ff_q_mce_mdr_selected_det_existsdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix)) * mdr_fc_selected_det_existsdeterminanths) + (ff_bn_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_det_existsdeterminanthsf_prefix_positive. ff_h_mce_mdr_selected_det_existsdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_selected_det_existsdeterminanthsf)) /\ exists ff_q_mce_mdr_selected_det_existsdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_selected_det_existsdeterminanthsf = ff_q_mce_mdr_selected_det_existsdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_selected_det_existsdeterminanthsf) + (ff_p_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_det_existsdeterminanthsf_prefix_negative. ff_h_mce_mdr_selected_det_existsdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_selected_det_existsdeterminanthsf)) /\ exists ff_q_mce_mdr_selected_det_existsdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_selected_det_existsdeterminanthsf = ff_q_mce_mdr_selected_det_existsdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_selected_det_existsdeterminanthsf) + (ff_n_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_selected_det_existsdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_selected_det_existsdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_selected_det_existsdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_selected_det_existsdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_selected_det_existsdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_selected_det_existsdeterminanthsf_positive ff_v_mce_mdr_selected_det_existsdeterminanthsf_positive. ((((exists ff_h_mce_mdr_selected_det_existsdeterminanthsf_positive_start. ff_h_mce_mdr_selected_det_existsdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_selected_det_existsdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_selected_det_existsdeterminanthsf_positive_start. ff_u_mce_mdr_selected_det_existsdeterminanthsf_positive = ff_q_mce_mdr_selected_det_existsdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_selected_det_existsdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_selected_det_existsdeterminanthsf_positive_terminal. ff_h_mce_mdr_selected_det_existsdeterminanthsf_positive_terminal + S (mdr_p_selected_det_existsdeterminanth) = S ((S ((S (mdr_q_selected_det_existsdeterminanths)))) * ff_v_mce_mdr_selected_det_existsdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_selected_det_existsdeterminanthsf_positive_terminal. ff_u_mce_mdr_selected_det_existsdeterminanthsf_positive = ff_q_mce_mdr_selected_det_existsdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_selected_det_existsdeterminanths)))) * ff_v_mce_mdr_selected_det_existsdeterminanthsf_positive) + (mdr_p_selected_det_existsdeterminanth))) /\ forall ff_i_mce_mdr_selected_det_existsdeterminanthsf_positive. (exists ff_lt_mce_mdr_selected_det_existsdeterminanthsf_positive_bound. ff_lt_mce_mdr_selected_det_existsdeterminanthsf_positive_bound + S ff_i_mce_mdr_selected_det_existsdeterminanthsf_positive = (S (mdr_q_selected_det_existsdeterminanths))) -> exists ff_a_mce_mdr_selected_det_existsdeterminanthsf_positive ff_r_mce_mdr_selected_det_existsdeterminanthsf_positive ff_s_mce_mdr_selected_det_existsdeterminanthsf_positive. ((((exists ff_h_mce_mdr_selected_det_existsdeterminanthsf_positive_summand. ff_h_mce_mdr_selected_det_existsdeterminanthsf_positive_summand + S (ff_a_mce_mdr_selected_det_existsdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_selected_det_existsdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_selected_det_existsdeterminanthsf)) /\ exists ff_q_mce_mdr_selected_det_existsdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_selected_det_existsdeterminanthsf = ff_q_mce_mdr_selected_det_existsdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_selected_det_existsdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_selected_det_existsdeterminanthsf) + (ff_a_mce_mdr_selected_det_existsdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_selected_det_existsdeterminanthsf_positive_partial. ff_h_mce_mdr_selected_det_existsdeterminanthsf_positive_partial + S (ff_r_mce_mdr_selected_det_existsdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_selected_det_existsdeterminanthsf_positive)) * ff_v_mce_mdr_selected_det_existsdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_selected_det_existsdeterminanthsf_positive_partial. ff_u_mce_mdr_selected_det_existsdeterminanthsf_positive = ff_q_mce_mdr_selected_det_existsdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_selected_det_existsdeterminanthsf_positive)) * ff_v_mce_mdr_selected_det_existsdeterminanthsf_positive) + (ff_r_mce_mdr_selected_det_existsdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_selected_det_existsdeterminanthsf_positive_successor. ff_h_mce_mdr_selected_det_existsdeterminanthsf_positive_successor + S (ff_s_mce_mdr_selected_det_existsdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_selected_det_existsdeterminanthsf_positive)) * ff_v_mce_mdr_selected_det_existsdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_selected_det_existsdeterminanthsf_positive_successor. ff_u_mce_mdr_selected_det_existsdeterminanthsf_positive = ff_q_mce_mdr_selected_det_existsdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_selected_det_existsdeterminanthsf_positive)) * ff_v_mce_mdr_selected_det_existsdeterminanthsf_positive) + (ff_s_mce_mdr_selected_det_existsdeterminanthsf_positive))) /\ ff_s_mce_mdr_selected_det_existsdeterminanthsf_positive = ff_r_mce_mdr_selected_det_existsdeterminanthsf_positive + ff_a_mce_mdr_selected_det_existsdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_selected_det_existsdeterminanthsf_negative ff_v_mce_mdr_selected_det_existsdeterminanthsf_negative. ((((exists ff_h_mce_mdr_selected_det_existsdeterminanthsf_negative_start. ff_h_mce_mdr_selected_det_existsdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_selected_det_existsdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_selected_det_existsdeterminanthsf_negative_start. ff_u_mce_mdr_selected_det_existsdeterminanthsf_negative = ff_q_mce_mdr_selected_det_existsdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_selected_det_existsdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_selected_det_existsdeterminanthsf_negative_terminal. ff_h_mce_mdr_selected_det_existsdeterminanthsf_negative_terminal + S (mdr_n_selected_det_existsdeterminanth) = S ((S ((S (mdr_q_selected_det_existsdeterminanths)))) * ff_v_mce_mdr_selected_det_existsdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_selected_det_existsdeterminanthsf_negative_terminal. ff_u_mce_mdr_selected_det_existsdeterminanthsf_negative = ff_q_mce_mdr_selected_det_existsdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_selected_det_existsdeterminanths)))) * ff_v_mce_mdr_selected_det_existsdeterminanthsf_negative) + (mdr_n_selected_det_existsdeterminanth))) /\ forall ff_i_mce_mdr_selected_det_existsdeterminanthsf_negative. (exists ff_lt_mce_mdr_selected_det_existsdeterminanthsf_negative_bound. ff_lt_mce_mdr_selected_det_existsdeterminanthsf_negative_bound + S ff_i_mce_mdr_selected_det_existsdeterminanthsf_negative = (S (mdr_q_selected_det_existsdeterminanths))) -> exists ff_a_mce_mdr_selected_det_existsdeterminanthsf_negative ff_r_mce_mdr_selected_det_existsdeterminanthsf_negative ff_s_mce_mdr_selected_det_existsdeterminanthsf_negative. ((((exists ff_h_mce_mdr_selected_det_existsdeterminanthsf_negative_summand. ff_h_mce_mdr_selected_det_existsdeterminanthsf_negative_summand + S (ff_a_mce_mdr_selected_det_existsdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_selected_det_existsdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_selected_det_existsdeterminanthsf)) /\ exists ff_q_mce_mdr_selected_det_existsdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_selected_det_existsdeterminanthsf = ff_q_mce_mdr_selected_det_existsdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_selected_det_existsdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_selected_det_existsdeterminanthsf) + (ff_a_mce_mdr_selected_det_existsdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_selected_det_existsdeterminanthsf_negative_partial. ff_h_mce_mdr_selected_det_existsdeterminanthsf_negative_partial + S (ff_r_mce_mdr_selected_det_existsdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_selected_det_existsdeterminanthsf_negative)) * ff_v_mce_mdr_selected_det_existsdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_selected_det_existsdeterminanthsf_negative_partial. ff_u_mce_mdr_selected_det_existsdeterminanthsf_negative = ff_q_mce_mdr_selected_det_existsdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_selected_det_existsdeterminanthsf_negative)) * ff_v_mce_mdr_selected_det_existsdeterminanthsf_negative) + (ff_r_mce_mdr_selected_det_existsdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_selected_det_existsdeterminanthsf_negative_successor. ff_h_mce_mdr_selected_det_existsdeterminanthsf_negative_successor + S (ff_s_mce_mdr_selected_det_existsdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_selected_det_existsdeterminanthsf_negative)) * ff_v_mce_mdr_selected_det_existsdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_selected_det_existsdeterminanthsf_negative_successor. ff_u_mce_mdr_selected_det_existsdeterminanthsf_negative = ff_q_mce_mdr_selected_det_existsdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_selected_det_existsdeterminanthsf_negative)) * ff_v_mce_mdr_selected_det_existsdeterminanthsf_negative) + (ff_s_mce_mdr_selected_det_existsdeterminanthsf_negative))) /\ ff_s_mce_mdr_selected_det_existsdeterminanthsf_negative = ff_r_mce_mdr_selected_det_existsdeterminanthsf_negative + ff_a_mce_mdr_selected_det_existsdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_selected_det_existsdeterminanti. mdr_gap_selected_det_existsdeterminanti + S (mdr_i_selected_det_existsdeterminant) = (mdr_l_selected_det_existsdeterminant)) /\ (exists mdr_z_selected_det_existsdeterminantr. ((exists mdr_a_selected_det_existsdeterminantrc mdr_b_selected_det_existsdeterminantrc mdr_c_selected_det_existsdeterminantrc mdr_e_selected_det_existsdeterminantrc mdr_f_selected_det_existsdeterminantrc. ((mdr_a_selected_det_existsdeterminantrc = ((q) + (mdr_ub_selected_det_exists)) * S ((q) + (mdr_ub_selected_det_exists)) + ((mdr_ub_selected_det_exists) + (mdr_ub_selected_det_exists))) /\ ((mdr_b_selected_det_existsdeterminantrc = ((mdr_uc_selected_det_exists) + (mdr_vb_selected_det_exists)) * S ((mdr_uc_selected_det_exists) + (mdr_vb_selected_det_exists)) + ((mdr_vb_selected_det_exists) + (mdr_vb_selected_det_exists))) /\ ((mdr_c_selected_det_existsdeterminantrc = ((mdr_a_selected_det_existsdeterminantrc) + (mdr_b_selected_det_existsdeterminantrc)) * S ((mdr_a_selected_det_existsdeterminantrc) + (mdr_b_selected_det_existsdeterminantrc)) + ((mdr_b_selected_det_existsdeterminantrc) + (mdr_b_selected_det_existsdeterminantrc))) /\ ((mdr_e_selected_det_existsdeterminantrc = ((p) + (n)) * S ((p) + (n)) + ((n) + (n))) /\ ((mdr_f_selected_det_existsdeterminantrc = ((mdr_vc_selected_det_exists) + (mdr_e_selected_det_existsdeterminantrc)) * S ((mdr_vc_selected_det_exists) + (mdr_e_selected_det_existsdeterminantrc)) + ((mdr_e_selected_det_existsdeterminantrc) + (mdr_e_selected_det_existsdeterminantrc))) /\ ((mdr_z_selected_det_existsdeterminantr) = ((mdr_c_selected_det_existsdeterminantrc) + (mdr_f_selected_det_existsdeterminantrc)) * S ((mdr_c_selected_det_existsdeterminantrc) + (mdr_f_selected_det_existsdeterminantrc)) + ((mdr_f_selected_det_existsdeterminantrc) + (mdr_f_selected_det_existsdeterminantrc))))))))) /\ (((exists ff_h_mdr_selected_det_existsdeterminantrb. ff_h_mdr_selected_det_existsdeterminantrb + S (mdr_z_selected_det_existsdeterminantr) = S ((S (mdr_i_selected_det_existsdeterminant)) * mdr_c_selected_det_existsdeterminant)) /\ exists ff_q_mdr_selected_det_existsdeterminantrb. mdr_b_selected_det_existsdeterminant = ff_q_mdr_selected_det_existsdeterminantrb * S ((S (mdr_i_selected_det_existsdeterminant)) * mdr_c_selected_det_existsdeterminant) + (mdr_z_selected_det_existsdeterminantr))))))))))