matrix_rank_nonzero_minor_of_box_search

forall pb pc nb nc r w q rc cc R C. (exists mdr_a_found_minorrows. (((exists mdr_gap_found_minorrowsbound. mdr_gap_found_minorrowsbound + S (mdr_a_found_minorrows) = (R)) /\ (exists mdr_a_found_minorrowcolumns. (((exists mdr_gap_found_minorrowcolumnsbound. mdr_gap_found_minorrowcolumnsbound + S (mdr_a_found_minorrowcolumns) = (C)) /\ (((((forall fom_index_mrf_found_minorrowminorrowsbound. (exists fom_gap_mrf_found_minorrowminorrowsbound_index_bound. fom_gap_mrf_found_minorrowminorrowsbound_index_bound + S (fom_index_mrf_found_minorrowminorrowsbound) = q) -> exists fom_value_mrf_found_minorrowminorrowsbound. ((((exists fom_beta_height_mrf_found_minorrowminorrowsbound_entry. fom_beta_height_mrf_found_minorrowminorrowsbound_entry + S (fom_value_mrf_found_minorrowminorrowsbound) = S ((S (fom_index_mrf_found_minorrowminorrowsbound)) * rc)) /\ exists fom_beta_quotient_mrf_found_minorrowminorrowsbound_entry. mdr_a_found_minorrows = fom_beta_quotient_mrf_found_minorrowminorrowsbound_entry * S ((S (fom_index_mrf_found_minorrowminorrowsbound)) * rc) + (fom_value_mrf_found_minorrowminorrowsbound))) /\ (exists fom_gap_mrf_found_minorrowminorrowsbound_value_bound. fom_gap_mrf_found_minorrowminorrowsbound_value_bound + S (fom_value_mrf_found_minorrowminorrowsbound) = r))) /\ (forall mdr_i_found_minorrowminorrowsdistinct mdr_j_found_minorrowminorrowsdistinct mdr_a_found_minorrowminorrowsdistinct. (exists mdr_gap_found_minorrowminorrowsdistincti. mdr_gap_found_minorrowminorrowsdistincti + S (mdr_i_found_minorrowminorrowsdistinct) = (q)) -> (exists mdr_gap_found_minorrowminorrowsdistinctj. mdr_gap_found_minorrowminorrowsdistinctj + S (mdr_j_found_minorrowminorrowsdistinct) = (q)) -> (((exists ff_h_mdr_found_minorrowminorrowsdistinctfirst. ff_h_mdr_found_minorrowminorrowsdistinctfirst + S (mdr_a_found_minorrowminorrowsdistinct) = S ((S (mdr_i_found_minorrowminorrowsdistinct)) * rc)) /\ exists ff_q_mdr_found_minorrowminorrowsdistinctfirst. mdr_a_found_minorrows = ff_q_mdr_found_minorrowminorrowsdistinctfirst * S ((S (mdr_i_found_minorrowminorrowsdistinct)) * rc) + (mdr_a_found_minorrowminorrowsdistinct))) -> (((exists ff_h_mdr_found_minorrowminorrowsdistinctsecond. ff_h_mdr_found_minorrowminorrowsdistinctsecond + S (mdr_a_found_minorrowminorrowsdistinct) = S ((S (mdr_j_found_minorrowminorrowsdistinct)) * rc)) /\ exists ff_q_mdr_found_minorrowminorrowsdistinctsecond. mdr_a_found_minorrows = ff_q_mdr_found_minorrowminorrowsdistinctsecond * S ((S (mdr_j_found_minorrowminorrowsdistinct)) * rc) + (mdr_a_found_minorrowminorrowsdistinct))) -> mdr_i_found_minorrowminorrowsdistinct = mdr_j_found_minorrowminorrowsdistinct))) /\ ((((forall fom_index_mrf_found_minorrowminorcolumnsbound. (exists fom_gap_mrf_found_minorrowminorcolumnsbound_index_bound. fom_gap_mrf_found_minorrowminorcolumnsbound_index_bound + S (fom_index_mrf_found_minorrowminorcolumnsbound) = q) -> exists fom_value_mrf_found_minorrowminorcolumnsbound. ((((exists fom_beta_height_mrf_found_minorrowminorcolumnsbound_entry. fom_beta_height_mrf_found_minorrowminorcolumnsbound_entry + S (fom_value_mrf_found_minorrowminorcolumnsbound) = S ((S (fom_index_mrf_found_minorrowminorcolumnsbound)) * cc)) /\ exists fom_beta_quotient_mrf_found_minorrowminorcolumnsbound_entry. mdr_a_found_minorrowcolumns = fom_beta_quotient_mrf_found_minorrowminorcolumnsbound_entry * S ((S (fom_index_mrf_found_minorrowminorcolumnsbound)) * cc) + (fom_value_mrf_found_minorrowminorcolumnsbound))) /\ (exists fom_gap_mrf_found_minorrowminorcolumnsbound_value_bound. fom_gap_mrf_found_minorrowminorcolumnsbound_value_bound + S (fom_value_mrf_found_minorrowminorcolumnsbound) = w))) /\ (forall mdr_i_found_minorrowminorcolumnsdistinct mdr_j_found_minorrowminorcolumnsdistinct mdr_a_found_minorrowminorcolumnsdistinct. (exists mdr_gap_found_minorrowminorcolumnsdistincti. mdr_gap_found_minorrowminorcolumnsdistincti + S (mdr_i_found_minorrowminorcolumnsdistinct) = (q)) -> (exists mdr_gap_found_minorrowminorcolumnsdistinctj. mdr_gap_found_minorrowminorcolumnsdistinctj + S (mdr_j_found_minorrowminorcolumnsdistinct) = (q)) -> (((exists ff_h_mdr_found_minorrowminorcolumnsdistinctfirst. ff_h_mdr_found_minorrowminorcolumnsdistinctfirst + S (mdr_a_found_minorrowminorcolumnsdistinct) = S ((S (mdr_i_found_minorrowminorcolumnsdistinct)) * cc)) /\ exists ff_q_mdr_found_minorrowminorcolumnsdistinctfirst. mdr_a_found_minorrowcolumns = ff_q_mdr_found_minorrowminorcolumnsdistinctfirst * S ((S (mdr_i_found_minorrowminorcolumnsdistinct)) * cc) + (mdr_a_found_minorrowminorcolumnsdistinct))) -> (((exists ff_h_mdr_found_minorrowminorcolumnsdistinctsecond. ff_h_mdr_found_minorrowminorcolumnsdistinctsecond + S (mdr_a_found_minorrowminorcolumnsdistinct) = S ((S (mdr_j_found_minorrowminorcolumnsdistinct)) * cc)) /\ exists ff_q_mdr_found_minorrowminorcolumnsdistinctsecond. mdr_a_found_minorrowcolumns = ff_q_mdr_found_minorrowminorcolumnsdistinctsecond * S ((S (mdr_j_found_minorrowminorcolumnsdistinct)) * cc) + (mdr_a_found_minorrowminorcolumnsdistinct))) -> mdr_i_found_minorrowminorcolumnsdistinct = mdr_j_found_minorrowminorcolumnsdistinct))) /\ (exists mdr_p_found_minorrowminornonzero mdr_n_found_minorrowminornonzero. ((exists mdr_ub_found_minorrowminornonzeroevaluation mdr_uc_found_minorrowminornonzeroevaluation mdr_vb_found_minorrowminornonzeroevaluation mdr_vc_found_minorrowminornonzeroevaluation. ((((forall mdr_i_found_minorrowminornonzeroevaluationmatrixpositive. (exists mdr_gap_found_minorrowminornonzeroevaluationmatrixpositivebound. mdr_gap_found_minorrowminornonzeroevaluationmatrixpositivebound + S (mdr_i_found_minorrowminornonzeroevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_found_minorrowminornonzeroevaluationmatrixpositive. (((exists mdr_r_found_minorrowminornonzeroevaluationmatrixpositivepoint mdr_s_found_minorrowminornonzeroevaluationmatrixpositivepoint mdr_u_found_minorrowminornonzeroevaluationmatrixpositivepoint mdr_v_found_minorrowminornonzeroevaluationmatrixpositivepoint. ((mdr_i_found_minorrowminornonzeroevaluationmatrixpositive = (q) * mdr_r_found_minorrowminornonzeroevaluationmatrixpositivepoint + mdr_s_found_minorrowminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_found_minorrowminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_found_minorrowminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_found_minorrowminornonzeroevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_found_minorrowminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_found_minorrowminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_found_minorrowminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_found_minorrowminornonzeroevaluationmatrixpositivepoint)) * rc)) /\ exists ff_q_mdr_found_minorrowminornonzeroevaluationmatrixpositivepointrow_index. mdr_a_found_minorrows = ff_q_mdr_found_minorrowminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_found_minorrowminornonzeroevaluationmatrixpositivepoint)) * rc) + (mdr_u_found_minorrowminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_found_minorrowminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_found_minorrowminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_found_minorrowminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_found_minorrowminornonzeroevaluationmatrixpositivepoint)) * cc)) /\ exists ff_q_mdr_found_minorrowminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_a_found_minorrowcolumns = ff_q_mdr_found_minorrowminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_found_minorrowminornonzeroevaluationmatrixpositivepoint)) * cc) + (mdr_v_found_minorrowminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_found_minorrowminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_found_minorrowminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_found_minorrowminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_found_minorrowminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_found_minorrowminornonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_found_minorrowminornonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_found_minorrowminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_found_minorrowminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_found_minorrowminornonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_found_minorrowminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_found_minorrowminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_found_minorrowminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_found_minorrowminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_found_minorrowminornonzeroevaluationmatrixpositive)) * mdr_uc_found_minorrowminornonzeroevaluation)) /\ exists ff_q_mdr_found_minorrowminornonzeroevaluationmatrixpositiveoutput. mdr_ub_found_minorrowminornonzeroevaluation = ff_q_mdr_found_minorrowminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_found_minorrowminornonzeroevaluationmatrixpositive)) * mdr_uc_found_minorrowminornonzeroevaluation) + (mdr_a_found_minorrowminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_found_minorrowminornonzeroevaluationmatrixnegative. (exists mdr_gap_found_minorrowminornonzeroevaluationmatrixnegativebound. mdr_gap_found_minorrowminornonzeroevaluationmatrixnegativebound + S (mdr_i_found_minorrowminornonzeroevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_found_minorrowminornonzeroevaluationmatrixnegative. (((exists mdr_r_found_minorrowminornonzeroevaluationmatrixnegativepoint mdr_s_found_minorrowminornonzeroevaluationmatrixnegativepoint mdr_u_found_minorrowminornonzeroevaluationmatrixnegativepoint mdr_v_found_minorrowminornonzeroevaluationmatrixnegativepoint. ((mdr_i_found_minorrowminornonzeroevaluationmatrixnegative = (q) * mdr_r_found_minorrowminornonzeroevaluationmatrixnegativepoint + mdr_s_found_minorrowminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_found_minorrowminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_found_minorrowminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_found_minorrowminornonzeroevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_found_minorrowminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_found_minorrowminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_found_minorrowminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_found_minorrowminornonzeroevaluationmatrixnegativepoint)) * rc)) /\ exists ff_q_mdr_found_minorrowminornonzeroevaluationmatrixnegativepointrow_index. mdr_a_found_minorrows = ff_q_mdr_found_minorrowminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_found_minorrowminornonzeroevaluationmatrixnegativepoint)) * rc) + (mdr_u_found_minorrowminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_found_minorrowminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_found_minorrowminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_found_minorrowminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_found_minorrowminornonzeroevaluationmatrixnegativepoint)) * cc)) /\ exists ff_q_mdr_found_minorrowminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_a_found_minorrowcolumns = ff_q_mdr_found_minorrowminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_found_minorrowminornonzeroevaluationmatrixnegativepoint)) * cc) + (mdr_v_found_minorrowminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_found_minorrowminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_found_minorrowminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_found_minorrowminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_found_minorrowminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_found_minorrowminornonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_found_minorrowminornonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_found_minorrowminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_found_minorrowminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_found_minorrowminornonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_found_minorrowminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_found_minorrowminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_found_minorrowminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_found_minorrowminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_found_minorrowminornonzeroevaluationmatrixnegative)) * mdr_vc_found_minorrowminornonzeroevaluation)) /\ exists ff_q_mdr_found_minorrowminornonzeroevaluationmatrixnegativeoutput. mdr_vb_found_minorrowminornonzeroevaluation = ff_q_mdr_found_minorrowminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_found_minorrowminornonzeroevaluationmatrixnegative)) * mdr_vc_found_minorrowminornonzeroevaluation) + (mdr_a_found_minorrowminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_found_minorrowminornonzeroevaluationdeterminant mdr_c_found_minorrowminornonzeroevaluationdeterminant mdr_l_found_minorrowminornonzeroevaluationdeterminant mdr_i_found_minorrowminornonzeroevaluationdeterminant. ((forall mdr_i_found_minorrowminornonzeroevaluationdeterminanth. (exists mdr_gap_found_minorrowminornonzeroevaluationdeterminanthi. mdr_gap_found_minorrowminornonzeroevaluationdeterminanthi + S (mdr_i_found_minorrowminornonzeroevaluationdeterminanth) = (mdr_l_found_minorrowminornonzeroevaluationdeterminant)) -> exists mdr_d_found_minorrowminornonzeroevaluationdeterminanth mdr_pb_found_minorrowminornonzeroevaluationdeterminanth mdr_pc_found_minorrowminornonzeroevaluationdeterminanth mdr_nb_found_minorrowminornonzeroevaluationdeterminanth mdr_nc_found_minorrowminornonzeroevaluationdeterminanth mdr_p_found_minorrowminornonzeroevaluationdeterminanth mdr_n_found_minorrowminornonzeroevaluationdeterminanth. ((exists mdr_z_found_minorrowminornonzeroevaluationdeterminanthr. ((exists mdr_a_found_minorrowminornonzeroevaluationdeterminanthrc mdr_b_found_minorrowminornonzeroevaluationdeterminanthrc mdr_c_found_minorrowminornonzeroevaluationdeterminanthrc mdr_e_found_minorrowminornonzeroevaluationdeterminanthrc mdr_f_found_minorrowminornonzeroevaluationdeterminanthrc. ((mdr_a_found_minorrowminornonzeroevaluationdeterminanthrc = ((mdr_d_found_minorrowminornonzeroevaluationdeterminanth) + (mdr_pb_found_minorrowminornonzeroevaluationdeterminanth)) * S ((mdr_d_found_minorrowminornonzeroevaluationdeterminanth) + (mdr_pb_found_minorrowminornonzeroevaluationdeterminanth)) + ((mdr_pb_found_minorrowminornonzeroevaluationdeterminanth) + (mdr_pb_found_minorrowminornonzeroevaluationdeterminanth))) /\ ((mdr_b_found_minorrowminornonzeroevaluationdeterminanthrc = ((mdr_pc_found_minorrowminornonzeroevaluationdeterminanth) + (mdr_nb_found_minorrowminornonzeroevaluationdeterminanth)) * S ((mdr_pc_found_minorrowminornonzeroevaluationdeterminanth) + (mdr_nb_found_minorrowminornonzeroevaluationdeterminanth)) + ((mdr_nb_found_minorrowminornonzeroevaluationdeterminanth) + (mdr_nb_found_minorrowminornonzeroevaluationdeterminanth))) /\ ((mdr_c_found_minorrowminornonzeroevaluationdeterminanthrc = ((mdr_a_found_minorrowminornonzeroevaluationdeterminanthrc) + (mdr_b_found_minorrowminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_found_minorrowminornonzeroevaluationdeterminanthrc) + (mdr_b_found_minorrowminornonzeroevaluationdeterminanthrc)) + ((mdr_b_found_minorrowminornonzeroevaluationdeterminanthrc) + (mdr_b_found_minorrowminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_found_minorrowminornonzeroevaluationdeterminanthrc = ((mdr_p_found_minorrowminornonzeroevaluationdeterminanth) + (mdr_n_found_minorrowminornonzeroevaluationdeterminanth)) * S ((mdr_p_found_minorrowminornonzeroevaluationdeterminanth) + (mdr_n_found_minorrowminornonzeroevaluationdeterminanth)) + ((mdr_n_found_minorrowminornonzeroevaluationdeterminanth) + (mdr_n_found_minorrowminornonzeroevaluationdeterminanth))) /\ ((mdr_f_found_minorrowminornonzeroevaluationdeterminanthrc = ((mdr_nc_found_minorrowminornonzeroevaluationdeterminanth) + (mdr_e_found_minorrowminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_found_minorrowminornonzeroevaluationdeterminanth) + (mdr_e_found_minorrowminornonzeroevaluationdeterminanthrc)) + ((mdr_e_found_minorrowminornonzeroevaluationdeterminanthrc) + (mdr_e_found_minorrowminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_found_minorrowminornonzeroevaluationdeterminanthr) = ((mdr_c_found_minorrowminornonzeroevaluationdeterminanthrc) + (mdr_f_found_minorrowminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_found_minorrowminornonzeroevaluationdeterminanthrc) + (mdr_f_found_minorrowminornonzeroevaluationdeterminanthrc)) + ((mdr_f_found_minorrowminornonzeroevaluationdeterminanthrc) + (mdr_f_found_minorrowminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_found_minorrowminornonzeroevaluationdeterminanthrb. ff_h_mdr_found_minorrowminornonzeroevaluationdeterminanthrb + S (mdr_z_found_minorrowminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_found_minorrowminornonzeroevaluationdeterminanth)) * mdr_c_found_minorrowminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_found_minorrowminornonzeroevaluationdeterminanthrb. mdr_b_found_minorrowminornonzeroevaluationdeterminant = ff_q_mdr_found_minorrowminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_found_minorrowminornonzeroevaluationdeterminanth)) * mdr_c_found_minorrowminornonzeroevaluationdeterminant) + (mdr_z_found_minorrowminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_found_minorrowminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_found_minorrowminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_found_minorrowminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_found_minorrowminornonzeroevaluationdeterminanths mdr_eb_found_minorrowminornonzeroevaluationdeterminanths mdr_ec_found_minorrowminornonzeroevaluationdeterminanths mdr_fb_found_minorrowminornonzeroevaluationdeterminanths mdr_fc_found_minorrowminornonzeroevaluationdeterminanths. (((mdr_d_found_minorrowminornonzeroevaluationdeterminanth) = S (mdr_q_found_minorrowminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_found_minorrowminornonzeroevaluationdeterminanthsc. (exists mdr_gap_found_minorrowminornonzeroevaluationdeterminanthscj. mdr_gap_found_minorrowminornonzeroevaluationdeterminanthscj + S (mdr_j_found_minorrowminornonzeroevaluationdeterminanthsc) = (S (mdr_q_found_minorrowminornonzeroevaluationdeterminanths))) -> exists mdr_i_found_minorrowminornonzeroevaluationdeterminanthsc mdr_up_found_minorrowminornonzeroevaluationdeterminanthsc mdr_us_found_minorrowminornonzeroevaluationdeterminanthsc mdr_un_found_minorrowminornonzeroevaluationdeterminanthsc mdr_ut_found_minorrowminornonzeroevaluationdeterminanthsc mdr_p_found_minorrowminornonzeroevaluationdeterminanthsc mdr_n_found_minorrowminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_found_minorrowminornonzeroevaluationdeterminanthsci. mdr_gap_found_minorrowminornonzeroevaluationdeterminanthsci + S (mdr_i_found_minorrowminornonzeroevaluationdeterminanthsc) = (mdr_i_found_minorrowminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_found_minorrowminornonzeroevaluationdeterminanthscr. ((exists mdr_a_found_minorrowminornonzeroevaluationdeterminanthscrc mdr_b_found_minorrowminornonzeroevaluationdeterminanthscrc mdr_c_found_minorrowminornonzeroevaluationdeterminanthscrc mdr_e_found_minorrowminornonzeroevaluationdeterminanthscrc mdr_f_found_minorrowminornonzeroevaluationdeterminanthscrc. ((mdr_a_found_minorrowminornonzeroevaluationdeterminanthscrc = ((mdr_q_found_minorrowminornonzeroevaluationdeterminanths) + (mdr_up_found_minorrowminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_found_minorrowminornonzeroevaluationdeterminanths) + (mdr_up_found_minorrowminornonzeroevaluationdeterminanthsc)) + ((mdr_up_found_minorrowminornonzeroevaluationdeterminanthsc) + (mdr_up_found_minorrowminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_found_minorrowminornonzeroevaluationdeterminanthscrc = ((mdr_us_found_minorrowminornonzeroevaluationdeterminanthsc) + (mdr_un_found_minorrowminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_found_minorrowminornonzeroevaluationdeterminanthsc) + (mdr_un_found_minorrowminornonzeroevaluationdeterminanthsc)) + ((mdr_un_found_minorrowminornonzeroevaluationdeterminanthsc) + (mdr_un_found_minorrowminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_found_minorrowminornonzeroevaluationdeterminanthscrc = ((mdr_a_found_minorrowminornonzeroevaluationdeterminanthscrc) + (mdr_b_found_minorrowminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_found_minorrowminornonzeroevaluationdeterminanthscrc) + (mdr_b_found_minorrowminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_found_minorrowminornonzeroevaluationdeterminanthscrc) + (mdr_b_found_minorrowminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_found_minorrowminornonzeroevaluationdeterminanthscrc = ((mdr_p_found_minorrowminornonzeroevaluationdeterminanthsc) + (mdr_n_found_minorrowminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_found_minorrowminornonzeroevaluationdeterminanthsc) + (mdr_n_found_minorrowminornonzeroevaluationdeterminanthsc)) + ((mdr_n_found_minorrowminornonzeroevaluationdeterminanthsc) + (mdr_n_found_minorrowminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_found_minorrowminornonzeroevaluationdeterminanthscrc = ((mdr_ut_found_minorrowminornonzeroevaluationdeterminanthsc) + (mdr_e_found_minorrowminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_found_minorrowminornonzeroevaluationdeterminanthsc) + (mdr_e_found_minorrowminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_found_minorrowminornonzeroevaluationdeterminanthscrc) + (mdr_e_found_minorrowminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_found_minorrowminornonzeroevaluationdeterminanthscr) = ((mdr_c_found_minorrowminornonzeroevaluationdeterminanthscrc) + (mdr_f_found_minorrowminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_found_minorrowminornonzeroevaluationdeterminanthscrc) + (mdr_f_found_minorrowminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_found_minorrowminornonzeroevaluationdeterminanthscrc) + (mdr_f_found_minorrowminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_found_minorrowminornonzeroevaluationdeterminanthscrb. ff_h_mdr_found_minorrowminornonzeroevaluationdeterminanthscrb + S (mdr_z_found_minorrowminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_found_minorrowminornonzeroevaluationdeterminanthsc)) * mdr_c_found_minorrowminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_found_minorrowminornonzeroevaluationdeterminanthscrb. mdr_b_found_minorrowminornonzeroevaluationdeterminant = ff_q_mdr_found_minorrowminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_found_minorrowminornonzeroevaluationdeterminanthsc)) * mdr_c_found_minorrowminornonzeroevaluationdeterminant) + (mdr_z_found_minorrowminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_found_minorrowminornonzeroevaluationdeterminanths) * (mdr_q_found_minorrowminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive = (mdr_q_found_minorrowminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_found_minorrowminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_found_minorrowminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_found_minorrowminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_found_minorrowminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_found_minorrowminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_found_minorrowminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_found_minorrowminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_found_minorrowminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_found_minorrowminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_found_minorrowminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_found_minorrowminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_found_minorrowminornonzeroevaluationdeterminanths) * (mdr_q_found_minorrowminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative = (mdr_q_found_minorrowminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_found_minorrowminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_found_minorrowminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_found_minorrowminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_found_minorrowminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_found_minorrowminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_found_minorrowminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_found_minorrowminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_found_minorrowminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_found_minorrowminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_found_minorrowminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_found_minorrowminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_found_minorrowminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_found_minorrowminornonzeroevaluationdeterminanthscp. ff_h_mdr_found_minorrowminornonzeroevaluationdeterminanthscp + S (mdr_p_found_minorrowminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_found_minorrowminornonzeroevaluationdeterminanthsc)) * mdr_ec_found_minorrowminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_found_minorrowminornonzeroevaluationdeterminanthscp. mdr_eb_found_minorrowminornonzeroevaluationdeterminanths = ff_q_mdr_found_minorrowminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_found_minorrowminornonzeroevaluationdeterminanthsc)) * mdr_ec_found_minorrowminornonzeroevaluationdeterminanths) + (mdr_p_found_minorrowminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_found_minorrowminornonzeroevaluationdeterminanthscn. ff_h_mdr_found_minorrowminornonzeroevaluationdeterminanthscn + S (mdr_n_found_minorrowminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_found_minorrowminornonzeroevaluationdeterminanthsc)) * mdr_fc_found_minorrowminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_found_minorrowminornonzeroevaluationdeterminanthscn. mdr_fb_found_minorrowminornonzeroevaluationdeterminanths = ff_q_mdr_found_minorrowminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_found_minorrowminornonzeroevaluationdeterminanthsc)) * mdr_fc_found_minorrowminornonzeroevaluationdeterminanths) + (mdr_n_found_minorrowminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_found_minorrowminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_found_minorrowminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_found_minorrowminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_found_minorrowminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_found_minorrowminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_found_minorrowminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_found_minorrowminornonzeroevaluationdeterminanth = ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_found_minorrowminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_found_minorrowminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_found_minorrowminornonzeroevaluationdeterminanth = ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_found_minorrowminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_found_minorrowminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_found_minorrowminornonzeroevaluationdeterminanths = ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_found_minorrowminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_found_minorrowminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_found_minorrowminornonzeroevaluationdeterminanths = ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_found_minorrowminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_found_minorrowminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_found_minorrowminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_found_minorrowminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_found_minorrowminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_found_minorrowminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_found_minorrowminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_found_minorrowminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_found_minorrowminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_found_minorrowminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_found_minorrowminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_found_minorrowminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_found_minorrowminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_found_minorrowminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_found_minorrowminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_found_minorrowminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_found_minorrowminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_found_minorrowminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_found_minorrowminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_found_minorrowminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_found_minorrowminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_found_minorrowminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_found_minorrowminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_found_minorrowminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_found_minorrowminornonzeroevaluationdeterminanti. mdr_gap_found_minorrowminornonzeroevaluationdeterminanti + S (mdr_i_found_minorrowminornonzeroevaluationdeterminant) = (mdr_l_found_minorrowminornonzeroevaluationdeterminant)) /\ (exists mdr_z_found_minorrowminornonzeroevaluationdeterminantr. ((exists mdr_a_found_minorrowminornonzeroevaluationdeterminantrc mdr_b_found_minorrowminornonzeroevaluationdeterminantrc mdr_c_found_minorrowminornonzeroevaluationdeterminantrc mdr_e_found_minorrowminornonzeroevaluationdeterminantrc mdr_f_found_minorrowminornonzeroevaluationdeterminantrc. ((mdr_a_found_minorrowminornonzeroevaluationdeterminantrc = ((q) + (mdr_ub_found_minorrowminornonzeroevaluation)) * S ((q) + (mdr_ub_found_minorrowminornonzeroevaluation)) + ((mdr_ub_found_minorrowminornonzeroevaluation) + (mdr_ub_found_minorrowminornonzeroevaluation))) /\ ((mdr_b_found_minorrowminornonzeroevaluationdeterminantrc = ((mdr_uc_found_minorrowminornonzeroevaluation) + (mdr_vb_found_minorrowminornonzeroevaluation)) * S ((mdr_uc_found_minorrowminornonzeroevaluation) + (mdr_vb_found_minorrowminornonzeroevaluation)) + ((mdr_vb_found_minorrowminornonzeroevaluation) + (mdr_vb_found_minorrowminornonzeroevaluation))) /\ ((mdr_c_found_minorrowminornonzeroevaluationdeterminantrc = ((mdr_a_found_minorrowminornonzeroevaluationdeterminantrc) + (mdr_b_found_minorrowminornonzeroevaluationdeterminantrc)) * S ((mdr_a_found_minorrowminornonzeroevaluationdeterminantrc) + (mdr_b_found_minorrowminornonzeroevaluationdeterminantrc)) + ((mdr_b_found_minorrowminornonzeroevaluationdeterminantrc) + (mdr_b_found_minorrowminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_found_minorrowminornonzeroevaluationdeterminantrc = ((mdr_p_found_minorrowminornonzero) + (mdr_n_found_minorrowminornonzero)) * S ((mdr_p_found_minorrowminornonzero) + (mdr_n_found_minorrowminornonzero)) + ((mdr_n_found_minorrowminornonzero) + (mdr_n_found_minorrowminornonzero))) /\ ((mdr_f_found_minorrowminornonzeroevaluationdeterminantrc = ((mdr_vc_found_minorrowminornonzeroevaluation) + (mdr_e_found_minorrowminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_found_minorrowminornonzeroevaluation) + (mdr_e_found_minorrowminornonzeroevaluationdeterminantrc)) + ((mdr_e_found_minorrowminornonzeroevaluationdeterminantrc) + (mdr_e_found_minorrowminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_found_minorrowminornonzeroevaluationdeterminantr) = ((mdr_c_found_minorrowminornonzeroevaluationdeterminantrc) + (mdr_f_found_minorrowminornonzeroevaluationdeterminantrc)) * S ((mdr_c_found_minorrowminornonzeroevaluationdeterminantrc) + (mdr_f_found_minorrowminornonzeroevaluationdeterminantrc)) + ((mdr_f_found_minorrowminornonzeroevaluationdeterminantrc) + (mdr_f_found_minorrowminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_found_minorrowminornonzeroevaluationdeterminantrb. ff_h_mdr_found_minorrowminornonzeroevaluationdeterminantrb + S (mdr_z_found_minorrowminornonzeroevaluationdeterminantr) = S ((S (mdr_i_found_minorrowminornonzeroevaluationdeterminant)) * mdr_c_found_minorrowminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_found_minorrowminornonzeroevaluationdeterminantrb. mdr_b_found_minorrowminornonzeroevaluationdeterminant = ff_q_mdr_found_minorrowminornonzeroevaluationdeterminantrb * S ((S (mdr_i_found_minorrowminornonzeroevaluationdeterminant)) * mdr_c_found_minorrowminornonzeroevaluationdeterminant) + (mdr_z_found_minorrowminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_found_minorrowminornonzero = mdr_n_found_minorrowminornonzero))))))))))))) -> (exists mdr_rb_actual_minor mdr_rc_actual_minor mdr_cb_actual_minor mdr_cc_actual_minor. (((((forall fom_index_mrf_actual_minorminorrowsbound. (exists fom_gap_mrf_actual_minorminorrowsbound_index_bound. fom_gap_mrf_actual_minorminorrowsbound_index_bound + S (fom_index_mrf_actual_minorminorrowsbound) = q) -> exists fom_value_mrf_actual_minorminorrowsbound. ((((exists fom_beta_height_mrf_actual_minorminorrowsbound_entry. fom_beta_height_mrf_actual_minorminorrowsbound_entry + S (fom_value_mrf_actual_minorminorrowsbound) = S ((S (fom_index_mrf_actual_minorminorrowsbound)) * mdr_rc_actual_minor)) /\ exists fom_beta_quotient_mrf_actual_minorminorrowsbound_entry. mdr_rb_actual_minor = fom_beta_quotient_mrf_actual_minorminorrowsbound_entry * S ((S (fom_index_mrf_actual_minorminorrowsbound)) * mdr_rc_actual_minor) + (fom_value_mrf_actual_minorminorrowsbound))) /\ (exists fom_gap_mrf_actual_minorminorrowsbound_value_bound. fom_gap_mrf_actual_minorminorrowsbound_value_bound + S (fom_value_mrf_actual_minorminorrowsbound) = r))) /\ (forall mdr_i_actual_minorminorrowsdistinct mdr_j_actual_minorminorrowsdistinct mdr_a_actual_minorminorrowsdistinct. (exists mdr_gap_actual_minorminorrowsdistincti. mdr_gap_actual_minorminorrowsdistincti + S (mdr_i_actual_minorminorrowsdistinct) = (q)) -> (exists mdr_gap_actual_minorminorrowsdistinctj. mdr_gap_actual_minorminorrowsdistinctj + S (mdr_j_actual_minorminorrowsdistinct) = (q)) -> (((exists ff_h_mdr_actual_minorminorrowsdistinctfirst. ff_h_mdr_actual_minorminorrowsdistinctfirst + S (mdr_a_actual_minorminorrowsdistinct) = S ((S (mdr_i_actual_minorminorrowsdistinct)) * mdr_rc_actual_minor)) /\ exists ff_q_mdr_actual_minorminorrowsdistinctfirst. mdr_rb_actual_minor = ff_q_mdr_actual_minorminorrowsdistinctfirst * S ((S (mdr_i_actual_minorminorrowsdistinct)) * mdr_rc_actual_minor) + (mdr_a_actual_minorminorrowsdistinct))) -> (((exists ff_h_mdr_actual_minorminorrowsdistinctsecond. ff_h_mdr_actual_minorminorrowsdistinctsecond + S (mdr_a_actual_minorminorrowsdistinct) = S ((S (mdr_j_actual_minorminorrowsdistinct)) * mdr_rc_actual_minor)) /\ exists ff_q_mdr_actual_minorminorrowsdistinctsecond. mdr_rb_actual_minor = ff_q_mdr_actual_minorminorrowsdistinctsecond * S ((S (mdr_j_actual_minorminorrowsdistinct)) * mdr_rc_actual_minor) + (mdr_a_actual_minorminorrowsdistinct))) -> mdr_i_actual_minorminorrowsdistinct = mdr_j_actual_minorminorrowsdistinct))) /\ ((((forall fom_index_mrf_actual_minorminorcolumnsbound. (exists fom_gap_mrf_actual_minorminorcolumnsbound_index_bound. fom_gap_mrf_actual_minorminorcolumnsbound_index_bound + S (fom_index_mrf_actual_minorminorcolumnsbound) = q) -> exists fom_value_mrf_actual_minorminorcolumnsbound. ((((exists fom_beta_height_mrf_actual_minorminorcolumnsbound_entry. fom_beta_height_mrf_actual_minorminorcolumnsbound_entry + S (fom_value_mrf_actual_minorminorcolumnsbound) = S ((S (fom_index_mrf_actual_minorminorcolumnsbound)) * mdr_cc_actual_minor)) /\ exists fom_beta_quotient_mrf_actual_minorminorcolumnsbound_entry. mdr_cb_actual_minor = fom_beta_quotient_mrf_actual_minorminorcolumnsbound_entry * S ((S (fom_index_mrf_actual_minorminorcolumnsbound)) * mdr_cc_actual_minor) + (fom_value_mrf_actual_minorminorcolumnsbound))) /\ (exists fom_gap_mrf_actual_minorminorcolumnsbound_value_bound. fom_gap_mrf_actual_minorminorcolumnsbound_value_bound + S (fom_value_mrf_actual_minorminorcolumnsbound) = w))) /\ (forall mdr_i_actual_minorminorcolumnsdistinct mdr_j_actual_minorminorcolumnsdistinct mdr_a_actual_minorminorcolumnsdistinct. (exists mdr_gap_actual_minorminorcolumnsdistincti. mdr_gap_actual_minorminorcolumnsdistincti + S (mdr_i_actual_minorminorcolumnsdistinct) = (q)) -> (exists mdr_gap_actual_minorminorcolumnsdistinctj. mdr_gap_actual_minorminorcolumnsdistinctj + S (mdr_j_actual_minorminorcolumnsdistinct) = (q)) -> (((exists ff_h_mdr_actual_minorminorcolumnsdistinctfirst. ff_h_mdr_actual_minorminorcolumnsdistinctfirst + S (mdr_a_actual_minorminorcolumnsdistinct) = S ((S (mdr_i_actual_minorminorcolumnsdistinct)) * mdr_cc_actual_minor)) /\ exists ff_q_mdr_actual_minorminorcolumnsdistinctfirst. mdr_cb_actual_minor = ff_q_mdr_actual_minorminorcolumnsdistinctfirst * S ((S (mdr_i_actual_minorminorcolumnsdistinct)) * mdr_cc_actual_minor) + (mdr_a_actual_minorminorcolumnsdistinct))) -> (((exists ff_h_mdr_actual_minorminorcolumnsdistinctsecond. ff_h_mdr_actual_minorminorcolumnsdistinctsecond + S (mdr_a_actual_minorminorcolumnsdistinct) = S ((S (mdr_j_actual_minorminorcolumnsdistinct)) * mdr_cc_actual_minor)) /\ exists ff_q_mdr_actual_minorminorcolumnsdistinctsecond. mdr_cb_actual_minor = ff_q_mdr_actual_minorminorcolumnsdistinctsecond * S ((S (mdr_j_actual_minorminorcolumnsdistinct)) * mdr_cc_actual_minor) + (mdr_a_actual_minorminorcolumnsdistinct))) -> mdr_i_actual_minorminorcolumnsdistinct = mdr_j_actual_minorminorcolumnsdistinct))) /\ (exists mdr_p_actual_minorminornonzero mdr_n_actual_minorminornonzero. ((exists mdr_ub_actual_minorminornonzeroevaluation mdr_uc_actual_minorminornonzeroevaluation mdr_vb_actual_minorminornonzeroevaluation mdr_vc_actual_minorminornonzeroevaluation. ((((forall mdr_i_actual_minorminornonzeroevaluationmatrixpositive. (exists mdr_gap_actual_minorminornonzeroevaluationmatrixpositivebound. mdr_gap_actual_minorminornonzeroevaluationmatrixpositivebound + S (mdr_i_actual_minorminornonzeroevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_actual_minorminornonzeroevaluationmatrixpositive. (((exists mdr_r_actual_minorminornonzeroevaluationmatrixpositivepoint mdr_s_actual_minorminornonzeroevaluationmatrixpositivepoint mdr_u_actual_minorminornonzeroevaluationmatrixpositivepoint mdr_v_actual_minorminornonzeroevaluationmatrixpositivepoint. ((mdr_i_actual_minorminornonzeroevaluationmatrixpositive = (q) * mdr_r_actual_minorminornonzeroevaluationmatrixpositivepoint + mdr_s_actual_minorminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_actual_minorminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_actual_minorminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_actual_minorminornonzeroevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_actual_minorminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_actual_minorminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_actual_minorminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_actual_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_actual_minor)) /\ exists ff_q_mdr_actual_minorminornonzeroevaluationmatrixpositivepointrow_index. mdr_rb_actual_minor = ff_q_mdr_actual_minorminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_actual_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_actual_minor) + (mdr_u_actual_minorminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_actual_minorminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_actual_minorminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_actual_minorminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_actual_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_actual_minor)) /\ exists ff_q_mdr_actual_minorminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_actual_minor = ff_q_mdr_actual_minorminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_actual_minorminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_actual_minor) + (mdr_v_actual_minorminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_actual_minorminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_actual_minorminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_actual_minorminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_actual_minorminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_actual_minorminornonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_actual_minorminornonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_actual_minorminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_actual_minorminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_actual_minorminornonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_actual_minorminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_actual_minorminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_actual_minorminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_actual_minorminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_actual_minorminornonzeroevaluationmatrixpositive)) * mdr_uc_actual_minorminornonzeroevaluation)) /\ exists ff_q_mdr_actual_minorminornonzeroevaluationmatrixpositiveoutput. mdr_ub_actual_minorminornonzeroevaluation = ff_q_mdr_actual_minorminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_actual_minorminornonzeroevaluationmatrixpositive)) * mdr_uc_actual_minorminornonzeroevaluation) + (mdr_a_actual_minorminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_actual_minorminornonzeroevaluationmatrixnegative. (exists mdr_gap_actual_minorminornonzeroevaluationmatrixnegativebound. mdr_gap_actual_minorminornonzeroevaluationmatrixnegativebound + S (mdr_i_actual_minorminornonzeroevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_actual_minorminornonzeroevaluationmatrixnegative. (((exists mdr_r_actual_minorminornonzeroevaluationmatrixnegativepoint mdr_s_actual_minorminornonzeroevaluationmatrixnegativepoint mdr_u_actual_minorminornonzeroevaluationmatrixnegativepoint mdr_v_actual_minorminornonzeroevaluationmatrixnegativepoint. ((mdr_i_actual_minorminornonzeroevaluationmatrixnegative = (q) * mdr_r_actual_minorminornonzeroevaluationmatrixnegativepoint + mdr_s_actual_minorminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_actual_minorminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_actual_minorminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_actual_minorminornonzeroevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_actual_minorminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_actual_minorminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_actual_minorminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_actual_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_actual_minor)) /\ exists ff_q_mdr_actual_minorminornonzeroevaluationmatrixnegativepointrow_index. mdr_rb_actual_minor = ff_q_mdr_actual_minorminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_actual_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_actual_minor) + (mdr_u_actual_minorminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_actual_minorminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_actual_minorminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_actual_minorminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_actual_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_actual_minor)) /\ exists ff_q_mdr_actual_minorminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_actual_minor = ff_q_mdr_actual_minorminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_actual_minorminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_actual_minor) + (mdr_v_actual_minorminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_actual_minorminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_actual_minorminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_actual_minorminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_actual_minorminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_actual_minorminornonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_actual_minorminornonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_actual_minorminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_actual_minorminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_actual_minorminornonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_actual_minorminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_actual_minorminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_actual_minorminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_actual_minorminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_actual_minorminornonzeroevaluationmatrixnegative)) * mdr_vc_actual_minorminornonzeroevaluation)) /\ exists ff_q_mdr_actual_minorminornonzeroevaluationmatrixnegativeoutput. mdr_vb_actual_minorminornonzeroevaluation = ff_q_mdr_actual_minorminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_actual_minorminornonzeroevaluationmatrixnegative)) * mdr_vc_actual_minorminornonzeroevaluation) + (mdr_a_actual_minorminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_actual_minorminornonzeroevaluationdeterminant mdr_c_actual_minorminornonzeroevaluationdeterminant mdr_l_actual_minorminornonzeroevaluationdeterminant mdr_i_actual_minorminornonzeroevaluationdeterminant. ((forall mdr_i_actual_minorminornonzeroevaluationdeterminanth. (exists mdr_gap_actual_minorminornonzeroevaluationdeterminanthi. mdr_gap_actual_minorminornonzeroevaluationdeterminanthi + S (mdr_i_actual_minorminornonzeroevaluationdeterminanth) = (mdr_l_actual_minorminornonzeroevaluationdeterminant)) -> exists mdr_d_actual_minorminornonzeroevaluationdeterminanth mdr_pb_actual_minorminornonzeroevaluationdeterminanth mdr_pc_actual_minorminornonzeroevaluationdeterminanth mdr_nb_actual_minorminornonzeroevaluationdeterminanth mdr_nc_actual_minorminornonzeroevaluationdeterminanth mdr_p_actual_minorminornonzeroevaluationdeterminanth mdr_n_actual_minorminornonzeroevaluationdeterminanth. ((exists mdr_z_actual_minorminornonzeroevaluationdeterminanthr. ((exists mdr_a_actual_minorminornonzeroevaluationdeterminanthrc mdr_b_actual_minorminornonzeroevaluationdeterminanthrc mdr_c_actual_minorminornonzeroevaluationdeterminanthrc mdr_e_actual_minorminornonzeroevaluationdeterminanthrc mdr_f_actual_minorminornonzeroevaluationdeterminanthrc. ((mdr_a_actual_minorminornonzeroevaluationdeterminanthrc = ((mdr_d_actual_minorminornonzeroevaluationdeterminanth) + (mdr_pb_actual_minorminornonzeroevaluationdeterminanth)) * S ((mdr_d_actual_minorminornonzeroevaluationdeterminanth) + (mdr_pb_actual_minorminornonzeroevaluationdeterminanth)) + ((mdr_pb_actual_minorminornonzeroevaluationdeterminanth) + (mdr_pb_actual_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_b_actual_minorminornonzeroevaluationdeterminanthrc = ((mdr_pc_actual_minorminornonzeroevaluationdeterminanth) + (mdr_nb_actual_minorminornonzeroevaluationdeterminanth)) * S ((mdr_pc_actual_minorminornonzeroevaluationdeterminanth) + (mdr_nb_actual_minorminornonzeroevaluationdeterminanth)) + ((mdr_nb_actual_minorminornonzeroevaluationdeterminanth) + (mdr_nb_actual_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_c_actual_minorminornonzeroevaluationdeterminanthrc = ((mdr_a_actual_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_actual_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_actual_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_actual_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_b_actual_minorminornonzeroevaluationdeterminanthrc) + (mdr_b_actual_minorminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_actual_minorminornonzeroevaluationdeterminanthrc = ((mdr_p_actual_minorminornonzeroevaluationdeterminanth) + (mdr_n_actual_minorminornonzeroevaluationdeterminanth)) * S ((mdr_p_actual_minorminornonzeroevaluationdeterminanth) + (mdr_n_actual_minorminornonzeroevaluationdeterminanth)) + ((mdr_n_actual_minorminornonzeroevaluationdeterminanth) + (mdr_n_actual_minorminornonzeroevaluationdeterminanth))) /\ ((mdr_f_actual_minorminornonzeroevaluationdeterminanthrc = ((mdr_nc_actual_minorminornonzeroevaluationdeterminanth) + (mdr_e_actual_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_actual_minorminornonzeroevaluationdeterminanth) + (mdr_e_actual_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_e_actual_minorminornonzeroevaluationdeterminanthrc) + (mdr_e_actual_minorminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_actual_minorminornonzeroevaluationdeterminanthr) = ((mdr_c_actual_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_actual_minorminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_actual_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_actual_minorminornonzeroevaluationdeterminanthrc)) + ((mdr_f_actual_minorminornonzeroevaluationdeterminanthrc) + (mdr_f_actual_minorminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_actual_minorminornonzeroevaluationdeterminanthrb. ff_h_mdr_actual_minorminornonzeroevaluationdeterminanthrb + S (mdr_z_actual_minorminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_actual_minorminornonzeroevaluationdeterminanth)) * mdr_c_actual_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_actual_minorminornonzeroevaluationdeterminanthrb. mdr_b_actual_minorminornonzeroevaluationdeterminant = ff_q_mdr_actual_minorminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_actual_minorminornonzeroevaluationdeterminanth)) * mdr_c_actual_minorminornonzeroevaluationdeterminant) + (mdr_z_actual_minorminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_actual_minorminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_actual_minorminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_actual_minorminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_actual_minorminornonzeroevaluationdeterminanths mdr_eb_actual_minorminornonzeroevaluationdeterminanths mdr_ec_actual_minorminornonzeroevaluationdeterminanths mdr_fb_actual_minorminornonzeroevaluationdeterminanths mdr_fc_actual_minorminornonzeroevaluationdeterminanths. (((mdr_d_actual_minorminornonzeroevaluationdeterminanth) = S (mdr_q_actual_minorminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_actual_minorminornonzeroevaluationdeterminanthsc. (exists mdr_gap_actual_minorminornonzeroevaluationdeterminanthscj. mdr_gap_actual_minorminornonzeroevaluationdeterminanthscj + S (mdr_j_actual_minorminornonzeroevaluationdeterminanthsc) = (S (mdr_q_actual_minorminornonzeroevaluationdeterminanths))) -> exists mdr_i_actual_minorminornonzeroevaluationdeterminanthsc mdr_up_actual_minorminornonzeroevaluationdeterminanthsc mdr_us_actual_minorminornonzeroevaluationdeterminanthsc mdr_un_actual_minorminornonzeroevaluationdeterminanthsc mdr_ut_actual_minorminornonzeroevaluationdeterminanthsc mdr_p_actual_minorminornonzeroevaluationdeterminanthsc mdr_n_actual_minorminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_actual_minorminornonzeroevaluationdeterminanthsci. mdr_gap_actual_minorminornonzeroevaluationdeterminanthsci + S (mdr_i_actual_minorminornonzeroevaluationdeterminanthsc) = (mdr_i_actual_minorminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_actual_minorminornonzeroevaluationdeterminanthscr. ((exists mdr_a_actual_minorminornonzeroevaluationdeterminanthscrc mdr_b_actual_minorminornonzeroevaluationdeterminanthscrc mdr_c_actual_minorminornonzeroevaluationdeterminanthscrc mdr_e_actual_minorminornonzeroevaluationdeterminanthscrc mdr_f_actual_minorminornonzeroevaluationdeterminanthscrc. ((mdr_a_actual_minorminornonzeroevaluationdeterminanthscrc = ((mdr_q_actual_minorminornonzeroevaluationdeterminanths) + (mdr_up_actual_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_actual_minorminornonzeroevaluationdeterminanths) + (mdr_up_actual_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_up_actual_minorminornonzeroevaluationdeterminanthsc) + (mdr_up_actual_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_actual_minorminornonzeroevaluationdeterminanthscrc = ((mdr_us_actual_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_actual_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_actual_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_actual_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_un_actual_minorminornonzeroevaluationdeterminanthsc) + (mdr_un_actual_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_actual_minorminornonzeroevaluationdeterminanthscrc = ((mdr_a_actual_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_actual_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_actual_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_actual_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_actual_minorminornonzeroevaluationdeterminanthscrc) + (mdr_b_actual_minorminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_actual_minorminornonzeroevaluationdeterminanthscrc = ((mdr_p_actual_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_actual_minorminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_actual_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_actual_minorminornonzeroevaluationdeterminanthsc)) + ((mdr_n_actual_minorminornonzeroevaluationdeterminanthsc) + (mdr_n_actual_minorminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_actual_minorminornonzeroevaluationdeterminanthscrc = ((mdr_ut_actual_minorminornonzeroevaluationdeterminanthsc) + (mdr_e_actual_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_actual_minorminornonzeroevaluationdeterminanthsc) + (mdr_e_actual_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_actual_minorminornonzeroevaluationdeterminanthscrc) + (mdr_e_actual_minorminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_actual_minorminornonzeroevaluationdeterminanthscr) = ((mdr_c_actual_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_actual_minorminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_actual_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_actual_minorminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_actual_minorminornonzeroevaluationdeterminanthscrc) + (mdr_f_actual_minorminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_actual_minorminornonzeroevaluationdeterminanthscrb. ff_h_mdr_actual_minorminornonzeroevaluationdeterminanthscrb + S (mdr_z_actual_minorminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_actual_minorminornonzeroevaluationdeterminanthsc)) * mdr_c_actual_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_actual_minorminornonzeroevaluationdeterminanthscrb. mdr_b_actual_minorminornonzeroevaluationdeterminant = ff_q_mdr_actual_minorminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_actual_minorminornonzeroevaluationdeterminanthsc)) * mdr_c_actual_minorminornonzeroevaluationdeterminant) + (mdr_z_actual_minorminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_actual_minorminornonzeroevaluationdeterminanths) * (mdr_q_actual_minorminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive = (mdr_q_actual_minorminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_actual_minorminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_actual_minorminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_actual_minorminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_actual_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_actual_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_actual_minorminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_actual_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_actual_minorminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_actual_minorminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_actual_minorminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_actual_minorminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_actual_minorminornonzeroevaluationdeterminanths) * (mdr_q_actual_minorminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative = (mdr_q_actual_minorminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_actual_minorminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_actual_minorminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_actual_minorminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_actual_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_actual_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_actual_minorminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_actual_minorminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_actual_minorminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_actual_minorminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_actual_minorminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_actual_minorminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_actual_minorminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_actual_minorminornonzeroevaluationdeterminanthscp. ff_h_mdr_actual_minorminornonzeroevaluationdeterminanthscp + S (mdr_p_actual_minorminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_actual_minorminornonzeroevaluationdeterminanthsc)) * mdr_ec_actual_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_actual_minorminornonzeroevaluationdeterminanthscp. mdr_eb_actual_minorminornonzeroevaluationdeterminanths = ff_q_mdr_actual_minorminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_actual_minorminornonzeroevaluationdeterminanthsc)) * mdr_ec_actual_minorminornonzeroevaluationdeterminanths) + (mdr_p_actual_minorminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_actual_minorminornonzeroevaluationdeterminanthscn. ff_h_mdr_actual_minorminornonzeroevaluationdeterminanthscn + S (mdr_n_actual_minorminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_actual_minorminornonzeroevaluationdeterminanthsc)) * mdr_fc_actual_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_actual_minorminornonzeroevaluationdeterminanthscn. mdr_fb_actual_minorminornonzeroevaluationdeterminanths = ff_q_mdr_actual_minorminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_actual_minorminornonzeroevaluationdeterminanthsc)) * mdr_fc_actual_minorminornonzeroevaluationdeterminanths) + (mdr_n_actual_minorminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_actual_minorminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_actual_minorminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_actual_minorminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_actual_minorminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_actual_minorminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_actual_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_actual_minorminornonzeroevaluationdeterminanth = ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_actual_minorminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_actual_minorminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_actual_minorminornonzeroevaluationdeterminanth = ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_actual_minorminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_actual_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_actual_minorminornonzeroevaluationdeterminanths = ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_actual_minorminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_actual_minorminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_actual_minorminornonzeroevaluationdeterminanths = ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_actual_minorminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_actual_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_actual_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_actual_minorminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_actual_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_actual_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_actual_minorminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_actual_minorminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_actual_minorminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_actual_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_actual_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_actual_minorminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_actual_minorminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_actual_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_actual_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_actual_minorminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_actual_minorminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_actual_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_actual_minorminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_actual_minorminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_actual_minorminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_actual_minorminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_actual_minorminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_actual_minorminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_actual_minorminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_actual_minorminornonzeroevaluationdeterminanti. mdr_gap_actual_minorminornonzeroevaluationdeterminanti + S (mdr_i_actual_minorminornonzeroevaluationdeterminant) = (mdr_l_actual_minorminornonzeroevaluationdeterminant)) /\ (exists mdr_z_actual_minorminornonzeroevaluationdeterminantr. ((exists mdr_a_actual_minorminornonzeroevaluationdeterminantrc mdr_b_actual_minorminornonzeroevaluationdeterminantrc mdr_c_actual_minorminornonzeroevaluationdeterminantrc mdr_e_actual_minorminornonzeroevaluationdeterminantrc mdr_f_actual_minorminornonzeroevaluationdeterminantrc. ((mdr_a_actual_minorminornonzeroevaluationdeterminantrc = ((q) + (mdr_ub_actual_minorminornonzeroevaluation)) * S ((q) + (mdr_ub_actual_minorminornonzeroevaluation)) + ((mdr_ub_actual_minorminornonzeroevaluation) + (mdr_ub_actual_minorminornonzeroevaluation))) /\ ((mdr_b_actual_minorminornonzeroevaluationdeterminantrc = ((mdr_uc_actual_minorminornonzeroevaluation) + (mdr_vb_actual_minorminornonzeroevaluation)) * S ((mdr_uc_actual_minorminornonzeroevaluation) + (mdr_vb_actual_minorminornonzeroevaluation)) + ((mdr_vb_actual_minorminornonzeroevaluation) + (mdr_vb_actual_minorminornonzeroevaluation))) /\ ((mdr_c_actual_minorminornonzeroevaluationdeterminantrc = ((mdr_a_actual_minorminornonzeroevaluationdeterminantrc) + (mdr_b_actual_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_a_actual_minorminornonzeroevaluationdeterminantrc) + (mdr_b_actual_minorminornonzeroevaluationdeterminantrc)) + ((mdr_b_actual_minorminornonzeroevaluationdeterminantrc) + (mdr_b_actual_minorminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_actual_minorminornonzeroevaluationdeterminantrc = ((mdr_p_actual_minorminornonzero) + (mdr_n_actual_minorminornonzero)) * S ((mdr_p_actual_minorminornonzero) + (mdr_n_actual_minorminornonzero)) + ((mdr_n_actual_minorminornonzero) + (mdr_n_actual_minorminornonzero))) /\ ((mdr_f_actual_minorminornonzeroevaluationdeterminantrc = ((mdr_vc_actual_minorminornonzeroevaluation) + (mdr_e_actual_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_actual_minorminornonzeroevaluation) + (mdr_e_actual_minorminornonzeroevaluationdeterminantrc)) + ((mdr_e_actual_minorminornonzeroevaluationdeterminantrc) + (mdr_e_actual_minorminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_actual_minorminornonzeroevaluationdeterminantr) = ((mdr_c_actual_minorminornonzeroevaluationdeterminantrc) + (mdr_f_actual_minorminornonzeroevaluationdeterminantrc)) * S ((mdr_c_actual_minorminornonzeroevaluationdeterminantrc) + (mdr_f_actual_minorminornonzeroevaluationdeterminantrc)) + ((mdr_f_actual_minorminornonzeroevaluationdeterminantrc) + (mdr_f_actual_minorminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_actual_minorminornonzeroevaluationdeterminantrb. ff_h_mdr_actual_minorminornonzeroevaluationdeterminantrb + S (mdr_z_actual_minorminornonzeroevaluationdeterminantr) = S ((S (mdr_i_actual_minorminornonzeroevaluationdeterminant)) * mdr_c_actual_minorminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_actual_minorminornonzeroevaluationdeterminantrb. mdr_b_actual_minorminornonzeroevaluationdeterminant = ff_q_mdr_actual_minorminornonzeroevaluationdeterminantrb * S ((S (mdr_i_actual_minorminornonzeroevaluationdeterminant)) * mdr_c_actual_minorminornonzeroevaluationdeterminant) + (mdr_z_actual_minorminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_actual_minorminornonzero = mdr_n_actual_minorminornonzero))))))))