matrix_rank_selected_column_search_decidable

Exact expanded first-order arithmetic statement

forall pb pc nb nc r w q rb rc cc L. (exists mdr_a_matrix_rank_selected_column_search_decidableyes. (((exists mdr_gap_matrix_rank_selected_column_search_decidableyesbound. mdr_gap_matrix_rank_selected_column_search_decidableyesbound + S (mdr_a_matrix_rank_selected_column_search_decidableyes) = (L)) /\ (((((forall fom_index_mrf_column_candidaterowsbound. (exists fom_gap_mrf_column_candidaterowsbound_index_bound. fom_gap_mrf_column_candidaterowsbound_index_bound + S (fom_index_mrf_column_candidaterowsbound) = q) -> exists fom_value_mrf_column_candidaterowsbound. ((((exists fom_beta_height_mrf_column_candidaterowsbound_entry. fom_beta_height_mrf_column_candidaterowsbound_entry + S (fom_value_mrf_column_candidaterowsbound) = S ((S (fom_index_mrf_column_candidaterowsbound)) * rc)) /\ exists fom_beta_quotient_mrf_column_candidaterowsbound_entry. rb = fom_beta_quotient_mrf_column_candidaterowsbound_entry * S ((S (fom_index_mrf_column_candidaterowsbound)) * rc) + (fom_value_mrf_column_candidaterowsbound))) /\ (exists fom_gap_mrf_column_candidaterowsbound_value_bound. fom_gap_mrf_column_candidaterowsbound_value_bound + S (fom_value_mrf_column_candidaterowsbound) = r))) /\ (forall mdr_i_column_candidaterowsdistinct mdr_j_column_candidaterowsdistinct mdr_a_column_candidaterowsdistinct. (exists mdr_gap_column_candidaterowsdistincti. mdr_gap_column_candidaterowsdistincti + S (mdr_i_column_candidaterowsdistinct) = (q)) -> (exists mdr_gap_column_candidaterowsdistinctj. mdr_gap_column_candidaterowsdistinctj + S (mdr_j_column_candidaterowsdistinct) = (q)) -> (((exists ff_h_mdr_column_candidaterowsdistinctfirst. ff_h_mdr_column_candidaterowsdistinctfirst + S (mdr_a_column_candidaterowsdistinct) = S ((S (mdr_i_column_candidaterowsdistinct)) * rc)) /\ exists ff_q_mdr_column_candidaterowsdistinctfirst. rb = ff_q_mdr_column_candidaterowsdistinctfirst * S ((S (mdr_i_column_candidaterowsdistinct)) * rc) + (mdr_a_column_candidaterowsdistinct))) -> (((exists ff_h_mdr_column_candidaterowsdistinctsecond. ff_h_mdr_column_candidaterowsdistinctsecond + S (mdr_a_column_candidaterowsdistinct) = S ((S (mdr_j_column_candidaterowsdistinct)) * rc)) /\ exists ff_q_mdr_column_candidaterowsdistinctsecond. rb = ff_q_mdr_column_candidaterowsdistinctsecond * S ((S (mdr_j_column_candidaterowsdistinct)) * rc) + (mdr_a_column_candidaterowsdistinct))) -> mdr_i_column_candidaterowsdistinct = mdr_j_column_candidaterowsdistinct))) /\ ((((forall fom_index_mrf_column_candidatecolumnsbound. (exists fom_gap_mrf_column_candidatecolumnsbound_index_bound. fom_gap_mrf_column_candidatecolumnsbound_index_bound + S (fom_index_mrf_column_candidatecolumnsbound) = q) -> exists fom_value_mrf_column_candidatecolumnsbound. ((((exists fom_beta_height_mrf_column_candidatecolumnsbound_entry. fom_beta_height_mrf_column_candidatecolumnsbound_entry + S (fom_value_mrf_column_candidatecolumnsbound) = S ((S (fom_index_mrf_column_candidatecolumnsbound)) * cc)) /\ exists fom_beta_quotient_mrf_column_candidatecolumnsbound_entry. mdr_a_matrix_rank_selected_column_search_decidableyes = fom_beta_quotient_mrf_column_candidatecolumnsbound_entry * S ((S (fom_index_mrf_column_candidatecolumnsbound)) * cc) + (fom_value_mrf_column_candidatecolumnsbound))) /\ (exists fom_gap_mrf_column_candidatecolumnsbound_value_bound. fom_gap_mrf_column_candidatecolumnsbound_value_bound + S (fom_value_mrf_column_candidatecolumnsbound) = w))) /\ (forall mdr_i_column_candidatecolumnsdistinct mdr_j_column_candidatecolumnsdistinct mdr_a_column_candidatecolumnsdistinct. (exists mdr_gap_column_candidatecolumnsdistincti. mdr_gap_column_candidatecolumnsdistincti + S (mdr_i_column_candidatecolumnsdistinct) = (q)) -> (exists mdr_gap_column_candidatecolumnsdistinctj. mdr_gap_column_candidatecolumnsdistinctj + S (mdr_j_column_candidatecolumnsdistinct) = (q)) -> (((exists ff_h_mdr_column_candidatecolumnsdistinctfirst. ff_h_mdr_column_candidatecolumnsdistinctfirst + S (mdr_a_column_candidatecolumnsdistinct) = S ((S (mdr_i_column_candidatecolumnsdistinct)) * cc)) /\ exists ff_q_mdr_column_candidatecolumnsdistinctfirst. mdr_a_matrix_rank_selected_column_search_decidableyes = ff_q_mdr_column_candidatecolumnsdistinctfirst * S ((S (mdr_i_column_candidatecolumnsdistinct)) * cc) + (mdr_a_column_candidatecolumnsdistinct))) -> (((exists ff_h_mdr_column_candidatecolumnsdistinctsecond. ff_h_mdr_column_candidatecolumnsdistinctsecond + S (mdr_a_column_candidatecolumnsdistinct) = S ((S (mdr_j_column_candidatecolumnsdistinct)) * cc)) /\ exists ff_q_mdr_column_candidatecolumnsdistinctsecond. mdr_a_matrix_rank_selected_column_search_decidableyes = ff_q_mdr_column_candidatecolumnsdistinctsecond * S ((S (mdr_j_column_candidatecolumnsdistinct)) * cc) + (mdr_a_column_candidatecolumnsdistinct))) -> mdr_i_column_candidatecolumnsdistinct = mdr_j_column_candidatecolumnsdistinct))) /\ (exists mdr_p_column_candidatenonzero mdr_n_column_candidatenonzero. ((exists mdr_ub_column_candidatenonzeroevaluation mdr_uc_column_candidatenonzeroevaluation mdr_vb_column_candidatenonzeroevaluation mdr_vc_column_candidatenonzeroevaluation. ((((forall mdr_i_column_candidatenonzeroevaluationmatrixpositive. (exists mdr_gap_column_candidatenonzeroevaluationmatrixpositivebound. mdr_gap_column_candidatenonzeroevaluationmatrixpositivebound + S (mdr_i_column_candidatenonzeroevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_column_candidatenonzeroevaluationmatrixpositive. (((exists mdr_r_column_candidatenonzeroevaluationmatrixpositivepoint mdr_s_column_candidatenonzeroevaluationmatrixpositivepoint mdr_u_column_candidatenonzeroevaluationmatrixpositivepoint mdr_v_column_candidatenonzeroevaluationmatrixpositivepoint. ((mdr_i_column_candidatenonzeroevaluationmatrixpositive = (q) * mdr_r_column_candidatenonzeroevaluationmatrixpositivepoint + mdr_s_column_candidatenonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_column_candidatenonzeroevaluationmatrixpositivepointcolumn. mdr_gap_column_candidatenonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_column_candidatenonzeroevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_column_candidatenonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_column_candidatenonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_column_candidatenonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_column_candidatenonzeroevaluationmatrixpositivepoint)) * rc)) /\ exists ff_q_mdr_column_candidatenonzeroevaluationmatrixpositivepointrow_index. rb = ff_q_mdr_column_candidatenonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_column_candidatenonzeroevaluationmatrixpositivepoint)) * rc) + (mdr_u_column_candidatenonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_column_candidatenonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_column_candidatenonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_column_candidatenonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_column_candidatenonzeroevaluationmatrixpositivepoint)) * cc)) /\ exists ff_q_mdr_column_candidatenonzeroevaluationmatrixpositivepointcolumn_index. mdr_a_matrix_rank_selected_column_search_decidableyes = ff_q_mdr_column_candidatenonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_column_candidatenonzeroevaluationmatrixpositivepoint)) * cc) + (mdr_v_column_candidatenonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_column_candidatenonzeroevaluationmatrixpositivepointsource. ff_h_mdr_column_candidatenonzeroevaluationmatrixpositivepointsource + S (mdr_a_column_candidatenonzeroevaluationmatrixpositive) = S ((S ((mdr_u_column_candidatenonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_column_candidatenonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_column_candidatenonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_column_candidatenonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_column_candidatenonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_column_candidatenonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_column_candidatenonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_column_candidatenonzeroevaluationmatrixpositiveoutput. ff_h_mdr_column_candidatenonzeroevaluationmatrixpositiveoutput + S (mdr_a_column_candidatenonzeroevaluationmatrixpositive) = S ((S (mdr_i_column_candidatenonzeroevaluationmatrixpositive)) * mdr_uc_column_candidatenonzeroevaluation)) /\ exists ff_q_mdr_column_candidatenonzeroevaluationmatrixpositiveoutput. mdr_ub_column_candidatenonzeroevaluation = ff_q_mdr_column_candidatenonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_column_candidatenonzeroevaluationmatrixpositive)) * mdr_uc_column_candidatenonzeroevaluation) + (mdr_a_column_candidatenonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_column_candidatenonzeroevaluationmatrixnegative. (exists mdr_gap_column_candidatenonzeroevaluationmatrixnegativebound. mdr_gap_column_candidatenonzeroevaluationmatrixnegativebound + S (mdr_i_column_candidatenonzeroevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_column_candidatenonzeroevaluationmatrixnegative. (((exists mdr_r_column_candidatenonzeroevaluationmatrixnegativepoint mdr_s_column_candidatenonzeroevaluationmatrixnegativepoint mdr_u_column_candidatenonzeroevaluationmatrixnegativepoint mdr_v_column_candidatenonzeroevaluationmatrixnegativepoint. ((mdr_i_column_candidatenonzeroevaluationmatrixnegative = (q) * mdr_r_column_candidatenonzeroevaluationmatrixnegativepoint + mdr_s_column_candidatenonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_column_candidatenonzeroevaluationmatrixnegativepointcolumn. mdr_gap_column_candidatenonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_column_candidatenonzeroevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_column_candidatenonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_column_candidatenonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_column_candidatenonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_column_candidatenonzeroevaluationmatrixnegativepoint)) * rc)) /\ exists ff_q_mdr_column_candidatenonzeroevaluationmatrixnegativepointrow_index. rb = ff_q_mdr_column_candidatenonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_column_candidatenonzeroevaluationmatrixnegativepoint)) * rc) + (mdr_u_column_candidatenonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_column_candidatenonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_column_candidatenonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_column_candidatenonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_column_candidatenonzeroevaluationmatrixnegativepoint)) * cc)) /\ exists ff_q_mdr_column_candidatenonzeroevaluationmatrixnegativepointcolumn_index. mdr_a_matrix_rank_selected_column_search_decidableyes = ff_q_mdr_column_candidatenonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_column_candidatenonzeroevaluationmatrixnegativepoint)) * cc) + (mdr_v_column_candidatenonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_column_candidatenonzeroevaluationmatrixnegativepointsource. ff_h_mdr_column_candidatenonzeroevaluationmatrixnegativepointsource + S (mdr_a_column_candidatenonzeroevaluationmatrixnegative) = S ((S ((mdr_u_column_candidatenonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_column_candidatenonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_column_candidatenonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_column_candidatenonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_column_candidatenonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_column_candidatenonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_column_candidatenonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_column_candidatenonzeroevaluationmatrixnegativeoutput. ff_h_mdr_column_candidatenonzeroevaluationmatrixnegativeoutput + S (mdr_a_column_candidatenonzeroevaluationmatrixnegative) = S ((S (mdr_i_column_candidatenonzeroevaluationmatrixnegative)) * mdr_vc_column_candidatenonzeroevaluation)) /\ exists ff_q_mdr_column_candidatenonzeroevaluationmatrixnegativeoutput. mdr_vb_column_candidatenonzeroevaluation = ff_q_mdr_column_candidatenonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_column_candidatenonzeroevaluationmatrixnegative)) * mdr_vc_column_candidatenonzeroevaluation) + (mdr_a_column_candidatenonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_column_candidatenonzeroevaluationdeterminant mdr_c_column_candidatenonzeroevaluationdeterminant mdr_l_column_candidatenonzeroevaluationdeterminant mdr_i_column_candidatenonzeroevaluationdeterminant. ((forall mdr_i_column_candidatenonzeroevaluationdeterminanth. (exists mdr_gap_column_candidatenonzeroevaluationdeterminanthi. mdr_gap_column_candidatenonzeroevaluationdeterminanthi + S (mdr_i_column_candidatenonzeroevaluationdeterminanth) = (mdr_l_column_candidatenonzeroevaluationdeterminant)) -> exists mdr_d_column_candidatenonzeroevaluationdeterminanth mdr_pb_column_candidatenonzeroevaluationdeterminanth mdr_pc_column_candidatenonzeroevaluationdeterminanth mdr_nb_column_candidatenonzeroevaluationdeterminanth mdr_nc_column_candidatenonzeroevaluationdeterminanth mdr_p_column_candidatenonzeroevaluationdeterminanth mdr_n_column_candidatenonzeroevaluationdeterminanth. ((exists mdr_z_column_candidatenonzeroevaluationdeterminanthr. ((exists mdr_a_column_candidatenonzeroevaluationdeterminanthrc mdr_b_column_candidatenonzeroevaluationdeterminanthrc mdr_c_column_candidatenonzeroevaluationdeterminanthrc mdr_e_column_candidatenonzeroevaluationdeterminanthrc mdr_f_column_candidatenonzeroevaluationdeterminanthrc. ((mdr_a_column_candidatenonzeroevaluationdeterminanthrc = ((mdr_d_column_candidatenonzeroevaluationdeterminanth) + (mdr_pb_column_candidatenonzeroevaluationdeterminanth)) * S ((mdr_d_column_candidatenonzeroevaluationdeterminanth) + (mdr_pb_column_candidatenonzeroevaluationdeterminanth)) + ((mdr_pb_column_candidatenonzeroevaluationdeterminanth) + (mdr_pb_column_candidatenonzeroevaluationdeterminanth))) /\ ((mdr_b_column_candidatenonzeroevaluationdeterminanthrc = ((mdr_pc_column_candidatenonzeroevaluationdeterminanth) + (mdr_nb_column_candidatenonzeroevaluationdeterminanth)) * S ((mdr_pc_column_candidatenonzeroevaluationdeterminanth) + (mdr_nb_column_candidatenonzeroevaluationdeterminanth)) + ((mdr_nb_column_candidatenonzeroevaluationdeterminanth) + (mdr_nb_column_candidatenonzeroevaluationdeterminanth))) /\ ((mdr_c_column_candidatenonzeroevaluationdeterminanthrc = ((mdr_a_column_candidatenonzeroevaluationdeterminanthrc) + (mdr_b_column_candidatenonzeroevaluationdeterminanthrc)) * S ((mdr_a_column_candidatenonzeroevaluationdeterminanthrc) + (mdr_b_column_candidatenonzeroevaluationdeterminanthrc)) + ((mdr_b_column_candidatenonzeroevaluationdeterminanthrc) + (mdr_b_column_candidatenonzeroevaluationdeterminanthrc))) /\ ((mdr_e_column_candidatenonzeroevaluationdeterminanthrc = ((mdr_p_column_candidatenonzeroevaluationdeterminanth) + (mdr_n_column_candidatenonzeroevaluationdeterminanth)) * S ((mdr_p_column_candidatenonzeroevaluationdeterminanth) + (mdr_n_column_candidatenonzeroevaluationdeterminanth)) + ((mdr_n_column_candidatenonzeroevaluationdeterminanth) + (mdr_n_column_candidatenonzeroevaluationdeterminanth))) /\ ((mdr_f_column_candidatenonzeroevaluationdeterminanthrc = ((mdr_nc_column_candidatenonzeroevaluationdeterminanth) + (mdr_e_column_candidatenonzeroevaluationdeterminanthrc)) * S ((mdr_nc_column_candidatenonzeroevaluationdeterminanth) + (mdr_e_column_candidatenonzeroevaluationdeterminanthrc)) + ((mdr_e_column_candidatenonzeroevaluationdeterminanthrc) + (mdr_e_column_candidatenonzeroevaluationdeterminanthrc))) /\ ((mdr_z_column_candidatenonzeroevaluationdeterminanthr) = ((mdr_c_column_candidatenonzeroevaluationdeterminanthrc) + (mdr_f_column_candidatenonzeroevaluationdeterminanthrc)) * S ((mdr_c_column_candidatenonzeroevaluationdeterminanthrc) + (mdr_f_column_candidatenonzeroevaluationdeterminanthrc)) + ((mdr_f_column_candidatenonzeroevaluationdeterminanthrc) + (mdr_f_column_candidatenonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_column_candidatenonzeroevaluationdeterminanthrb. ff_h_mdr_column_candidatenonzeroevaluationdeterminanthrb + S (mdr_z_column_candidatenonzeroevaluationdeterminanthr) = S ((S (mdr_i_column_candidatenonzeroevaluationdeterminanth)) * mdr_c_column_candidatenonzeroevaluationdeterminant)) /\ exists ff_q_mdr_column_candidatenonzeroevaluationdeterminanthrb. mdr_b_column_candidatenonzeroevaluationdeterminant = ff_q_mdr_column_candidatenonzeroevaluationdeterminanthrb * S ((S (mdr_i_column_candidatenonzeroevaluationdeterminanth)) * mdr_c_column_candidatenonzeroevaluationdeterminant) + (mdr_z_column_candidatenonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_column_candidatenonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_column_candidatenonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_column_candidatenonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_column_candidatenonzeroevaluationdeterminanths mdr_eb_column_candidatenonzeroevaluationdeterminanths mdr_ec_column_candidatenonzeroevaluationdeterminanths mdr_fb_column_candidatenonzeroevaluationdeterminanths mdr_fc_column_candidatenonzeroevaluationdeterminanths. (((mdr_d_column_candidatenonzeroevaluationdeterminanth) = S (mdr_q_column_candidatenonzeroevaluationdeterminanths)) /\ ((forall mdr_j_column_candidatenonzeroevaluationdeterminanthsc. (exists mdr_gap_column_candidatenonzeroevaluationdeterminanthscj. mdr_gap_column_candidatenonzeroevaluationdeterminanthscj + S (mdr_j_column_candidatenonzeroevaluationdeterminanthsc) = (S (mdr_q_column_candidatenonzeroevaluationdeterminanths))) -> exists mdr_i_column_candidatenonzeroevaluationdeterminanthsc mdr_up_column_candidatenonzeroevaluationdeterminanthsc mdr_us_column_candidatenonzeroevaluationdeterminanthsc mdr_un_column_candidatenonzeroevaluationdeterminanthsc mdr_ut_column_candidatenonzeroevaluationdeterminanthsc mdr_p_column_candidatenonzeroevaluationdeterminanthsc mdr_n_column_candidatenonzeroevaluationdeterminanthsc. ((exists mdr_gap_column_candidatenonzeroevaluationdeterminanthsci. mdr_gap_column_candidatenonzeroevaluationdeterminanthsci + S (mdr_i_column_candidatenonzeroevaluationdeterminanthsc) = (mdr_i_column_candidatenonzeroevaluationdeterminanth)) /\ ((exists mdr_z_column_candidatenonzeroevaluationdeterminanthscr. ((exists mdr_a_column_candidatenonzeroevaluationdeterminanthscrc mdr_b_column_candidatenonzeroevaluationdeterminanthscrc mdr_c_column_candidatenonzeroevaluationdeterminanthscrc mdr_e_column_candidatenonzeroevaluationdeterminanthscrc mdr_f_column_candidatenonzeroevaluationdeterminanthscrc. ((mdr_a_column_candidatenonzeroevaluationdeterminanthscrc = ((mdr_q_column_candidatenonzeroevaluationdeterminanths) + (mdr_up_column_candidatenonzeroevaluationdeterminanthsc)) * S ((mdr_q_column_candidatenonzeroevaluationdeterminanths) + (mdr_up_column_candidatenonzeroevaluationdeterminanthsc)) + ((mdr_up_column_candidatenonzeroevaluationdeterminanthsc) + (mdr_up_column_candidatenonzeroevaluationdeterminanthsc))) /\ ((mdr_b_column_candidatenonzeroevaluationdeterminanthscrc = ((mdr_us_column_candidatenonzeroevaluationdeterminanthsc) + (mdr_un_column_candidatenonzeroevaluationdeterminanthsc)) * S ((mdr_us_column_candidatenonzeroevaluationdeterminanthsc) + (mdr_un_column_candidatenonzeroevaluationdeterminanthsc)) + ((mdr_un_column_candidatenonzeroevaluationdeterminanthsc) + (mdr_un_column_candidatenonzeroevaluationdeterminanthsc))) /\ ((mdr_c_column_candidatenonzeroevaluationdeterminanthscrc = ((mdr_a_column_candidatenonzeroevaluationdeterminanthscrc) + (mdr_b_column_candidatenonzeroevaluationdeterminanthscrc)) * S ((mdr_a_column_candidatenonzeroevaluationdeterminanthscrc) + (mdr_b_column_candidatenonzeroevaluationdeterminanthscrc)) + ((mdr_b_column_candidatenonzeroevaluationdeterminanthscrc) + (mdr_b_column_candidatenonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_column_candidatenonzeroevaluationdeterminanthscrc = ((mdr_p_column_candidatenonzeroevaluationdeterminanthsc) + (mdr_n_column_candidatenonzeroevaluationdeterminanthsc)) * S ((mdr_p_column_candidatenonzeroevaluationdeterminanthsc) + (mdr_n_column_candidatenonzeroevaluationdeterminanthsc)) + ((mdr_n_column_candidatenonzeroevaluationdeterminanthsc) + (mdr_n_column_candidatenonzeroevaluationdeterminanthsc))) /\ ((mdr_f_column_candidatenonzeroevaluationdeterminanthscrc = ((mdr_ut_column_candidatenonzeroevaluationdeterminanthsc) + (mdr_e_column_candidatenonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_column_candidatenonzeroevaluationdeterminanthsc) + (mdr_e_column_candidatenonzeroevaluationdeterminanthscrc)) + ((mdr_e_column_candidatenonzeroevaluationdeterminanthscrc) + (mdr_e_column_candidatenonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_column_candidatenonzeroevaluationdeterminanthscr) = ((mdr_c_column_candidatenonzeroevaluationdeterminanthscrc) + (mdr_f_column_candidatenonzeroevaluationdeterminanthscrc)) * S ((mdr_c_column_candidatenonzeroevaluationdeterminanthscrc) + (mdr_f_column_candidatenonzeroevaluationdeterminanthscrc)) + ((mdr_f_column_candidatenonzeroevaluationdeterminanthscrc) + (mdr_f_column_candidatenonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_column_candidatenonzeroevaluationdeterminanthscrb. ff_h_mdr_column_candidatenonzeroevaluationdeterminanthscrb + S (mdr_z_column_candidatenonzeroevaluationdeterminanthscr) = S ((S (mdr_i_column_candidatenonzeroevaluationdeterminanthsc)) * mdr_c_column_candidatenonzeroevaluationdeterminant)) /\ exists ff_q_mdr_column_candidatenonzeroevaluationdeterminanthscrb. mdr_b_column_candidatenonzeroevaluationdeterminant = ff_q_mdr_column_candidatenonzeroevaluationdeterminanthscrb * S ((S (mdr_i_column_candidatenonzeroevaluationdeterminanthsc)) * mdr_c_column_candidatenonzeroevaluationdeterminant) + (mdr_z_column_candidatenonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive) = ((mdr_q_column_candidatenonzeroevaluationdeterminanths) * (mdr_q_column_candidatenonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive = (mdr_q_column_candidatenonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive) = (mdr_q_column_candidatenonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive) = (mdr_j_column_candidatenonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_column_candidatenonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_column_candidatenonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_column_candidatenonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_column_candidatenonzeroevaluationdeterminanth = ff_q_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_column_candidatenonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_column_candidatenonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive)) * mdr_us_column_candidatenonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_target. mdr_up_column_candidatenonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive)) * mdr_us_column_candidatenonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative) = ((mdr_q_column_candidatenonzeroevaluationdeterminanths) * (mdr_q_column_candidatenonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative = (mdr_q_column_candidatenonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative) = (mdr_q_column_candidatenonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative) = (mdr_j_column_candidatenonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_column_candidatenonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_column_candidatenonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_column_candidatenonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_column_candidatenonzeroevaluationdeterminanth = ff_q_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_column_candidatenonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_column_candidatenonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative)) * mdr_ut_column_candidatenonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_target. mdr_un_column_candidatenonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative)) * mdr_ut_column_candidatenonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_column_candidatenonzeroevaluationdeterminanthscp. ff_h_mdr_column_candidatenonzeroevaluationdeterminanthscp + S (mdr_p_column_candidatenonzeroevaluationdeterminanthsc) = S ((S (mdr_j_column_candidatenonzeroevaluationdeterminanthsc)) * mdr_ec_column_candidatenonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_column_candidatenonzeroevaluationdeterminanthscp. mdr_eb_column_candidatenonzeroevaluationdeterminanths = ff_q_mdr_column_candidatenonzeroevaluationdeterminanthscp * S ((S (mdr_j_column_candidatenonzeroevaluationdeterminanthsc)) * mdr_ec_column_candidatenonzeroevaluationdeterminanths) + (mdr_p_column_candidatenonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_column_candidatenonzeroevaluationdeterminanthscn. ff_h_mdr_column_candidatenonzeroevaluationdeterminanthscn + S (mdr_n_column_candidatenonzeroevaluationdeterminanthsc) = S ((S (mdr_j_column_candidatenonzeroevaluationdeterminanthsc)) * mdr_fc_column_candidatenonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_column_candidatenonzeroevaluationdeterminanthscn. mdr_fb_column_candidatenonzeroevaluationdeterminanths = ff_q_mdr_column_candidatenonzeroevaluationdeterminanthscn * S ((S (mdr_j_column_candidatenonzeroevaluationdeterminanthsc)) * mdr_fc_column_candidatenonzeroevaluationdeterminanths) + (mdr_n_column_candidatenonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_column_candidatenonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_column_candidatenonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_column_candidatenonzeroevaluationdeterminanth = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_column_candidatenonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_column_candidatenonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_column_candidatenonzeroevaluationdeterminanth = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_column_candidatenonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_column_candidatenonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_column_candidatenonzeroevaluationdeterminanths = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_column_candidatenonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_column_candidatenonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_column_candidatenonzeroevaluationdeterminanths = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_column_candidatenonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_column_candidatenonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_column_candidatenonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_column_candidatenonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive) + (mdr_p_column_candidatenonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive = (S (mdr_q_column_candidatenonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_column_candidatenonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_column_candidatenonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_column_candidatenonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative) + (mdr_n_column_candidatenonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative = (S (mdr_q_column_candidatenonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_column_candidatenonzeroevaluationdeterminanti. mdr_gap_column_candidatenonzeroevaluationdeterminanti + S (mdr_i_column_candidatenonzeroevaluationdeterminant) = (mdr_l_column_candidatenonzeroevaluationdeterminant)) /\ (exists mdr_z_column_candidatenonzeroevaluationdeterminantr. ((exists mdr_a_column_candidatenonzeroevaluationdeterminantrc mdr_b_column_candidatenonzeroevaluationdeterminantrc mdr_c_column_candidatenonzeroevaluationdeterminantrc mdr_e_column_candidatenonzeroevaluationdeterminantrc mdr_f_column_candidatenonzeroevaluationdeterminantrc. ((mdr_a_column_candidatenonzeroevaluationdeterminantrc = ((q) + (mdr_ub_column_candidatenonzeroevaluation)) * S ((q) + (mdr_ub_column_candidatenonzeroevaluation)) + ((mdr_ub_column_candidatenonzeroevaluation) + (mdr_ub_column_candidatenonzeroevaluation))) /\ ((mdr_b_column_candidatenonzeroevaluationdeterminantrc = ((mdr_uc_column_candidatenonzeroevaluation) + (mdr_vb_column_candidatenonzeroevaluation)) * S ((mdr_uc_column_candidatenonzeroevaluation) + (mdr_vb_column_candidatenonzeroevaluation)) + ((mdr_vb_column_candidatenonzeroevaluation) + (mdr_vb_column_candidatenonzeroevaluation))) /\ ((mdr_c_column_candidatenonzeroevaluationdeterminantrc = ((mdr_a_column_candidatenonzeroevaluationdeterminantrc) + (mdr_b_column_candidatenonzeroevaluationdeterminantrc)) * S ((mdr_a_column_candidatenonzeroevaluationdeterminantrc) + (mdr_b_column_candidatenonzeroevaluationdeterminantrc)) + ((mdr_b_column_candidatenonzeroevaluationdeterminantrc) + (mdr_b_column_candidatenonzeroevaluationdeterminantrc))) /\ ((mdr_e_column_candidatenonzeroevaluationdeterminantrc = ((mdr_p_column_candidatenonzero) + (mdr_n_column_candidatenonzero)) * S ((mdr_p_column_candidatenonzero) + (mdr_n_column_candidatenonzero)) + ((mdr_n_column_candidatenonzero) + (mdr_n_column_candidatenonzero))) /\ ((mdr_f_column_candidatenonzeroevaluationdeterminantrc = ((mdr_vc_column_candidatenonzeroevaluation) + (mdr_e_column_candidatenonzeroevaluationdeterminantrc)) * S ((mdr_vc_column_candidatenonzeroevaluation) + (mdr_e_column_candidatenonzeroevaluationdeterminantrc)) + ((mdr_e_column_candidatenonzeroevaluationdeterminantrc) + (mdr_e_column_candidatenonzeroevaluationdeterminantrc))) /\ ((mdr_z_column_candidatenonzeroevaluationdeterminantr) = ((mdr_c_column_candidatenonzeroevaluationdeterminantrc) + (mdr_f_column_candidatenonzeroevaluationdeterminantrc)) * S ((mdr_c_column_candidatenonzeroevaluationdeterminantrc) + (mdr_f_column_candidatenonzeroevaluationdeterminantrc)) + ((mdr_f_column_candidatenonzeroevaluationdeterminantrc) + (mdr_f_column_candidatenonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_column_candidatenonzeroevaluationdeterminantrb. ff_h_mdr_column_candidatenonzeroevaluationdeterminantrb + S (mdr_z_column_candidatenonzeroevaluationdeterminantr) = S ((S (mdr_i_column_candidatenonzeroevaluationdeterminant)) * mdr_c_column_candidatenonzeroevaluationdeterminant)) /\ exists ff_q_mdr_column_candidatenonzeroevaluationdeterminantrb. mdr_b_column_candidatenonzeroevaluationdeterminant = ff_q_mdr_column_candidatenonzeroevaluationdeterminantrb * S ((S (mdr_i_column_candidatenonzeroevaluationdeterminant)) * mdr_c_column_candidatenonzeroevaluationdeterminant) + (mdr_z_column_candidatenonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_column_candidatenonzero = mdr_n_column_candidatenonzero)))))))))) \/ ~(exists mdr_a_matrix_rank_selected_column_search_decidableno. (((exists mdr_gap_matrix_rank_selected_column_search_decidablenobound. mdr_gap_matrix_rank_selected_column_search_decidablenobound + S (mdr_a_matrix_rank_selected_column_search_decidableno) = (L)) /\ (((((forall fom_index_mrf_column_candidaterowsbound. (exists fom_gap_mrf_column_candidaterowsbound_index_bound. fom_gap_mrf_column_candidaterowsbound_index_bound + S (fom_index_mrf_column_candidaterowsbound) = q) -> exists fom_value_mrf_column_candidaterowsbound. ((((exists fom_beta_height_mrf_column_candidaterowsbound_entry. fom_beta_height_mrf_column_candidaterowsbound_entry + S (fom_value_mrf_column_candidaterowsbound) = S ((S (fom_index_mrf_column_candidaterowsbound)) * rc)) /\ exists fom_beta_quotient_mrf_column_candidaterowsbound_entry. rb = fom_beta_quotient_mrf_column_candidaterowsbound_entry * S ((S (fom_index_mrf_column_candidaterowsbound)) * rc) + (fom_value_mrf_column_candidaterowsbound))) /\ (exists fom_gap_mrf_column_candidaterowsbound_value_bound. fom_gap_mrf_column_candidaterowsbound_value_bound + S (fom_value_mrf_column_candidaterowsbound) = r))) /\ (forall mdr_i_column_candidaterowsdistinct mdr_j_column_candidaterowsdistinct mdr_a_column_candidaterowsdistinct. (exists mdr_gap_column_candidaterowsdistincti. mdr_gap_column_candidaterowsdistincti + S (mdr_i_column_candidaterowsdistinct) = (q)) -> (exists mdr_gap_column_candidaterowsdistinctj. mdr_gap_column_candidaterowsdistinctj + S (mdr_j_column_candidaterowsdistinct) = (q)) -> (((exists ff_h_mdr_column_candidaterowsdistinctfirst. ff_h_mdr_column_candidaterowsdistinctfirst + S (mdr_a_column_candidaterowsdistinct) = S ((S (mdr_i_column_candidaterowsdistinct)) * rc)) /\ exists ff_q_mdr_column_candidaterowsdistinctfirst. rb = ff_q_mdr_column_candidaterowsdistinctfirst * S ((S (mdr_i_column_candidaterowsdistinct)) * rc) + (mdr_a_column_candidaterowsdistinct))) -> (((exists ff_h_mdr_column_candidaterowsdistinctsecond. ff_h_mdr_column_candidaterowsdistinctsecond + S (mdr_a_column_candidaterowsdistinct) = S ((S (mdr_j_column_candidaterowsdistinct)) * rc)) /\ exists ff_q_mdr_column_candidaterowsdistinctsecond. rb = ff_q_mdr_column_candidaterowsdistinctsecond * S ((S (mdr_j_column_candidaterowsdistinct)) * rc) + (mdr_a_column_candidaterowsdistinct))) -> mdr_i_column_candidaterowsdistinct = mdr_j_column_candidaterowsdistinct))) /\ ((((forall fom_index_mrf_column_candidatecolumnsbound. (exists fom_gap_mrf_column_candidatecolumnsbound_index_bound. fom_gap_mrf_column_candidatecolumnsbound_index_bound + S (fom_index_mrf_column_candidatecolumnsbound) = q) -> exists fom_value_mrf_column_candidatecolumnsbound. ((((exists fom_beta_height_mrf_column_candidatecolumnsbound_entry. fom_beta_height_mrf_column_candidatecolumnsbound_entry + S (fom_value_mrf_column_candidatecolumnsbound) = S ((S (fom_index_mrf_column_candidatecolumnsbound)) * cc)) /\ exists fom_beta_quotient_mrf_column_candidatecolumnsbound_entry. mdr_a_matrix_rank_selected_column_search_decidableno = fom_beta_quotient_mrf_column_candidatecolumnsbound_entry * S ((S (fom_index_mrf_column_candidatecolumnsbound)) * cc) + (fom_value_mrf_column_candidatecolumnsbound))) /\ (exists fom_gap_mrf_column_candidatecolumnsbound_value_bound. fom_gap_mrf_column_candidatecolumnsbound_value_bound + S (fom_value_mrf_column_candidatecolumnsbound) = w))) /\ (forall mdr_i_column_candidatecolumnsdistinct mdr_j_column_candidatecolumnsdistinct mdr_a_column_candidatecolumnsdistinct. (exists mdr_gap_column_candidatecolumnsdistincti. mdr_gap_column_candidatecolumnsdistincti + S (mdr_i_column_candidatecolumnsdistinct) = (q)) -> (exists mdr_gap_column_candidatecolumnsdistinctj. mdr_gap_column_candidatecolumnsdistinctj + S (mdr_j_column_candidatecolumnsdistinct) = (q)) -> (((exists ff_h_mdr_column_candidatecolumnsdistinctfirst. ff_h_mdr_column_candidatecolumnsdistinctfirst + S (mdr_a_column_candidatecolumnsdistinct) = S ((S (mdr_i_column_candidatecolumnsdistinct)) * cc)) /\ exists ff_q_mdr_column_candidatecolumnsdistinctfirst. mdr_a_matrix_rank_selected_column_search_decidableno = ff_q_mdr_column_candidatecolumnsdistinctfirst * S ((S (mdr_i_column_candidatecolumnsdistinct)) * cc) + (mdr_a_column_candidatecolumnsdistinct))) -> (((exists ff_h_mdr_column_candidatecolumnsdistinctsecond. ff_h_mdr_column_candidatecolumnsdistinctsecond + S (mdr_a_column_candidatecolumnsdistinct) = S ((S (mdr_j_column_candidatecolumnsdistinct)) * cc)) /\ exists ff_q_mdr_column_candidatecolumnsdistinctsecond. mdr_a_matrix_rank_selected_column_search_decidableno = ff_q_mdr_column_candidatecolumnsdistinctsecond * S ((S (mdr_j_column_candidatecolumnsdistinct)) * cc) + (mdr_a_column_candidatecolumnsdistinct))) -> mdr_i_column_candidatecolumnsdistinct = mdr_j_column_candidatecolumnsdistinct))) /\ (exists mdr_p_column_candidatenonzero mdr_n_column_candidatenonzero. ((exists mdr_ub_column_candidatenonzeroevaluation mdr_uc_column_candidatenonzeroevaluation mdr_vb_column_candidatenonzeroevaluation mdr_vc_column_candidatenonzeroevaluation. ((((forall mdr_i_column_candidatenonzeroevaluationmatrixpositive. (exists mdr_gap_column_candidatenonzeroevaluationmatrixpositivebound. mdr_gap_column_candidatenonzeroevaluationmatrixpositivebound + S (mdr_i_column_candidatenonzeroevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_column_candidatenonzeroevaluationmatrixpositive. (((exists mdr_r_column_candidatenonzeroevaluationmatrixpositivepoint mdr_s_column_candidatenonzeroevaluationmatrixpositivepoint mdr_u_column_candidatenonzeroevaluationmatrixpositivepoint mdr_v_column_candidatenonzeroevaluationmatrixpositivepoint. ((mdr_i_column_candidatenonzeroevaluationmatrixpositive = (q) * mdr_r_column_candidatenonzeroevaluationmatrixpositivepoint + mdr_s_column_candidatenonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_column_candidatenonzeroevaluationmatrixpositivepointcolumn. mdr_gap_column_candidatenonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_column_candidatenonzeroevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_column_candidatenonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_column_candidatenonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_column_candidatenonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_column_candidatenonzeroevaluationmatrixpositivepoint)) * rc)) /\ exists ff_q_mdr_column_candidatenonzeroevaluationmatrixpositivepointrow_index. rb = ff_q_mdr_column_candidatenonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_column_candidatenonzeroevaluationmatrixpositivepoint)) * rc) + (mdr_u_column_candidatenonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_column_candidatenonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_column_candidatenonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_column_candidatenonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_column_candidatenonzeroevaluationmatrixpositivepoint)) * cc)) /\ exists ff_q_mdr_column_candidatenonzeroevaluationmatrixpositivepointcolumn_index. mdr_a_matrix_rank_selected_column_search_decidableno = ff_q_mdr_column_candidatenonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_column_candidatenonzeroevaluationmatrixpositivepoint)) * cc) + (mdr_v_column_candidatenonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_column_candidatenonzeroevaluationmatrixpositivepointsource. ff_h_mdr_column_candidatenonzeroevaluationmatrixpositivepointsource + S (mdr_a_column_candidatenonzeroevaluationmatrixpositive) = S ((S ((mdr_u_column_candidatenonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_column_candidatenonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_column_candidatenonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_column_candidatenonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_column_candidatenonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_column_candidatenonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_column_candidatenonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_column_candidatenonzeroevaluationmatrixpositiveoutput. ff_h_mdr_column_candidatenonzeroevaluationmatrixpositiveoutput + S (mdr_a_column_candidatenonzeroevaluationmatrixpositive) = S ((S (mdr_i_column_candidatenonzeroevaluationmatrixpositive)) * mdr_uc_column_candidatenonzeroevaluation)) /\ exists ff_q_mdr_column_candidatenonzeroevaluationmatrixpositiveoutput. mdr_ub_column_candidatenonzeroevaluation = ff_q_mdr_column_candidatenonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_column_candidatenonzeroevaluationmatrixpositive)) * mdr_uc_column_candidatenonzeroevaluation) + (mdr_a_column_candidatenonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_column_candidatenonzeroevaluationmatrixnegative. (exists mdr_gap_column_candidatenonzeroevaluationmatrixnegativebound. mdr_gap_column_candidatenonzeroevaluationmatrixnegativebound + S (mdr_i_column_candidatenonzeroevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_column_candidatenonzeroevaluationmatrixnegative. (((exists mdr_r_column_candidatenonzeroevaluationmatrixnegativepoint mdr_s_column_candidatenonzeroevaluationmatrixnegativepoint mdr_u_column_candidatenonzeroevaluationmatrixnegativepoint mdr_v_column_candidatenonzeroevaluationmatrixnegativepoint. ((mdr_i_column_candidatenonzeroevaluationmatrixnegative = (q) * mdr_r_column_candidatenonzeroevaluationmatrixnegativepoint + mdr_s_column_candidatenonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_column_candidatenonzeroevaluationmatrixnegativepointcolumn. mdr_gap_column_candidatenonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_column_candidatenonzeroevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_column_candidatenonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_column_candidatenonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_column_candidatenonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_column_candidatenonzeroevaluationmatrixnegativepoint)) * rc)) /\ exists ff_q_mdr_column_candidatenonzeroevaluationmatrixnegativepointrow_index. rb = ff_q_mdr_column_candidatenonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_column_candidatenonzeroevaluationmatrixnegativepoint)) * rc) + (mdr_u_column_candidatenonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_column_candidatenonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_column_candidatenonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_column_candidatenonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_column_candidatenonzeroevaluationmatrixnegativepoint)) * cc)) /\ exists ff_q_mdr_column_candidatenonzeroevaluationmatrixnegativepointcolumn_index. mdr_a_matrix_rank_selected_column_search_decidableno = ff_q_mdr_column_candidatenonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_column_candidatenonzeroevaluationmatrixnegativepoint)) * cc) + (mdr_v_column_candidatenonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_column_candidatenonzeroevaluationmatrixnegativepointsource. ff_h_mdr_column_candidatenonzeroevaluationmatrixnegativepointsource + S (mdr_a_column_candidatenonzeroevaluationmatrixnegative) = S ((S ((mdr_u_column_candidatenonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_column_candidatenonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_column_candidatenonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_column_candidatenonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_column_candidatenonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_column_candidatenonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_column_candidatenonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_column_candidatenonzeroevaluationmatrixnegativeoutput. ff_h_mdr_column_candidatenonzeroevaluationmatrixnegativeoutput + S (mdr_a_column_candidatenonzeroevaluationmatrixnegative) = S ((S (mdr_i_column_candidatenonzeroevaluationmatrixnegative)) * mdr_vc_column_candidatenonzeroevaluation)) /\ exists ff_q_mdr_column_candidatenonzeroevaluationmatrixnegativeoutput. mdr_vb_column_candidatenonzeroevaluation = ff_q_mdr_column_candidatenonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_column_candidatenonzeroevaluationmatrixnegative)) * mdr_vc_column_candidatenonzeroevaluation) + (mdr_a_column_candidatenonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_column_candidatenonzeroevaluationdeterminant mdr_c_column_candidatenonzeroevaluationdeterminant mdr_l_column_candidatenonzeroevaluationdeterminant mdr_i_column_candidatenonzeroevaluationdeterminant. ((forall mdr_i_column_candidatenonzeroevaluationdeterminanth. (exists mdr_gap_column_candidatenonzeroevaluationdeterminanthi. mdr_gap_column_candidatenonzeroevaluationdeterminanthi + S (mdr_i_column_candidatenonzeroevaluationdeterminanth) = (mdr_l_column_candidatenonzeroevaluationdeterminant)) -> exists mdr_d_column_candidatenonzeroevaluationdeterminanth mdr_pb_column_candidatenonzeroevaluationdeterminanth mdr_pc_column_candidatenonzeroevaluationdeterminanth mdr_nb_column_candidatenonzeroevaluationdeterminanth mdr_nc_column_candidatenonzeroevaluationdeterminanth mdr_p_column_candidatenonzeroevaluationdeterminanth mdr_n_column_candidatenonzeroevaluationdeterminanth. ((exists mdr_z_column_candidatenonzeroevaluationdeterminanthr. ((exists mdr_a_column_candidatenonzeroevaluationdeterminanthrc mdr_b_column_candidatenonzeroevaluationdeterminanthrc mdr_c_column_candidatenonzeroevaluationdeterminanthrc mdr_e_column_candidatenonzeroevaluationdeterminanthrc mdr_f_column_candidatenonzeroevaluationdeterminanthrc. ((mdr_a_column_candidatenonzeroevaluationdeterminanthrc = ((mdr_d_column_candidatenonzeroevaluationdeterminanth) + (mdr_pb_column_candidatenonzeroevaluationdeterminanth)) * S ((mdr_d_column_candidatenonzeroevaluationdeterminanth) + (mdr_pb_column_candidatenonzeroevaluationdeterminanth)) + ((mdr_pb_column_candidatenonzeroevaluationdeterminanth) + (mdr_pb_column_candidatenonzeroevaluationdeterminanth))) /\ ((mdr_b_column_candidatenonzeroevaluationdeterminanthrc = ((mdr_pc_column_candidatenonzeroevaluationdeterminanth) + (mdr_nb_column_candidatenonzeroevaluationdeterminanth)) * S ((mdr_pc_column_candidatenonzeroevaluationdeterminanth) + (mdr_nb_column_candidatenonzeroevaluationdeterminanth)) + ((mdr_nb_column_candidatenonzeroevaluationdeterminanth) + (mdr_nb_column_candidatenonzeroevaluationdeterminanth))) /\ ((mdr_c_column_candidatenonzeroevaluationdeterminanthrc = ((mdr_a_column_candidatenonzeroevaluationdeterminanthrc) + (mdr_b_column_candidatenonzeroevaluationdeterminanthrc)) * S ((mdr_a_column_candidatenonzeroevaluationdeterminanthrc) + (mdr_b_column_candidatenonzeroevaluationdeterminanthrc)) + ((mdr_b_column_candidatenonzeroevaluationdeterminanthrc) + (mdr_b_column_candidatenonzeroevaluationdeterminanthrc))) /\ ((mdr_e_column_candidatenonzeroevaluationdeterminanthrc = ((mdr_p_column_candidatenonzeroevaluationdeterminanth) + (mdr_n_column_candidatenonzeroevaluationdeterminanth)) * S ((mdr_p_column_candidatenonzeroevaluationdeterminanth) + (mdr_n_column_candidatenonzeroevaluationdeterminanth)) + ((mdr_n_column_candidatenonzeroevaluationdeterminanth) + (mdr_n_column_candidatenonzeroevaluationdeterminanth))) /\ ((mdr_f_column_candidatenonzeroevaluationdeterminanthrc = ((mdr_nc_column_candidatenonzeroevaluationdeterminanth) + (mdr_e_column_candidatenonzeroevaluationdeterminanthrc)) * S ((mdr_nc_column_candidatenonzeroevaluationdeterminanth) + (mdr_e_column_candidatenonzeroevaluationdeterminanthrc)) + ((mdr_e_column_candidatenonzeroevaluationdeterminanthrc) + (mdr_e_column_candidatenonzeroevaluationdeterminanthrc))) /\ ((mdr_z_column_candidatenonzeroevaluationdeterminanthr) = ((mdr_c_column_candidatenonzeroevaluationdeterminanthrc) + (mdr_f_column_candidatenonzeroevaluationdeterminanthrc)) * S ((mdr_c_column_candidatenonzeroevaluationdeterminanthrc) + (mdr_f_column_candidatenonzeroevaluationdeterminanthrc)) + ((mdr_f_column_candidatenonzeroevaluationdeterminanthrc) + (mdr_f_column_candidatenonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_column_candidatenonzeroevaluationdeterminanthrb. ff_h_mdr_column_candidatenonzeroevaluationdeterminanthrb + S (mdr_z_column_candidatenonzeroevaluationdeterminanthr) = S ((S (mdr_i_column_candidatenonzeroevaluationdeterminanth)) * mdr_c_column_candidatenonzeroevaluationdeterminant)) /\ exists ff_q_mdr_column_candidatenonzeroevaluationdeterminanthrb. mdr_b_column_candidatenonzeroevaluationdeterminant = ff_q_mdr_column_candidatenonzeroevaluationdeterminanthrb * S ((S (mdr_i_column_candidatenonzeroevaluationdeterminanth)) * mdr_c_column_candidatenonzeroevaluationdeterminant) + (mdr_z_column_candidatenonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_column_candidatenonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_column_candidatenonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_column_candidatenonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_column_candidatenonzeroevaluationdeterminanths mdr_eb_column_candidatenonzeroevaluationdeterminanths mdr_ec_column_candidatenonzeroevaluationdeterminanths mdr_fb_column_candidatenonzeroevaluationdeterminanths mdr_fc_column_candidatenonzeroevaluationdeterminanths. (((mdr_d_column_candidatenonzeroevaluationdeterminanth) = S (mdr_q_column_candidatenonzeroevaluationdeterminanths)) /\ ((forall mdr_j_column_candidatenonzeroevaluationdeterminanthsc. (exists mdr_gap_column_candidatenonzeroevaluationdeterminanthscj. mdr_gap_column_candidatenonzeroevaluationdeterminanthscj + S (mdr_j_column_candidatenonzeroevaluationdeterminanthsc) = (S (mdr_q_column_candidatenonzeroevaluationdeterminanths))) -> exists mdr_i_column_candidatenonzeroevaluationdeterminanthsc mdr_up_column_candidatenonzeroevaluationdeterminanthsc mdr_us_column_candidatenonzeroevaluationdeterminanthsc mdr_un_column_candidatenonzeroevaluationdeterminanthsc mdr_ut_column_candidatenonzeroevaluationdeterminanthsc mdr_p_column_candidatenonzeroevaluationdeterminanthsc mdr_n_column_candidatenonzeroevaluationdeterminanthsc. ((exists mdr_gap_column_candidatenonzeroevaluationdeterminanthsci. mdr_gap_column_candidatenonzeroevaluationdeterminanthsci + S (mdr_i_column_candidatenonzeroevaluationdeterminanthsc) = (mdr_i_column_candidatenonzeroevaluationdeterminanth)) /\ ((exists mdr_z_column_candidatenonzeroevaluationdeterminanthscr. ((exists mdr_a_column_candidatenonzeroevaluationdeterminanthscrc mdr_b_column_candidatenonzeroevaluationdeterminanthscrc mdr_c_column_candidatenonzeroevaluationdeterminanthscrc mdr_e_column_candidatenonzeroevaluationdeterminanthscrc mdr_f_column_candidatenonzeroevaluationdeterminanthscrc. ((mdr_a_column_candidatenonzeroevaluationdeterminanthscrc = ((mdr_q_column_candidatenonzeroevaluationdeterminanths) + (mdr_up_column_candidatenonzeroevaluationdeterminanthsc)) * S ((mdr_q_column_candidatenonzeroevaluationdeterminanths) + (mdr_up_column_candidatenonzeroevaluationdeterminanthsc)) + ((mdr_up_column_candidatenonzeroevaluationdeterminanthsc) + (mdr_up_column_candidatenonzeroevaluationdeterminanthsc))) /\ ((mdr_b_column_candidatenonzeroevaluationdeterminanthscrc = ((mdr_us_column_candidatenonzeroevaluationdeterminanthsc) + (mdr_un_column_candidatenonzeroevaluationdeterminanthsc)) * S ((mdr_us_column_candidatenonzeroevaluationdeterminanthsc) + (mdr_un_column_candidatenonzeroevaluationdeterminanthsc)) + ((mdr_un_column_candidatenonzeroevaluationdeterminanthsc) + (mdr_un_column_candidatenonzeroevaluationdeterminanthsc))) /\ ((mdr_c_column_candidatenonzeroevaluationdeterminanthscrc = ((mdr_a_column_candidatenonzeroevaluationdeterminanthscrc) + (mdr_b_column_candidatenonzeroevaluationdeterminanthscrc)) * S ((mdr_a_column_candidatenonzeroevaluationdeterminanthscrc) + (mdr_b_column_candidatenonzeroevaluationdeterminanthscrc)) + ((mdr_b_column_candidatenonzeroevaluationdeterminanthscrc) + (mdr_b_column_candidatenonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_column_candidatenonzeroevaluationdeterminanthscrc = ((mdr_p_column_candidatenonzeroevaluationdeterminanthsc) + (mdr_n_column_candidatenonzeroevaluationdeterminanthsc)) * S ((mdr_p_column_candidatenonzeroevaluationdeterminanthsc) + (mdr_n_column_candidatenonzeroevaluationdeterminanthsc)) + ((mdr_n_column_candidatenonzeroevaluationdeterminanthsc) + (mdr_n_column_candidatenonzeroevaluationdeterminanthsc))) /\ ((mdr_f_column_candidatenonzeroevaluationdeterminanthscrc = ((mdr_ut_column_candidatenonzeroevaluationdeterminanthsc) + (mdr_e_column_candidatenonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_column_candidatenonzeroevaluationdeterminanthsc) + (mdr_e_column_candidatenonzeroevaluationdeterminanthscrc)) + ((mdr_e_column_candidatenonzeroevaluationdeterminanthscrc) + (mdr_e_column_candidatenonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_column_candidatenonzeroevaluationdeterminanthscr) = ((mdr_c_column_candidatenonzeroevaluationdeterminanthscrc) + (mdr_f_column_candidatenonzeroevaluationdeterminanthscrc)) * S ((mdr_c_column_candidatenonzeroevaluationdeterminanthscrc) + (mdr_f_column_candidatenonzeroevaluationdeterminanthscrc)) + ((mdr_f_column_candidatenonzeroevaluationdeterminanthscrc) + (mdr_f_column_candidatenonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_column_candidatenonzeroevaluationdeterminanthscrb. ff_h_mdr_column_candidatenonzeroevaluationdeterminanthscrb + S (mdr_z_column_candidatenonzeroevaluationdeterminanthscr) = S ((S (mdr_i_column_candidatenonzeroevaluationdeterminanthsc)) * mdr_c_column_candidatenonzeroevaluationdeterminant)) /\ exists ff_q_mdr_column_candidatenonzeroevaluationdeterminanthscrb. mdr_b_column_candidatenonzeroevaluationdeterminant = ff_q_mdr_column_candidatenonzeroevaluationdeterminanthscrb * S ((S (mdr_i_column_candidatenonzeroevaluationdeterminanthsc)) * mdr_c_column_candidatenonzeroevaluationdeterminant) + (mdr_z_column_candidatenonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive) = ((mdr_q_column_candidatenonzeroevaluationdeterminanths) * (mdr_q_column_candidatenonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive = (mdr_q_column_candidatenonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive) = (mdr_q_column_candidatenonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive) = (mdr_j_column_candidatenonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_column_candidatenonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_column_candidatenonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_column_candidatenonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_column_candidatenonzeroevaluationdeterminanth = ff_q_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_column_candidatenonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_column_candidatenonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive)) * mdr_us_column_candidatenonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_target. mdr_up_column_candidatenonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive)) * mdr_us_column_candidatenonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative) = ((mdr_q_column_candidatenonzeroevaluationdeterminanths) * (mdr_q_column_candidatenonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative = (mdr_q_column_candidatenonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative) = (mdr_q_column_candidatenonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative) = (mdr_j_column_candidatenonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_column_candidatenonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_column_candidatenonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_column_candidatenonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_column_candidatenonzeroevaluationdeterminanth = ff_q_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_column_candidatenonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_column_candidatenonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative)) * mdr_ut_column_candidatenonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_target. mdr_un_column_candidatenonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative)) * mdr_ut_column_candidatenonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_column_candidatenonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_column_candidatenonzeroevaluationdeterminanthscp. ff_h_mdr_column_candidatenonzeroevaluationdeterminanthscp + S (mdr_p_column_candidatenonzeroevaluationdeterminanthsc) = S ((S (mdr_j_column_candidatenonzeroevaluationdeterminanthsc)) * mdr_ec_column_candidatenonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_column_candidatenonzeroevaluationdeterminanthscp. mdr_eb_column_candidatenonzeroevaluationdeterminanths = ff_q_mdr_column_candidatenonzeroevaluationdeterminanthscp * S ((S (mdr_j_column_candidatenonzeroevaluationdeterminanthsc)) * mdr_ec_column_candidatenonzeroevaluationdeterminanths) + (mdr_p_column_candidatenonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_column_candidatenonzeroevaluationdeterminanthscn. ff_h_mdr_column_candidatenonzeroevaluationdeterminanthscn + S (mdr_n_column_candidatenonzeroevaluationdeterminanthsc) = S ((S (mdr_j_column_candidatenonzeroevaluationdeterminanthsc)) * mdr_fc_column_candidatenonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_column_candidatenonzeroevaluationdeterminanthscn. mdr_fb_column_candidatenonzeroevaluationdeterminanths = ff_q_mdr_column_candidatenonzeroevaluationdeterminanthscn * S ((S (mdr_j_column_candidatenonzeroevaluationdeterminanthsc)) * mdr_fc_column_candidatenonzeroevaluationdeterminanths) + (mdr_n_column_candidatenonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_column_candidatenonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_column_candidatenonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_column_candidatenonzeroevaluationdeterminanth = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_column_candidatenonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_column_candidatenonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_column_candidatenonzeroevaluationdeterminanth = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_column_candidatenonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_column_candidatenonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_column_candidatenonzeroevaluationdeterminanths = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_column_candidatenonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_column_candidatenonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_column_candidatenonzeroevaluationdeterminanths = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_column_candidatenonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_column_candidatenonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_column_candidatenonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_column_candidatenonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_column_candidatenonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive) + (mdr_p_column_candidatenonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive = (S (mdr_q_column_candidatenonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_column_candidatenonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_column_candidatenonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_column_candidatenonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative) + (mdr_n_column_candidatenonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative = (S (mdr_q_column_candidatenonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_column_candidatenonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_column_candidatenonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_column_candidatenonzeroevaluationdeterminanti. mdr_gap_column_candidatenonzeroevaluationdeterminanti + S (mdr_i_column_candidatenonzeroevaluationdeterminant) = (mdr_l_column_candidatenonzeroevaluationdeterminant)) /\ (exists mdr_z_column_candidatenonzeroevaluationdeterminantr. ((exists mdr_a_column_candidatenonzeroevaluationdeterminantrc mdr_b_column_candidatenonzeroevaluationdeterminantrc mdr_c_column_candidatenonzeroevaluationdeterminantrc mdr_e_column_candidatenonzeroevaluationdeterminantrc mdr_f_column_candidatenonzeroevaluationdeterminantrc. ((mdr_a_column_candidatenonzeroevaluationdeterminantrc = ((q) + (mdr_ub_column_candidatenonzeroevaluation)) * S ((q) + (mdr_ub_column_candidatenonzeroevaluation)) + ((mdr_ub_column_candidatenonzeroevaluation) + (mdr_ub_column_candidatenonzeroevaluation))) /\ ((mdr_b_column_candidatenonzeroevaluationdeterminantrc = ((mdr_uc_column_candidatenonzeroevaluation) + (mdr_vb_column_candidatenonzeroevaluation)) * S ((mdr_uc_column_candidatenonzeroevaluation) + (mdr_vb_column_candidatenonzeroevaluation)) + ((mdr_vb_column_candidatenonzeroevaluation) + (mdr_vb_column_candidatenonzeroevaluation))) /\ ((mdr_c_column_candidatenonzeroevaluationdeterminantrc = ((mdr_a_column_candidatenonzeroevaluationdeterminantrc) + (mdr_b_column_candidatenonzeroevaluationdeterminantrc)) * S ((mdr_a_column_candidatenonzeroevaluationdeterminantrc) + (mdr_b_column_candidatenonzeroevaluationdeterminantrc)) + ((mdr_b_column_candidatenonzeroevaluationdeterminantrc) + (mdr_b_column_candidatenonzeroevaluationdeterminantrc))) /\ ((mdr_e_column_candidatenonzeroevaluationdeterminantrc = ((mdr_p_column_candidatenonzero) + (mdr_n_column_candidatenonzero)) * S ((mdr_p_column_candidatenonzero) + (mdr_n_column_candidatenonzero)) + ((mdr_n_column_candidatenonzero) + (mdr_n_column_candidatenonzero))) /\ ((mdr_f_column_candidatenonzeroevaluationdeterminantrc = ((mdr_vc_column_candidatenonzeroevaluation) + (mdr_e_column_candidatenonzeroevaluationdeterminantrc)) * S ((mdr_vc_column_candidatenonzeroevaluation) + (mdr_e_column_candidatenonzeroevaluationdeterminantrc)) + ((mdr_e_column_candidatenonzeroevaluationdeterminantrc) + (mdr_e_column_candidatenonzeroevaluationdeterminantrc))) /\ ((mdr_z_column_candidatenonzeroevaluationdeterminantr) = ((mdr_c_column_candidatenonzeroevaluationdeterminantrc) + (mdr_f_column_candidatenonzeroevaluationdeterminantrc)) * S ((mdr_c_column_candidatenonzeroevaluationdeterminantrc) + (mdr_f_column_candidatenonzeroevaluationdeterminantrc)) + ((mdr_f_column_candidatenonzeroevaluationdeterminantrc) + (mdr_f_column_candidatenonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_column_candidatenonzeroevaluationdeterminantrb. ff_h_mdr_column_candidatenonzeroevaluationdeterminantrb + S (mdr_z_column_candidatenonzeroevaluationdeterminantr) = S ((S (mdr_i_column_candidatenonzeroevaluationdeterminant)) * mdr_c_column_candidatenonzeroevaluationdeterminant)) /\ exists ff_q_mdr_column_candidatenonzeroevaluationdeterminantrb. mdr_b_column_candidatenonzeroevaluationdeterminant = ff_q_mdr_column_candidatenonzeroevaluationdeterminantrb * S ((S (mdr_i_column_candidatenonzeroevaluationdeterminant)) * mdr_c_column_candidatenonzeroevaluationdeterminant) + (mdr_z_column_candidatenonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_column_candidatenonzero = mdr_n_column_candidatenonzero))))))))))