NonzeroMatrixMinor(pb,pc,nb,nc,r,w,q)

exists mdr_rb_secondwave mdr_rc_secondwave mdr_cb_secondwave mdr_cc_secondwave. (((((forall fom_index_mrf_secondwaveminorrowsbound. (exists fom_gap_mrf_secondwaveminorrowsbound_index_bound. fom_gap_mrf_secondwaveminorrowsbound_index_bound + S (fom_index_mrf_secondwaveminorrowsbound) = q) -> exists fom_value_mrf_secondwaveminorrowsbound. ((((exists fom_beta_height_mrf_secondwaveminorrowsbound_entry. fom_beta_height_mrf_secondwaveminorrowsbound_entry + S (fom_value_mrf_secondwaveminorrowsbound) = S ((S (fom_index_mrf_secondwaveminorrowsbound)) * mdr_rc_secondwave)) /\ exists fom_beta_quotient_mrf_secondwaveminorrowsbound_entry. mdr_rb_secondwave = fom_beta_quotient_mrf_secondwaveminorrowsbound_entry * S ((S (fom_index_mrf_secondwaveminorrowsbound)) * mdr_rc_secondwave) + (fom_value_mrf_secondwaveminorrowsbound))) /\ (exists fom_gap_mrf_secondwaveminorrowsbound_value_bound. fom_gap_mrf_secondwaveminorrowsbound_value_bound + S (fom_value_mrf_secondwaveminorrowsbound) = r))) /\ (forall mdr_i_secondwaveminorrowsdistinct mdr_j_secondwaveminorrowsdistinct mdr_a_secondwaveminorrowsdistinct. (exists mdr_gap_secondwaveminorrowsdistincti. mdr_gap_secondwaveminorrowsdistincti + S (mdr_i_secondwaveminorrowsdistinct) = (q)) -> (exists mdr_gap_secondwaveminorrowsdistinctj. mdr_gap_secondwaveminorrowsdistinctj + S (mdr_j_secondwaveminorrowsdistinct) = (q)) -> (((exists ff_h_mdr_secondwaveminorrowsdistinctfirst. ff_h_mdr_secondwaveminorrowsdistinctfirst + S (mdr_a_secondwaveminorrowsdistinct) = S ((S (mdr_i_secondwaveminorrowsdistinct)) * mdr_rc_secondwave)) /\ exists ff_q_mdr_secondwaveminorrowsdistinctfirst. mdr_rb_secondwave = ff_q_mdr_secondwaveminorrowsdistinctfirst * S ((S (mdr_i_secondwaveminorrowsdistinct)) * mdr_rc_secondwave) + (mdr_a_secondwaveminorrowsdistinct))) -> (((exists ff_h_mdr_secondwaveminorrowsdistinctsecond. ff_h_mdr_secondwaveminorrowsdistinctsecond + S (mdr_a_secondwaveminorrowsdistinct) = S ((S (mdr_j_secondwaveminorrowsdistinct)) * mdr_rc_secondwave)) /\ exists ff_q_mdr_secondwaveminorrowsdistinctsecond. mdr_rb_secondwave = ff_q_mdr_secondwaveminorrowsdistinctsecond * S ((S (mdr_j_secondwaveminorrowsdistinct)) * mdr_rc_secondwave) + (mdr_a_secondwaveminorrowsdistinct))) -> mdr_i_secondwaveminorrowsdistinct = mdr_j_secondwaveminorrowsdistinct))) /\ ((((forall fom_index_mrf_secondwaveminorcolumnsbound. (exists fom_gap_mrf_secondwaveminorcolumnsbound_index_bound. fom_gap_mrf_secondwaveminorcolumnsbound_index_bound + S (fom_index_mrf_secondwaveminorcolumnsbound) = q) -> exists fom_value_mrf_secondwaveminorcolumnsbound. ((((exists fom_beta_height_mrf_secondwaveminorcolumnsbound_entry. fom_beta_height_mrf_secondwaveminorcolumnsbound_entry + S (fom_value_mrf_secondwaveminorcolumnsbound) = S ((S (fom_index_mrf_secondwaveminorcolumnsbound)) * mdr_cc_secondwave)) /\ exists fom_beta_quotient_mrf_secondwaveminorcolumnsbound_entry. mdr_cb_secondwave = fom_beta_quotient_mrf_secondwaveminorcolumnsbound_entry * S ((S (fom_index_mrf_secondwaveminorcolumnsbound)) * mdr_cc_secondwave) + (fom_value_mrf_secondwaveminorcolumnsbound))) /\ (exists fom_gap_mrf_secondwaveminorcolumnsbound_value_bound. fom_gap_mrf_secondwaveminorcolumnsbound_value_bound + S (fom_value_mrf_secondwaveminorcolumnsbound) = w))) /\ (forall mdr_i_secondwaveminorcolumnsdistinct mdr_j_secondwaveminorcolumnsdistinct mdr_a_secondwaveminorcolumnsdistinct. (exists mdr_gap_secondwaveminorcolumnsdistincti. mdr_gap_secondwaveminorcolumnsdistincti + S (mdr_i_secondwaveminorcolumnsdistinct) = (q)) -> (exists mdr_gap_secondwaveminorcolumnsdistinctj. mdr_gap_secondwaveminorcolumnsdistinctj + S (mdr_j_secondwaveminorcolumnsdistinct) = (q)) -> (((exists ff_h_mdr_secondwaveminorcolumnsdistinctfirst. ff_h_mdr_secondwaveminorcolumnsdistinctfirst + S (mdr_a_secondwaveminorcolumnsdistinct) = S ((S (mdr_i_secondwaveminorcolumnsdistinct)) * mdr_cc_secondwave)) /\ exists ff_q_mdr_secondwaveminorcolumnsdistinctfirst. mdr_cb_secondwave = ff_q_mdr_secondwaveminorcolumnsdistinctfirst * S ((S (mdr_i_secondwaveminorcolumnsdistinct)) * mdr_cc_secondwave) + (mdr_a_secondwaveminorcolumnsdistinct))) -> (((exists ff_h_mdr_secondwaveminorcolumnsdistinctsecond. ff_h_mdr_secondwaveminorcolumnsdistinctsecond + S (mdr_a_secondwaveminorcolumnsdistinct) = S ((S (mdr_j_secondwaveminorcolumnsdistinct)) * mdr_cc_secondwave)) /\ exists ff_q_mdr_secondwaveminorcolumnsdistinctsecond. mdr_cb_secondwave = ff_q_mdr_secondwaveminorcolumnsdistinctsecond * S ((S (mdr_j_secondwaveminorcolumnsdistinct)) * mdr_cc_secondwave) + (mdr_a_secondwaveminorcolumnsdistinct))) -> mdr_i_secondwaveminorcolumnsdistinct = mdr_j_secondwaveminorcolumnsdistinct))) /\ (exists mdr_p_secondwaveminornonzero mdr_n_secondwaveminornonzero. ((exists mdr_ub_secondwaveminornonzeroevaluation mdr_uc_secondwaveminornonzeroevaluation mdr_vb_secondwaveminornonzeroevaluation mdr_vc_secondwaveminornonzeroevaluation. ((((forall mdr_i_secondwaveminornonzeroevaluationmatrixpositive. (exists mdr_gap_secondwaveminornonzeroevaluationmatrixpositivebound. mdr_gap_secondwaveminornonzeroevaluationmatrixpositivebound + S (mdr_i_secondwaveminornonzeroevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_secondwaveminornonzeroevaluationmatrixpositive. (((exists mdr_r_secondwaveminornonzeroevaluationmatrixpositivepoint mdr_s_secondwaveminornonzeroevaluationmatrixpositivepoint mdr_u_secondwaveminornonzeroevaluationmatrixpositivepoint mdr_v_secondwaveminornonzeroevaluationmatrixpositivepoint. ((mdr_i_secondwaveminornonzeroevaluationmatrixpositive = (q) * mdr_r_secondwaveminornonzeroevaluationmatrixpositivepoint + mdr_s_secondwaveminornonzeroevaluationmatrixpositivepoint) /\ ((exists mdr_gap_secondwaveminornonzeroevaluationmatrixpositivepointcolumn. mdr_gap_secondwaveminornonzeroevaluationmatrixpositivepointcolumn + S (mdr_s_secondwaveminornonzeroevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_secondwaveminornonzeroevaluationmatrixpositivepointrow_index. ff_h_mdr_secondwaveminornonzeroevaluationmatrixpositivepointrow_index + S (mdr_u_secondwaveminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_r_secondwaveminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_secondwave)) /\ exists ff_q_mdr_secondwaveminornonzeroevaluationmatrixpositivepointrow_index. mdr_rb_secondwave = ff_q_mdr_secondwaveminornonzeroevaluationmatrixpositivepointrow_index * S ((S (mdr_r_secondwaveminornonzeroevaluationmatrixpositivepoint)) * mdr_rc_secondwave) + (mdr_u_secondwaveminornonzeroevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_secondwaveminornonzeroevaluationmatrixpositivepointcolumn_index. ff_h_mdr_secondwaveminornonzeroevaluationmatrixpositivepointcolumn_index + S (mdr_v_secondwaveminornonzeroevaluationmatrixpositivepoint) = S ((S (mdr_s_secondwaveminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_secondwave)) /\ exists ff_q_mdr_secondwaveminornonzeroevaluationmatrixpositivepointcolumn_index. mdr_cb_secondwave = ff_q_mdr_secondwaveminornonzeroevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_secondwaveminornonzeroevaluationmatrixpositivepoint)) * mdr_cc_secondwave) + (mdr_v_secondwaveminornonzeroevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_secondwaveminornonzeroevaluationmatrixpositivepointsource. ff_h_mdr_secondwaveminornonzeroevaluationmatrixpositivepointsource + S (mdr_a_secondwaveminornonzeroevaluationmatrixpositive) = S ((S ((mdr_u_secondwaveminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_secondwaveminornonzeroevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_secondwaveminornonzeroevaluationmatrixpositivepointsource. pb = ff_q_mdr_secondwaveminornonzeroevaluationmatrixpositivepointsource * S ((S ((mdr_u_secondwaveminornonzeroevaluationmatrixpositivepoint) * (w) + (mdr_v_secondwaveminornonzeroevaluationmatrixpositivepoint))) * pc) + (mdr_a_secondwaveminornonzeroevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_secondwaveminornonzeroevaluationmatrixpositiveoutput. ff_h_mdr_secondwaveminornonzeroevaluationmatrixpositiveoutput + S (mdr_a_secondwaveminornonzeroevaluationmatrixpositive) = S ((S (mdr_i_secondwaveminornonzeroevaluationmatrixpositive)) * mdr_uc_secondwaveminornonzeroevaluation)) /\ exists ff_q_mdr_secondwaveminornonzeroevaluationmatrixpositiveoutput. mdr_ub_secondwaveminornonzeroevaluation = ff_q_mdr_secondwaveminornonzeroevaluationmatrixpositiveoutput * S ((S (mdr_i_secondwaveminornonzeroevaluationmatrixpositive)) * mdr_uc_secondwaveminornonzeroevaluation) + (mdr_a_secondwaveminornonzeroevaluationmatrixpositive)))))) /\ (forall mdr_i_secondwaveminornonzeroevaluationmatrixnegative. (exists mdr_gap_secondwaveminornonzeroevaluationmatrixnegativebound. mdr_gap_secondwaveminornonzeroevaluationmatrixnegativebound + S (mdr_i_secondwaveminornonzeroevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_secondwaveminornonzeroevaluationmatrixnegative. (((exists mdr_r_secondwaveminornonzeroevaluationmatrixnegativepoint mdr_s_secondwaveminornonzeroevaluationmatrixnegativepoint mdr_u_secondwaveminornonzeroevaluationmatrixnegativepoint mdr_v_secondwaveminornonzeroevaluationmatrixnegativepoint. ((mdr_i_secondwaveminornonzeroevaluationmatrixnegative = (q) * mdr_r_secondwaveminornonzeroevaluationmatrixnegativepoint + mdr_s_secondwaveminornonzeroevaluationmatrixnegativepoint) /\ ((exists mdr_gap_secondwaveminornonzeroevaluationmatrixnegativepointcolumn. mdr_gap_secondwaveminornonzeroevaluationmatrixnegativepointcolumn + S (mdr_s_secondwaveminornonzeroevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_secondwaveminornonzeroevaluationmatrixnegativepointrow_index. ff_h_mdr_secondwaveminornonzeroevaluationmatrixnegativepointrow_index + S (mdr_u_secondwaveminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_r_secondwaveminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_secondwave)) /\ exists ff_q_mdr_secondwaveminornonzeroevaluationmatrixnegativepointrow_index. mdr_rb_secondwave = ff_q_mdr_secondwaveminornonzeroevaluationmatrixnegativepointrow_index * S ((S (mdr_r_secondwaveminornonzeroevaluationmatrixnegativepoint)) * mdr_rc_secondwave) + (mdr_u_secondwaveminornonzeroevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_secondwaveminornonzeroevaluationmatrixnegativepointcolumn_index. ff_h_mdr_secondwaveminornonzeroevaluationmatrixnegativepointcolumn_index + S (mdr_v_secondwaveminornonzeroevaluationmatrixnegativepoint) = S ((S (mdr_s_secondwaveminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_secondwave)) /\ exists ff_q_mdr_secondwaveminornonzeroevaluationmatrixnegativepointcolumn_index. mdr_cb_secondwave = ff_q_mdr_secondwaveminornonzeroevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_secondwaveminornonzeroevaluationmatrixnegativepoint)) * mdr_cc_secondwave) + (mdr_v_secondwaveminornonzeroevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_secondwaveminornonzeroevaluationmatrixnegativepointsource. ff_h_mdr_secondwaveminornonzeroevaluationmatrixnegativepointsource + S (mdr_a_secondwaveminornonzeroevaluationmatrixnegative) = S ((S ((mdr_u_secondwaveminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_secondwaveminornonzeroevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_secondwaveminornonzeroevaluationmatrixnegativepointsource. nb = ff_q_mdr_secondwaveminornonzeroevaluationmatrixnegativepointsource * S ((S ((mdr_u_secondwaveminornonzeroevaluationmatrixnegativepoint) * (w) + (mdr_v_secondwaveminornonzeroevaluationmatrixnegativepoint))) * nc) + (mdr_a_secondwaveminornonzeroevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_secondwaveminornonzeroevaluationmatrixnegativeoutput. ff_h_mdr_secondwaveminornonzeroevaluationmatrixnegativeoutput + S (mdr_a_secondwaveminornonzeroevaluationmatrixnegative) = S ((S (mdr_i_secondwaveminornonzeroevaluationmatrixnegative)) * mdr_vc_secondwaveminornonzeroevaluation)) /\ exists ff_q_mdr_secondwaveminornonzeroevaluationmatrixnegativeoutput. mdr_vb_secondwaveminornonzeroevaluation = ff_q_mdr_secondwaveminornonzeroevaluationmatrixnegativeoutput * S ((S (mdr_i_secondwaveminornonzeroevaluationmatrixnegative)) * mdr_vc_secondwaveminornonzeroevaluation) + (mdr_a_secondwaveminornonzeroevaluationmatrixnegative)))))))) /\ (exists mdr_b_secondwaveminornonzeroevaluationdeterminant mdr_c_secondwaveminornonzeroevaluationdeterminant mdr_l_secondwaveminornonzeroevaluationdeterminant mdr_i_secondwaveminornonzeroevaluationdeterminant. ((forall mdr_i_secondwaveminornonzeroevaluationdeterminanth. (exists mdr_gap_secondwaveminornonzeroevaluationdeterminanthi. mdr_gap_secondwaveminornonzeroevaluationdeterminanthi + S (mdr_i_secondwaveminornonzeroevaluationdeterminanth) = (mdr_l_secondwaveminornonzeroevaluationdeterminant)) -> exists mdr_d_secondwaveminornonzeroevaluationdeterminanth mdr_pb_secondwaveminornonzeroevaluationdeterminanth mdr_pc_secondwaveminornonzeroevaluationdeterminanth mdr_nb_secondwaveminornonzeroevaluationdeterminanth mdr_nc_secondwaveminornonzeroevaluationdeterminanth mdr_p_secondwaveminornonzeroevaluationdeterminanth mdr_n_secondwaveminornonzeroevaluationdeterminanth. ((exists mdr_z_secondwaveminornonzeroevaluationdeterminanthr. ((exists mdr_a_secondwaveminornonzeroevaluationdeterminanthrc mdr_b_secondwaveminornonzeroevaluationdeterminanthrc mdr_c_secondwaveminornonzeroevaluationdeterminanthrc mdr_e_secondwaveminornonzeroevaluationdeterminanthrc mdr_f_secondwaveminornonzeroevaluationdeterminanthrc. ((mdr_a_secondwaveminornonzeroevaluationdeterminanthrc = ((mdr_d_secondwaveminornonzeroevaluationdeterminanth) + (mdr_pb_secondwaveminornonzeroevaluationdeterminanth)) * S ((mdr_d_secondwaveminornonzeroevaluationdeterminanth) + (mdr_pb_secondwaveminornonzeroevaluationdeterminanth)) + ((mdr_pb_secondwaveminornonzeroevaluationdeterminanth) + (mdr_pb_secondwaveminornonzeroevaluationdeterminanth))) /\ ((mdr_b_secondwaveminornonzeroevaluationdeterminanthrc = ((mdr_pc_secondwaveminornonzeroevaluationdeterminanth) + (mdr_nb_secondwaveminornonzeroevaluationdeterminanth)) * S ((mdr_pc_secondwaveminornonzeroevaluationdeterminanth) + (mdr_nb_secondwaveminornonzeroevaluationdeterminanth)) + ((mdr_nb_secondwaveminornonzeroevaluationdeterminanth) + (mdr_nb_secondwaveminornonzeroevaluationdeterminanth))) /\ ((mdr_c_secondwaveminornonzeroevaluationdeterminanthrc = ((mdr_a_secondwaveminornonzeroevaluationdeterminanthrc) + (mdr_b_secondwaveminornonzeroevaluationdeterminanthrc)) * S ((mdr_a_secondwaveminornonzeroevaluationdeterminanthrc) + (mdr_b_secondwaveminornonzeroevaluationdeterminanthrc)) + ((mdr_b_secondwaveminornonzeroevaluationdeterminanthrc) + (mdr_b_secondwaveminornonzeroevaluationdeterminanthrc))) /\ ((mdr_e_secondwaveminornonzeroevaluationdeterminanthrc = ((mdr_p_secondwaveminornonzeroevaluationdeterminanth) + (mdr_n_secondwaveminornonzeroevaluationdeterminanth)) * S ((mdr_p_secondwaveminornonzeroevaluationdeterminanth) + (mdr_n_secondwaveminornonzeroevaluationdeterminanth)) + ((mdr_n_secondwaveminornonzeroevaluationdeterminanth) + (mdr_n_secondwaveminornonzeroevaluationdeterminanth))) /\ ((mdr_f_secondwaveminornonzeroevaluationdeterminanthrc = ((mdr_nc_secondwaveminornonzeroevaluationdeterminanth) + (mdr_e_secondwaveminornonzeroevaluationdeterminanthrc)) * S ((mdr_nc_secondwaveminornonzeroevaluationdeterminanth) + (mdr_e_secondwaveminornonzeroevaluationdeterminanthrc)) + ((mdr_e_secondwaveminornonzeroevaluationdeterminanthrc) + (mdr_e_secondwaveminornonzeroevaluationdeterminanthrc))) /\ ((mdr_z_secondwaveminornonzeroevaluationdeterminanthr) = ((mdr_c_secondwaveminornonzeroevaluationdeterminanthrc) + (mdr_f_secondwaveminornonzeroevaluationdeterminanthrc)) * S ((mdr_c_secondwaveminornonzeroevaluationdeterminanthrc) + (mdr_f_secondwaveminornonzeroevaluationdeterminanthrc)) + ((mdr_f_secondwaveminornonzeroevaluationdeterminanthrc) + (mdr_f_secondwaveminornonzeroevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_secondwaveminornonzeroevaluationdeterminanthrb. ff_h_mdr_secondwaveminornonzeroevaluationdeterminanthrb + S (mdr_z_secondwaveminornonzeroevaluationdeterminanthr) = S ((S (mdr_i_secondwaveminornonzeroevaluationdeterminanth)) * mdr_c_secondwaveminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_secondwaveminornonzeroevaluationdeterminanthrb. mdr_b_secondwaveminornonzeroevaluationdeterminant = ff_q_mdr_secondwaveminornonzeroevaluationdeterminanthrb * S ((S (mdr_i_secondwaveminornonzeroevaluationdeterminanth)) * mdr_c_secondwaveminornonzeroevaluationdeterminant) + (mdr_z_secondwaveminornonzeroevaluationdeterminanthr))))) /\ (((((mdr_d_secondwaveminornonzeroevaluationdeterminanth) = 0) /\ (((mdr_p_secondwaveminornonzeroevaluationdeterminanth) = 1) /\ ((mdr_n_secondwaveminornonzeroevaluationdeterminanth) = 0))) \/ exists mdr_q_secondwaveminornonzeroevaluationdeterminanths mdr_eb_secondwaveminornonzeroevaluationdeterminanths mdr_ec_secondwaveminornonzeroevaluationdeterminanths mdr_fb_secondwaveminornonzeroevaluationdeterminanths mdr_fc_secondwaveminornonzeroevaluationdeterminanths. (((mdr_d_secondwaveminornonzeroevaluationdeterminanth) = S (mdr_q_secondwaveminornonzeroevaluationdeterminanths)) /\ ((forall mdr_j_secondwaveminornonzeroevaluationdeterminanthsc. (exists mdr_gap_secondwaveminornonzeroevaluationdeterminanthscj. mdr_gap_secondwaveminornonzeroevaluationdeterminanthscj + S (mdr_j_secondwaveminornonzeroevaluationdeterminanthsc) = (S (mdr_q_secondwaveminornonzeroevaluationdeterminanths))) -> exists mdr_i_secondwaveminornonzeroevaluationdeterminanthsc mdr_up_secondwaveminornonzeroevaluationdeterminanthsc mdr_us_secondwaveminornonzeroevaluationdeterminanthsc mdr_un_secondwaveminornonzeroevaluationdeterminanthsc mdr_ut_secondwaveminornonzeroevaluationdeterminanthsc mdr_p_secondwaveminornonzeroevaluationdeterminanthsc mdr_n_secondwaveminornonzeroevaluationdeterminanthsc. ((exists mdr_gap_secondwaveminornonzeroevaluationdeterminanthsci. mdr_gap_secondwaveminornonzeroevaluationdeterminanthsci + S (mdr_i_secondwaveminornonzeroevaluationdeterminanthsc) = (mdr_i_secondwaveminornonzeroevaluationdeterminanth)) /\ ((exists mdr_z_secondwaveminornonzeroevaluationdeterminanthscr. ((exists mdr_a_secondwaveminornonzeroevaluationdeterminanthscrc mdr_b_secondwaveminornonzeroevaluationdeterminanthscrc mdr_c_secondwaveminornonzeroevaluationdeterminanthscrc mdr_e_secondwaveminornonzeroevaluationdeterminanthscrc mdr_f_secondwaveminornonzeroevaluationdeterminanthscrc. ((mdr_a_secondwaveminornonzeroevaluationdeterminanthscrc = ((mdr_q_secondwaveminornonzeroevaluationdeterminanths) + (mdr_up_secondwaveminornonzeroevaluationdeterminanthsc)) * S ((mdr_q_secondwaveminornonzeroevaluationdeterminanths) + (mdr_up_secondwaveminornonzeroevaluationdeterminanthsc)) + ((mdr_up_secondwaveminornonzeroevaluationdeterminanthsc) + (mdr_up_secondwaveminornonzeroevaluationdeterminanthsc))) /\ ((mdr_b_secondwaveminornonzeroevaluationdeterminanthscrc = ((mdr_us_secondwaveminornonzeroevaluationdeterminanthsc) + (mdr_un_secondwaveminornonzeroevaluationdeterminanthsc)) * S ((mdr_us_secondwaveminornonzeroevaluationdeterminanthsc) + (mdr_un_secondwaveminornonzeroevaluationdeterminanthsc)) + ((mdr_un_secondwaveminornonzeroevaluationdeterminanthsc) + (mdr_un_secondwaveminornonzeroevaluationdeterminanthsc))) /\ ((mdr_c_secondwaveminornonzeroevaluationdeterminanthscrc = ((mdr_a_secondwaveminornonzeroevaluationdeterminanthscrc) + (mdr_b_secondwaveminornonzeroevaluationdeterminanthscrc)) * S ((mdr_a_secondwaveminornonzeroevaluationdeterminanthscrc) + (mdr_b_secondwaveminornonzeroevaluationdeterminanthscrc)) + ((mdr_b_secondwaveminornonzeroevaluationdeterminanthscrc) + (mdr_b_secondwaveminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_e_secondwaveminornonzeroevaluationdeterminanthscrc = ((mdr_p_secondwaveminornonzeroevaluationdeterminanthsc) + (mdr_n_secondwaveminornonzeroevaluationdeterminanthsc)) * S ((mdr_p_secondwaveminornonzeroevaluationdeterminanthsc) + (mdr_n_secondwaveminornonzeroevaluationdeterminanthsc)) + ((mdr_n_secondwaveminornonzeroevaluationdeterminanthsc) + (mdr_n_secondwaveminornonzeroevaluationdeterminanthsc))) /\ ((mdr_f_secondwaveminornonzeroevaluationdeterminanthscrc = ((mdr_ut_secondwaveminornonzeroevaluationdeterminanthsc) + (mdr_e_secondwaveminornonzeroevaluationdeterminanthscrc)) * S ((mdr_ut_secondwaveminornonzeroevaluationdeterminanthsc) + (mdr_e_secondwaveminornonzeroevaluationdeterminanthscrc)) + ((mdr_e_secondwaveminornonzeroevaluationdeterminanthscrc) + (mdr_e_secondwaveminornonzeroevaluationdeterminanthscrc))) /\ ((mdr_z_secondwaveminornonzeroevaluationdeterminanthscr) = ((mdr_c_secondwaveminornonzeroevaluationdeterminanthscrc) + (mdr_f_secondwaveminornonzeroevaluationdeterminanthscrc)) * S ((mdr_c_secondwaveminornonzeroevaluationdeterminanthscrc) + (mdr_f_secondwaveminornonzeroevaluationdeterminanthscrc)) + ((mdr_f_secondwaveminornonzeroevaluationdeterminanthscrc) + (mdr_f_secondwaveminornonzeroevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_secondwaveminornonzeroevaluationdeterminanthscrb. ff_h_mdr_secondwaveminornonzeroevaluationdeterminanthscrb + S (mdr_z_secondwaveminornonzeroevaluationdeterminanthscr) = S ((S (mdr_i_secondwaveminornonzeroevaluationdeterminanthsc)) * mdr_c_secondwaveminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_secondwaveminornonzeroevaluationdeterminanthscrb. mdr_b_secondwaveminornonzeroevaluationdeterminant = ff_q_mdr_secondwaveminornonzeroevaluationdeterminanthscrb * S ((S (mdr_i_secondwaveminornonzeroevaluationdeterminanthsc)) * mdr_c_secondwaveminornonzeroevaluationdeterminant) + (mdr_z_secondwaveminornonzeroevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive) = ((mdr_q_secondwaveminornonzeroevaluationdeterminanths) * (mdr_q_secondwaveminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive = (mdr_q_secondwaveminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive) = (mdr_q_secondwaveminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive) = (mdr_j_secondwaveminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_secondwaveminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_secondwaveminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_secondwaveminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_cell_source. mdr_pb_secondwaveminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_cell) * (S (mdr_q_secondwaveminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_cell))) * mdr_pc_secondwaveminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_secondwaveminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_target. mdr_up_secondwaveminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive)) * mdr_us_secondwaveminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative) = ((mdr_q_secondwaveminornonzeroevaluationdeterminanths) * (mdr_q_secondwaveminornonzeroevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative = (mdr_q_secondwaveminornonzeroevaluationdeterminanths) * ff_row_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative) = (mdr_q_secondwaveminornonzeroevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative) = (mdr_j_secondwaveminornonzeroevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_secondwaveminornonzeroevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_secondwaveminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_secondwaveminornonzeroevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_cell_source. mdr_nb_secondwaveminornonzeroevaluationdeterminanth = ff_q_mdm_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_cell) * (S (mdr_q_secondwaveminornonzeroevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_cell))) * mdr_nc_secondwaveminornonzeroevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_secondwaveminornonzeroevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_target. mdr_un_secondwaveminornonzeroevaluationdeterminanthsc = ff_q_mdm_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative)) * mdr_ut_secondwaveminornonzeroevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_secondwaveminornonzeroevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_secondwaveminornonzeroevaluationdeterminanthscp. ff_h_mdr_secondwaveminornonzeroevaluationdeterminanthscp + S (mdr_p_secondwaveminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_secondwaveminornonzeroevaluationdeterminanthsc)) * mdr_ec_secondwaveminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_secondwaveminornonzeroevaluationdeterminanthscp. mdr_eb_secondwaveminornonzeroevaluationdeterminanths = ff_q_mdr_secondwaveminornonzeroevaluationdeterminanthscp * S ((S (mdr_j_secondwaveminornonzeroevaluationdeterminanthsc)) * mdr_ec_secondwaveminornonzeroevaluationdeterminanths) + (mdr_p_secondwaveminornonzeroevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_secondwaveminornonzeroevaluationdeterminanthscn. ff_h_mdr_secondwaveminornonzeroevaluationdeterminanthscn + S (mdr_n_secondwaveminornonzeroevaluationdeterminanthsc) = S ((S (mdr_j_secondwaveminornonzeroevaluationdeterminanthsc)) * mdr_fc_secondwaveminornonzeroevaluationdeterminanths)) /\ exists ff_q_mdr_secondwaveminornonzeroevaluationdeterminanthscn. mdr_fb_secondwaveminornonzeroevaluationdeterminanths = ff_q_mdr_secondwaveminornonzeroevaluationdeterminanthscn * S ((S (mdr_j_secondwaveminornonzeroevaluationdeterminanthsc)) * mdr_fc_secondwaveminornonzeroevaluationdeterminanths) + (mdr_n_secondwaveminornonzeroevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_secondwaveminornonzeroevaluationdeterminanthsf ff_uc_mce_fold_mdr_secondwaveminornonzeroevaluationdeterminanthsf ff_vb_mce_fold_mdr_secondwaveminornonzeroevaluationdeterminanthsf ff_vc_mce_fold_mdr_secondwaveminornonzeroevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix) = (S (mdr_q_secondwaveminornonzeroevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_secondwaveminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_ap. mdr_pb_secondwaveminornonzeroevaluationdeterminanth = ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix)) * mdr_pc_secondwaveminornonzeroevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_secondwaveminornonzeroevaluationdeterminanth)) /\ exists ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_an. mdr_nb_secondwaveminornonzeroevaluationdeterminanth = ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix)) * mdr_nc_secondwaveminornonzeroevaluationdeterminanth) + (ff_an_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_secondwaveminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_bp. mdr_eb_secondwaveminornonzeroevaluationdeterminanths = ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix)) * mdr_ec_secondwaveminornonzeroevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_secondwaveminornonzeroevaluationdeterminanths)) /\ exists ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_bn. mdr_fb_secondwaveminornonzeroevaluationdeterminanths = ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix)) * mdr_fc_secondwaveminornonzeroevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_secondwaveminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_secondwaveminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_secondwaveminornonzeroevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_secondwaveminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_secondwaveminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_secondwaveminornonzeroevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_secondwaveminornonzeroevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive ff_v_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive_terminal + S (mdr_p_secondwaveminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_secondwaveminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_secondwaveminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive) + (mdr_p_secondwaveminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive = (S (mdr_q_secondwaveminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive ff_r_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive ff_s_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_secondwaveminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_secondwaveminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_secondwaveminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive = ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive = ff_r_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive + ff_a_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative ff_v_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative_terminal + S (mdr_n_secondwaveminornonzeroevaluationdeterminanth) = S ((S ((S (mdr_q_secondwaveminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_secondwaveminornonzeroevaluationdeterminanths)))) * ff_v_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative) + (mdr_n_secondwaveminornonzeroevaluationdeterminanth))) /\ forall ff_i_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative = (S (mdr_q_secondwaveminornonzeroevaluationdeterminanths))) -> exists ff_a_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative ff_r_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative ff_s_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_secondwaveminornonzeroevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_secondwaveminornonzeroevaluationdeterminanthsf = ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_secondwaveminornonzeroevaluationdeterminanthsf) + (ff_a_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative = ff_q_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative = ff_r_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative + ff_a_mce_mdr_secondwaveminornonzeroevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_secondwaveminornonzeroevaluationdeterminanti. mdr_gap_secondwaveminornonzeroevaluationdeterminanti + S (mdr_i_secondwaveminornonzeroevaluationdeterminant) = (mdr_l_secondwaveminornonzeroevaluationdeterminant)) /\ (exists mdr_z_secondwaveminornonzeroevaluationdeterminantr. ((exists mdr_a_secondwaveminornonzeroevaluationdeterminantrc mdr_b_secondwaveminornonzeroevaluationdeterminantrc mdr_c_secondwaveminornonzeroevaluationdeterminantrc mdr_e_secondwaveminornonzeroevaluationdeterminantrc mdr_f_secondwaveminornonzeroevaluationdeterminantrc. ((mdr_a_secondwaveminornonzeroevaluationdeterminantrc = ((q) + (mdr_ub_secondwaveminornonzeroevaluation)) * S ((q) + (mdr_ub_secondwaveminornonzeroevaluation)) + ((mdr_ub_secondwaveminornonzeroevaluation) + (mdr_ub_secondwaveminornonzeroevaluation))) /\ ((mdr_b_secondwaveminornonzeroevaluationdeterminantrc = ((mdr_uc_secondwaveminornonzeroevaluation) + (mdr_vb_secondwaveminornonzeroevaluation)) * S ((mdr_uc_secondwaveminornonzeroevaluation) + (mdr_vb_secondwaveminornonzeroevaluation)) + ((mdr_vb_secondwaveminornonzeroevaluation) + (mdr_vb_secondwaveminornonzeroevaluation))) /\ ((mdr_c_secondwaveminornonzeroevaluationdeterminantrc = ((mdr_a_secondwaveminornonzeroevaluationdeterminantrc) + (mdr_b_secondwaveminornonzeroevaluationdeterminantrc)) * S ((mdr_a_secondwaveminornonzeroevaluationdeterminantrc) + (mdr_b_secondwaveminornonzeroevaluationdeterminantrc)) + ((mdr_b_secondwaveminornonzeroevaluationdeterminantrc) + (mdr_b_secondwaveminornonzeroevaluationdeterminantrc))) /\ ((mdr_e_secondwaveminornonzeroevaluationdeterminantrc = ((mdr_p_secondwaveminornonzero) + (mdr_n_secondwaveminornonzero)) * S ((mdr_p_secondwaveminornonzero) + (mdr_n_secondwaveminornonzero)) + ((mdr_n_secondwaveminornonzero) + (mdr_n_secondwaveminornonzero))) /\ ((mdr_f_secondwaveminornonzeroevaluationdeterminantrc = ((mdr_vc_secondwaveminornonzeroevaluation) + (mdr_e_secondwaveminornonzeroevaluationdeterminantrc)) * S ((mdr_vc_secondwaveminornonzeroevaluation) + (mdr_e_secondwaveminornonzeroevaluationdeterminantrc)) + ((mdr_e_secondwaveminornonzeroevaluationdeterminantrc) + (mdr_e_secondwaveminornonzeroevaluationdeterminantrc))) /\ ((mdr_z_secondwaveminornonzeroevaluationdeterminantr) = ((mdr_c_secondwaveminornonzeroevaluationdeterminantrc) + (mdr_f_secondwaveminornonzeroevaluationdeterminantrc)) * S ((mdr_c_secondwaveminornonzeroevaluationdeterminantrc) + (mdr_f_secondwaveminornonzeroevaluationdeterminantrc)) + ((mdr_f_secondwaveminornonzeroevaluationdeterminantrc) + (mdr_f_secondwaveminornonzeroevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_secondwaveminornonzeroevaluationdeterminantrb. ff_h_mdr_secondwaveminornonzeroevaluationdeterminantrb + S (mdr_z_secondwaveminornonzeroevaluationdeterminantr) = S ((S (mdr_i_secondwaveminornonzeroevaluationdeterminant)) * mdr_c_secondwaveminornonzeroevaluationdeterminant)) /\ exists ff_q_mdr_secondwaveminornonzeroevaluationdeterminantrb. mdr_b_secondwaveminornonzeroevaluationdeterminant = ff_q_mdr_secondwaveminornonzeroevaluationdeterminantrb * S ((S (mdr_i_secondwaveminornonzeroevaluationdeterminant)) * mdr_c_secondwaveminornonzeroevaluationdeterminant) + (mdr_z_secondwaveminornonzeroevaluationdeterminantr)))))))))) /\ (~(mdr_p_secondwaveminornonzero = mdr_n_secondwaveminornonzero)))))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.