matrix_rank_selected_box_search_decidable

forall pb pc nb nc r w q rc cc C L. (exists mdr_a_matrix_rank_selected_box_search_decidableyes. (((exists mdr_gap_matrix_rank_selected_box_search_decidableyesbound. mdr_gap_matrix_rank_selected_box_search_decidableyesbound + S (mdr_a_matrix_rank_selected_box_search_decidableyes) = (L)) /\ (exists mdr_a_row_candidatecolumns. (((exists mdr_gap_row_candidatecolumnsbound. mdr_gap_row_candidatecolumnsbound + S (mdr_a_row_candidatecolumns) = (C)) /\ (((((forall fom_index_mrf_row_candidateminorrowsbound. (exists fom_gap_mrf_row_candidateminorrowsbound_index_bound. fom_gap_mrf_row_candidateminorrowsbound_index_bound + S (fom_index_mrf_row_candidateminorrowsbound) = q) -> exists fom_value_mrf_row_candidateminorrowsbound. ((((exists fom_beta_height_mrf_row_candidateminorrowsbound_entry. fom_beta_height_mrf_row_candidateminorrowsbound_entry + S (fom_value_mrf_row_candidateminorrowsbound) = S ((S (fom_index_mrf_row_candidateminorrowsbound)) * rc)) /\ exists fom_beta_quotient_mrf_row_candidateminorrowsbound_entry. mdr_a_matrix_rank_selected_box_search_decidableyes = fom_beta_quotient_mrf_row_candidateminorrowsbound_entry * S ((S (fom_index_mrf_row_candidateminorrowsbound)) * rc) + (fom_value_mrf_row_candidateminorrowsbound))) /\ (exists fom_gap_mrf_row_candidateminorrowsbound_value_bound. fom_gap_mrf_row_candidateminorrowsbound_value_bound + S (fom_value_mrf_row_candidateminorrowsbound) = r))) /\ (forall mdr_i_row_candidateminorrowsdistinct mdr_j_row_candidateminorrowsdistinct mdr_a_row_candidateminorrowsdistinct. (exists mdr_gap_row_candidateminorrowsdistincti. mdr_gap_row_candidateminorrowsdistincti + S (mdr_i_row_candidateminorrowsdistinct) = (q)) -> (exists mdr_gap_row_candidateminorrowsdistinctj. mdr_gap_row_candidateminorrowsdistinctj + S (mdr_j_row_candidateminorrowsdistinct) = (q)) -> (((exists ff_h_mdr_row_candidateminorrowsdistinctfirst. ff_h_mdr_row_candidateminorrowsdistinctfirst + S (mdr_a_row_candidateminorrowsdistinct) = S ((S (mdr_i_row_candidateminorrowsdistinct)) * rc)) /\ exists ff_q_mdr_row_candidateminorrowsdistinctfirst. mdr_a_matrix_rank_selected_box_search_decidableyes = ff_q_mdr_row_candidateminorrowsdistinctfirst * S ((S (mdr_i_row_candidateminorrowsdistinct)) * rc) + (mdr_a_row_candidateminorrowsdistinct))) -> (((exists ff_h_mdr_row_candidateminorrowsdistinctsecond. ff_h_mdr_row_candidateminorrowsdistinctsecond + S (mdr_a_row_candidateminorrowsdistinct) = S ((S (mdr_j_row_candidateminorrowsdistinct)) * rc)) /\ exists ff_q_mdr_row_candidateminorrowsdistinctsecond. mdr_a_matrix_rank_selected_box_search_decidableyes = ff_q_mdr_row_candidateminorrowsdistinctsecond * S ((S (mdr_j_row_candidateminorrowsdistinct)) * rc) + (mdr_a_row_candidateminorrowsdistinct))) -> mdr_i_row_candidateminorrowsdistinct = mdr_j_row_candidateminorrowsdistinct))) /\ ((((forall fom_index_mrf_row_candidateminorcolumnsbound. (exists fom_gap_mrf_row_candidateminorcolumnsbound_index_bound. fom_gap_mrf_row_candidateminorcolumnsbound_index_bound + S (fom_index_mrf_row_candidateminorcolumnsbound) = q) -> exists fom_value_mrf_row_candidateminorcolumnsbound. ((((exists fom_beta_height_mrf_row_candidateminorcolumnsbound_entry. fom_beta_height_mrf_row_candidateminorcolumnsbound_entry + S (fom_value_mrf_row_candidateminorcolumnsbound) = S ((S (fom_index_mrf_row_candidateminorcolumnsbound)) * cc)) /\ exists fom_beta_quotient_mrf_row_candidateminorcolumnsbound_entry. mdr_a_row_candidatecolumns = fom_beta_quotient_mrf_row_candidateminorcolumnsbound_entry * S ((S (fom_index_mrf_row_candidateminorcolumnsbound)) * cc) + (fom_value_mrf_row_candidateminorcolumnsbound))) /\ (exists fom_gap_mrf_row_candidateminorcolumnsbound_value_bound. fom_gap_mrf_row_candidateminorcolumnsbound_value_bound + S (fom_value_mrf_row_candidateminorcolumnsbound) = w))) /\ (forall mdr_i_row_candidateminorcolumnsdistinct mdr_j_row_candidateminorcolumnsdistinct mdr_a_row_candidateminorcolumnsdistinct. (exists mdr_gap_row_candidateminorcolumnsdistincti. mdr_gap_row_candidateminorcolumnsdistincti + S (mdr_i_row_candidateminorcolumnsdistinct) = (q)) -> (exists mdr_gap_row_candidateminorcolumnsdistinctj. mdr_gap_row_candidateminorcolumnsdistinctj + S (mdr_j_row_candidateminorcolumnsdistinct) = (q)) -> (((exists ff_h_mdr_row_candidateminorcolumnsdistinctfirst. ff_h_mdr_row_candidateminorcolumnsdistinctfirst + S (mdr_a_row_candidateminorcolumnsdistinct) = S ((S (mdr_i_row_candidateminorcolumnsdistinct)) * cc)) /\ exists ff_q_mdr_row_candidateminorcolumnsdistinctfirst. mdr_a_row_candidatecolumns = ff_q_mdr_row_candidateminorcolumnsdistinctfirst * S ((S (mdr_i_row_candidateminorcolumnsdistinct)) * cc) + (mdr_a_row_candidateminorcolumnsdistinct))) -> (((exists ff_h_mdr_row_candidateminorcolumnsdistinctsecond. ff_h_mdr_row_candidateminorcolumnsdistinctsecond + S (mdr_a_row_candidateminorcolumnsdistinct) = S ((S (mdr_j_row_candidateminorcolumnsdistinct)) * cc)) /\ exists ff_q_mdr_row_candidateminorcolumnsdistinctsecond. mdr_a_row_candidatecolumns = ff_q_mdr_row_candidateminorcolumnsdistinctsecond * S ((S (mdr_j_row_candidateminorcolumnsdistinct)) * cc) + (mdr_a_row_candidateminorcolumnsdistinct))) -> mdr_i_row_candidateminorcolumnsdistinct = mdr_j_row_candidateminorcolumnsdistinct))) /\ (exists mdr_p_row_candidateminornonzero mdr_n_row_candidateminornonzero. ((exists mdr_ub_row_candidateminornonzeroevaluation mdr_uc_row_candidateminornonzeroevaluation mdr_vb_row_candidateminornonzeroevaluation mdr_vc_row_candidateminornonzeroevaluation. ((((forall mdr_i_row_candidateminornonzeroevaluationmatrixpositive. (exists mdr_gap_row_candidateminornonzeroevaluationmatrixpositivebound. mdr_gap_row_candidateminornonzeroevaluationmatrixpositivebound + S (mdr_i_row_candidateminornonzeroevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_row_candidateminornonzeroevaluationmatrixpositive. (((exists mdr_r_row_candidateminornonzeroevaluationmatrixpositivepoint mdr_s_row_candidateminornonzeroevaluationmatrixpositivepoint mdr_u_row_candidateminornonzeroevaluationmatrixpositivepoint mdr_v_row_candidateminornonzeroevaluationmatrixpositivepoint. ((mdr_i_row_candidateminornonzeroevaluationmatrixpositive = (q) * mdr_r_row_candidateminornonzeroevaluationmatrixpositivepoint + mdr_s_row_candidateminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_row_candidateminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_row_candidateminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_row_candidateminornonzeroevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_row_candidateminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_row_candidateminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_row_candidateminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_row_candidateminornonzeroevaluationmatrixpositivepoint)) * rc)) /\ exists ff_q_mdr_row_candidateminornonzeroevaluationmatrixpositivepointrow_index. mdr_a_matrix_rank_selected_box_search_decidableyes = ff_q_mdr_row_candidateminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_row_candidateminornonzeroevaluationmatrixpositivepoint)) * rc) + (mdr_u_row_candidateminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_row_candidateminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_row_candidateminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_row_candidateminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_row_candidateminornonzeroevaluationmatrixpositivepoint)) * cc)) /\ exists ff_q_mdr_row_candidateminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_a_row_candidatecolumns = ff_q_mdr_row_candidateminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_row_candidateminornonzeroevaluationmatrixpositivepoint)) * cc) + (mdr_v_row_candidateminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_row_candidateminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_row_candidateminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_row_candidateminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_row_candidateminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_row_candidateminornonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_row_candidateminornonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_row_candidateminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_row_candidateminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_row_candidateminornonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_row_candidateminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_row_candidateminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_row_candidateminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_row_candidateminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_row_candidateminornonzeroevaluationmatrixpositive)) * mdr_uc_row_candidateminornonzeroevaluation)) /\ exists ff_q_mdr_row_candidateminornonzeroevaluationmatrixpositiveoutput. mdr_ub_row_candidateminornonzeroevaluation = ff_q_mdr_row_candidateminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_row_candidateminornonzeroevaluationmatrixpositive)) * mdr_uc_row_candidateminornonzeroevaluation) + (mdr_a_row_candidateminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_row_candidateminornonzeroevaluationmatrixnegative. (exists mdr_gap_row_candidateminornonzeroevaluationmatrixnegativebound. mdr_gap_row_candidateminornonzeroevaluationmatrixnegativebound + S (mdr_i_row_candidateminornonzeroevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_row_candidateminornonzeroevaluationmatrixnegative. (((exists mdr_r_row_candidateminornonzeroevaluationmatrixnegativepoint mdr_s_row_candidateminornonzeroevaluationmatrixnegativepoint mdr_u_row_candidateminornonzeroevaluationmatrixnegativepoint mdr_v_row_candidateminornonzeroevaluationmatrixnegativepoint. ((mdr_i_row_candidateminornonzeroevaluationmatrixnegative = (q) * mdr_r_row_candidateminornonzeroevaluationmatrixnegativepoint + mdr_s_row_candidateminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_row_candidateminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_row_candidateminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_row_candidateminornonzeroevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_row_candidateminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_row_candidateminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_row_candidateminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_row_candidateminornonzeroevaluationmatrixnegativepoint)) * rc)) /\ exists ff_q_mdr_row_candidateminornonzeroevaluationmatrixnegativepointrow_index. mdr_a_matrix_rank_selected_box_search_decidableyes = ff_q_mdr_row_candidateminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_row_candidateminornonzeroevaluationmatrixnegativepoint)) * rc) + (mdr_u_row_candidateminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_row_candidateminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_row_candidateminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_row_candidateminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_row_candidateminornonzeroevaluationmatrixnegativepoint)) * cc)) /\ exists ff_q_mdr_row_candidateminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_a_row_candidatecolumns = ff_q_mdr_row_candidateminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_row_candidateminornonzeroevaluationmatrixnegativepoint)) * cc) + (mdr_v_row_candidateminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_row_candidateminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_row_candidateminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_row_candidateminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_row_candidateminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_row_candidateminornonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_row_candidateminornonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_row_candidateminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_row_candidateminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_row_candidateminornonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_row_candidateminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_row_candidateminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_row_candidateminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_row_candidateminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_row_candidateminornonzeroevaluationmatrixnegative)) * mdr_vc_row_candidateminornonzeroevaluation)) /\ exists ff_q_mdr_row_candidateminornonzeroevaluationmatrixnegativeoutput. mdr_vb_row_candidateminornonzeroevaluation = ff_q_mdr_row_candidateminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_row_candidateminornonzeroevaluationmatrixnegative)) * mdr_vc_row_candidateminornonzeroevaluation) + (mdr_a_row_candidateminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_row_candidateminornonzeroevaluationdeterminant mdr_c_row_candidateminornonzeroevaluationdeterminant mdr_l_row_candidateminornonzeroevaluationdeterminant mdr_i_row_candidateminornonzeroevaluationdeterminant. ((forall mdr_i_row_candidateminornonzeroevaluationdeterminanth. (exists mdr_gap_row_candidateminornonzeroevaluationdeterminanthi. mdr_gap_row_candidateminornonzeroevaluationdeterminanthi + S (mdr_i_row_candidateminornonzeroevaluationdeterminanth) = (mdr_l_row_candidateminornonzeroevaluationdeterminant)) -> exists mdr_d_row_candidateminornonzeroevaluationdeterminanth mdr_pb_row_candidateminornonzeroevaluationdeterminanth mdr_pc_row_candidateminornonzeroevaluationdeterminanth mdr_nb_row_candidateminornonzeroevaluationdeterminanth mdr_nc_row_candidateminornonzeroevaluationdeterminanth mdr_p_row_candidateminornonzeroevaluationdeterminanth mdr_n_row_candidateminornonzeroevaluationdeterminanth. ((exists mdr_z_row_candidateminornonzeroevaluationdeterminanthr. ((exists mdr_a_row_candidateminornonzeroevaluationdeterminanthrc mdr_b_row_candidateminornonzeroevaluationdeterminanthrc mdr_c_row_candidateminornonzeroevaluationdeterminanthrc mdr_e_row_candidateminornonzeroevaluationdeterminanthrc mdr_f_row_candidateminornonzeroevaluationdeterminanthrc. ((mdr_a_row_candidateminornonzeroevaluationdeterminanthrc = ((mdr_d_row_candidateminornonzeroevaluationdeterminanth) + (mdr_pb_row_candidateminornonzeroevaluationdeterminanth)) * S ((mdr_d_row_candidateminornonzeroevaluationdeterminanth) + (mdr_pb_row_candidateminornonzeroevaluationdeterminanth)) + ((mdr_pb_row_candidateminornonzeroevaluationdeterminanth) + (mdr_pb_row_candidateminornonzeroevaluationdeterminanth))) /\ ((mdr_b_row_candidateminornonzeroevaluationdeterminanthrc = ((mdr_pc_row_candidateminornonzeroevaluationdeterminanth) + (mdr_nb_row_candidateminornonzeroevaluationdeterminanth)) * S ((mdr_pc_row_candidateminornonzeroevaluationdeterminanth) + (mdr_nb_row_candidateminornonzeroevaluationdeterminanth)) + ((mdr_nb_row_candidateminornonzeroevaluationdeterminanth) + (mdr_nb_row_candidateminornonzeroevaluationdeterminanth))) /\ ((mdr_c_row_candidateminornonzeroevaluationdeterminanthrc = ((mdr_a_row_candidateminornonzeroevaluationdeterminanthrc) + (mdr_b_row_candidateminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_row_candidateminornonzeroevaluationdeterminanthrc) + (mdr_b_row_candidateminornonzeroevaluationdeterminanthrc)) + ((mdr_b_row_candidateminornonzeroevaluationdeterminanthrc) + (mdr_b_row_candidateminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_row_candidateminornonzeroevaluationdeterminanthrc = ((mdr_p_row_candidateminornonzeroevaluationdeterminanth) + (mdr_n_row_candidateminornonzeroevaluationdeterminanth)) * S ((mdr_p_row_candidateminornonzeroevaluationdeterminanth) + (mdr_n_row_candidateminornonzeroevaluationdeterminanth)) + ((mdr_n_row_candidateminornonzeroevaluationdeterminanth) + (mdr_n_row_candidateminornonzeroevaluationdeterminanth))) /\ ((mdr_f_row_candidateminornonzeroevaluationdeterminanthrc = ((mdr_nc_row_candidateminornonzeroevaluationdeterminanth) + (mdr_e_row_candidateminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_row_candidateminornonzeroevaluationdeterminanth) + (mdr_e_row_candidateminornonzeroevaluationdeterminanthrc)) + ((mdr_e_row_candidateminornonzeroevaluationdeterminanthrc) + (mdr_e_row_candidateminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_row_candidateminornonzeroevaluationdeterminanthr) = ((mdr_c_row_candidateminornonzeroevaluationdeterminanthrc) + (mdr_f_row_candidateminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_row_candidateminornonzeroevaluationdeterminanthrc) + (mdr_f_row_candidateminornonzeroevaluationdeterminanthrc)) + ((mdr_f_row_candidateminornonzeroevaluationdeterminanthrc) + (mdr_f_row_candidateminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_row_candidateminornonzeroevaluationdeterminanthrb. ff_h_mdr_row_candidateminornonzeroevaluationdeterminanthrb + S (mdr_z_row_candidateminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_row_candidateminornonzeroevaluationdeterminanth)) * mdr_c_row_candidateminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_row_candidateminornonzeroevaluationdeterminanthrb. mdr_b_row_candidateminornonzeroevaluationdeterminant = ff_q_mdr_row_candidateminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_row_candidateminornonzeroevaluationdeterminanth)) * mdr_c_row_candidateminornonzeroevaluationdeterminant) + (mdr_z_row_candidateminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_row_candidateminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_row_candidateminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_row_candidateminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_row_candidateminornonzeroevaluationdeterminanths mdr_eb_row_candidateminornonzeroevaluationdeterminanths mdr_ec_row_candidateminornonzeroevaluationdeterminanths mdr_fb_row_candidateminornonzeroevaluationdeterminanths mdr_fc_row_candidateminornonzeroevaluationdeterminanths. (((mdr_d_row_candidateminornonzeroevaluationdeterminanth) = S (mdr_q_row_candidateminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_row_candidateminornonzeroevaluationdeterminanthsc. (exists mdr_gap_row_candidateminornonzeroevaluationdeterminanthscj. mdr_gap_row_candidateminornonzeroevaluationdeterminanthscj + S (mdr_j_row_candidateminornonzeroevaluationdeterminanthsc) = (S (mdr_q_row_candidateminornonzeroevaluationdeterminanths))) -> exists mdr_i_row_candidateminornonzeroevaluationdeterminanthsc mdr_up_row_candidateminornonzeroevaluationdeterminanthsc mdr_us_row_candidateminornonzeroevaluationdeterminanthsc mdr_un_row_candidateminornonzeroevaluationdeterminanthsc mdr_ut_row_candidateminornonzeroevaluationdeterminanthsc mdr_p_row_candidateminornonzeroevaluationdeterminanthsc mdr_n_row_candidateminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_row_candidateminornonzeroevaluationdeterminanthsci. mdr_gap_row_candidateminornonzeroevaluationdeterminanthsci + S (mdr_i_row_candidateminornonzeroevaluationdeterminanthsc) = (mdr_i_row_candidateminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_row_candidateminornonzeroevaluationdeterminanthscr. ((exists mdr_a_row_candidateminornonzeroevaluationdeterminanthscrc mdr_b_row_candidateminornonzeroevaluationdeterminanthscrc mdr_c_row_candidateminornonzeroevaluationdeterminanthscrc mdr_e_row_candidateminornonzeroevaluationdeterminanthscrc mdr_f_row_candidateminornonzeroevaluationdeterminanthscrc. ((mdr_a_row_candidateminornonzeroevaluationdeterminanthscrc = ((mdr_q_row_candidateminornonzeroevaluationdeterminanths) + (mdr_up_row_candidateminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_row_candidateminornonzeroevaluationdeterminanths) + (mdr_up_row_candidateminornonzeroevaluationdeterminanthsc)) + ((mdr_up_row_candidateminornonzeroevaluationdeterminanthsc) + (mdr_up_row_candidateminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_row_candidateminornonzeroevaluationdeterminanthscrc = ((mdr_us_row_candidateminornonzeroevaluationdeterminanthsc) + (mdr_un_row_candidateminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_row_candidateminornonzeroevaluationdeterminanthsc) + (mdr_un_row_candidateminornonzeroevaluationdeterminanthsc)) + ((mdr_un_row_candidateminornonzeroevaluationdeterminanthsc) + (mdr_un_row_candidateminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_row_candidateminornonzeroevaluationdeterminanthscrc = ((mdr_a_row_candidateminornonzeroevaluationdeterminanthscrc) + (mdr_b_row_candidateminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_row_candidateminornonzeroevaluationdeterminanthscrc) + (mdr_b_row_candidateminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_row_candidateminornonzeroevaluationdeterminanthscrc) + (mdr_b_row_candidateminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_row_candidateminornonzeroevaluationdeterminanthscrc = ((mdr_p_row_candidateminornonzeroevaluationdeterminanthsc) + (mdr_n_row_candidateminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_row_candidateminornonzeroevaluationdeterminanthsc) + (mdr_n_row_candidateminornonzeroevaluationdeterminanthsc)) + ((mdr_n_row_candidateminornonzeroevaluationdeterminanthsc) + (mdr_n_row_candidateminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_row_candidateminornonzeroevaluationdeterminanthscrc = ((mdr_ut_row_candidateminornonzeroevaluationdeterminanthsc) + (mdr_e_row_candidateminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_row_candidateminornonzeroevaluationdeterminanthsc) + (mdr_e_row_candidateminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_row_candidateminornonzeroevaluationdeterminanthscrc) + (mdr_e_row_candidateminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_row_candidateminornonzeroevaluationdeterminanthscr) = ((mdr_c_row_candidateminornonzeroevaluationdeterminanthscrc) + (mdr_f_row_candidateminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_row_candidateminornonzeroevaluationdeterminanthscrc) + (mdr_f_row_candidateminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_row_candidateminornonzeroevaluationdeterminanthscrc) + (mdr_f_row_candidateminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_row_candidateminornonzeroevaluationdeterminanthscrb. ff_h_mdr_row_candidateminornonzeroevaluationdeterminanthscrb + S (mdr_z_row_candidateminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_row_candidateminornonzeroevaluationdeterminanthsc)) * mdr_c_row_candidateminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_row_candidateminornonzeroevaluationdeterminanthscrb. mdr_b_row_candidateminornonzeroevaluationdeterminant = ff_q_mdr_row_candidateminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_row_candidateminornonzeroevaluationdeterminanthsc)) * mdr_c_row_candidateminornonzeroevaluationdeterminant) + (mdr_z_row_candidateminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_row_candidateminornonzeroevaluationdeterminanths) * (mdr_q_row_candidateminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive = (mdr_q_row_candidateminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_row_candidateminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_row_candidateminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_row_candidateminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_row_candidateminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_row_candidateminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_row_candidateminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_row_candidateminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_row_candidateminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_row_candidateminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_row_candidateminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_row_candidateminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_row_candidateminornonzeroevaluationdeterminanths) * (mdr_q_row_candidateminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative = (mdr_q_row_candidateminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_row_candidateminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_row_candidateminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_row_candidateminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_row_candidateminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_row_candidateminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_row_candidateminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_row_candidateminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_row_candidateminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_row_candidateminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_row_candidateminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_row_candidateminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_row_candidateminornonzeroevaluationdeterminanthscp. ff_h_mdr_row_candidateminornonzeroevaluationdeterminanthscp + S (mdr_p_row_candidateminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_row_candidateminornonzeroevaluationdeterminanthsc)) * mdr_ec_row_candidateminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_row_candidateminornonzeroevaluationdeterminanthscp. mdr_eb_row_candidateminornonzeroevaluationdeterminanths = ff_q_mdr_row_candidateminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_row_candidateminornonzeroevaluationdeterminanthsc)) * mdr_ec_row_candidateminornonzeroevaluationdeterminanths) + (mdr_p_row_candidateminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_row_candidateminornonzeroevaluationdeterminanthscn. ff_h_mdr_row_candidateminornonzeroevaluationdeterminanthscn + S (mdr_n_row_candidateminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_row_candidateminornonzeroevaluationdeterminanthsc)) * mdr_fc_row_candidateminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_row_candidateminornonzeroevaluationdeterminanthscn. mdr_fb_row_candidateminornonzeroevaluationdeterminanths = ff_q_mdr_row_candidateminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_row_candidateminornonzeroevaluationdeterminanthsc)) * mdr_fc_row_candidateminornonzeroevaluationdeterminanths) + (mdr_n_row_candidateminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_row_candidateminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_row_candidateminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_row_candidateminornonzeroevaluationdeterminanth = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_row_candidateminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_row_candidateminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_row_candidateminornonzeroevaluationdeterminanth = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_row_candidateminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_row_candidateminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_row_candidateminornonzeroevaluationdeterminanths = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_row_candidateminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_row_candidateminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_row_candidateminornonzeroevaluationdeterminanths = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_row_candidateminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_row_candidateminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_row_candidateminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_row_candidateminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_row_candidateminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_row_candidateminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_row_candidateminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_row_candidateminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_row_candidateminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_row_candidateminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_row_candidateminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_row_candidateminornonzeroevaluationdeterminanti. mdr_gap_row_candidateminornonzeroevaluationdeterminanti + S (mdr_i_row_candidateminornonzeroevaluationdeterminant) = (mdr_l_row_candidateminornonzeroevaluationdeterminant)) /\ (exists mdr_z_row_candidateminornonzeroevaluationdeterminantr. ((exists mdr_a_row_candidateminornonzeroevaluationdeterminantrc mdr_b_row_candidateminornonzeroevaluationdeterminantrc mdr_c_row_candidateminornonzeroevaluationdeterminantrc mdr_e_row_candidateminornonzeroevaluationdeterminantrc mdr_f_row_candidateminornonzeroevaluationdeterminantrc. ((mdr_a_row_candidateminornonzeroevaluationdeterminantrc = ((q) + (mdr_ub_row_candidateminornonzeroevaluation)) * S ((q) + (mdr_ub_row_candidateminornonzeroevaluation)) + ((mdr_ub_row_candidateminornonzeroevaluation) + (mdr_ub_row_candidateminornonzeroevaluation))) /\ ((mdr_b_row_candidateminornonzeroevaluationdeterminantrc = ((mdr_uc_row_candidateminornonzeroevaluation) + (mdr_vb_row_candidateminornonzeroevaluation)) * S ((mdr_uc_row_candidateminornonzeroevaluation) + (mdr_vb_row_candidateminornonzeroevaluation)) + ((mdr_vb_row_candidateminornonzeroevaluation) + (mdr_vb_row_candidateminornonzeroevaluation))) /\ ((mdr_c_row_candidateminornonzeroevaluationdeterminantrc = ((mdr_a_row_candidateminornonzeroevaluationdeterminantrc) + (mdr_b_row_candidateminornonzeroevaluationdeterminantrc)) * S ((mdr_a_row_candidateminornonzeroevaluationdeterminantrc) + (mdr_b_row_candidateminornonzeroevaluationdeterminantrc)) + ((mdr_b_row_candidateminornonzeroevaluationdeterminantrc) + (mdr_b_row_candidateminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_row_candidateminornonzeroevaluationdeterminantrc = ((mdr_p_row_candidateminornonzero) + (mdr_n_row_candidateminornonzero)) * S ((mdr_p_row_candidateminornonzero) + (mdr_n_row_candidateminornonzero)) + ((mdr_n_row_candidateminornonzero) + (mdr_n_row_candidateminornonzero))) /\ ((mdr_f_row_candidateminornonzeroevaluationdeterminantrc = ((mdr_vc_row_candidateminornonzeroevaluation) + (mdr_e_row_candidateminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_row_candidateminornonzeroevaluation) + (mdr_e_row_candidateminornonzeroevaluationdeterminantrc)) + ((mdr_e_row_candidateminornonzeroevaluationdeterminantrc) + (mdr_e_row_candidateminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_row_candidateminornonzeroevaluationdeterminantr) = ((mdr_c_row_candidateminornonzeroevaluationdeterminantrc) + (mdr_f_row_candidateminornonzeroevaluationdeterminantrc)) * S ((mdr_c_row_candidateminornonzeroevaluationdeterminantrc) + (mdr_f_row_candidateminornonzeroevaluationdeterminantrc)) + ((mdr_f_row_candidateminornonzeroevaluationdeterminantrc) + (mdr_f_row_candidateminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_row_candidateminornonzeroevaluationdeterminantrb. ff_h_mdr_row_candidateminornonzeroevaluationdeterminantrb + S (mdr_z_row_candidateminornonzeroevaluationdeterminantr) = S ((S (mdr_i_row_candidateminornonzeroevaluationdeterminant)) * mdr_c_row_candidateminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_row_candidateminornonzeroevaluationdeterminantrb. mdr_b_row_candidateminornonzeroevaluationdeterminant = ff_q_mdr_row_candidateminornonzeroevaluationdeterminantrb * S ((S (mdr_i_row_candidateminornonzeroevaluationdeterminant)) * mdr_c_row_candidateminornonzeroevaluationdeterminant) + (mdr_z_row_candidateminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_row_candidateminornonzero = mdr_n_row_candidateminornonzero))))))))))))) \/ ~(exists mdr_a_matrix_rank_selected_box_search_decidableno. (((exists mdr_gap_matrix_rank_selected_box_search_decidablenobound. mdr_gap_matrix_rank_selected_box_search_decidablenobound + S (mdr_a_matrix_rank_selected_box_search_decidableno) = (L)) /\ (exists mdr_a_row_candidatecolumns. (((exists mdr_gap_row_candidatecolumnsbound. mdr_gap_row_candidatecolumnsbound + S (mdr_a_row_candidatecolumns) = (C)) /\ (((((forall fom_index_mrf_row_candidateminorrowsbound. (exists fom_gap_mrf_row_candidateminorrowsbound_index_bound. fom_gap_mrf_row_candidateminorrowsbound_index_bound + S (fom_index_mrf_row_candidateminorrowsbound) = q) -> exists fom_value_mrf_row_candidateminorrowsbound. ((((exists fom_beta_height_mrf_row_candidateminorrowsbound_entry. fom_beta_height_mrf_row_candidateminorrowsbound_entry + S (fom_value_mrf_row_candidateminorrowsbound) = S ((S (fom_index_mrf_row_candidateminorrowsbound)) * rc)) /\ exists fom_beta_quotient_mrf_row_candidateminorrowsbound_entry. mdr_a_matrix_rank_selected_box_search_decidableno = fom_beta_quotient_mrf_row_candidateminorrowsbound_entry * S ((S (fom_index_mrf_row_candidateminorrowsbound)) * rc) + (fom_value_mrf_row_candidateminorrowsbound))) /\ (exists fom_gap_mrf_row_candidateminorrowsbound_value_bound. fom_gap_mrf_row_candidateminorrowsbound_value_bound + S (fom_value_mrf_row_candidateminorrowsbound) = r))) /\ (forall mdr_i_row_candidateminorrowsdistinct mdr_j_row_candidateminorrowsdistinct mdr_a_row_candidateminorrowsdistinct. (exists mdr_gap_row_candidateminorrowsdistincti. mdr_gap_row_candidateminorrowsdistincti + S (mdr_i_row_candidateminorrowsdistinct) = (q)) -> (exists mdr_gap_row_candidateminorrowsdistinctj. mdr_gap_row_candidateminorrowsdistinctj + S (mdr_j_row_candidateminorrowsdistinct) = (q)) -> (((exists ff_h_mdr_row_candidateminorrowsdistinctfirst. ff_h_mdr_row_candidateminorrowsdistinctfirst + S (mdr_a_row_candidateminorrowsdistinct) = S ((S (mdr_i_row_candidateminorrowsdistinct)) * rc)) /\ exists ff_q_mdr_row_candidateminorrowsdistinctfirst. mdr_a_matrix_rank_selected_box_search_decidableno = ff_q_mdr_row_candidateminorrowsdistinctfirst * S ((S (mdr_i_row_candidateminorrowsdistinct)) * rc) + (mdr_a_row_candidateminorrowsdistinct))) -> (((exists ff_h_mdr_row_candidateminorrowsdistinctsecond. ff_h_mdr_row_candidateminorrowsdistinctsecond + S (mdr_a_row_candidateminorrowsdistinct) = S ((S (mdr_j_row_candidateminorrowsdistinct)) * rc)) /\ exists ff_q_mdr_row_candidateminorrowsdistinctsecond. mdr_a_matrix_rank_selected_box_search_decidableno = ff_q_mdr_row_candidateminorrowsdistinctsecond * S ((S (mdr_j_row_candidateminorrowsdistinct)) * rc) + (mdr_a_row_candidateminorrowsdistinct))) -> mdr_i_row_candidateminorrowsdistinct = mdr_j_row_candidateminorrowsdistinct))) /\ ((((forall fom_index_mrf_row_candidateminorcolumnsbound. (exists fom_gap_mrf_row_candidateminorcolumnsbound_index_bound. fom_gap_mrf_row_candidateminorcolumnsbound_index_bound + S (fom_index_mrf_row_candidateminorcolumnsbound) = q) -> exists fom_value_mrf_row_candidateminorcolumnsbound. ((((exists fom_beta_height_mrf_row_candidateminorcolumnsbound_entry. fom_beta_height_mrf_row_candidateminorcolumnsbound_entry + S (fom_value_mrf_row_candidateminorcolumnsbound) = S ((S (fom_index_mrf_row_candidateminorcolumnsbound)) * cc)) /\ exists fom_beta_quotient_mrf_row_candidateminorcolumnsbound_entry. mdr_a_row_candidatecolumns = fom_beta_quotient_mrf_row_candidateminorcolumnsbound_entry * S ((S (fom_index_mrf_row_candidateminorcolumnsbound)) * cc) + (fom_value_mrf_row_candidateminorcolumnsbound))) /\ (exists fom_gap_mrf_row_candidateminorcolumnsbound_value_bound. fom_gap_mrf_row_candidateminorcolumnsbound_value_bound + S (fom_value_mrf_row_candidateminorcolumnsbound) = w))) /\ (forall mdr_i_row_candidateminorcolumnsdistinct mdr_j_row_candidateminorcolumnsdistinct mdr_a_row_candidateminorcolumnsdistinct. (exists mdr_gap_row_candidateminorcolumnsdistincti. mdr_gap_row_candidateminorcolumnsdistincti + S (mdr_i_row_candidateminorcolumnsdistinct) = (q)) -> (exists mdr_gap_row_candidateminorcolumnsdistinctj. mdr_gap_row_candidateminorcolumnsdistinctj + S (mdr_j_row_candidateminorcolumnsdistinct) = (q)) -> (((exists ff_h_mdr_row_candidateminorcolumnsdistinctfirst. ff_h_mdr_row_candidateminorcolumnsdistinctfirst + S (mdr_a_row_candidateminorcolumnsdistinct) = S ((S (mdr_i_row_candidateminorcolumnsdistinct)) * cc)) /\ exists ff_q_mdr_row_candidateminorcolumnsdistinctfirst. mdr_a_row_candidatecolumns = ff_q_mdr_row_candidateminorcolumnsdistinctfirst * S ((S (mdr_i_row_candidateminorcolumnsdistinct)) * cc) + (mdr_a_row_candidateminorcolumnsdistinct))) -> (((exists ff_h_mdr_row_candidateminorcolumnsdistinctsecond. ff_h_mdr_row_candidateminorcolumnsdistinctsecond + S (mdr_a_row_candidateminorcolumnsdistinct) = S ((S (mdr_j_row_candidateminorcolumnsdistinct)) * cc)) /\ exists ff_q_mdr_row_candidateminorcolumnsdistinctsecond. mdr_a_row_candidatecolumns = ff_q_mdr_row_candidateminorcolumnsdistinctsecond * S ((S (mdr_j_row_candidateminorcolumnsdistinct)) * cc) + (mdr_a_row_candidateminorcolumnsdistinct))) -> mdr_i_row_candidateminorcolumnsdistinct = mdr_j_row_candidateminorcolumnsdistinct))) /\ (exists mdr_p_row_candidateminornonzero mdr_n_row_candidateminornonzero. ((exists mdr_ub_row_candidateminornonzeroevaluation mdr_uc_row_candidateminornonzeroevaluation mdr_vb_row_candidateminornonzeroevaluation mdr_vc_row_candidateminornonzeroevaluation. ((((forall mdr_i_row_candidateminornonzeroevaluationmatrixpositive. (exists mdr_gap_row_candidateminornonzeroevaluationmatrixpositivebound. mdr_gap_row_candidateminornonzeroevaluationmatrixpositivebound + S (mdr_i_row_candidateminornonzeroevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_row_candidateminornonzeroevaluationmatrixpositive. (((exists mdr_r_row_candidateminornonzeroevaluationmatrixpositivepoint mdr_s_row_candidateminornonzeroevaluationmatrixpositivepoint mdr_u_row_candidateminornonzeroevaluationmatrixpositivepoint mdr_v_row_candidateminornonzeroevaluationmatrixpositivepoint. ((mdr_i_row_candidateminornonzeroevaluationmatrixpositive = (q) * mdr_r_row_candidateminornonzeroevaluationmatrixpositivepoint + mdr_s_row_candidateminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_row_candidateminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_row_candidateminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_row_candidateminornonzeroevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_row_candidateminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_row_candidateminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_row_candidateminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_row_candidateminornonzeroevaluationmatrixpositivepoint)) * rc)) /\ exists ff_q_mdr_row_candidateminornonzeroevaluationmatrixpositivepointrow_index. mdr_a_matrix_rank_selected_box_search_decidableno = ff_q_mdr_row_candidateminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_row_candidateminornonzeroevaluationmatrixpositivepoint)) * rc) + (mdr_u_row_candidateminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_row_candidateminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_row_candidateminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_row_candidateminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_row_candidateminornonzeroevaluationmatrixpositivepoint)) * cc)) /\ exists ff_q_mdr_row_candidateminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_a_row_candidatecolumns = ff_q_mdr_row_candidateminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_row_candidateminornonzeroevaluationmatrixpositivepoint)) * cc) + (mdr_v_row_candidateminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_row_candidateminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_row_candidateminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_row_candidateminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_row_candidateminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_row_candidateminornonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_row_candidateminornonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_row_candidateminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_row_candidateminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_row_candidateminornonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_row_candidateminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_row_candidateminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_row_candidateminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_row_candidateminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_row_candidateminornonzeroevaluationmatrixpositive)) * mdr_uc_row_candidateminornonzeroevaluation)) /\ exists ff_q_mdr_row_candidateminornonzeroevaluationmatrixpositiveoutput. mdr_ub_row_candidateminornonzeroevaluation = ff_q_mdr_row_candidateminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_row_candidateminornonzeroevaluationmatrixpositive)) * mdr_uc_row_candidateminornonzeroevaluation) + (mdr_a_row_candidateminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_row_candidateminornonzeroevaluationmatrixnegative. (exists mdr_gap_row_candidateminornonzeroevaluationmatrixnegativebound. mdr_gap_row_candidateminornonzeroevaluationmatrixnegativebound + S (mdr_i_row_candidateminornonzeroevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_row_candidateminornonzeroevaluationmatrixnegative. (((exists mdr_r_row_candidateminornonzeroevaluationmatrixnegativepoint mdr_s_row_candidateminornonzeroevaluationmatrixnegativepoint mdr_u_row_candidateminornonzeroevaluationmatrixnegativepoint mdr_v_row_candidateminornonzeroevaluationmatrixnegativepoint. ((mdr_i_row_candidateminornonzeroevaluationmatrixnegative = (q) * mdr_r_row_candidateminornonzeroevaluationmatrixnegativepoint + mdr_s_row_candidateminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_row_candidateminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_row_candidateminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_row_candidateminornonzeroevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_row_candidateminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_row_candidateminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_row_candidateminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_row_candidateminornonzeroevaluationmatrixnegativepoint)) * rc)) /\ exists ff_q_mdr_row_candidateminornonzeroevaluationmatrixnegativepointrow_index. mdr_a_matrix_rank_selected_box_search_decidableno = ff_q_mdr_row_candidateminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_row_candidateminornonzeroevaluationmatrixnegativepoint)) * rc) + (mdr_u_row_candidateminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_row_candidateminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_row_candidateminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_row_candidateminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_row_candidateminornonzeroevaluationmatrixnegativepoint)) * cc)) /\ exists ff_q_mdr_row_candidateminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_a_row_candidatecolumns = ff_q_mdr_row_candidateminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_row_candidateminornonzeroevaluationmatrixnegativepoint)) * cc) + (mdr_v_row_candidateminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_row_candidateminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_row_candidateminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_row_candidateminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_row_candidateminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_row_candidateminornonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_row_candidateminornonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_row_candidateminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_row_candidateminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_row_candidateminornonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_row_candidateminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_row_candidateminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_row_candidateminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_row_candidateminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_row_candidateminornonzeroevaluationmatrixnegative)) * mdr_vc_row_candidateminornonzeroevaluation)) /\ exists ff_q_mdr_row_candidateminornonzeroevaluationmatrixnegativeoutput. mdr_vb_row_candidateminornonzeroevaluation = ff_q_mdr_row_candidateminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_row_candidateminornonzeroevaluationmatrixnegative)) * mdr_vc_row_candidateminornonzeroevaluation) + (mdr_a_row_candidateminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_row_candidateminornonzeroevaluationdeterminant mdr_c_row_candidateminornonzeroevaluationdeterminant mdr_l_row_candidateminornonzeroevaluationdeterminant mdr_i_row_candidateminornonzeroevaluationdeterminant. ((forall mdr_i_row_candidateminornonzeroevaluationdeterminanth. (exists mdr_gap_row_candidateminornonzeroevaluationdeterminanthi. mdr_gap_row_candidateminornonzeroevaluationdeterminanthi + S (mdr_i_row_candidateminornonzeroevaluationdeterminanth) = (mdr_l_row_candidateminornonzeroevaluationdeterminant)) -> exists mdr_d_row_candidateminornonzeroevaluationdeterminanth mdr_pb_row_candidateminornonzeroevaluationdeterminanth mdr_pc_row_candidateminornonzeroevaluationdeterminanth mdr_nb_row_candidateminornonzeroevaluationdeterminanth mdr_nc_row_candidateminornonzeroevaluationdeterminanth mdr_p_row_candidateminornonzeroevaluationdeterminanth mdr_n_row_candidateminornonzeroevaluationdeterminanth. ((exists mdr_z_row_candidateminornonzeroevaluationdeterminanthr. ((exists mdr_a_row_candidateminornonzeroevaluationdeterminanthrc mdr_b_row_candidateminornonzeroevaluationdeterminanthrc mdr_c_row_candidateminornonzeroevaluationdeterminanthrc mdr_e_row_candidateminornonzeroevaluationdeterminanthrc mdr_f_row_candidateminornonzeroevaluationdeterminanthrc. ((mdr_a_row_candidateminornonzeroevaluationdeterminanthrc = ((mdr_d_row_candidateminornonzeroevaluationdeterminanth) + (mdr_pb_row_candidateminornonzeroevaluationdeterminanth)) * S ((mdr_d_row_candidateminornonzeroevaluationdeterminanth) + (mdr_pb_row_candidateminornonzeroevaluationdeterminanth)) + ((mdr_pb_row_candidateminornonzeroevaluationdeterminanth) + (mdr_pb_row_candidateminornonzeroevaluationdeterminanth))) /\ ((mdr_b_row_candidateminornonzeroevaluationdeterminanthrc = ((mdr_pc_row_candidateminornonzeroevaluationdeterminanth) + (mdr_nb_row_candidateminornonzeroevaluationdeterminanth)) * S ((mdr_pc_row_candidateminornonzeroevaluationdeterminanth) + (mdr_nb_row_candidateminornonzeroevaluationdeterminanth)) + ((mdr_nb_row_candidateminornonzeroevaluationdeterminanth) + (mdr_nb_row_candidateminornonzeroevaluationdeterminanth))) /\ ((mdr_c_row_candidateminornonzeroevaluationdeterminanthrc = ((mdr_a_row_candidateminornonzeroevaluationdeterminanthrc) + (mdr_b_row_candidateminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_row_candidateminornonzeroevaluationdeterminanthrc) + (mdr_b_row_candidateminornonzeroevaluationdeterminanthrc)) + ((mdr_b_row_candidateminornonzeroevaluationdeterminanthrc) + (mdr_b_row_candidateminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_row_candidateminornonzeroevaluationdeterminanthrc = ((mdr_p_row_candidateminornonzeroevaluationdeterminanth) + (mdr_n_row_candidateminornonzeroevaluationdeterminanth)) * S ((mdr_p_row_candidateminornonzeroevaluationdeterminanth) + (mdr_n_row_candidateminornonzeroevaluationdeterminanth)) + ((mdr_n_row_candidateminornonzeroevaluationdeterminanth) + (mdr_n_row_candidateminornonzeroevaluationdeterminanth))) /\ ((mdr_f_row_candidateminornonzeroevaluationdeterminanthrc = ((mdr_nc_row_candidateminornonzeroevaluationdeterminanth) + (mdr_e_row_candidateminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_row_candidateminornonzeroevaluationdeterminanth) + (mdr_e_row_candidateminornonzeroevaluationdeterminanthrc)) + ((mdr_e_row_candidateminornonzeroevaluationdeterminanthrc) + (mdr_e_row_candidateminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_row_candidateminornonzeroevaluationdeterminanthr) = ((mdr_c_row_candidateminornonzeroevaluationdeterminanthrc) + (mdr_f_row_candidateminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_row_candidateminornonzeroevaluationdeterminanthrc) + (mdr_f_row_candidateminornonzeroevaluationdeterminanthrc)) + ((mdr_f_row_candidateminornonzeroevaluationdeterminanthrc) + (mdr_f_row_candidateminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_row_candidateminornonzeroevaluationdeterminanthrb. ff_h_mdr_row_candidateminornonzeroevaluationdeterminanthrb + S (mdr_z_row_candidateminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_row_candidateminornonzeroevaluationdeterminanth)) * mdr_c_row_candidateminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_row_candidateminornonzeroevaluationdeterminanthrb. mdr_b_row_candidateminornonzeroevaluationdeterminant = ff_q_mdr_row_candidateminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_row_candidateminornonzeroevaluationdeterminanth)) * mdr_c_row_candidateminornonzeroevaluationdeterminant) + (mdr_z_row_candidateminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_row_candidateminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_row_candidateminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_row_candidateminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_row_candidateminornonzeroevaluationdeterminanths mdr_eb_row_candidateminornonzeroevaluationdeterminanths mdr_ec_row_candidateminornonzeroevaluationdeterminanths mdr_fb_row_candidateminornonzeroevaluationdeterminanths mdr_fc_row_candidateminornonzeroevaluationdeterminanths. (((mdr_d_row_candidateminornonzeroevaluationdeterminanth) = S (mdr_q_row_candidateminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_row_candidateminornonzeroevaluationdeterminanthsc. (exists mdr_gap_row_candidateminornonzeroevaluationdeterminanthscj. mdr_gap_row_candidateminornonzeroevaluationdeterminanthscj + S (mdr_j_row_candidateminornonzeroevaluationdeterminanthsc) = (S (mdr_q_row_candidateminornonzeroevaluationdeterminanths))) -> exists mdr_i_row_candidateminornonzeroevaluationdeterminanthsc mdr_up_row_candidateminornonzeroevaluationdeterminanthsc mdr_us_row_candidateminornonzeroevaluationdeterminanthsc mdr_un_row_candidateminornonzeroevaluationdeterminanthsc mdr_ut_row_candidateminornonzeroevaluationdeterminanthsc mdr_p_row_candidateminornonzeroevaluationdeterminanthsc mdr_n_row_candidateminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_row_candidateminornonzeroevaluationdeterminanthsci. mdr_gap_row_candidateminornonzeroevaluationdeterminanthsci + S (mdr_i_row_candidateminornonzeroevaluationdeterminanthsc) = (mdr_i_row_candidateminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_row_candidateminornonzeroevaluationdeterminanthscr. ((exists mdr_a_row_candidateminornonzeroevaluationdeterminanthscrc mdr_b_row_candidateminornonzeroevaluationdeterminanthscrc mdr_c_row_candidateminornonzeroevaluationdeterminanthscrc mdr_e_row_candidateminornonzeroevaluationdeterminanthscrc mdr_f_row_candidateminornonzeroevaluationdeterminanthscrc. ((mdr_a_row_candidateminornonzeroevaluationdeterminanthscrc = ((mdr_q_row_candidateminornonzeroevaluationdeterminanths) + (mdr_up_row_candidateminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_row_candidateminornonzeroevaluationdeterminanths) + (mdr_up_row_candidateminornonzeroevaluationdeterminanthsc)) + ((mdr_up_row_candidateminornonzeroevaluationdeterminanthsc) + (mdr_up_row_candidateminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_row_candidateminornonzeroevaluationdeterminanthscrc = ((mdr_us_row_candidateminornonzeroevaluationdeterminanthsc) + (mdr_un_row_candidateminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_row_candidateminornonzeroevaluationdeterminanthsc) + (mdr_un_row_candidateminornonzeroevaluationdeterminanthsc)) + ((mdr_un_row_candidateminornonzeroevaluationdeterminanthsc) + (mdr_un_row_candidateminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_row_candidateminornonzeroevaluationdeterminanthscrc = ((mdr_a_row_candidateminornonzeroevaluationdeterminanthscrc) + (mdr_b_row_candidateminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_row_candidateminornonzeroevaluationdeterminanthscrc) + (mdr_b_row_candidateminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_row_candidateminornonzeroevaluationdeterminanthscrc) + (mdr_b_row_candidateminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_row_candidateminornonzeroevaluationdeterminanthscrc = ((mdr_p_row_candidateminornonzeroevaluationdeterminanthsc) + (mdr_n_row_candidateminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_row_candidateminornonzeroevaluationdeterminanthsc) + (mdr_n_row_candidateminornonzeroevaluationdeterminanthsc)) + ((mdr_n_row_candidateminornonzeroevaluationdeterminanthsc) + (mdr_n_row_candidateminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_row_candidateminornonzeroevaluationdeterminanthscrc = ((mdr_ut_row_candidateminornonzeroevaluationdeterminanthsc) + (mdr_e_row_candidateminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_row_candidateminornonzeroevaluationdeterminanthsc) + (mdr_e_row_candidateminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_row_candidateminornonzeroevaluationdeterminanthscrc) + (mdr_e_row_candidateminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_row_candidateminornonzeroevaluationdeterminanthscr) = ((mdr_c_row_candidateminornonzeroevaluationdeterminanthscrc) + (mdr_f_row_candidateminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_row_candidateminornonzeroevaluationdeterminanthscrc) + (mdr_f_row_candidateminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_row_candidateminornonzeroevaluationdeterminanthscrc) + (mdr_f_row_candidateminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_row_candidateminornonzeroevaluationdeterminanthscrb. ff_h_mdr_row_candidateminornonzeroevaluationdeterminanthscrb + S (mdr_z_row_candidateminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_row_candidateminornonzeroevaluationdeterminanthsc)) * mdr_c_row_candidateminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_row_candidateminornonzeroevaluationdeterminanthscrb. mdr_b_row_candidateminornonzeroevaluationdeterminant = ff_q_mdr_row_candidateminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_row_candidateminornonzeroevaluationdeterminanthsc)) * mdr_c_row_candidateminornonzeroevaluationdeterminant) + (mdr_z_row_candidateminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_row_candidateminornonzeroevaluationdeterminanths) * (mdr_q_row_candidateminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive = (mdr_q_row_candidateminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_row_candidateminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_row_candidateminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_row_candidateminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_row_candidateminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_row_candidateminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_row_candidateminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_row_candidateminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_row_candidateminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_row_candidateminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_row_candidateminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_row_candidateminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_row_candidateminornonzeroevaluationdeterminanths) * (mdr_q_row_candidateminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative = (mdr_q_row_candidateminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_row_candidateminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_row_candidateminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_row_candidateminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_row_candidateminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_row_candidateminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_row_candidateminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_row_candidateminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_row_candidateminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_row_candidateminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_row_candidateminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_row_candidateminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_row_candidateminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_row_candidateminornonzeroevaluationdeterminanthscp. ff_h_mdr_row_candidateminornonzeroevaluationdeterminanthscp + S (mdr_p_row_candidateminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_row_candidateminornonzeroevaluationdeterminanthsc)) * mdr_ec_row_candidateminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_row_candidateminornonzeroevaluationdeterminanthscp. mdr_eb_row_candidateminornonzeroevaluationdeterminanths = ff_q_mdr_row_candidateminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_row_candidateminornonzeroevaluationdeterminanthsc)) * mdr_ec_row_candidateminornonzeroevaluationdeterminanths) + (mdr_p_row_candidateminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_row_candidateminornonzeroevaluationdeterminanthscn. ff_h_mdr_row_candidateminornonzeroevaluationdeterminanthscn + S (mdr_n_row_candidateminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_row_candidateminornonzeroevaluationdeterminanthsc)) * mdr_fc_row_candidateminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_row_candidateminornonzeroevaluationdeterminanthscn. mdr_fb_row_candidateminornonzeroevaluationdeterminanths = ff_q_mdr_row_candidateminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_row_candidateminornonzeroevaluationdeterminanthsc)) * mdr_fc_row_candidateminornonzeroevaluationdeterminanths) + (mdr_n_row_candidateminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_row_candidateminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_row_candidateminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_row_candidateminornonzeroevaluationdeterminanth = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_row_candidateminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_row_candidateminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_row_candidateminornonzeroevaluationdeterminanth = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_row_candidateminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_row_candidateminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_row_candidateminornonzeroevaluationdeterminanths = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_row_candidateminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_row_candidateminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_row_candidateminornonzeroevaluationdeterminanths = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_row_candidateminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_row_candidateminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_row_candidateminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_row_candidateminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_row_candidateminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_row_candidateminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_row_candidateminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_row_candidateminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_row_candidateminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_row_candidateminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_row_candidateminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_row_candidateminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_row_candidateminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_row_candidateminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_row_candidateminornonzeroevaluationdeterminanti. mdr_gap_row_candidateminornonzeroevaluationdeterminanti + S (mdr_i_row_candidateminornonzeroevaluationdeterminant) = (mdr_l_row_candidateminornonzeroevaluationdeterminant)) /\ (exists mdr_z_row_candidateminornonzeroevaluationdeterminantr. ((exists mdr_a_row_candidateminornonzeroevaluationdeterminantrc mdr_b_row_candidateminornonzeroevaluationdeterminantrc mdr_c_row_candidateminornonzeroevaluationdeterminantrc mdr_e_row_candidateminornonzeroevaluationdeterminantrc mdr_f_row_candidateminornonzeroevaluationdeterminantrc. ((mdr_a_row_candidateminornonzeroevaluationdeterminantrc = ((q) + (mdr_ub_row_candidateminornonzeroevaluation)) * S ((q) + (mdr_ub_row_candidateminornonzeroevaluation)) + ((mdr_ub_row_candidateminornonzeroevaluation) + (mdr_ub_row_candidateminornonzeroevaluation))) /\ ((mdr_b_row_candidateminornonzeroevaluationdeterminantrc = ((mdr_uc_row_candidateminornonzeroevaluation) + (mdr_vb_row_candidateminornonzeroevaluation)) * S ((mdr_uc_row_candidateminornonzeroevaluation) + (mdr_vb_row_candidateminornonzeroevaluation)) + ((mdr_vb_row_candidateminornonzeroevaluation) + (mdr_vb_row_candidateminornonzeroevaluation))) /\ ((mdr_c_row_candidateminornonzeroevaluationdeterminantrc = ((mdr_a_row_candidateminornonzeroevaluationdeterminantrc) + (mdr_b_row_candidateminornonzeroevaluationdeterminantrc)) * S ((mdr_a_row_candidateminornonzeroevaluationdeterminantrc) + (mdr_b_row_candidateminornonzeroevaluationdeterminantrc)) + ((mdr_b_row_candidateminornonzeroevaluationdeterminantrc) + (mdr_b_row_candidateminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_row_candidateminornonzeroevaluationdeterminantrc = ((mdr_p_row_candidateminornonzero) + (mdr_n_row_candidateminornonzero)) * S ((mdr_p_row_candidateminornonzero) + (mdr_n_row_candidateminornonzero)) + ((mdr_n_row_candidateminornonzero) + (mdr_n_row_candidateminornonzero))) /\ ((mdr_f_row_candidateminornonzeroevaluationdeterminantrc = ((mdr_vc_row_candidateminornonzeroevaluation) + (mdr_e_row_candidateminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_row_candidateminornonzeroevaluation) + (mdr_e_row_candidateminornonzeroevaluationdeterminantrc)) + ((mdr_e_row_candidateminornonzeroevaluationdeterminantrc) + (mdr_e_row_candidateminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_row_candidateminornonzeroevaluationdeterminantr) = ((mdr_c_row_candidateminornonzeroevaluationdeterminantrc) + (mdr_f_row_candidateminornonzeroevaluationdeterminantrc)) * S ((mdr_c_row_candidateminornonzeroevaluationdeterminantrc) + (mdr_f_row_candidateminornonzeroevaluationdeterminantrc)) + ((mdr_f_row_candidateminornonzeroevaluationdeterminantrc) + (mdr_f_row_candidateminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_row_candidateminornonzeroevaluationdeterminantrb. ff_h_mdr_row_candidateminornonzeroevaluationdeterminantrb + S (mdr_z_row_candidateminornonzeroevaluationdeterminantr) = S ((S (mdr_i_row_candidateminornonzeroevaluationdeterminant)) * mdr_c_row_candidateminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_row_candidateminornonzeroevaluationdeterminantrb. mdr_b_row_candidateminornonzeroevaluationdeterminant = ff_q_mdr_row_candidateminornonzeroevaluationdeterminantrb * S ((S (mdr_i_row_candidateminornonzeroevaluationdeterminant)) * mdr_c_row_candidateminornonzeroevaluationdeterminant) + (mdr_z_row_candidateminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_row_candidateminornonzero = mdr_n_row_candidateminornonzero)))))))))))))