rectangular_matrix_rank_exists_unique

Exact expanded first-order arithmetic statement

forall pb pc nb nc r w. exists rank. (((((exists mdr_gap_unique_rankrows_bound. mdr_gap_unique_rankrows_bound + (rank) = (r)) /\ ((exists mdr_gap_unique_rankcolumns_bound. mdr_gap_unique_rankcolumns_bound + (rank) = (w)) /\ ((exists mdr_rb_unique_rankwitness mdr_rc_unique_rankwitness mdr_cb_unique_rankwitness mdr_cc_unique_rankwitness. (((((forall fom_index_mrf_unique_rankwitnessminorrowsbound. (exists fom_gap_mrf_unique_rankwitnessminorrowsbound_index_bound. fom_gap_mrf_unique_rankwitnessminorrowsbound_index_bound + S (fom_index_mrf_unique_rankwitnessminorrowsbound) = rank) -> exists fom_value_mrf_unique_rankwitnessminorrowsbound. ((((exists fom_beta_height_mrf_unique_rankwitnessminorrowsbound_entry. fom_beta_height_mrf_unique_rankwitnessminorrowsbound_entry + S (fom_value_mrf_unique_rankwitnessminorrowsbound) = S ((S (fom_index_mrf_unique_rankwitnessminorrowsbound)) * mdr_rc_unique_rankwitness)) /\ exists fom_beta_quotient_mrf_unique_rankwitnessminorrowsbound_entry. mdr_rb_unique_rankwitness = fom_beta_quotient_mrf_unique_rankwitnessminorrowsbound_entry * S ((S (fom_index_mrf_unique_rankwitnessminorrowsbound)) * mdr_rc_unique_rankwitness) + (fom_value_mrf_unique_rankwitnessminorrowsbound))) /\ (exists fom_gap_mrf_unique_rankwitnessminorrowsbound_value_bound. fom_gap_mrf_unique_rankwitnessminorrowsbound_value_bound + S (fom_value_mrf_unique_rankwitnessminorrowsbound) = r))) /\ (forall mdr_i_unique_rankwitnessminorrowsdistinct mdr_j_unique_rankwitnessminorrowsdistinct mdr_a_unique_rankwitnessminorrowsdistinct. (exists mdr_gap_unique_rankwitnessminorrowsdistincti. mdr_gap_unique_rankwitnessminorrowsdistincti + S (mdr_i_unique_rankwitnessminorrowsdistinct) = (rank)) -> (exists mdr_gap_unique_rankwitnessminorrowsdistinctj. mdr_gap_unique_rankwitnessminorrowsdistinctj + S (mdr_j_unique_rankwitnessminorrowsdistinct) = (rank)) -> (((exists ff_h_mdr_unique_rankwitnessminorrowsdistinctfirst. ff_h_mdr_unique_rankwitnessminorrowsdistinctfirst + S (mdr_a_unique_rankwitnessminorrowsdistinct) = S ((S (mdr_i_unique_rankwitnessminorrowsdistinct)) * mdr_rc_unique_rankwitness)) /\ exists ff_q_mdr_unique_rankwitnessminorrowsdistinctfirst. mdr_rb_unique_rankwitness = ff_q_mdr_unique_rankwitnessminorrowsdistinctfirst * S ((S (mdr_i_unique_rankwitnessminorrowsdistinct)) * mdr_rc_unique_rankwitness) + (mdr_a_unique_rankwitnessminorrowsdistinct))) -> (((exists ff_h_mdr_unique_rankwitnessminorrowsdistinctsecond. ff_h_mdr_unique_rankwitnessminorrowsdistinctsecond + S (mdr_a_unique_rankwitnessminorrowsdistinct) = S ((S (mdr_j_unique_rankwitnessminorrowsdistinct)) * mdr_rc_unique_rankwitness)) /\ exists ff_q_mdr_unique_rankwitnessminorrowsdistinctsecond. mdr_rb_unique_rankwitness = ff_q_mdr_unique_rankwitnessminorrowsdistinctsecond * S ((S (mdr_j_unique_rankwitnessminorrowsdistinct)) * mdr_rc_unique_rankwitness) + (mdr_a_unique_rankwitnessminorrowsdistinct))) -> mdr_i_unique_rankwitnessminorrowsdistinct = mdr_j_unique_rankwitnessminorrowsdistinct))) /\ ((((forall fom_index_mrf_unique_rankwitnessminorcolumnsbound. (exists fom_gap_mrf_unique_rankwitnessminorcolumnsbound_index_bound. fom_gap_mrf_unique_rankwitnessminorcolumnsbound_index_bound + S (fom_index_mrf_unique_rankwitnessminorcolumnsbound) = rank) -> exists fom_value_mrf_unique_rankwitnessminorcolumnsbound. ((((exists fom_beta_height_mrf_unique_rankwitnessminorcolumnsbound_entry. fom_beta_height_mrf_unique_rankwitnessminorcolumnsbound_entry + S (fom_value_mrf_unique_rankwitnessminorcolumnsbound) = S ((S (fom_index_mrf_unique_rankwitnessminorcolumnsbound)) * mdr_cc_unique_rankwitness)) /\ exists fom_beta_quotient_mrf_unique_rankwitnessminorcolumnsbound_entry. mdr_cb_unique_rankwitness = fom_beta_quotient_mrf_unique_rankwitnessminorcolumnsbound_entry * S ((S (fom_index_mrf_unique_rankwitnessminorcolumnsbound)) * mdr_cc_unique_rankwitness) + (fom_value_mrf_unique_rankwitnessminorcolumnsbound))) /\ (exists fom_gap_mrf_unique_rankwitnessminorcolumnsbound_value_bound. fom_gap_mrf_unique_rankwitnessminorcolumnsbound_value_bound + S (fom_value_mrf_unique_rankwitnessminorcolumnsbound) = w))) /\ (forall mdr_i_unique_rankwitnessminorcolumnsdistinct mdr_j_unique_rankwitnessminorcolumnsdistinct mdr_a_unique_rankwitnessminorcolumnsdistinct. (exists mdr_gap_unique_rankwitnessminorcolumnsdistincti. mdr_gap_unique_rankwitnessminorcolumnsdistincti + S (mdr_i_unique_rankwitnessminorcolumnsdistinct) = (rank)) -> (exists mdr_gap_unique_rankwitnessminorcolumnsdistinctj. mdr_gap_unique_rankwitnessminorcolumnsdistinctj + S (mdr_j_unique_rankwitnessminorcolumnsdistinct) = (rank)) -> (((exists ff_h_mdr_unique_rankwitnessminorcolumnsdistinctfirst. ff_h_mdr_unique_rankwitnessminorcolumnsdistinctfirst + S (mdr_a_unique_rankwitnessminorcolumnsdistinct) = S ((S (mdr_i_unique_rankwitnessminorcolumnsdistinct)) * mdr_cc_unique_rankwitness)) /\ exists ff_q_mdr_unique_rankwitnessminorcolumnsdistinctfirst. mdr_cb_unique_rankwitness = ff_q_mdr_unique_rankwitnessminorcolumnsdistinctfirst * S ((S (mdr_i_unique_rankwitnessminorcolumnsdistinct)) * mdr_cc_unique_rankwitness) + (mdr_a_unique_rankwitnessminorcolumnsdistinct))) -> (((exists ff_h_mdr_unique_rankwitnessminorcolumnsdistinctsecond. ff_h_mdr_unique_rankwitnessminorcolumnsdistinctsecond + S (mdr_a_unique_rankwitnessminorcolumnsdistinct) = S ((S (mdr_j_unique_rankwitnessminorcolumnsdistinct)) * mdr_cc_unique_rankwitness)) /\ exists ff_q_mdr_unique_rankwitnessminorcolumnsdistinctsecond. mdr_cb_unique_rankwitness = ff_q_mdr_unique_rankwitnessminorcolumnsdistinctsecond * S ((S (mdr_j_unique_rankwitnessminorcolumnsdistinct)) * mdr_cc_unique_rankwitness) + (mdr_a_unique_rankwitnessminorcolumnsdistinct))) -> mdr_i_unique_rankwitnessminorcolumnsdistinct = mdr_j_unique_rankwitnessminorcolumnsdistinct))) /\ (exists mdr_p_unique_rankwitnessminornonzero mdr_n_unique_rankwitnessminornonzero. ((exists mdr_ub_unique_rankwitnessminornonzeroevaluation mdr_uc_unique_rankwitnessminornonzeroevaluation mdr_vb_unique_rankwitnessminornonzeroevaluation mdr_vc_unique_rankwitnessminornonzeroevaluation. ((((forall mdr_i_unique_rankwitnessminornonzeroevaluationmatrixpositive. (exists mdr_gap_unique_rankwitnessminornonzeroevaluationmatrixpositivebound. mdr_gap_unique_rankwitnessminornonzeroevaluationmatrixpositivebound + S (mdr_i_unique_rankwitnessminornonzeroevaluationmatrixpositive) = ((rank) * (rank))) -> exists mdr_a_unique_rankwitnessminornonzeroevaluationmatrixpositive. (((exists mdr_r_unique_rankwitnessminornonzeroevaluationmatrixpositivepoint mdr_s_unique_rankwitnessminornonzeroevaluationmatrixpositivepoint mdr_u_unique_rankwitnessminornonzeroevaluationmatrixpositivepoint mdr_v_unique_rankwitnessminornonzeroevaluationmatrixpositivepoint. ((mdr_i_unique_rankwitnessminornonzeroevaluationmatrixpositive = (rank) * mdr_r_unique_rankwitnessminornonzeroevaluationmatrixpositivepoint + mdr_s_unique_rankwitnessminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_unique_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_unique_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_unique_rankwitnessminornonzeroevaluationmatrixpositivepoint) = (rank)) /\ ((((exists ff_h_mdr_unique_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_unique_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_unique_rankwitnessminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_unique_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_unique_rankwitness)) /\ exists ff_q_mdr_unique_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index. mdr_rb_unique_rankwitness = ff_q_mdr_unique_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_unique_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_unique_rankwitness) + (mdr_u_unique_rankwitnessminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_unique_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_unique_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_unique_rankwitnessminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_unique_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_unique_rankwitness)) /\ exists ff_q_mdr_unique_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_unique_rankwitness = ff_q_mdr_unique_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_unique_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_unique_rankwitness) + (mdr_v_unique_rankwitnessminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_unique_rankwitnessminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_unique_rankwitnessminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_unique_rankwitnessminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_unique_rankwitnessminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_unique_rankwitnessminornonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_unique_rankwitnessminornonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_unique_rankwitnessminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_unique_rankwitnessminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_unique_rankwitnessminornonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_unique_rankwitnessminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_unique_rankwitnessminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_unique_rankwitnessminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_unique_rankwitnessminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_unique_rankwitnessminornonzeroevaluationmatrixpositive)) * mdr_uc_unique_rankwitnessminornonzeroevaluation)) /\ exists ff_q_mdr_unique_rankwitnessminornonzeroevaluationmatrixpositiveoutput. mdr_ub_unique_rankwitnessminornonzeroevaluation = ff_q_mdr_unique_rankwitnessminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_unique_rankwitnessminornonzeroevaluationmatrixpositive)) * mdr_uc_unique_rankwitnessminornonzeroevaluation) + (mdr_a_unique_rankwitnessminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_unique_rankwitnessminornonzeroevaluationmatrixnegative. (exists mdr_gap_unique_rankwitnessminornonzeroevaluationmatrixnegativebound. mdr_gap_unique_rankwitnessminornonzeroevaluationmatrixnegativebound + S (mdr_i_unique_rankwitnessminornonzeroevaluationmatrixnegative) = ((rank) * (rank))) -> exists mdr_a_unique_rankwitnessminornonzeroevaluationmatrixnegative. (((exists mdr_r_unique_rankwitnessminornonzeroevaluationmatrixnegativepoint mdr_s_unique_rankwitnessminornonzeroevaluationmatrixnegativepoint mdr_u_unique_rankwitnessminornonzeroevaluationmatrixnegativepoint mdr_v_unique_rankwitnessminornonzeroevaluationmatrixnegativepoint. ((mdr_i_unique_rankwitnessminornonzeroevaluationmatrixnegative = (rank) * mdr_r_unique_rankwitnessminornonzeroevaluationmatrixnegativepoint + mdr_s_unique_rankwitnessminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_unique_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_unique_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_unique_rankwitnessminornonzeroevaluationmatrixnegativepoint) = (rank)) /\ ((((exists ff_h_mdr_unique_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_unique_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_unique_rankwitnessminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_unique_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_unique_rankwitness)) /\ exists ff_q_mdr_unique_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index. mdr_rb_unique_rankwitness = ff_q_mdr_unique_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_unique_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_unique_rankwitness) + (mdr_u_unique_rankwitnessminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_unique_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_unique_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_unique_rankwitnessminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_unique_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_unique_rankwitness)) /\ exists ff_q_mdr_unique_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_unique_rankwitness = ff_q_mdr_unique_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_unique_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_unique_rankwitness) + (mdr_v_unique_rankwitnessminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_unique_rankwitnessminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_unique_rankwitnessminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_unique_rankwitnessminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_unique_rankwitnessminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_unique_rankwitnessminornonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_unique_rankwitnessminornonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_unique_rankwitnessminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_unique_rankwitnessminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_unique_rankwitnessminornonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_unique_rankwitnessminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_unique_rankwitnessminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_unique_rankwitnessminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_unique_rankwitnessminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_unique_rankwitnessminornonzeroevaluationmatrixnegative)) * mdr_vc_unique_rankwitnessminornonzeroevaluation)) /\ exists ff_q_mdr_unique_rankwitnessminornonzeroevaluationmatrixnegativeoutput. mdr_vb_unique_rankwitnessminornonzeroevaluation = ff_q_mdr_unique_rankwitnessminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_unique_rankwitnessminornonzeroevaluationmatrixnegative)) * mdr_vc_unique_rankwitnessminornonzeroevaluation) + (mdr_a_unique_rankwitnessminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_unique_rankwitnessminornonzeroevaluationdeterminant mdr_c_unique_rankwitnessminornonzeroevaluationdeterminant mdr_l_unique_rankwitnessminornonzeroevaluationdeterminant mdr_i_unique_rankwitnessminornonzeroevaluationdeterminant. ((forall mdr_i_unique_rankwitnessminornonzeroevaluationdeterminanth. (exists mdr_gap_unique_rankwitnessminornonzeroevaluationdeterminanthi. mdr_gap_unique_rankwitnessminornonzeroevaluationdeterminanthi + S (mdr_i_unique_rankwitnessminornonzeroevaluationdeterminanth) = (mdr_l_unique_rankwitnessminornonzeroevaluationdeterminant)) -> exists mdr_d_unique_rankwitnessminornonzeroevaluationdeterminanth mdr_pb_unique_rankwitnessminornonzeroevaluationdeterminanth mdr_pc_unique_rankwitnessminornonzeroevaluationdeterminanth mdr_nb_unique_rankwitnessminornonzeroevaluationdeterminanth mdr_nc_unique_rankwitnessminornonzeroevaluationdeterminanth mdr_p_unique_rankwitnessminornonzeroevaluationdeterminanth mdr_n_unique_rankwitnessminornonzeroevaluationdeterminanth. ((exists mdr_z_unique_rankwitnessminornonzeroevaluationdeterminanthr. ((exists mdr_a_unique_rankwitnessminornonzeroevaluationdeterminanthrc mdr_b_unique_rankwitnessminornonzeroevaluationdeterminanthrc mdr_c_unique_rankwitnessminornonzeroevaluationdeterminanthrc mdr_e_unique_rankwitnessminornonzeroevaluationdeterminanthrc mdr_f_unique_rankwitnessminornonzeroevaluationdeterminanthrc. ((mdr_a_unique_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_d_unique_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_unique_rankwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_d_unique_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_unique_rankwitnessminornonzeroevaluationdeterminanth)) + ((mdr_pb_unique_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_unique_rankwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_b_unique_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_pc_unique_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_unique_rankwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_pc_unique_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_unique_rankwitnessminornonzeroevaluationdeterminanth)) + ((mdr_nb_unique_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_unique_rankwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_c_unique_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_a_unique_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_unique_rankwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_unique_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_unique_rankwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_b_unique_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_unique_rankwitnessminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_unique_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_p_unique_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_n_unique_rankwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_p_unique_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_n_unique_rankwitnessminornonzeroevaluationdeterminanth)) + ((mdr_n_unique_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_n_unique_rankwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_f_unique_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_nc_unique_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_e_unique_rankwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_unique_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_e_unique_rankwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_e_unique_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_e_unique_rankwitnessminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_unique_rankwitnessminornonzeroevaluationdeterminanthr) = ((mdr_c_unique_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_unique_rankwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_unique_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_unique_rankwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_f_unique_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_unique_rankwitnessminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthrb. ff_h_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthrb + S (mdr_z_unique_rankwitnessminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_unique_rankwitnessminornonzeroevaluationdeterminanth)) * mdr_c_unique_rankwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthrb. mdr_b_unique_rankwitnessminornonzeroevaluationdeterminant = ff_q_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_unique_rankwitnessminornonzeroevaluationdeterminanth)) * mdr_c_unique_rankwitnessminornonzeroevaluationdeterminant) + (mdr_z_unique_rankwitnessminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_unique_rankwitnessminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_unique_rankwitnessminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_unique_rankwitnessminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_unique_rankwitnessminornonzeroevaluationdeterminanths mdr_eb_unique_rankwitnessminornonzeroevaluationdeterminanths mdr_ec_unique_rankwitnessminornonzeroevaluationdeterminanths mdr_fb_unique_rankwitnessminornonzeroevaluationdeterminanths mdr_fc_unique_rankwitnessminornonzeroevaluationdeterminanths. (((mdr_d_unique_rankwitnessminornonzeroevaluationdeterminanth) = S (mdr_q_unique_rankwitnessminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_unique_rankwitnessminornonzeroevaluationdeterminanthsc. (exists mdr_gap_unique_rankwitnessminornonzeroevaluationdeterminanthscj. mdr_gap_unique_rankwitnessminornonzeroevaluationdeterminanthscj + S (mdr_j_unique_rankwitnessminornonzeroevaluationdeterminanthsc) = (S (mdr_q_unique_rankwitnessminornonzeroevaluationdeterminanths))) -> exists mdr_i_unique_rankwitnessminornonzeroevaluationdeterminanthsc mdr_up_unique_rankwitnessminornonzeroevaluationdeterminanthsc mdr_us_unique_rankwitnessminornonzeroevaluationdeterminanthsc mdr_un_unique_rankwitnessminornonzeroevaluationdeterminanthsc mdr_ut_unique_rankwitnessminornonzeroevaluationdeterminanthsc mdr_p_unique_rankwitnessminornonzeroevaluationdeterminanthsc mdr_n_unique_rankwitnessminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_unique_rankwitnessminornonzeroevaluationdeterminanthsci. mdr_gap_unique_rankwitnessminornonzeroevaluationdeterminanthsci + S (mdr_i_unique_rankwitnessminornonzeroevaluationdeterminanthsc) = (mdr_i_unique_rankwitnessminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_unique_rankwitnessminornonzeroevaluationdeterminanthscr. ((exists mdr_a_unique_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_b_unique_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_c_unique_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_e_unique_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_f_unique_rankwitnessminornonzeroevaluationdeterminanthscrc. ((mdr_a_unique_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_q_unique_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_up_unique_rankwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_unique_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_up_unique_rankwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_up_unique_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_up_unique_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_unique_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_us_unique_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_unique_rankwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_unique_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_unique_rankwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_un_unique_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_unique_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_unique_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_a_unique_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_unique_rankwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_unique_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_unique_rankwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_unique_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_unique_rankwitnessminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_unique_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_p_unique_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_unique_rankwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_unique_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_unique_rankwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_n_unique_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_unique_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_unique_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_ut_unique_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_e_unique_rankwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_unique_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_e_unique_rankwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_unique_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_e_unique_rankwitnessminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_unique_rankwitnessminornonzeroevaluationdeterminanthscr) = ((mdr_c_unique_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_unique_rankwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_unique_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_unique_rankwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_unique_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_unique_rankwitnessminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscrb. ff_h_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscrb + S (mdr_z_unique_rankwitnessminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_unique_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_c_unique_rankwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscrb. mdr_b_unique_rankwitnessminornonzeroevaluationdeterminant = ff_q_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_unique_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_c_unique_rankwitnessminornonzeroevaluationdeterminant) + (mdr_z_unique_rankwitnessminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_unique_rankwitnessminornonzeroevaluationdeterminanths) * (mdr_q_unique_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive = (mdr_q_unique_rankwitnessminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_unique_rankwitnessminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_unique_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_unique_rankwitnessminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_unique_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_unique_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_unique_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_unique_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_unique_rankwitnessminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_unique_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_unique_rankwitnessminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_unique_rankwitnessminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_unique_rankwitnessminornonzeroevaluationdeterminanths) * (mdr_q_unique_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative = (mdr_q_unique_rankwitnessminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_unique_rankwitnessminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_unique_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_unique_rankwitnessminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_unique_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_unique_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_unique_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_unique_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_unique_rankwitnessminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_unique_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_unique_rankwitnessminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_unique_rankwitnessminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscp. ff_h_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscp + S (mdr_p_unique_rankwitnessminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_unique_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_ec_unique_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscp. mdr_eb_unique_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_unique_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_ec_unique_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_p_unique_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscn. ff_h_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscn + S (mdr_n_unique_rankwitnessminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_unique_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_fc_unique_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscn. mdr_fb_unique_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_unique_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_fc_unique_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_n_unique_rankwitnessminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_unique_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_unique_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_unique_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_unique_rankwitnessminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_unique_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_unique_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_unique_rankwitnessminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_unique_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_unique_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_unique_rankwitnessminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_unique_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_unique_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_unique_rankwitnessminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_unique_rankwitnessminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_unique_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_unique_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_unique_rankwitnessminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_unique_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_unique_rankwitnessminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_unique_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_unique_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_unique_rankwitnessminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_unique_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_unique_rankwitnessminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_unique_rankwitnessminornonzeroevaluationdeterminanti. mdr_gap_unique_rankwitnessminornonzeroevaluationdeterminanti + S (mdr_i_unique_rankwitnessminornonzeroevaluationdeterminant) = (mdr_l_unique_rankwitnessminornonzeroevaluationdeterminant)) /\ (exists mdr_z_unique_rankwitnessminornonzeroevaluationdeterminantr. ((exists mdr_a_unique_rankwitnessminornonzeroevaluationdeterminantrc mdr_b_unique_rankwitnessminornonzeroevaluationdeterminantrc mdr_c_unique_rankwitnessminornonzeroevaluationdeterminantrc mdr_e_unique_rankwitnessminornonzeroevaluationdeterminantrc mdr_f_unique_rankwitnessminornonzeroevaluationdeterminantrc. ((mdr_a_unique_rankwitnessminornonzeroevaluationdeterminantrc = ((rank) + (mdr_ub_unique_rankwitnessminornonzeroevaluation)) * S ((rank) + (mdr_ub_unique_rankwitnessminornonzeroevaluation)) + ((mdr_ub_unique_rankwitnessminornonzeroevaluation) + (mdr_ub_unique_rankwitnessminornonzeroevaluation))) /\ ((mdr_b_unique_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_uc_unique_rankwitnessminornonzeroevaluation) + (mdr_vb_unique_rankwitnessminornonzeroevaluation)) * S ((mdr_uc_unique_rankwitnessminornonzeroevaluation) + (mdr_vb_unique_rankwitnessminornonzeroevaluation)) + ((mdr_vb_unique_rankwitnessminornonzeroevaluation) + (mdr_vb_unique_rankwitnessminornonzeroevaluation))) /\ ((mdr_c_unique_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_a_unique_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_unique_rankwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_a_unique_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_unique_rankwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_b_unique_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_unique_rankwitnessminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_unique_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_p_unique_rankwitnessminornonzero) + (mdr_n_unique_rankwitnessminornonzero)) * S ((mdr_p_unique_rankwitnessminornonzero) + (mdr_n_unique_rankwitnessminornonzero)) + ((mdr_n_unique_rankwitnessminornonzero) + (mdr_n_unique_rankwitnessminornonzero))) /\ ((mdr_f_unique_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_vc_unique_rankwitnessminornonzeroevaluation) + (mdr_e_unique_rankwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_unique_rankwitnessminornonzeroevaluation) + (mdr_e_unique_rankwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_e_unique_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_e_unique_rankwitnessminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_unique_rankwitnessminornonzeroevaluationdeterminantr) = ((mdr_c_unique_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_unique_rankwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_c_unique_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_unique_rankwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_f_unique_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_unique_rankwitnessminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_unique_rankwitnessminornonzeroevaluationdeterminantrb. ff_h_mdr_unique_rankwitnessminornonzeroevaluationdeterminantrb + S (mdr_z_unique_rankwitnessminornonzeroevaluationdeterminantr) = S ((S (mdr_i_unique_rankwitnessminornonzeroevaluationdeterminant)) * mdr_c_unique_rankwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_unique_rankwitnessminornonzeroevaluationdeterminantrb. mdr_b_unique_rankwitnessminornonzeroevaluationdeterminant = ff_q_mdr_unique_rankwitnessminornonzeroevaluationdeterminantrb * S ((S (mdr_i_unique_rankwitnessminornonzeroevaluationdeterminant)) * mdr_c_unique_rankwitnessminornonzeroevaluationdeterminant) + (mdr_z_unique_rankwitnessminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_unique_rankwitnessminornonzero = mdr_n_unique_rankwitnessminornonzero)))))))) /\ (forall mdr_q_unique_rank. (exists mdr_gap_unique_rankhigher. mdr_gap_unique_rankhigher + S (rank) = (mdr_q_unique_rank)) -> (forall mdr_rb_unique_rankzero mdr_rc_unique_rankzero mdr_cb_unique_rankzero mdr_cc_unique_rankzero mdr_p_unique_rankzero mdr_n_unique_rankzero. (((forall fom_index_mrf_unique_rankzerorowsbound. (exists fom_gap_mrf_unique_rankzerorowsbound_index_bound. fom_gap_mrf_unique_rankzerorowsbound_index_bound + S (fom_index_mrf_unique_rankzerorowsbound) = mdr_q_unique_rank) -> exists fom_value_mrf_unique_rankzerorowsbound. ((((exists fom_beta_height_mrf_unique_rankzerorowsbound_entry. fom_beta_height_mrf_unique_rankzerorowsbound_entry + S (fom_value_mrf_unique_rankzerorowsbound) = S ((S (fom_index_mrf_unique_rankzerorowsbound)) * mdr_rc_unique_rankzero)) /\ exists fom_beta_quotient_mrf_unique_rankzerorowsbound_entry. mdr_rb_unique_rankzero = fom_beta_quotient_mrf_unique_rankzerorowsbound_entry * S ((S (fom_index_mrf_unique_rankzerorowsbound)) * mdr_rc_unique_rankzero) + (fom_value_mrf_unique_rankzerorowsbound))) /\ (exists fom_gap_mrf_unique_rankzerorowsbound_value_bound. fom_gap_mrf_unique_rankzerorowsbound_value_bound + S (fom_value_mrf_unique_rankzerorowsbound) = r))) /\ (forall mdr_i_unique_rankzerorowsdistinct mdr_j_unique_rankzerorowsdistinct mdr_a_unique_rankzerorowsdistinct. (exists mdr_gap_unique_rankzerorowsdistincti. mdr_gap_unique_rankzerorowsdistincti + S (mdr_i_unique_rankzerorowsdistinct) = (mdr_q_unique_rank)) -> (exists mdr_gap_unique_rankzerorowsdistinctj. mdr_gap_unique_rankzerorowsdistinctj + S (mdr_j_unique_rankzerorowsdistinct) = (mdr_q_unique_rank)) -> (((exists ff_h_mdr_unique_rankzerorowsdistinctfirst. ff_h_mdr_unique_rankzerorowsdistinctfirst + S (mdr_a_unique_rankzerorowsdistinct) = S ((S (mdr_i_unique_rankzerorowsdistinct)) * mdr_rc_unique_rankzero)) /\ exists ff_q_mdr_unique_rankzerorowsdistinctfirst. mdr_rb_unique_rankzero = ff_q_mdr_unique_rankzerorowsdistinctfirst * S ((S (mdr_i_unique_rankzerorowsdistinct)) * mdr_rc_unique_rankzero) + (mdr_a_unique_rankzerorowsdistinct))) -> (((exists ff_h_mdr_unique_rankzerorowsdistinctsecond. ff_h_mdr_unique_rankzerorowsdistinctsecond + S (mdr_a_unique_rankzerorowsdistinct) = S ((S (mdr_j_unique_rankzerorowsdistinct)) * mdr_rc_unique_rankzero)) /\ exists ff_q_mdr_unique_rankzerorowsdistinctsecond. mdr_rb_unique_rankzero = ff_q_mdr_unique_rankzerorowsdistinctsecond * S ((S (mdr_j_unique_rankzerorowsdistinct)) * mdr_rc_unique_rankzero) + (mdr_a_unique_rankzerorowsdistinct))) -> mdr_i_unique_rankzerorowsdistinct = mdr_j_unique_rankzerorowsdistinct))) -> (((forall fom_index_mrf_unique_rankzerocolumnsbound. (exists fom_gap_mrf_unique_rankzerocolumnsbound_index_bound. fom_gap_mrf_unique_rankzerocolumnsbound_index_bound + S (fom_index_mrf_unique_rankzerocolumnsbound) = mdr_q_unique_rank) -> exists fom_value_mrf_unique_rankzerocolumnsbound. ((((exists fom_beta_height_mrf_unique_rankzerocolumnsbound_entry. fom_beta_height_mrf_unique_rankzerocolumnsbound_entry + S (fom_value_mrf_unique_rankzerocolumnsbound) = S ((S (fom_index_mrf_unique_rankzerocolumnsbound)) * mdr_cc_unique_rankzero)) /\ exists fom_beta_quotient_mrf_unique_rankzerocolumnsbound_entry. mdr_cb_unique_rankzero = fom_beta_quotient_mrf_unique_rankzerocolumnsbound_entry * S ((S (fom_index_mrf_unique_rankzerocolumnsbound)) * mdr_cc_unique_rankzero) + (fom_value_mrf_unique_rankzerocolumnsbound))) /\ (exists fom_gap_mrf_unique_rankzerocolumnsbound_value_bound. fom_gap_mrf_unique_rankzerocolumnsbound_value_bound + S (fom_value_mrf_unique_rankzerocolumnsbound) = w))) /\ (forall mdr_i_unique_rankzerocolumnsdistinct mdr_j_unique_rankzerocolumnsdistinct mdr_a_unique_rankzerocolumnsdistinct. (exists mdr_gap_unique_rankzerocolumnsdistincti. mdr_gap_unique_rankzerocolumnsdistincti + S (mdr_i_unique_rankzerocolumnsdistinct) = (mdr_q_unique_rank)) -> (exists mdr_gap_unique_rankzerocolumnsdistinctj. mdr_gap_unique_rankzerocolumnsdistinctj + S (mdr_j_unique_rankzerocolumnsdistinct) = (mdr_q_unique_rank)) -> (((exists ff_h_mdr_unique_rankzerocolumnsdistinctfirst. ff_h_mdr_unique_rankzerocolumnsdistinctfirst + S (mdr_a_unique_rankzerocolumnsdistinct) = S ((S (mdr_i_unique_rankzerocolumnsdistinct)) * mdr_cc_unique_rankzero)) /\ exists ff_q_mdr_unique_rankzerocolumnsdistinctfirst. mdr_cb_unique_rankzero = ff_q_mdr_unique_rankzerocolumnsdistinctfirst * S ((S (mdr_i_unique_rankzerocolumnsdistinct)) * mdr_cc_unique_rankzero) + (mdr_a_unique_rankzerocolumnsdistinct))) -> (((exists ff_h_mdr_unique_rankzerocolumnsdistinctsecond. ff_h_mdr_unique_rankzerocolumnsdistinctsecond + S (mdr_a_unique_rankzerocolumnsdistinct) = S ((S (mdr_j_unique_rankzerocolumnsdistinct)) * mdr_cc_unique_rankzero)) /\ exists ff_q_mdr_unique_rankzerocolumnsdistinctsecond. mdr_cb_unique_rankzero = ff_q_mdr_unique_rankzerocolumnsdistinctsecond * S ((S (mdr_j_unique_rankzerocolumnsdistinct)) * mdr_cc_unique_rankzero) + (mdr_a_unique_rankzerocolumnsdistinct))) -> mdr_i_unique_rankzerocolumnsdistinct = mdr_j_unique_rankzerocolumnsdistinct))) -> (exists mdr_ub_unique_rankzeroevaluation mdr_uc_unique_rankzeroevaluation mdr_vb_unique_rankzeroevaluation mdr_vc_unique_rankzeroevaluation. ((((forall mdr_i_unique_rankzeroevaluationmatrixpositive. (exists mdr_gap_unique_rankzeroevaluationmatrixpositivebound. mdr_gap_unique_rankzeroevaluationmatrixpositivebound + S (mdr_i_unique_rankzeroevaluationmatrixpositive) = ((mdr_q_unique_rank) * (mdr_q_unique_rank))) -> exists mdr_a_unique_rankzeroevaluationmatrixpositive. (((exists mdr_r_unique_rankzeroevaluationmatrixpositivepoint mdr_s_unique_rankzeroevaluationmatrixpositivepoint mdr_u_unique_rankzeroevaluationmatrixpositivepoint mdr_v_unique_rankzeroevaluationmatrixpositivepoint. ((mdr_i_unique_rankzeroevaluationmatrixpositive = (mdr_q_unique_rank) * mdr_r_unique_rankzeroevaluationmatrixpositivepoint + mdr_s_unique_rankzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_unique_rankzeroevaluationmatrixpositivepointcolumn. mdr_gap_unique_rankzeroevaluationmatrixpositivepointcolumn + S (mdr_s_unique_rankzeroevaluationmatrixpositivepoint) = (mdr_q_unique_rank)) /\ ((((exists ff_h_mdr_unique_rankzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_unique_rankzeroevaluationmatrixpositivepointrow_index + S (mdr_u_unique_rankzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_unique_rankzeroevaluationmatrixpositivepoint)) * mdr_rc_unique_rankzero)) /\ exists ff_q_mdr_unique_rankzeroevaluationmatrixpositivepointrow_index. mdr_rb_unique_rankzero = ff_q_mdr_unique_rankzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_unique_rankzeroevaluationmatrixpositivepoint)) * mdr_rc_unique_rankzero) + (mdr_u_unique_rankzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_unique_rankzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_unique_rankzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_unique_rankzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_unique_rankzeroevaluationmatrixpositivepoint)) * mdr_cc_unique_rankzero)) /\ exists ff_q_mdr_unique_rankzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_unique_rankzero = ff_q_mdr_unique_rankzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_unique_rankzeroevaluationmatrixpositivepoint)) * mdr_cc_unique_rankzero) + (mdr_v_unique_rankzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_unique_rankzeroevaluationmatrixpositivepointsource. ff_h_mdr_unique_rankzeroevaluationmatrixpositivepointsource + S (mdr_a_unique_rankzeroevaluationmatrixpositive) = S ((S ((mdr_u_unique_rankzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_unique_rankzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_unique_rankzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_unique_rankzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_unique_rankzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_unique_rankzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_unique_rankzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_unique_rankzeroevaluationmatrixpositiveoutput. ff_h_mdr_unique_rankzeroevaluationmatrixpositiveoutput + S (mdr_a_unique_rankzeroevaluationmatrixpositive) = S ((S (mdr_i_unique_rankzeroevaluationmatrixpositive)) * mdr_uc_unique_rankzeroevaluation)) /\ exists ff_q_mdr_unique_rankzeroevaluationmatrixpositiveoutput. mdr_ub_unique_rankzeroevaluation = ff_q_mdr_unique_rankzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_unique_rankzeroevaluationmatrixpositive)) * mdr_uc_unique_rankzeroevaluation) + (mdr_a_unique_rankzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_unique_rankzeroevaluationmatrixnegative. (exists mdr_gap_unique_rankzeroevaluationmatrixnegativebound. mdr_gap_unique_rankzeroevaluationmatrixnegativebound + S (mdr_i_unique_rankzeroevaluationmatrixnegative) = ((mdr_q_unique_rank) * (mdr_q_unique_rank))) -> exists mdr_a_unique_rankzeroevaluationmatrixnegative. (((exists mdr_r_unique_rankzeroevaluationmatrixnegativepoint mdr_s_unique_rankzeroevaluationmatrixnegativepoint mdr_u_unique_rankzeroevaluationmatrixnegativepoint mdr_v_unique_rankzeroevaluationmatrixnegativepoint. ((mdr_i_unique_rankzeroevaluationmatrixnegative = (mdr_q_unique_rank) * mdr_r_unique_rankzeroevaluationmatrixnegativepoint + mdr_s_unique_rankzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_unique_rankzeroevaluationmatrixnegativepointcolumn. mdr_gap_unique_rankzeroevaluationmatrixnegativepointcolumn + S (mdr_s_unique_rankzeroevaluationmatrixnegativepoint) = (mdr_q_unique_rank)) /\ ((((exists ff_h_mdr_unique_rankzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_unique_rankzeroevaluationmatrixnegativepointrow_index + S (mdr_u_unique_rankzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_unique_rankzeroevaluationmatrixnegativepoint)) * mdr_rc_unique_rankzero)) /\ exists ff_q_mdr_unique_rankzeroevaluationmatrixnegativepointrow_index. mdr_rb_unique_rankzero = ff_q_mdr_unique_rankzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_unique_rankzeroevaluationmatrixnegativepoint)) * mdr_rc_unique_rankzero) + (mdr_u_unique_rankzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_unique_rankzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_unique_rankzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_unique_rankzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_unique_rankzeroevaluationmatrixnegativepoint)) * mdr_cc_unique_rankzero)) /\ exists ff_q_mdr_unique_rankzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_unique_rankzero = ff_q_mdr_unique_rankzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_unique_rankzeroevaluationmatrixnegativepoint)) * mdr_cc_unique_rankzero) + (mdr_v_unique_rankzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_unique_rankzeroevaluationmatrixnegativepointsource. ff_h_mdr_unique_rankzeroevaluationmatrixnegativepointsource + S (mdr_a_unique_rankzeroevaluationmatrixnegative) = S ((S ((mdr_u_unique_rankzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_unique_rankzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_unique_rankzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_unique_rankzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_unique_rankzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_unique_rankzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_unique_rankzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_unique_rankzeroevaluationmatrixnegativeoutput. ff_h_mdr_unique_rankzeroevaluationmatrixnegativeoutput + S (mdr_a_unique_rankzeroevaluationmatrixnegative) = S ((S (mdr_i_unique_rankzeroevaluationmatrixnegative)) * mdr_vc_unique_rankzeroevaluation)) /\ exists ff_q_mdr_unique_rankzeroevaluationmatrixnegativeoutput. mdr_vb_unique_rankzeroevaluation = ff_q_mdr_unique_rankzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_unique_rankzeroevaluationmatrixnegative)) * mdr_vc_unique_rankzeroevaluation) + (mdr_a_unique_rankzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_unique_rankzeroevaluationdeterminant mdr_c_unique_rankzeroevaluationdeterminant mdr_l_unique_rankzeroevaluationdeterminant mdr_i_unique_rankzeroevaluationdeterminant. ((forall mdr_i_unique_rankzeroevaluationdeterminanth. (exists mdr_gap_unique_rankzeroevaluationdeterminanthi. mdr_gap_unique_rankzeroevaluationdeterminanthi + S (mdr_i_unique_rankzeroevaluationdeterminanth) = (mdr_l_unique_rankzeroevaluationdeterminant)) -> exists mdr_d_unique_rankzeroevaluationdeterminanth mdr_pb_unique_rankzeroevaluationdeterminanth mdr_pc_unique_rankzeroevaluationdeterminanth mdr_nb_unique_rankzeroevaluationdeterminanth mdr_nc_unique_rankzeroevaluationdeterminanth mdr_p_unique_rankzeroevaluationdeterminanth mdr_n_unique_rankzeroevaluationdeterminanth. ((exists mdr_z_unique_rankzeroevaluationdeterminanthr. ((exists mdr_a_unique_rankzeroevaluationdeterminanthrc mdr_b_unique_rankzeroevaluationdeterminanthrc mdr_c_unique_rankzeroevaluationdeterminanthrc mdr_e_unique_rankzeroevaluationdeterminanthrc mdr_f_unique_rankzeroevaluationdeterminanthrc. ((mdr_a_unique_rankzeroevaluationdeterminanthrc = ((mdr_d_unique_rankzeroevaluationdeterminanth) + (mdr_pb_unique_rankzeroevaluationdeterminanth)) * S ((mdr_d_unique_rankzeroevaluationdeterminanth) + (mdr_pb_unique_rankzeroevaluationdeterminanth)) + ((mdr_pb_unique_rankzeroevaluationdeterminanth) + (mdr_pb_unique_rankzeroevaluationdeterminanth))) /\ ((mdr_b_unique_rankzeroevaluationdeterminanthrc = ((mdr_pc_unique_rankzeroevaluationdeterminanth) + (mdr_nb_unique_rankzeroevaluationdeterminanth)) * S ((mdr_pc_unique_rankzeroevaluationdeterminanth) + (mdr_nb_unique_rankzeroevaluationdeterminanth)) + ((mdr_nb_unique_rankzeroevaluationdeterminanth) + (mdr_nb_unique_rankzeroevaluationdeterminanth))) /\ ((mdr_c_unique_rankzeroevaluationdeterminanthrc = ((mdr_a_unique_rankzeroevaluationdeterminanthrc) + (mdr_b_unique_rankzeroevaluationdeterminanthrc)) * S ((mdr_a_unique_rankzeroevaluationdeterminanthrc) + (mdr_b_unique_rankzeroevaluationdeterminanthrc)) + ((mdr_b_unique_rankzeroevaluationdeterminanthrc) + (mdr_b_unique_rankzeroevaluationdeterminanthrc))) /\ ((mdr_e_unique_rankzeroevaluationdeterminanthrc = ((mdr_p_unique_rankzeroevaluationdeterminanth) + (mdr_n_unique_rankzeroevaluationdeterminanth)) * S ((mdr_p_unique_rankzeroevaluationdeterminanth) + (mdr_n_unique_rankzeroevaluationdeterminanth)) + ((mdr_n_unique_rankzeroevaluationdeterminanth) + (mdr_n_unique_rankzeroevaluationdeterminanth))) /\ ((mdr_f_unique_rankzeroevaluationdeterminanthrc = ((mdr_nc_unique_rankzeroevaluationdeterminanth) + (mdr_e_unique_rankzeroevaluationdeterminanthrc)) * S ((mdr_nc_unique_rankzeroevaluationdeterminanth) + (mdr_e_unique_rankzeroevaluationdeterminanthrc)) + ((mdr_e_unique_rankzeroevaluationdeterminanthrc) + (mdr_e_unique_rankzeroevaluationdeterminanthrc))) /\ ((mdr_z_unique_rankzeroevaluationdeterminanthr) = ((mdr_c_unique_rankzeroevaluationdeterminanthrc) + (mdr_f_unique_rankzeroevaluationdeterminanthrc)) * S ((mdr_c_unique_rankzeroevaluationdeterminanthrc) + (mdr_f_unique_rankzeroevaluationdeterminanthrc)) + ((mdr_f_unique_rankzeroevaluationdeterminanthrc) + (mdr_f_unique_rankzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_unique_rankzeroevaluationdeterminanthrb. ff_h_mdr_unique_rankzeroevaluationdeterminanthrb + S (mdr_z_unique_rankzeroevaluationdeterminanthr) = S ((S (mdr_i_unique_rankzeroevaluationdeterminanth)) * mdr_c_unique_rankzeroevaluationdeterminant)) /\ exists ff_q_mdr_unique_rankzeroevaluationdeterminanthrb. mdr_b_unique_rankzeroevaluationdeterminant = ff_q_mdr_unique_rankzeroevaluationdeterminanthrb * S ((S (mdr_i_unique_rankzeroevaluationdeterminanth)) * mdr_c_unique_rankzeroevaluationdeterminant) + (mdr_z_unique_rankzeroevaluationdeterminanthr))))) /\ (((((mdr_d_unique_rankzeroevaluationdeterminanth) = 0) /\ (((mdr_p_unique_rankzeroevaluationdeterminanth) = 1) /\ ((mdr_n_unique_rankzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_unique_rankzeroevaluationdeterminanths mdr_eb_unique_rankzeroevaluationdeterminanths mdr_ec_unique_rankzeroevaluationdeterminanths mdr_fb_unique_rankzeroevaluationdeterminanths mdr_fc_unique_rankzeroevaluationdeterminanths. (((mdr_d_unique_rankzeroevaluationdeterminanth) = S (mdr_q_unique_rankzeroevaluationdeterminanths)) /\ ((forall mdr_j_unique_rankzeroevaluationdeterminanthsc. (exists mdr_gap_unique_rankzeroevaluationdeterminanthscj. mdr_gap_unique_rankzeroevaluationdeterminanthscj + S (mdr_j_unique_rankzeroevaluationdeterminanthsc) = (S (mdr_q_unique_rankzeroevaluationdeterminanths))) -> exists mdr_i_unique_rankzeroevaluationdeterminanthsc mdr_up_unique_rankzeroevaluationdeterminanthsc mdr_us_unique_rankzeroevaluationdeterminanthsc mdr_un_unique_rankzeroevaluationdeterminanthsc mdr_ut_unique_rankzeroevaluationdeterminanthsc mdr_p_unique_rankzeroevaluationdeterminanthsc mdr_n_unique_rankzeroevaluationdeterminanthsc. ((exists mdr_gap_unique_rankzeroevaluationdeterminanthsci. mdr_gap_unique_rankzeroevaluationdeterminanthsci + S (mdr_i_unique_rankzeroevaluationdeterminanthsc) = (mdr_i_unique_rankzeroevaluationdeterminanth)) /\ ((exists mdr_z_unique_rankzeroevaluationdeterminanthscr. ((exists mdr_a_unique_rankzeroevaluationdeterminanthscrc mdr_b_unique_rankzeroevaluationdeterminanthscrc mdr_c_unique_rankzeroevaluationdeterminanthscrc mdr_e_unique_rankzeroevaluationdeterminanthscrc mdr_f_unique_rankzeroevaluationdeterminanthscrc. ((mdr_a_unique_rankzeroevaluationdeterminanthscrc = ((mdr_q_unique_rankzeroevaluationdeterminanths) + (mdr_up_unique_rankzeroevaluationdeterminanthsc)) * S ((mdr_q_unique_rankzeroevaluationdeterminanths) + (mdr_up_unique_rankzeroevaluationdeterminanthsc)) + ((mdr_up_unique_rankzeroevaluationdeterminanthsc) + (mdr_up_unique_rankzeroevaluationdeterminanthsc))) /\ ((mdr_b_unique_rankzeroevaluationdeterminanthscrc = ((mdr_us_unique_rankzeroevaluationdeterminanthsc) + (mdr_un_unique_rankzeroevaluationdeterminanthsc)) * S ((mdr_us_unique_rankzeroevaluationdeterminanthsc) + (mdr_un_unique_rankzeroevaluationdeterminanthsc)) + ((mdr_un_unique_rankzeroevaluationdeterminanthsc) + (mdr_un_unique_rankzeroevaluationdeterminanthsc))) /\ ((mdr_c_unique_rankzeroevaluationdeterminanthscrc = ((mdr_a_unique_rankzeroevaluationdeterminanthscrc) + (mdr_b_unique_rankzeroevaluationdeterminanthscrc)) * S ((mdr_a_unique_rankzeroevaluationdeterminanthscrc) + (mdr_b_unique_rankzeroevaluationdeterminanthscrc)) + ((mdr_b_unique_rankzeroevaluationdeterminanthscrc) + (mdr_b_unique_rankzeroevaluationdeterminanthscrc))) /\ ((mdr_e_unique_rankzeroevaluationdeterminanthscrc = ((mdr_p_unique_rankzeroevaluationdeterminanthsc) + (mdr_n_unique_rankzeroevaluationdeterminanthsc)) * S ((mdr_p_unique_rankzeroevaluationdeterminanthsc) + (mdr_n_unique_rankzeroevaluationdeterminanthsc)) + ((mdr_n_unique_rankzeroevaluationdeterminanthsc) + (mdr_n_unique_rankzeroevaluationdeterminanthsc))) /\ ((mdr_f_unique_rankzeroevaluationdeterminanthscrc = ((mdr_ut_unique_rankzeroevaluationdeterminanthsc) + (mdr_e_unique_rankzeroevaluationdeterminanthscrc)) * S ((mdr_ut_unique_rankzeroevaluationdeterminanthsc) + (mdr_e_unique_rankzeroevaluationdeterminanthscrc)) + ((mdr_e_unique_rankzeroevaluationdeterminanthscrc) + (mdr_e_unique_rankzeroevaluationdeterminanthscrc))) /\ ((mdr_z_unique_rankzeroevaluationdeterminanthscr) = ((mdr_c_unique_rankzeroevaluationdeterminanthscrc) + (mdr_f_unique_rankzeroevaluationdeterminanthscrc)) * S ((mdr_c_unique_rankzeroevaluationdeterminanthscrc) + (mdr_f_unique_rankzeroevaluationdeterminanthscrc)) + ((mdr_f_unique_rankzeroevaluationdeterminanthscrc) + (mdr_f_unique_rankzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_unique_rankzeroevaluationdeterminanthscrb. ff_h_mdr_unique_rankzeroevaluationdeterminanthscrb + S (mdr_z_unique_rankzeroevaluationdeterminanthscr) = S ((S (mdr_i_unique_rankzeroevaluationdeterminanthsc)) * mdr_c_unique_rankzeroevaluationdeterminant)) /\ exists ff_q_mdr_unique_rankzeroevaluationdeterminanthscrb. mdr_b_unique_rankzeroevaluationdeterminant = ff_q_mdr_unique_rankzeroevaluationdeterminanthscrb * S ((S (mdr_i_unique_rankzeroevaluationdeterminanthsc)) * mdr_c_unique_rankzeroevaluationdeterminant) + (mdr_z_unique_rankzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_unique_rankzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_unique_rankzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_positive) = ((mdr_q_unique_rankzeroevaluationdeterminanths) * (mdr_q_unique_rankzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_positive = (mdr_q_unique_rankzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_unique_rankzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_unique_rankzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_positive) = (mdr_q_unique_rankzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_unique_rankzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_unique_rankzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_unique_rankzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_unique_rankzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_unique_rankzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_unique_rankzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_unique_rankzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_unique_rankzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_unique_rankzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_unique_rankzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_positive) = (mdr_j_unique_rankzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_unique_rankzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_unique_rankzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_unique_rankzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_unique_rankzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_unique_rankzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_unique_rankzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_unique_rankzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_unique_rankzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_unique_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_unique_rankzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_unique_rankzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_unique_rankzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_unique_rankzeroevaluationdeterminanth = ff_q_mdm_mdr_unique_rankzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_unique_rankzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_unique_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_unique_rankzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_unique_rankzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_unique_rankzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_unique_rankzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_positive)) * mdr_us_unique_rankzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_unique_rankzeroevaluationdeterminanthscm_positive_target. mdr_up_unique_rankzeroevaluationdeterminanthsc = ff_q_mdm_mdr_unique_rankzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_positive)) * mdr_us_unique_rankzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_unique_rankzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_unique_rankzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_negative) = ((mdr_q_unique_rankzeroevaluationdeterminanths) * (mdr_q_unique_rankzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_negative = (mdr_q_unique_rankzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_unique_rankzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_unique_rankzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_negative) = (mdr_q_unique_rankzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_unique_rankzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_unique_rankzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_unique_rankzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_unique_rankzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_unique_rankzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_unique_rankzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_unique_rankzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_unique_rankzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_unique_rankzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_unique_rankzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_negative) = (mdr_j_unique_rankzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_unique_rankzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_unique_rankzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_unique_rankzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_unique_rankzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_unique_rankzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_unique_rankzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_unique_rankzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_unique_rankzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_unique_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_unique_rankzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_unique_rankzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_unique_rankzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_unique_rankzeroevaluationdeterminanth = ff_q_mdm_mdr_unique_rankzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_unique_rankzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_unique_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_unique_rankzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_unique_rankzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_unique_rankzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_unique_rankzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_negative)) * mdr_ut_unique_rankzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_unique_rankzeroevaluationdeterminanthscm_negative_target. mdr_un_unique_rankzeroevaluationdeterminanthsc = ff_q_mdm_mdr_unique_rankzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_negative)) * mdr_ut_unique_rankzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_unique_rankzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_unique_rankzeroevaluationdeterminanthscp. ff_h_mdr_unique_rankzeroevaluationdeterminanthscp + S (mdr_p_unique_rankzeroevaluationdeterminanthsc) = S ((S (mdr_j_unique_rankzeroevaluationdeterminanthsc)) * mdr_ec_unique_rankzeroevaluationdeterminanths)) /\ exists ff_q_mdr_unique_rankzeroevaluationdeterminanthscp. mdr_eb_unique_rankzeroevaluationdeterminanths = ff_q_mdr_unique_rankzeroevaluationdeterminanthscp * S ((S (mdr_j_unique_rankzeroevaluationdeterminanthsc)) * mdr_ec_unique_rankzeroevaluationdeterminanths) + (mdr_p_unique_rankzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_unique_rankzeroevaluationdeterminanthscn. ff_h_mdr_unique_rankzeroevaluationdeterminanthscn + S (mdr_n_unique_rankzeroevaluationdeterminanthsc) = S ((S (mdr_j_unique_rankzeroevaluationdeterminanthsc)) * mdr_fc_unique_rankzeroevaluationdeterminanths)) /\ exists ff_q_mdr_unique_rankzeroevaluationdeterminanthscn. mdr_fb_unique_rankzeroevaluationdeterminanths = ff_q_mdr_unique_rankzeroevaluationdeterminanthscn * S ((S (mdr_j_unique_rankzeroevaluationdeterminanthsc)) * mdr_fc_unique_rankzeroevaluationdeterminanths) + (mdr_n_unique_rankzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_unique_rankzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_unique_rankzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_unique_rankzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_unique_rankzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_unique_rankzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix)) * mdr_pc_unique_rankzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_unique_rankzeroevaluationdeterminanth = ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix)) * mdr_pc_unique_rankzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix)) * mdr_nc_unique_rankzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_an. mdr_nb_unique_rankzeroevaluationdeterminanth = ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix)) * mdr_nc_unique_rankzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix)) * mdr_ec_unique_rankzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_unique_rankzeroevaluationdeterminanths = ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix)) * mdr_ec_unique_rankzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix)) * mdr_fc_unique_rankzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_unique_rankzeroevaluationdeterminanths = ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix)) * mdr_fc_unique_rankzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_unique_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_unique_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_unique_rankzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_unique_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_unique_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_unique_rankzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_unique_rankzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_unique_rankzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_unique_rankzeroevaluationdeterminanth) = S ((S ((S (mdr_q_unique_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_unique_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive) + (mdr_p_unique_rankzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive = (S (mdr_q_unique_rankzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_unique_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_unique_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_unique_rankzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_unique_rankzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_unique_rankzeroevaluationdeterminanth) = S ((S ((S (mdr_q_unique_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_unique_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative) + (mdr_n_unique_rankzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative = (S (mdr_q_unique_rankzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_unique_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_unique_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_unique_rankzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_unique_rankzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_unique_rankzeroevaluationdeterminanti. mdr_gap_unique_rankzeroevaluationdeterminanti + S (mdr_i_unique_rankzeroevaluationdeterminant) = (mdr_l_unique_rankzeroevaluationdeterminant)) /\ (exists mdr_z_unique_rankzeroevaluationdeterminantr. ((exists mdr_a_unique_rankzeroevaluationdeterminantrc mdr_b_unique_rankzeroevaluationdeterminantrc mdr_c_unique_rankzeroevaluationdeterminantrc mdr_e_unique_rankzeroevaluationdeterminantrc mdr_f_unique_rankzeroevaluationdeterminantrc. ((mdr_a_unique_rankzeroevaluationdeterminantrc = ((mdr_q_unique_rank) + (mdr_ub_unique_rankzeroevaluation)) * S ((mdr_q_unique_rank) + (mdr_ub_unique_rankzeroevaluation)) + ((mdr_ub_unique_rankzeroevaluation) + (mdr_ub_unique_rankzeroevaluation))) /\ ((mdr_b_unique_rankzeroevaluationdeterminantrc = ((mdr_uc_unique_rankzeroevaluation) + (mdr_vb_unique_rankzeroevaluation)) * S ((mdr_uc_unique_rankzeroevaluation) + (mdr_vb_unique_rankzeroevaluation)) + ((mdr_vb_unique_rankzeroevaluation) + (mdr_vb_unique_rankzeroevaluation))) /\ ((mdr_c_unique_rankzeroevaluationdeterminantrc = ((mdr_a_unique_rankzeroevaluationdeterminantrc) + (mdr_b_unique_rankzeroevaluationdeterminantrc)) * S ((mdr_a_unique_rankzeroevaluationdeterminantrc) + (mdr_b_unique_rankzeroevaluationdeterminantrc)) + ((mdr_b_unique_rankzeroevaluationdeterminantrc) + (mdr_b_unique_rankzeroevaluationdeterminantrc))) /\ ((mdr_e_unique_rankzeroevaluationdeterminantrc = ((mdr_p_unique_rankzero) + (mdr_n_unique_rankzero)) * S ((mdr_p_unique_rankzero) + (mdr_n_unique_rankzero)) + ((mdr_n_unique_rankzero) + (mdr_n_unique_rankzero))) /\ ((mdr_f_unique_rankzeroevaluationdeterminantrc = ((mdr_vc_unique_rankzeroevaluation) + (mdr_e_unique_rankzeroevaluationdeterminantrc)) * S ((mdr_vc_unique_rankzeroevaluation) + (mdr_e_unique_rankzeroevaluationdeterminantrc)) + ((mdr_e_unique_rankzeroevaluationdeterminantrc) + (mdr_e_unique_rankzeroevaluationdeterminantrc))) /\ ((mdr_z_unique_rankzeroevaluationdeterminantr) = ((mdr_c_unique_rankzeroevaluationdeterminantrc) + (mdr_f_unique_rankzeroevaluationdeterminantrc)) * S ((mdr_c_unique_rankzeroevaluationdeterminantrc) + (mdr_f_unique_rankzeroevaluationdeterminantrc)) + ((mdr_f_unique_rankzeroevaluationdeterminantrc) + (mdr_f_unique_rankzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_unique_rankzeroevaluationdeterminantrb. ff_h_mdr_unique_rankzeroevaluationdeterminantrb + S (mdr_z_unique_rankzeroevaluationdeterminantr) = S ((S (mdr_i_unique_rankzeroevaluationdeterminant)) * mdr_c_unique_rankzeroevaluationdeterminant)) /\ exists ff_q_mdr_unique_rankzeroevaluationdeterminantrb. mdr_b_unique_rankzeroevaluationdeterminant = ff_q_mdr_unique_rankzeroevaluationdeterminantrb * S ((S (mdr_i_unique_rankzeroevaluationdeterminant)) * mdr_c_unique_rankzeroevaluationdeterminant) + (mdr_z_unique_rankzeroevaluationdeterminantr)))))))))) -> mdr_p_unique_rankzero = mdr_n_unique_rankzero)))))) /\ (forall other. (((exists mdr_gap_other_rankrows_bound. mdr_gap_other_rankrows_bound + (other) = (r)) /\ ((exists mdr_gap_other_rankcolumns_bound. mdr_gap_other_rankcolumns_bound + (other) = (w)) /\ ((exists mdr_rb_other_rankwitness mdr_rc_other_rankwitness mdr_cb_other_rankwitness mdr_cc_other_rankwitness. (((((forall fom_index_mrf_other_rankwitnessminorrowsbound. (exists fom_gap_mrf_other_rankwitnessminorrowsbound_index_bound. fom_gap_mrf_other_rankwitnessminorrowsbound_index_bound + S (fom_index_mrf_other_rankwitnessminorrowsbound) = other) -> exists fom_value_mrf_other_rankwitnessminorrowsbound. ((((exists fom_beta_height_mrf_other_rankwitnessminorrowsbound_entry. fom_beta_height_mrf_other_rankwitnessminorrowsbound_entry + S (fom_value_mrf_other_rankwitnessminorrowsbound) = S ((S (fom_index_mrf_other_rankwitnessminorrowsbound)) * mdr_rc_other_rankwitness)) /\ exists fom_beta_quotient_mrf_other_rankwitnessminorrowsbound_entry. mdr_rb_other_rankwitness = fom_beta_quotient_mrf_other_rankwitnessminorrowsbound_entry * S ((S (fom_index_mrf_other_rankwitnessminorrowsbound)) * mdr_rc_other_rankwitness) + (fom_value_mrf_other_rankwitnessminorrowsbound))) /\ (exists fom_gap_mrf_other_rankwitnessminorrowsbound_value_bound. fom_gap_mrf_other_rankwitnessminorrowsbound_value_bound + S (fom_value_mrf_other_rankwitnessminorrowsbound) = r))) /\ (forall mdr_i_other_rankwitnessminorrowsdistinct mdr_j_other_rankwitnessminorrowsdistinct mdr_a_other_rankwitnessminorrowsdistinct. (exists mdr_gap_other_rankwitnessminorrowsdistincti. mdr_gap_other_rankwitnessminorrowsdistincti + S (mdr_i_other_rankwitnessminorrowsdistinct) = (other)) -> (exists mdr_gap_other_rankwitnessminorrowsdistinctj. mdr_gap_other_rankwitnessminorrowsdistinctj + S (mdr_j_other_rankwitnessminorrowsdistinct) = (other)) -> (((exists ff_h_mdr_other_rankwitnessminorrowsdistinctfirst. ff_h_mdr_other_rankwitnessminorrowsdistinctfirst + S (mdr_a_other_rankwitnessminorrowsdistinct) = S ((S (mdr_i_other_rankwitnessminorrowsdistinct)) * mdr_rc_other_rankwitness)) /\ exists ff_q_mdr_other_rankwitnessminorrowsdistinctfirst. mdr_rb_other_rankwitness = ff_q_mdr_other_rankwitnessminorrowsdistinctfirst * S ((S (mdr_i_other_rankwitnessminorrowsdistinct)) * mdr_rc_other_rankwitness) + (mdr_a_other_rankwitnessminorrowsdistinct))) -> (((exists ff_h_mdr_other_rankwitnessminorrowsdistinctsecond. ff_h_mdr_other_rankwitnessminorrowsdistinctsecond + S (mdr_a_other_rankwitnessminorrowsdistinct) = S ((S (mdr_j_other_rankwitnessminorrowsdistinct)) * mdr_rc_other_rankwitness)) /\ exists ff_q_mdr_other_rankwitnessminorrowsdistinctsecond. mdr_rb_other_rankwitness = ff_q_mdr_other_rankwitnessminorrowsdistinctsecond * S ((S (mdr_j_other_rankwitnessminorrowsdistinct)) * mdr_rc_other_rankwitness) + (mdr_a_other_rankwitnessminorrowsdistinct))) -> mdr_i_other_rankwitnessminorrowsdistinct = mdr_j_other_rankwitnessminorrowsdistinct))) /\ ((((forall fom_index_mrf_other_rankwitnessminorcolumnsbound. (exists fom_gap_mrf_other_rankwitnessminorcolumnsbound_index_bound. fom_gap_mrf_other_rankwitnessminorcolumnsbound_index_bound + S (fom_index_mrf_other_rankwitnessminorcolumnsbound) = other) -> exists fom_value_mrf_other_rankwitnessminorcolumnsbound. ((((exists fom_beta_height_mrf_other_rankwitnessminorcolumnsbound_entry. fom_beta_height_mrf_other_rankwitnessminorcolumnsbound_entry + S (fom_value_mrf_other_rankwitnessminorcolumnsbound) = S ((S (fom_index_mrf_other_rankwitnessminorcolumnsbound)) * mdr_cc_other_rankwitness)) /\ exists fom_beta_quotient_mrf_other_rankwitnessminorcolumnsbound_entry. mdr_cb_other_rankwitness = fom_beta_quotient_mrf_other_rankwitnessminorcolumnsbound_entry * S ((S (fom_index_mrf_other_rankwitnessminorcolumnsbound)) * mdr_cc_other_rankwitness) + (fom_value_mrf_other_rankwitnessminorcolumnsbound))) /\ (exists fom_gap_mrf_other_rankwitnessminorcolumnsbound_value_bound. fom_gap_mrf_other_rankwitnessminorcolumnsbound_value_bound + S (fom_value_mrf_other_rankwitnessminorcolumnsbound) = w))) /\ (forall mdr_i_other_rankwitnessminorcolumnsdistinct mdr_j_other_rankwitnessminorcolumnsdistinct mdr_a_other_rankwitnessminorcolumnsdistinct. (exists mdr_gap_other_rankwitnessminorcolumnsdistincti. mdr_gap_other_rankwitnessminorcolumnsdistincti + S (mdr_i_other_rankwitnessminorcolumnsdistinct) = (other)) -> (exists mdr_gap_other_rankwitnessminorcolumnsdistinctj. mdr_gap_other_rankwitnessminorcolumnsdistinctj + S (mdr_j_other_rankwitnessminorcolumnsdistinct) = (other)) -> (((exists ff_h_mdr_other_rankwitnessminorcolumnsdistinctfirst. ff_h_mdr_other_rankwitnessminorcolumnsdistinctfirst + S (mdr_a_other_rankwitnessminorcolumnsdistinct) = S ((S (mdr_i_other_rankwitnessminorcolumnsdistinct)) * mdr_cc_other_rankwitness)) /\ exists ff_q_mdr_other_rankwitnessminorcolumnsdistinctfirst. mdr_cb_other_rankwitness = ff_q_mdr_other_rankwitnessminorcolumnsdistinctfirst * S ((S (mdr_i_other_rankwitnessminorcolumnsdistinct)) * mdr_cc_other_rankwitness) + (mdr_a_other_rankwitnessminorcolumnsdistinct))) -> (((exists ff_h_mdr_other_rankwitnessminorcolumnsdistinctsecond. ff_h_mdr_other_rankwitnessminorcolumnsdistinctsecond + S (mdr_a_other_rankwitnessminorcolumnsdistinct) = S ((S (mdr_j_other_rankwitnessminorcolumnsdistinct)) * mdr_cc_other_rankwitness)) /\ exists ff_q_mdr_other_rankwitnessminorcolumnsdistinctsecond. mdr_cb_other_rankwitness = ff_q_mdr_other_rankwitnessminorcolumnsdistinctsecond * S ((S (mdr_j_other_rankwitnessminorcolumnsdistinct)) * mdr_cc_other_rankwitness) + (mdr_a_other_rankwitnessminorcolumnsdistinct))) -> mdr_i_other_rankwitnessminorcolumnsdistinct = mdr_j_other_rankwitnessminorcolumnsdistinct))) /\ (exists mdr_p_other_rankwitnessminornonzero mdr_n_other_rankwitnessminornonzero. ((exists mdr_ub_other_rankwitnessminornonzeroevaluation mdr_uc_other_rankwitnessminornonzeroevaluation mdr_vb_other_rankwitnessminornonzeroevaluation mdr_vc_other_rankwitnessminornonzeroevaluation. ((((forall mdr_i_other_rankwitnessminornonzeroevaluationmatrixpositive. (exists mdr_gap_other_rankwitnessminornonzeroevaluationmatrixpositivebound. mdr_gap_other_rankwitnessminornonzeroevaluationmatrixpositivebound + S (mdr_i_other_rankwitnessminornonzeroevaluationmatrixpositive) = ((other) * (other))) -> exists mdr_a_other_rankwitnessminornonzeroevaluationmatrixpositive. (((exists mdr_r_other_rankwitnessminornonzeroevaluationmatrixpositivepoint mdr_s_other_rankwitnessminornonzeroevaluationmatrixpositivepoint mdr_u_other_rankwitnessminornonzeroevaluationmatrixpositivepoint mdr_v_other_rankwitnessminornonzeroevaluationmatrixpositivepoint. ((mdr_i_other_rankwitnessminornonzeroevaluationmatrixpositive = (other) * mdr_r_other_rankwitnessminornonzeroevaluationmatrixpositivepoint + mdr_s_other_rankwitnessminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_other_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_other_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_other_rankwitnessminornonzeroevaluationmatrixpositivepoint) = (other)) /\ ((((exists ff_h_mdr_other_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_other_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_other_rankwitnessminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_other_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_other_rankwitness)) /\ exists ff_q_mdr_other_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index. mdr_rb_other_rankwitness = ff_q_mdr_other_rankwitnessminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_other_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_other_rankwitness) + (mdr_u_other_rankwitnessminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_other_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_other_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_other_rankwitnessminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_other_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_other_rankwitness)) /\ exists ff_q_mdr_other_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_other_rankwitness = ff_q_mdr_other_rankwitnessminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_other_rankwitnessminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_other_rankwitness) + (mdr_v_other_rankwitnessminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_other_rankwitnessminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_other_rankwitnessminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_other_rankwitnessminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_other_rankwitnessminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_other_rankwitnessminornonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_other_rankwitnessminornonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_other_rankwitnessminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_other_rankwitnessminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_other_rankwitnessminornonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_other_rankwitnessminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_other_rankwitnessminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_other_rankwitnessminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_other_rankwitnessminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_other_rankwitnessminornonzeroevaluationmatrixpositive)) * mdr_uc_other_rankwitnessminornonzeroevaluation)) /\ exists ff_q_mdr_other_rankwitnessminornonzeroevaluationmatrixpositiveoutput. mdr_ub_other_rankwitnessminornonzeroevaluation = ff_q_mdr_other_rankwitnessminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_other_rankwitnessminornonzeroevaluationmatrixpositive)) * mdr_uc_other_rankwitnessminornonzeroevaluation) + (mdr_a_other_rankwitnessminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_other_rankwitnessminornonzeroevaluationmatrixnegative. (exists mdr_gap_other_rankwitnessminornonzeroevaluationmatrixnegativebound. mdr_gap_other_rankwitnessminornonzeroevaluationmatrixnegativebound + S (mdr_i_other_rankwitnessminornonzeroevaluationmatrixnegative) = ((other) * (other))) -> exists mdr_a_other_rankwitnessminornonzeroevaluationmatrixnegative. (((exists mdr_r_other_rankwitnessminornonzeroevaluationmatrixnegativepoint mdr_s_other_rankwitnessminornonzeroevaluationmatrixnegativepoint mdr_u_other_rankwitnessminornonzeroevaluationmatrixnegativepoint mdr_v_other_rankwitnessminornonzeroevaluationmatrixnegativepoint. ((mdr_i_other_rankwitnessminornonzeroevaluationmatrixnegative = (other) * mdr_r_other_rankwitnessminornonzeroevaluationmatrixnegativepoint + mdr_s_other_rankwitnessminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_other_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_other_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_other_rankwitnessminornonzeroevaluationmatrixnegativepoint) = (other)) /\ ((((exists ff_h_mdr_other_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_other_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_other_rankwitnessminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_other_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_other_rankwitness)) /\ exists ff_q_mdr_other_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index. mdr_rb_other_rankwitness = ff_q_mdr_other_rankwitnessminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_other_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_other_rankwitness) + (mdr_u_other_rankwitnessminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_other_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_other_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_other_rankwitnessminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_other_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_other_rankwitness)) /\ exists ff_q_mdr_other_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_other_rankwitness = ff_q_mdr_other_rankwitnessminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_other_rankwitnessminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_other_rankwitness) + (mdr_v_other_rankwitnessminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_other_rankwitnessminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_other_rankwitnessminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_other_rankwitnessminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_other_rankwitnessminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_other_rankwitnessminornonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_other_rankwitnessminornonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_other_rankwitnessminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_other_rankwitnessminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_other_rankwitnessminornonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_other_rankwitnessminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_other_rankwitnessminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_other_rankwitnessminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_other_rankwitnessminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_other_rankwitnessminornonzeroevaluationmatrixnegative)) * mdr_vc_other_rankwitnessminornonzeroevaluation)) /\ exists ff_q_mdr_other_rankwitnessminornonzeroevaluationmatrixnegativeoutput. mdr_vb_other_rankwitnessminornonzeroevaluation = ff_q_mdr_other_rankwitnessminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_other_rankwitnessminornonzeroevaluationmatrixnegative)) * mdr_vc_other_rankwitnessminornonzeroevaluation) + (mdr_a_other_rankwitnessminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_other_rankwitnessminornonzeroevaluationdeterminant mdr_c_other_rankwitnessminornonzeroevaluationdeterminant mdr_l_other_rankwitnessminornonzeroevaluationdeterminant mdr_i_other_rankwitnessminornonzeroevaluationdeterminant. ((forall mdr_i_other_rankwitnessminornonzeroevaluationdeterminanth. (exists mdr_gap_other_rankwitnessminornonzeroevaluationdeterminanthi. mdr_gap_other_rankwitnessminornonzeroevaluationdeterminanthi + S (mdr_i_other_rankwitnessminornonzeroevaluationdeterminanth) = (mdr_l_other_rankwitnessminornonzeroevaluationdeterminant)) -> exists mdr_d_other_rankwitnessminornonzeroevaluationdeterminanth mdr_pb_other_rankwitnessminornonzeroevaluationdeterminanth mdr_pc_other_rankwitnessminornonzeroevaluationdeterminanth mdr_nb_other_rankwitnessminornonzeroevaluationdeterminanth mdr_nc_other_rankwitnessminornonzeroevaluationdeterminanth mdr_p_other_rankwitnessminornonzeroevaluationdeterminanth mdr_n_other_rankwitnessminornonzeroevaluationdeterminanth. ((exists mdr_z_other_rankwitnessminornonzeroevaluationdeterminanthr. ((exists mdr_a_other_rankwitnessminornonzeroevaluationdeterminanthrc mdr_b_other_rankwitnessminornonzeroevaluationdeterminanthrc mdr_c_other_rankwitnessminornonzeroevaluationdeterminanthrc mdr_e_other_rankwitnessminornonzeroevaluationdeterminanthrc mdr_f_other_rankwitnessminornonzeroevaluationdeterminanthrc. ((mdr_a_other_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_d_other_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_other_rankwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_d_other_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_other_rankwitnessminornonzeroevaluationdeterminanth)) + ((mdr_pb_other_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_pb_other_rankwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_b_other_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_pc_other_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_other_rankwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_pc_other_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_other_rankwitnessminornonzeroevaluationdeterminanth)) + ((mdr_nb_other_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_nb_other_rankwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_c_other_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_a_other_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_other_rankwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_other_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_other_rankwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_b_other_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_b_other_rankwitnessminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_other_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_p_other_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_n_other_rankwitnessminornonzeroevaluationdeterminanth)) * S ((mdr_p_other_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_n_other_rankwitnessminornonzeroevaluationdeterminanth)) + ((mdr_n_other_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_n_other_rankwitnessminornonzeroevaluationdeterminanth))) /\ ((mdr_f_other_rankwitnessminornonzeroevaluationdeterminanthrc = ((mdr_nc_other_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_e_other_rankwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_other_rankwitnessminornonzeroevaluationdeterminanth) + (mdr_e_other_rankwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_e_other_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_e_other_rankwitnessminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_other_rankwitnessminornonzeroevaluationdeterminanthr) = ((mdr_c_other_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_other_rankwitnessminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_other_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_other_rankwitnessminornonzeroevaluationdeterminanthrc)) + ((mdr_f_other_rankwitnessminornonzeroevaluationdeterminanthrc) + (mdr_f_other_rankwitnessminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_other_rankwitnessminornonzeroevaluationdeterminanthrb. ff_h_mdr_other_rankwitnessminornonzeroevaluationdeterminanthrb + S (mdr_z_other_rankwitnessminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_other_rankwitnessminornonzeroevaluationdeterminanth)) * mdr_c_other_rankwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_other_rankwitnessminornonzeroevaluationdeterminanthrb. mdr_b_other_rankwitnessminornonzeroevaluationdeterminant = ff_q_mdr_other_rankwitnessminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_other_rankwitnessminornonzeroevaluationdeterminanth)) * mdr_c_other_rankwitnessminornonzeroevaluationdeterminant) + (mdr_z_other_rankwitnessminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_other_rankwitnessminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_other_rankwitnessminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_other_rankwitnessminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_other_rankwitnessminornonzeroevaluationdeterminanths mdr_eb_other_rankwitnessminornonzeroevaluationdeterminanths mdr_ec_other_rankwitnessminornonzeroevaluationdeterminanths mdr_fb_other_rankwitnessminornonzeroevaluationdeterminanths mdr_fc_other_rankwitnessminornonzeroevaluationdeterminanths. (((mdr_d_other_rankwitnessminornonzeroevaluationdeterminanth) = S (mdr_q_other_rankwitnessminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_other_rankwitnessminornonzeroevaluationdeterminanthsc. (exists mdr_gap_other_rankwitnessminornonzeroevaluationdeterminanthscj. mdr_gap_other_rankwitnessminornonzeroevaluationdeterminanthscj + S (mdr_j_other_rankwitnessminornonzeroevaluationdeterminanthsc) = (S (mdr_q_other_rankwitnessminornonzeroevaluationdeterminanths))) -> exists mdr_i_other_rankwitnessminornonzeroevaluationdeterminanthsc mdr_up_other_rankwitnessminornonzeroevaluationdeterminanthsc mdr_us_other_rankwitnessminornonzeroevaluationdeterminanthsc mdr_un_other_rankwitnessminornonzeroevaluationdeterminanthsc mdr_ut_other_rankwitnessminornonzeroevaluationdeterminanthsc mdr_p_other_rankwitnessminornonzeroevaluationdeterminanthsc mdr_n_other_rankwitnessminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_other_rankwitnessminornonzeroevaluationdeterminanthsci. mdr_gap_other_rankwitnessminornonzeroevaluationdeterminanthsci + S (mdr_i_other_rankwitnessminornonzeroevaluationdeterminanthsc) = (mdr_i_other_rankwitnessminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_other_rankwitnessminornonzeroevaluationdeterminanthscr. ((exists mdr_a_other_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_b_other_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_c_other_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_e_other_rankwitnessminornonzeroevaluationdeterminanthscrc mdr_f_other_rankwitnessminornonzeroevaluationdeterminanthscrc. ((mdr_a_other_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_q_other_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_up_other_rankwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_other_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_up_other_rankwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_up_other_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_up_other_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_other_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_us_other_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_other_rankwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_other_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_other_rankwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_un_other_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_un_other_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_other_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_a_other_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_other_rankwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_other_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_other_rankwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_other_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_b_other_rankwitnessminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_other_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_p_other_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_other_rankwitnessminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_other_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_other_rankwitnessminornonzeroevaluationdeterminanthsc)) + ((mdr_n_other_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_n_other_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_other_rankwitnessminornonzeroevaluationdeterminanthscrc = ((mdr_ut_other_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_e_other_rankwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_other_rankwitnessminornonzeroevaluationdeterminanthsc) + (mdr_e_other_rankwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_other_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_e_other_rankwitnessminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_other_rankwitnessminornonzeroevaluationdeterminanthscr) = ((mdr_c_other_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_other_rankwitnessminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_other_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_other_rankwitnessminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_other_rankwitnessminornonzeroevaluationdeterminanthscrc) + (mdr_f_other_rankwitnessminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscrb. ff_h_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscrb + S (mdr_z_other_rankwitnessminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_other_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_c_other_rankwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscrb. mdr_b_other_rankwitnessminornonzeroevaluationdeterminant = ff_q_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_other_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_c_other_rankwitnessminornonzeroevaluationdeterminant) + (mdr_z_other_rankwitnessminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_other_rankwitnessminornonzeroevaluationdeterminanths) * (mdr_q_other_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive = (mdr_q_other_rankwitnessminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_other_rankwitnessminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_other_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_other_rankwitnessminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_other_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_other_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_other_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_other_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_other_rankwitnessminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_other_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_other_rankwitnessminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_other_rankwitnessminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_other_rankwitnessminornonzeroevaluationdeterminanths) * (mdr_q_other_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative = (mdr_q_other_rankwitnessminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_other_rankwitnessminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_other_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_other_rankwitnessminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_other_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_other_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_other_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_other_rankwitnessminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_other_rankwitnessminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_other_rankwitnessminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_other_rankwitnessminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_other_rankwitnessminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscp. ff_h_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscp + S (mdr_p_other_rankwitnessminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_other_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_ec_other_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscp. mdr_eb_other_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_other_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_ec_other_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_p_other_rankwitnessminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscn. ff_h_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscn + S (mdr_n_other_rankwitnessminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_other_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_fc_other_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscn. mdr_fb_other_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mdr_other_rankwitnessminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_other_rankwitnessminornonzeroevaluationdeterminanthsc)) * mdr_fc_other_rankwitnessminornonzeroevaluationdeterminanths) + (mdr_n_other_rankwitnessminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_other_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_other_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_other_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_other_rankwitnessminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_other_rankwitnessminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_other_rankwitnessminornonzeroevaluationdeterminanth = ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_other_rankwitnessminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_other_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_other_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_other_rankwitnessminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_other_rankwitnessminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_other_rankwitnessminornonzeroevaluationdeterminanths = ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_other_rankwitnessminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_other_rankwitnessminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_other_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_other_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_other_rankwitnessminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_other_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_other_rankwitnessminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_other_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_other_rankwitnessminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_other_rankwitnessminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_other_rankwitnessminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_other_rankwitnessminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_other_rankwitnessminornonzeroevaluationdeterminanti. mdr_gap_other_rankwitnessminornonzeroevaluationdeterminanti + S (mdr_i_other_rankwitnessminornonzeroevaluationdeterminant) = (mdr_l_other_rankwitnessminornonzeroevaluationdeterminant)) /\ (exists mdr_z_other_rankwitnessminornonzeroevaluationdeterminantr. ((exists mdr_a_other_rankwitnessminornonzeroevaluationdeterminantrc mdr_b_other_rankwitnessminornonzeroevaluationdeterminantrc mdr_c_other_rankwitnessminornonzeroevaluationdeterminantrc mdr_e_other_rankwitnessminornonzeroevaluationdeterminantrc mdr_f_other_rankwitnessminornonzeroevaluationdeterminantrc. ((mdr_a_other_rankwitnessminornonzeroevaluationdeterminantrc = ((other) + (mdr_ub_other_rankwitnessminornonzeroevaluation)) * S ((other) + (mdr_ub_other_rankwitnessminornonzeroevaluation)) + ((mdr_ub_other_rankwitnessminornonzeroevaluation) + (mdr_ub_other_rankwitnessminornonzeroevaluation))) /\ ((mdr_b_other_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_uc_other_rankwitnessminornonzeroevaluation) + (mdr_vb_other_rankwitnessminornonzeroevaluation)) * S ((mdr_uc_other_rankwitnessminornonzeroevaluation) + (mdr_vb_other_rankwitnessminornonzeroevaluation)) + ((mdr_vb_other_rankwitnessminornonzeroevaluation) + (mdr_vb_other_rankwitnessminornonzeroevaluation))) /\ ((mdr_c_other_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_a_other_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_other_rankwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_a_other_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_other_rankwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_b_other_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_b_other_rankwitnessminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_other_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_p_other_rankwitnessminornonzero) + (mdr_n_other_rankwitnessminornonzero)) * S ((mdr_p_other_rankwitnessminornonzero) + (mdr_n_other_rankwitnessminornonzero)) + ((mdr_n_other_rankwitnessminornonzero) + (mdr_n_other_rankwitnessminornonzero))) /\ ((mdr_f_other_rankwitnessminornonzeroevaluationdeterminantrc = ((mdr_vc_other_rankwitnessminornonzeroevaluation) + (mdr_e_other_rankwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_other_rankwitnessminornonzeroevaluation) + (mdr_e_other_rankwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_e_other_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_e_other_rankwitnessminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_other_rankwitnessminornonzeroevaluationdeterminantr) = ((mdr_c_other_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_other_rankwitnessminornonzeroevaluationdeterminantrc)) * S ((mdr_c_other_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_other_rankwitnessminornonzeroevaluationdeterminantrc)) + ((mdr_f_other_rankwitnessminornonzeroevaluationdeterminantrc) + (mdr_f_other_rankwitnessminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_other_rankwitnessminornonzeroevaluationdeterminantrb. ff_h_mdr_other_rankwitnessminornonzeroevaluationdeterminantrb + S (mdr_z_other_rankwitnessminornonzeroevaluationdeterminantr) = S ((S (mdr_i_other_rankwitnessminornonzeroevaluationdeterminant)) * mdr_c_other_rankwitnessminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_other_rankwitnessminornonzeroevaluationdeterminantrb. mdr_b_other_rankwitnessminornonzeroevaluationdeterminant = ff_q_mdr_other_rankwitnessminornonzeroevaluationdeterminantrb * S ((S (mdr_i_other_rankwitnessminornonzeroevaluationdeterminant)) * mdr_c_other_rankwitnessminornonzeroevaluationdeterminant) + (mdr_z_other_rankwitnessminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_other_rankwitnessminornonzero = mdr_n_other_rankwitnessminornonzero)))))))) /\ (forall mdr_q_other_rank. (exists mdr_gap_other_rankhigher. mdr_gap_other_rankhigher + S (other) = (mdr_q_other_rank)) -> (forall mdr_rb_other_rankzero mdr_rc_other_rankzero mdr_cb_other_rankzero mdr_cc_other_rankzero mdr_p_other_rankzero mdr_n_other_rankzero. (((forall fom_index_mrf_other_rankzerorowsbound. (exists fom_gap_mrf_other_rankzerorowsbound_index_bound. fom_gap_mrf_other_rankzerorowsbound_index_bound + S (fom_index_mrf_other_rankzerorowsbound) = mdr_q_other_rank) -> exists fom_value_mrf_other_rankzerorowsbound. ((((exists fom_beta_height_mrf_other_rankzerorowsbound_entry. fom_beta_height_mrf_other_rankzerorowsbound_entry + S (fom_value_mrf_other_rankzerorowsbound) = S ((S (fom_index_mrf_other_rankzerorowsbound)) * mdr_rc_other_rankzero)) /\ exists fom_beta_quotient_mrf_other_rankzerorowsbound_entry. mdr_rb_other_rankzero = fom_beta_quotient_mrf_other_rankzerorowsbound_entry * S ((S (fom_index_mrf_other_rankzerorowsbound)) * mdr_rc_other_rankzero) + (fom_value_mrf_other_rankzerorowsbound))) /\ (exists fom_gap_mrf_other_rankzerorowsbound_value_bound. fom_gap_mrf_other_rankzerorowsbound_value_bound + S (fom_value_mrf_other_rankzerorowsbound) = r))) /\ (forall mdr_i_other_rankzerorowsdistinct mdr_j_other_rankzerorowsdistinct mdr_a_other_rankzerorowsdistinct. (exists mdr_gap_other_rankzerorowsdistincti. mdr_gap_other_rankzerorowsdistincti + S (mdr_i_other_rankzerorowsdistinct) = (mdr_q_other_rank)) -> (exists mdr_gap_other_rankzerorowsdistinctj. mdr_gap_other_rankzerorowsdistinctj + S (mdr_j_other_rankzerorowsdistinct) = (mdr_q_other_rank)) -> (((exists ff_h_mdr_other_rankzerorowsdistinctfirst. ff_h_mdr_other_rankzerorowsdistinctfirst + S (mdr_a_other_rankzerorowsdistinct) = S ((S (mdr_i_other_rankzerorowsdistinct)) * mdr_rc_other_rankzero)) /\ exists ff_q_mdr_other_rankzerorowsdistinctfirst. mdr_rb_other_rankzero = ff_q_mdr_other_rankzerorowsdistinctfirst * S ((S (mdr_i_other_rankzerorowsdistinct)) * mdr_rc_other_rankzero) + (mdr_a_other_rankzerorowsdistinct))) -> (((exists ff_h_mdr_other_rankzerorowsdistinctsecond. ff_h_mdr_other_rankzerorowsdistinctsecond + S (mdr_a_other_rankzerorowsdistinct) = S ((S (mdr_j_other_rankzerorowsdistinct)) * mdr_rc_other_rankzero)) /\ exists ff_q_mdr_other_rankzerorowsdistinctsecond. mdr_rb_other_rankzero = ff_q_mdr_other_rankzerorowsdistinctsecond * S ((S (mdr_j_other_rankzerorowsdistinct)) * mdr_rc_other_rankzero) + (mdr_a_other_rankzerorowsdistinct))) -> mdr_i_other_rankzerorowsdistinct = mdr_j_other_rankzerorowsdistinct))) -> (((forall fom_index_mrf_other_rankzerocolumnsbound. (exists fom_gap_mrf_other_rankzerocolumnsbound_index_bound. fom_gap_mrf_other_rankzerocolumnsbound_index_bound + S (fom_index_mrf_other_rankzerocolumnsbound) = mdr_q_other_rank) -> exists fom_value_mrf_other_rankzerocolumnsbound. ((((exists fom_beta_height_mrf_other_rankzerocolumnsbound_entry. fom_beta_height_mrf_other_rankzerocolumnsbound_entry + S (fom_value_mrf_other_rankzerocolumnsbound) = S ((S (fom_index_mrf_other_rankzerocolumnsbound)) * mdr_cc_other_rankzero)) /\ exists fom_beta_quotient_mrf_other_rankzerocolumnsbound_entry. mdr_cb_other_rankzero = fom_beta_quotient_mrf_other_rankzerocolumnsbound_entry * S ((S (fom_index_mrf_other_rankzerocolumnsbound)) * mdr_cc_other_rankzero) + (fom_value_mrf_other_rankzerocolumnsbound))) /\ (exists fom_gap_mrf_other_rankzerocolumnsbound_value_bound. fom_gap_mrf_other_rankzerocolumnsbound_value_bound + S (fom_value_mrf_other_rankzerocolumnsbound) = w))) /\ (forall mdr_i_other_rankzerocolumnsdistinct mdr_j_other_rankzerocolumnsdistinct mdr_a_other_rankzerocolumnsdistinct. (exists mdr_gap_other_rankzerocolumnsdistincti. mdr_gap_other_rankzerocolumnsdistincti + S (mdr_i_other_rankzerocolumnsdistinct) = (mdr_q_other_rank)) -> (exists mdr_gap_other_rankzerocolumnsdistinctj. mdr_gap_other_rankzerocolumnsdistinctj + S (mdr_j_other_rankzerocolumnsdistinct) = (mdr_q_other_rank)) -> (((exists ff_h_mdr_other_rankzerocolumnsdistinctfirst. ff_h_mdr_other_rankzerocolumnsdistinctfirst + S (mdr_a_other_rankzerocolumnsdistinct) = S ((S (mdr_i_other_rankzerocolumnsdistinct)) * mdr_cc_other_rankzero)) /\ exists ff_q_mdr_other_rankzerocolumnsdistinctfirst. mdr_cb_other_rankzero = ff_q_mdr_other_rankzerocolumnsdistinctfirst * S ((S (mdr_i_other_rankzerocolumnsdistinct)) * mdr_cc_other_rankzero) + (mdr_a_other_rankzerocolumnsdistinct))) -> (((exists ff_h_mdr_other_rankzerocolumnsdistinctsecond. ff_h_mdr_other_rankzerocolumnsdistinctsecond + S (mdr_a_other_rankzerocolumnsdistinct) = S ((S (mdr_j_other_rankzerocolumnsdistinct)) * mdr_cc_other_rankzero)) /\ exists ff_q_mdr_other_rankzerocolumnsdistinctsecond. mdr_cb_other_rankzero = ff_q_mdr_other_rankzerocolumnsdistinctsecond * S ((S (mdr_j_other_rankzerocolumnsdistinct)) * mdr_cc_other_rankzero) + (mdr_a_other_rankzerocolumnsdistinct))) -> mdr_i_other_rankzerocolumnsdistinct = mdr_j_other_rankzerocolumnsdistinct))) -> (exists mdr_ub_other_rankzeroevaluation mdr_uc_other_rankzeroevaluation mdr_vb_other_rankzeroevaluation mdr_vc_other_rankzeroevaluation. ((((forall mdr_i_other_rankzeroevaluationmatrixpositive. (exists mdr_gap_other_rankzeroevaluationmatrixpositivebound. mdr_gap_other_rankzeroevaluationmatrixpositivebound + S (mdr_i_other_rankzeroevaluationmatrixpositive) = ((mdr_q_other_rank) * (mdr_q_other_rank))) -> exists mdr_a_other_rankzeroevaluationmatrixpositive. (((exists mdr_r_other_rankzeroevaluationmatrixpositivepoint mdr_s_other_rankzeroevaluationmatrixpositivepoint mdr_u_other_rankzeroevaluationmatrixpositivepoint mdr_v_other_rankzeroevaluationmatrixpositivepoint. ((mdr_i_other_rankzeroevaluationmatrixpositive = (mdr_q_other_rank) * mdr_r_other_rankzeroevaluationmatrixpositivepoint + mdr_s_other_rankzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_other_rankzeroevaluationmatrixpositivepointcolumn. mdr_gap_other_rankzeroevaluationmatrixpositivepointcolumn + S (mdr_s_other_rankzeroevaluationmatrixpositivepoint) = (mdr_q_other_rank)) /\ ((((exists ff_h_mdr_other_rankzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_other_rankzeroevaluationmatrixpositivepointrow_index + S (mdr_u_other_rankzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_other_rankzeroevaluationmatrixpositivepoint)) * mdr_rc_other_rankzero)) /\ exists ff_q_mdr_other_rankzeroevaluationmatrixpositivepointrow_index. mdr_rb_other_rankzero = ff_q_mdr_other_rankzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_other_rankzeroevaluationmatrixpositivepoint)) * mdr_rc_other_rankzero) + (mdr_u_other_rankzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_other_rankzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_other_rankzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_other_rankzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_other_rankzeroevaluationmatrixpositivepoint)) * mdr_cc_other_rankzero)) /\ exists ff_q_mdr_other_rankzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_other_rankzero = ff_q_mdr_other_rankzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_other_rankzeroevaluationmatrixpositivepoint)) * mdr_cc_other_rankzero) + (mdr_v_other_rankzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_other_rankzeroevaluationmatrixpositivepointsource. ff_h_mdr_other_rankzeroevaluationmatrixpositivepointsource + S (mdr_a_other_rankzeroevaluationmatrixpositive) = S ((S ((mdr_u_other_rankzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_other_rankzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_other_rankzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_other_rankzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_other_rankzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_other_rankzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_other_rankzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_other_rankzeroevaluationmatrixpositiveoutput. ff_h_mdr_other_rankzeroevaluationmatrixpositiveoutput + S (mdr_a_other_rankzeroevaluationmatrixpositive) = S ((S (mdr_i_other_rankzeroevaluationmatrixpositive)) * mdr_uc_other_rankzeroevaluation)) /\ exists ff_q_mdr_other_rankzeroevaluationmatrixpositiveoutput. mdr_ub_other_rankzeroevaluation = ff_q_mdr_other_rankzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_other_rankzeroevaluationmatrixpositive)) * mdr_uc_other_rankzeroevaluation) + (mdr_a_other_rankzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_other_rankzeroevaluationmatrixnegative. (exists mdr_gap_other_rankzeroevaluationmatrixnegativebound. mdr_gap_other_rankzeroevaluationmatrixnegativebound + S (mdr_i_other_rankzeroevaluationmatrixnegative) = ((mdr_q_other_rank) * (mdr_q_other_rank))) -> exists mdr_a_other_rankzeroevaluationmatrixnegative. (((exists mdr_r_other_rankzeroevaluationmatrixnegativepoint mdr_s_other_rankzeroevaluationmatrixnegativepoint mdr_u_other_rankzeroevaluationmatrixnegativepoint mdr_v_other_rankzeroevaluationmatrixnegativepoint. ((mdr_i_other_rankzeroevaluationmatrixnegative = (mdr_q_other_rank) * mdr_r_other_rankzeroevaluationmatrixnegativepoint + mdr_s_other_rankzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_other_rankzeroevaluationmatrixnegativepointcolumn. mdr_gap_other_rankzeroevaluationmatrixnegativepointcolumn + S (mdr_s_other_rankzeroevaluationmatrixnegativepoint) = (mdr_q_other_rank)) /\ ((((exists ff_h_mdr_other_rankzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_other_rankzeroevaluationmatrixnegativepointrow_index + S (mdr_u_other_rankzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_other_rankzeroevaluationmatrixnegativepoint)) * mdr_rc_other_rankzero)) /\ exists ff_q_mdr_other_rankzeroevaluationmatrixnegativepointrow_index. mdr_rb_other_rankzero = ff_q_mdr_other_rankzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_other_rankzeroevaluationmatrixnegativepoint)) * mdr_rc_other_rankzero) + (mdr_u_other_rankzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_other_rankzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_other_rankzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_other_rankzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_other_rankzeroevaluationmatrixnegativepoint)) * mdr_cc_other_rankzero)) /\ exists ff_q_mdr_other_rankzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_other_rankzero = ff_q_mdr_other_rankzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_other_rankzeroevaluationmatrixnegativepoint)) * mdr_cc_other_rankzero) + (mdr_v_other_rankzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_other_rankzeroevaluationmatrixnegativepointsource. ff_h_mdr_other_rankzeroevaluationmatrixnegativepointsource + S (mdr_a_other_rankzeroevaluationmatrixnegative) = S ((S ((mdr_u_other_rankzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_other_rankzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_other_rankzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_other_rankzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_other_rankzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_other_rankzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_other_rankzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_other_rankzeroevaluationmatrixnegativeoutput. ff_h_mdr_other_rankzeroevaluationmatrixnegativeoutput + S (mdr_a_other_rankzeroevaluationmatrixnegative) = S ((S (mdr_i_other_rankzeroevaluationmatrixnegative)) * mdr_vc_other_rankzeroevaluation)) /\ exists ff_q_mdr_other_rankzeroevaluationmatrixnegativeoutput. mdr_vb_other_rankzeroevaluation = ff_q_mdr_other_rankzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_other_rankzeroevaluationmatrixnegative)) * mdr_vc_other_rankzeroevaluation) + (mdr_a_other_rankzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_other_rankzeroevaluationdeterminant mdr_c_other_rankzeroevaluationdeterminant mdr_l_other_rankzeroevaluationdeterminant mdr_i_other_rankzeroevaluationdeterminant. ((forall mdr_i_other_rankzeroevaluationdeterminanth. (exists mdr_gap_other_rankzeroevaluationdeterminanthi. mdr_gap_other_rankzeroevaluationdeterminanthi + S (mdr_i_other_rankzeroevaluationdeterminanth) = (mdr_l_other_rankzeroevaluationdeterminant)) -> exists mdr_d_other_rankzeroevaluationdeterminanth mdr_pb_other_rankzeroevaluationdeterminanth mdr_pc_other_rankzeroevaluationdeterminanth mdr_nb_other_rankzeroevaluationdeterminanth mdr_nc_other_rankzeroevaluationdeterminanth mdr_p_other_rankzeroevaluationdeterminanth mdr_n_other_rankzeroevaluationdeterminanth. ((exists mdr_z_other_rankzeroevaluationdeterminanthr. ((exists mdr_a_other_rankzeroevaluationdeterminanthrc mdr_b_other_rankzeroevaluationdeterminanthrc mdr_c_other_rankzeroevaluationdeterminanthrc mdr_e_other_rankzeroevaluationdeterminanthrc mdr_f_other_rankzeroevaluationdeterminanthrc. ((mdr_a_other_rankzeroevaluationdeterminanthrc = ((mdr_d_other_rankzeroevaluationdeterminanth) + (mdr_pb_other_rankzeroevaluationdeterminanth)) * S ((mdr_d_other_rankzeroevaluationdeterminanth) + (mdr_pb_other_rankzeroevaluationdeterminanth)) + ((mdr_pb_other_rankzeroevaluationdeterminanth) + (mdr_pb_other_rankzeroevaluationdeterminanth))) /\ ((mdr_b_other_rankzeroevaluationdeterminanthrc = ((mdr_pc_other_rankzeroevaluationdeterminanth) + (mdr_nb_other_rankzeroevaluationdeterminanth)) * S ((mdr_pc_other_rankzeroevaluationdeterminanth) + (mdr_nb_other_rankzeroevaluationdeterminanth)) + ((mdr_nb_other_rankzeroevaluationdeterminanth) + (mdr_nb_other_rankzeroevaluationdeterminanth))) /\ ((mdr_c_other_rankzeroevaluationdeterminanthrc = ((mdr_a_other_rankzeroevaluationdeterminanthrc) + (mdr_b_other_rankzeroevaluationdeterminanthrc)) * S ((mdr_a_other_rankzeroevaluationdeterminanthrc) + (mdr_b_other_rankzeroevaluationdeterminanthrc)) + ((mdr_b_other_rankzeroevaluationdeterminanthrc) + (mdr_b_other_rankzeroevaluationdeterminanthrc))) /\ ((mdr_e_other_rankzeroevaluationdeterminanthrc = ((mdr_p_other_rankzeroevaluationdeterminanth) + (mdr_n_other_rankzeroevaluationdeterminanth)) * S ((mdr_p_other_rankzeroevaluationdeterminanth) + (mdr_n_other_rankzeroevaluationdeterminanth)) + ((mdr_n_other_rankzeroevaluationdeterminanth) + (mdr_n_other_rankzeroevaluationdeterminanth))) /\ ((mdr_f_other_rankzeroevaluationdeterminanthrc = ((mdr_nc_other_rankzeroevaluationdeterminanth) + (mdr_e_other_rankzeroevaluationdeterminanthrc)) * S ((mdr_nc_other_rankzeroevaluationdeterminanth) + (mdr_e_other_rankzeroevaluationdeterminanthrc)) + ((mdr_e_other_rankzeroevaluationdeterminanthrc) + (mdr_e_other_rankzeroevaluationdeterminanthrc))) /\ ((mdr_z_other_rankzeroevaluationdeterminanthr) = ((mdr_c_other_rankzeroevaluationdeterminanthrc) + (mdr_f_other_rankzeroevaluationdeterminanthrc)) * S ((mdr_c_other_rankzeroevaluationdeterminanthrc) + (mdr_f_other_rankzeroevaluationdeterminanthrc)) + ((mdr_f_other_rankzeroevaluationdeterminanthrc) + (mdr_f_other_rankzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_other_rankzeroevaluationdeterminanthrb. ff_h_mdr_other_rankzeroevaluationdeterminanthrb + S (mdr_z_other_rankzeroevaluationdeterminanthr) = S ((S (mdr_i_other_rankzeroevaluationdeterminanth)) * mdr_c_other_rankzeroevaluationdeterminant)) /\ exists ff_q_mdr_other_rankzeroevaluationdeterminanthrb. mdr_b_other_rankzeroevaluationdeterminant = ff_q_mdr_other_rankzeroevaluationdeterminanthrb * S ((S (mdr_i_other_rankzeroevaluationdeterminanth)) * mdr_c_other_rankzeroevaluationdeterminant) + (mdr_z_other_rankzeroevaluationdeterminanthr))))) /\ (((((mdr_d_other_rankzeroevaluationdeterminanth) = 0) /\ (((mdr_p_other_rankzeroevaluationdeterminanth) = 1) /\ ((mdr_n_other_rankzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_other_rankzeroevaluationdeterminanths mdr_eb_other_rankzeroevaluationdeterminanths mdr_ec_other_rankzeroevaluationdeterminanths mdr_fb_other_rankzeroevaluationdeterminanths mdr_fc_other_rankzeroevaluationdeterminanths. (((mdr_d_other_rankzeroevaluationdeterminanth) = S (mdr_q_other_rankzeroevaluationdeterminanths)) /\ ((forall mdr_j_other_rankzeroevaluationdeterminanthsc. (exists mdr_gap_other_rankzeroevaluationdeterminanthscj. mdr_gap_other_rankzeroevaluationdeterminanthscj + S (mdr_j_other_rankzeroevaluationdeterminanthsc) = (S (mdr_q_other_rankzeroevaluationdeterminanths))) -> exists mdr_i_other_rankzeroevaluationdeterminanthsc mdr_up_other_rankzeroevaluationdeterminanthsc mdr_us_other_rankzeroevaluationdeterminanthsc mdr_un_other_rankzeroevaluationdeterminanthsc mdr_ut_other_rankzeroevaluationdeterminanthsc mdr_p_other_rankzeroevaluationdeterminanthsc mdr_n_other_rankzeroevaluationdeterminanthsc. ((exists mdr_gap_other_rankzeroevaluationdeterminanthsci. mdr_gap_other_rankzeroevaluationdeterminanthsci + S (mdr_i_other_rankzeroevaluationdeterminanthsc) = (mdr_i_other_rankzeroevaluationdeterminanth)) /\ ((exists mdr_z_other_rankzeroevaluationdeterminanthscr. ((exists mdr_a_other_rankzeroevaluationdeterminanthscrc mdr_b_other_rankzeroevaluationdeterminanthscrc mdr_c_other_rankzeroevaluationdeterminanthscrc mdr_e_other_rankzeroevaluationdeterminanthscrc mdr_f_other_rankzeroevaluationdeterminanthscrc. ((mdr_a_other_rankzeroevaluationdeterminanthscrc = ((mdr_q_other_rankzeroevaluationdeterminanths) + (mdr_up_other_rankzeroevaluationdeterminanthsc)) * S ((mdr_q_other_rankzeroevaluationdeterminanths) + (mdr_up_other_rankzeroevaluationdeterminanthsc)) + ((mdr_up_other_rankzeroevaluationdeterminanthsc) + (mdr_up_other_rankzeroevaluationdeterminanthsc))) /\ ((mdr_b_other_rankzeroevaluationdeterminanthscrc = ((mdr_us_other_rankzeroevaluationdeterminanthsc) + (mdr_un_other_rankzeroevaluationdeterminanthsc)) * S ((mdr_us_other_rankzeroevaluationdeterminanthsc) + (mdr_un_other_rankzeroevaluationdeterminanthsc)) + ((mdr_un_other_rankzeroevaluationdeterminanthsc) + (mdr_un_other_rankzeroevaluationdeterminanthsc))) /\ ((mdr_c_other_rankzeroevaluationdeterminanthscrc = ((mdr_a_other_rankzeroevaluationdeterminanthscrc) + (mdr_b_other_rankzeroevaluationdeterminanthscrc)) * S ((mdr_a_other_rankzeroevaluationdeterminanthscrc) + (mdr_b_other_rankzeroevaluationdeterminanthscrc)) + ((mdr_b_other_rankzeroevaluationdeterminanthscrc) + (mdr_b_other_rankzeroevaluationdeterminanthscrc))) /\ ((mdr_e_other_rankzeroevaluationdeterminanthscrc = ((mdr_p_other_rankzeroevaluationdeterminanthsc) + (mdr_n_other_rankzeroevaluationdeterminanthsc)) * S ((mdr_p_other_rankzeroevaluationdeterminanthsc) + (mdr_n_other_rankzeroevaluationdeterminanthsc)) + ((mdr_n_other_rankzeroevaluationdeterminanthsc) + (mdr_n_other_rankzeroevaluationdeterminanthsc))) /\ ((mdr_f_other_rankzeroevaluationdeterminanthscrc = ((mdr_ut_other_rankzeroevaluationdeterminanthsc) + (mdr_e_other_rankzeroevaluationdeterminanthscrc)) * S ((mdr_ut_other_rankzeroevaluationdeterminanthsc) + (mdr_e_other_rankzeroevaluationdeterminanthscrc)) + ((mdr_e_other_rankzeroevaluationdeterminanthscrc) + (mdr_e_other_rankzeroevaluationdeterminanthscrc))) /\ ((mdr_z_other_rankzeroevaluationdeterminanthscr) = ((mdr_c_other_rankzeroevaluationdeterminanthscrc) + (mdr_f_other_rankzeroevaluationdeterminanthscrc)) * S ((mdr_c_other_rankzeroevaluationdeterminanthscrc) + (mdr_f_other_rankzeroevaluationdeterminanthscrc)) + ((mdr_f_other_rankzeroevaluationdeterminanthscrc) + (mdr_f_other_rankzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_other_rankzeroevaluationdeterminanthscrb. ff_h_mdr_other_rankzeroevaluationdeterminanthscrb + S (mdr_z_other_rankzeroevaluationdeterminanthscr) = S ((S (mdr_i_other_rankzeroevaluationdeterminanthsc)) * mdr_c_other_rankzeroevaluationdeterminant)) /\ exists ff_q_mdr_other_rankzeroevaluationdeterminanthscrb. mdr_b_other_rankzeroevaluationdeterminant = ff_q_mdr_other_rankzeroevaluationdeterminanthscrb * S ((S (mdr_i_other_rankzeroevaluationdeterminanthsc)) * mdr_c_other_rankzeroevaluationdeterminant) + (mdr_z_other_rankzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_other_rankzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_other_rankzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_positive) = ((mdr_q_other_rankzeroevaluationdeterminanths) * (mdr_q_other_rankzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_positive = (mdr_q_other_rankzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_other_rankzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_other_rankzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_positive) = (mdr_q_other_rankzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_other_rankzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_other_rankzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_other_rankzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_other_rankzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_other_rankzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_other_rankzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_other_rankzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_other_rankzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_other_rankzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_other_rankzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_positive) = (mdr_j_other_rankzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_other_rankzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_other_rankzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_other_rankzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_other_rankzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_other_rankzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_other_rankzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_other_rankzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_other_rankzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_other_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_other_rankzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_other_rankzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_other_rankzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_other_rankzeroevaluationdeterminanth = ff_q_mdm_mdr_other_rankzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_other_rankzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_other_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_other_rankzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_other_rankzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_other_rankzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_other_rankzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_positive)) * mdr_us_other_rankzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_other_rankzeroevaluationdeterminanthscm_positive_target. mdr_up_other_rankzeroevaluationdeterminanthsc = ff_q_mdm_mdr_other_rankzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_positive)) * mdr_us_other_rankzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_other_rankzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_other_rankzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_negative) = ((mdr_q_other_rankzeroevaluationdeterminanths) * (mdr_q_other_rankzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_negative = (mdr_q_other_rankzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_other_rankzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_other_rankzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_negative) = (mdr_q_other_rankzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_other_rankzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_other_rankzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_other_rankzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_other_rankzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_other_rankzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_other_rankzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_other_rankzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_other_rankzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_other_rankzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_other_rankzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_negative) = (mdr_j_other_rankzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_other_rankzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_other_rankzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_other_rankzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_other_rankzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_other_rankzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_other_rankzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_other_rankzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_other_rankzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_other_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_other_rankzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_other_rankzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_other_rankzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_other_rankzeroevaluationdeterminanth = ff_q_mdm_mdr_other_rankzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_other_rankzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_other_rankzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_other_rankzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_other_rankzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_other_rankzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_other_rankzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_negative)) * mdr_ut_other_rankzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_other_rankzeroevaluationdeterminanthscm_negative_target. mdr_un_other_rankzeroevaluationdeterminanthsc = ff_q_mdm_mdr_other_rankzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_negative)) * mdr_ut_other_rankzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_other_rankzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_other_rankzeroevaluationdeterminanthscp. ff_h_mdr_other_rankzeroevaluationdeterminanthscp + S (mdr_p_other_rankzeroevaluationdeterminanthsc) = S ((S (mdr_j_other_rankzeroevaluationdeterminanthsc)) * mdr_ec_other_rankzeroevaluationdeterminanths)) /\ exists ff_q_mdr_other_rankzeroevaluationdeterminanthscp. mdr_eb_other_rankzeroevaluationdeterminanths = ff_q_mdr_other_rankzeroevaluationdeterminanthscp * S ((S (mdr_j_other_rankzeroevaluationdeterminanthsc)) * mdr_ec_other_rankzeroevaluationdeterminanths) + (mdr_p_other_rankzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_other_rankzeroevaluationdeterminanthscn. ff_h_mdr_other_rankzeroevaluationdeterminanthscn + S (mdr_n_other_rankzeroevaluationdeterminanthsc) = S ((S (mdr_j_other_rankzeroevaluationdeterminanthsc)) * mdr_fc_other_rankzeroevaluationdeterminanths)) /\ exists ff_q_mdr_other_rankzeroevaluationdeterminanthscn. mdr_fb_other_rankzeroevaluationdeterminanths = ff_q_mdr_other_rankzeroevaluationdeterminanthscn * S ((S (mdr_j_other_rankzeroevaluationdeterminanthsc)) * mdr_fc_other_rankzeroevaluationdeterminanths) + (mdr_n_other_rankzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_other_rankzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_other_rankzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_other_rankzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_other_rankzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_other_rankzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_other_rankzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_other_rankzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix)) * mdr_pc_other_rankzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_other_rankzeroevaluationdeterminanth = ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix)) * mdr_pc_other_rankzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix)) * mdr_nc_other_rankzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_prefix_an. mdr_nb_other_rankzeroevaluationdeterminanth = ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix)) * mdr_nc_other_rankzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix)) * mdr_ec_other_rankzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_other_rankzeroevaluationdeterminanths = ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix)) * mdr_ec_other_rankzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix)) * mdr_fc_other_rankzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_other_rankzeroevaluationdeterminanths = ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix)) * mdr_fc_other_rankzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_other_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_other_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_other_rankzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_other_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_other_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_other_rankzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_other_rankzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_other_rankzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_other_rankzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_other_rankzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_other_rankzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_other_rankzeroevaluationdeterminanth) = S ((S ((S (mdr_q_other_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_other_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive) + (mdr_p_other_rankzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive = (S (mdr_q_other_rankzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_other_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_other_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_other_rankzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_other_rankzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_other_rankzeroevaluationdeterminanth) = S ((S ((S (mdr_q_other_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_other_rankzeroevaluationdeterminanths)))) * ff_v_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative) + (mdr_n_other_rankzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative = (S (mdr_q_other_rankzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_other_rankzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_other_rankzeroevaluationdeterminanthsf = ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_other_rankzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_other_rankzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_other_rankzeroevaluationdeterminanti. mdr_gap_other_rankzeroevaluationdeterminanti + S (mdr_i_other_rankzeroevaluationdeterminant) = (mdr_l_other_rankzeroevaluationdeterminant)) /\ (exists mdr_z_other_rankzeroevaluationdeterminantr. ((exists mdr_a_other_rankzeroevaluationdeterminantrc mdr_b_other_rankzeroevaluationdeterminantrc mdr_c_other_rankzeroevaluationdeterminantrc mdr_e_other_rankzeroevaluationdeterminantrc mdr_f_other_rankzeroevaluationdeterminantrc. ((mdr_a_other_rankzeroevaluationdeterminantrc = ((mdr_q_other_rank) + (mdr_ub_other_rankzeroevaluation)) * S ((mdr_q_other_rank) + (mdr_ub_other_rankzeroevaluation)) + ((mdr_ub_other_rankzeroevaluation) + (mdr_ub_other_rankzeroevaluation))) /\ ((mdr_b_other_rankzeroevaluationdeterminantrc = ((mdr_uc_other_rankzeroevaluation) + (mdr_vb_other_rankzeroevaluation)) * S ((mdr_uc_other_rankzeroevaluation) + (mdr_vb_other_rankzeroevaluation)) + ((mdr_vb_other_rankzeroevaluation) + (mdr_vb_other_rankzeroevaluation))) /\ ((mdr_c_other_rankzeroevaluationdeterminantrc = ((mdr_a_other_rankzeroevaluationdeterminantrc) + (mdr_b_other_rankzeroevaluationdeterminantrc)) * S ((mdr_a_other_rankzeroevaluationdeterminantrc) + (mdr_b_other_rankzeroevaluationdeterminantrc)) + ((mdr_b_other_rankzeroevaluationdeterminantrc) + (mdr_b_other_rankzeroevaluationdeterminantrc))) /\ ((mdr_e_other_rankzeroevaluationdeterminantrc = ((mdr_p_other_rankzero) + (mdr_n_other_rankzero)) * S ((mdr_p_other_rankzero) + (mdr_n_other_rankzero)) + ((mdr_n_other_rankzero) + (mdr_n_other_rankzero))) /\ ((mdr_f_other_rankzeroevaluationdeterminantrc = ((mdr_vc_other_rankzeroevaluation) + (mdr_e_other_rankzeroevaluationdeterminantrc)) * S ((mdr_vc_other_rankzeroevaluation) + (mdr_e_other_rankzeroevaluationdeterminantrc)) + ((mdr_e_other_rankzeroevaluationdeterminantrc) + (mdr_e_other_rankzeroevaluationdeterminantrc))) /\ ((mdr_z_other_rankzeroevaluationdeterminantr) = ((mdr_c_other_rankzeroevaluationdeterminantrc) + (mdr_f_other_rankzeroevaluationdeterminantrc)) * S ((mdr_c_other_rankzeroevaluationdeterminantrc) + (mdr_f_other_rankzeroevaluationdeterminantrc)) + ((mdr_f_other_rankzeroevaluationdeterminantrc) + (mdr_f_other_rankzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_other_rankzeroevaluationdeterminantrb. ff_h_mdr_other_rankzeroevaluationdeterminantrb + S (mdr_z_other_rankzeroevaluationdeterminantr) = S ((S (mdr_i_other_rankzeroevaluationdeterminant)) * mdr_c_other_rankzeroevaluationdeterminant)) /\ exists ff_q_mdr_other_rankzeroevaluationdeterminantrb. mdr_b_other_rankzeroevaluationdeterminant = ff_q_mdr_other_rankzeroevaluationdeterminantrb * S ((S (mdr_i_other_rankzeroevaluationdeterminant)) * mdr_c_other_rankzeroevaluationdeterminant) + (mdr_z_other_rankzeroevaluationdeterminantr)))))))))) -> mdr_p_other_rankzero = mdr_n_other_rankzero)))))) -> other = rank)))