SignedSelectedDeterminant(pb,pc,nb,nc,w,rb,rc,cb,cc,q,p,n)

exists mdr_ub_secondwave mdr_uc_secondwave mdr_vb_secondwave mdr_vc_secondwave. ((((forall mdr_i_secondwavematrixpositive. (exists mdr_gap_secondwavematrixpositivebound. mdr_gap_secondwavematrixpositivebound + S (mdr_i_secondwavematrixpositive) = ((q) * (q))) -> exists mdr_a_secondwavematrixpositive. (((exists mdr_r_secondwavematrixpositivepoint mdr_s_secondwavematrixpositivepoint mdr_u_secondwavematrixpositivepoint mdr_v_secondwavematrixpositivepoint. ((mdr_i_secondwavematrixpositive = (q) * mdr_r_secondwavematrixpositivepoint + mdr_s_secondwavematrixpositivepoint) /\ ((exists mdr_gap_secondwavematrixpositivepointcolumn. mdr_gap_secondwavematrixpositivepointcolumn + S (mdr_s_secondwavematrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_secondwavematrixpositivepointrow_index. ff_h_mdr_secondwavematrixpositivepointrow_index + S (mdr_u_secondwavematrixpositivepoint) = S ((S (mdr_r_secondwavematrixpositivepoint)) * rc)) /\ exists ff_q_mdr_secondwavematrixpositivepointrow_index. rb = ff_q_mdr_secondwavematrixpositivepointrow_index * S ((S (mdr_r_secondwavematrixpositivepoint)) * rc) + (mdr_u_secondwavematrixpositivepoint))) /\ ((((exists ff_h_mdr_secondwavematrixpositivepointcolumn_index. ff_h_mdr_secondwavematrixpositivepointcolumn_index + S (mdr_v_secondwavematrixpositivepoint) = S ((S (mdr_s_secondwavematrixpositivepoint)) * cc)) /\ exists ff_q_mdr_secondwavematrixpositivepointcolumn_index. cb = ff_q_mdr_secondwavematrixpositivepointcolumn_index * S ((S (mdr_s_secondwavematrixpositivepoint)) * cc) + (mdr_v_secondwavematrixpositivepoint))) /\ (((exists ff_h_mdr_secondwavematrixpositivepointsource. ff_h_mdr_secondwavematrixpositivepointsource + S (mdr_a_secondwavematrixpositive) = S ((S ((mdr_u_secondwavematrixpositivepoint) * (w) + (mdr_v_secondwavematrixpositivepoint))) * pc)) /\ exists ff_q_mdr_secondwavematrixpositivepointsource. pb = ff_q_mdr_secondwavematrixpositivepointsource * S ((S ((mdr_u_secondwavematrixpositivepoint) * (w) + (mdr_v_secondwavematrixpositivepoint))) * pc) + (mdr_a_secondwavematrixpositive)))))))) /\ (((exists ff_h_mdr_secondwavematrixpositiveoutput. ff_h_mdr_secondwavematrixpositiveoutput + S (mdr_a_secondwavematrixpositive) = S ((S (mdr_i_secondwavematrixpositive)) * mdr_uc_secondwave)) /\ exists ff_q_mdr_secondwavematrixpositiveoutput. mdr_ub_secondwave = ff_q_mdr_secondwavematrixpositiveoutput * S ((S (mdr_i_secondwavematrixpositive)) * mdr_uc_secondwave) + (mdr_a_secondwavematrixpositive)))))) /\ (forall mdr_i_secondwavematrixnegative. (exists mdr_gap_secondwavematrixnegativebound. mdr_gap_secondwavematrixnegativebound + S (mdr_i_secondwavematrixnegative) = ((q) * (q))) -> exists mdr_a_secondwavematrixnegative. (((exists mdr_r_secondwavematrixnegativepoint mdr_s_secondwavematrixnegativepoint mdr_u_secondwavematrixnegativepoint mdr_v_secondwavematrixnegativepoint. ((mdr_i_secondwavematrixnegative = (q) * mdr_r_secondwavematrixnegativepoint + mdr_s_secondwavematrixnegativepoint) /\ ((exists mdr_gap_secondwavematrixnegativepointcolumn. mdr_gap_secondwavematrixnegativepointcolumn + S (mdr_s_secondwavematrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_secondwavematrixnegativepointrow_index. ff_h_mdr_secondwavematrixnegativepointrow_index + S (mdr_u_secondwavematrixnegativepoint) = S ((S (mdr_r_secondwavematrixnegativepoint)) * rc)) /\ exists ff_q_mdr_secondwavematrixnegativepointrow_index. rb = ff_q_mdr_secondwavematrixnegativepointrow_index * S ((S (mdr_r_secondwavematrixnegativepoint)) * rc) + (mdr_u_secondwavematrixnegativepoint))) /\ ((((exists ff_h_mdr_secondwavematrixnegativepointcolumn_index. ff_h_mdr_secondwavematrixnegativepointcolumn_index + S (mdr_v_secondwavematrixnegativepoint) = S ((S (mdr_s_secondwavematrixnegativepoint)) * cc)) /\ exists ff_q_mdr_secondwavematrixnegativepointcolumn_index. cb = ff_q_mdr_secondwavematrixnegativepointcolumn_index * S ((S (mdr_s_secondwavematrixnegativepoint)) * cc) + (mdr_v_secondwavematrixnegativepoint))) /\ (((exists ff_h_mdr_secondwavematrixnegativepointsource. ff_h_mdr_secondwavematrixnegativepointsource + S (mdr_a_secondwavematrixnegative) = S ((S ((mdr_u_secondwavematrixnegativepoint) * (w) + (mdr_v_secondwavematrixnegativepoint))) * nc)) /\ exists ff_q_mdr_secondwavematrixnegativepointsource. nb = ff_q_mdr_secondwavematrixnegativepointsource * S ((S ((mdr_u_secondwavematrixnegativepoint) * (w) + (mdr_v_secondwavematrixnegativepoint))) * nc) + (mdr_a_secondwavematrixnegative)))))))) /\ (((exists ff_h_mdr_secondwavematrixnegativeoutput. ff_h_mdr_secondwavematrixnegativeoutput + S (mdr_a_secondwavematrixnegative) = S ((S (mdr_i_secondwavematrixnegative)) * mdr_vc_secondwave)) /\ exists ff_q_mdr_secondwavematrixnegativeoutput. mdr_vb_secondwave = ff_q_mdr_secondwavematrixnegativeoutput * S ((S (mdr_i_secondwavematrixnegative)) * mdr_vc_secondwave) + (mdr_a_secondwavematrixnegative)))))))) /\ (exists mdr_b_secondwavedeterminant mdr_c_secondwavedeterminant mdr_l_secondwavedeterminant mdr_i_secondwavedeterminant. ((forall mdr_i_secondwavedeterminanth. (exists mdr_gap_secondwavedeterminanthi. mdr_gap_secondwavedeterminanthi + S (mdr_i_secondwavedeterminanth) = (mdr_l_secondwavedeterminant)) -> exists mdr_d_secondwavedeterminanth mdr_pb_secondwavedeterminanth mdr_pc_secondwavedeterminanth mdr_nb_secondwavedeterminanth mdr_nc_secondwavedeterminanth mdr_p_secondwavedeterminanth mdr_n_secondwavedeterminanth. ((exists mdr_z_secondwavedeterminanthr. ((exists mdr_a_secondwavedeterminanthrc mdr_b_secondwavedeterminanthrc mdr_c_secondwavedeterminanthrc mdr_e_secondwavedeterminanthrc mdr_f_secondwavedeterminanthrc. ((mdr_a_secondwavedeterminanthrc = ((mdr_d_secondwavedeterminanth) + (mdr_pb_secondwavedeterminanth)) * S ((mdr_d_secondwavedeterminanth) + (mdr_pb_secondwavedeterminanth)) + ((mdr_pb_secondwavedeterminanth) + (mdr_pb_secondwavedeterminanth))) /\ ((mdr_b_secondwavedeterminanthrc = ((mdr_pc_secondwavedeterminanth) + (mdr_nb_secondwavedeterminanth)) * S ((mdr_pc_secondwavedeterminanth) + (mdr_nb_secondwavedeterminanth)) + ((mdr_nb_secondwavedeterminanth) + (mdr_nb_secondwavedeterminanth))) /\ ((mdr_c_secondwavedeterminanthrc = ((mdr_a_secondwavedeterminanthrc) + (mdr_b_secondwavedeterminanthrc)) * S ((mdr_a_secondwavedeterminanthrc) + (mdr_b_secondwavedeterminanthrc)) + ((mdr_b_secondwavedeterminanthrc) + (mdr_b_secondwavedeterminanthrc))) /\ ((mdr_e_secondwavedeterminanthrc = ((mdr_p_secondwavedeterminanth) + (mdr_n_secondwavedeterminanth)) * S ((mdr_p_secondwavedeterminanth) + (mdr_n_secondwavedeterminanth)) + ((mdr_n_secondwavedeterminanth) + (mdr_n_secondwavedeterminanth))) /\ ((mdr_f_secondwavedeterminanthrc = ((mdr_nc_secondwavedeterminanth) + (mdr_e_secondwavedeterminanthrc)) * S ((mdr_nc_secondwavedeterminanth) + (mdr_e_secondwavedeterminanthrc)) + ((mdr_e_secondwavedeterminanthrc) + (mdr_e_secondwavedeterminanthrc))) /\ ((mdr_z_secondwavedeterminanthr) = ((mdr_c_secondwavedeterminanthrc) + (mdr_f_secondwavedeterminanthrc)) * S ((mdr_c_secondwavedeterminanthrc) + (mdr_f_secondwavedeterminanthrc)) + ((mdr_f_secondwavedeterminanthrc) + (mdr_f_secondwavedeterminanthrc))))))))) /\ (((exists ff_h_mdr_secondwavedeterminanthrb. ff_h_mdr_secondwavedeterminanthrb + S (mdr_z_secondwavedeterminanthr) = S ((S (mdr_i_secondwavedeterminanth)) * mdr_c_secondwavedeterminant)) /\ exists ff_q_mdr_secondwavedeterminanthrb. mdr_b_secondwavedeterminant = ff_q_mdr_secondwavedeterminanthrb * S ((S (mdr_i_secondwavedeterminanth)) * mdr_c_secondwavedeterminant) + (mdr_z_secondwavedeterminanthr))))) /\ (((((mdr_d_secondwavedeterminanth) = 0) /\ (((mdr_p_secondwavedeterminanth) = 1) /\ ((mdr_n_secondwavedeterminanth) = 0))) \/ exists mdr_q_secondwavedeterminanths mdr_eb_secondwavedeterminanths mdr_ec_secondwavedeterminanths mdr_fb_secondwavedeterminanths mdr_fc_secondwavedeterminanths. (((mdr_d_secondwavedeterminanth) = S (mdr_q_secondwavedeterminanths)) /\ ((forall mdr_j_secondwavedeterminanthsc. (exists mdr_gap_secondwavedeterminanthscj. mdr_gap_secondwavedeterminanthscj + S (mdr_j_secondwavedeterminanthsc) = (S (mdr_q_secondwavedeterminanths))) -> exists mdr_i_secondwavedeterminanthsc mdr_up_secondwavedeterminanthsc mdr_us_secondwavedeterminanthsc mdr_un_secondwavedeterminanthsc mdr_ut_secondwavedeterminanthsc mdr_p_secondwavedeterminanthsc mdr_n_secondwavedeterminanthsc. ((exists mdr_gap_secondwavedeterminanthsci. mdr_gap_secondwavedeterminanthsci + S (mdr_i_secondwavedeterminanthsc) = (mdr_i_secondwavedeterminanth)) /\ ((exists mdr_z_secondwavedeterminanthscr. ((exists mdr_a_secondwavedeterminanthscrc mdr_b_secondwavedeterminanthscrc mdr_c_secondwavedeterminanthscrc mdr_e_secondwavedeterminanthscrc mdr_f_secondwavedeterminanthscrc. ((mdr_a_secondwavedeterminanthscrc = ((mdr_q_secondwavedeterminanths) + (mdr_up_secondwavedeterminanthsc)) * S ((mdr_q_secondwavedeterminanths) + (mdr_up_secondwavedeterminanthsc)) + ((mdr_up_secondwavedeterminanthsc) + (mdr_up_secondwavedeterminanthsc))) /\ ((mdr_b_secondwavedeterminanthscrc = ((mdr_us_secondwavedeterminanthsc) + (mdr_un_secondwavedeterminanthsc)) * S ((mdr_us_secondwavedeterminanthsc) + (mdr_un_secondwavedeterminanthsc)) + ((mdr_un_secondwavedeterminanthsc) + (mdr_un_secondwavedeterminanthsc))) /\ ((mdr_c_secondwavedeterminanthscrc = ((mdr_a_secondwavedeterminanthscrc) + (mdr_b_secondwavedeterminanthscrc)) * S ((mdr_a_secondwavedeterminanthscrc) + (mdr_b_secondwavedeterminanthscrc)) + ((mdr_b_secondwavedeterminanthscrc) + (mdr_b_secondwavedeterminanthscrc))) /\ ((mdr_e_secondwavedeterminanthscrc = ((mdr_p_secondwavedeterminanthsc) + (mdr_n_secondwavedeterminanthsc)) * S ((mdr_p_secondwavedeterminanthsc) + (mdr_n_secondwavedeterminanthsc)) + ((mdr_n_secondwavedeterminanthsc) + (mdr_n_secondwavedeterminanthsc))) /\ ((mdr_f_secondwavedeterminanthscrc = ((mdr_ut_secondwavedeterminanthsc) + (mdr_e_secondwavedeterminanthscrc)) * S ((mdr_ut_secondwavedeterminanthsc) + (mdr_e_secondwavedeterminanthscrc)) + ((mdr_e_secondwavedeterminanthscrc) + (mdr_e_secondwavedeterminanthscrc))) /\ ((mdr_z_secondwavedeterminanthscr) = ((mdr_c_secondwavedeterminanthscrc) + (mdr_f_secondwavedeterminanthscrc)) * S ((mdr_c_secondwavedeterminanthscrc) + (mdr_f_secondwavedeterminanthscrc)) + ((mdr_f_secondwavedeterminanthscrc) + (mdr_f_secondwavedeterminanthscrc))))))))) /\ (((exists ff_h_mdr_secondwavedeterminanthscrb. ff_h_mdr_secondwavedeterminanthscrb + S (mdr_z_secondwavedeterminanthscr) = S ((S (mdr_i_secondwavedeterminanthsc)) * mdr_c_secondwavedeterminant)) /\ exists ff_q_mdr_secondwavedeterminanthscrb. mdr_b_secondwavedeterminant = ff_q_mdr_secondwavedeterminanthscrb * S ((S (mdr_i_secondwavedeterminanthsc)) * mdr_c_secondwavedeterminant) + (mdr_z_secondwavedeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_secondwavedeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_secondwavedeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_secondwavedeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_secondwavedeterminanthscm_positive) = ((mdr_q_secondwavedeterminanths) * (mdr_q_secondwavedeterminanths))) -> exists ff_row_mdm_prefix_mdr_secondwavedeterminanthscm_positive ff_column_mdm_prefix_mdr_secondwavedeterminanthscm_positive ff_value_mdm_prefix_mdr_secondwavedeterminanthscm_positive. (ff_index_mdm_prefix_mdr_secondwavedeterminanthscm_positive = (mdr_q_secondwavedeterminanths) * ff_row_mdm_prefix_mdr_secondwavedeterminanthscm_positive + ff_column_mdm_prefix_mdr_secondwavedeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_secondwavedeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_secondwavedeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_secondwavedeterminanthscm_positive) = (mdr_q_secondwavedeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_secondwavedeterminanthscm_positive_cell ff_column_mdm_cell_mdr_secondwavedeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_secondwavedeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_secondwavedeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_secondwavedeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_secondwavedeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_secondwavedeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_secondwavedeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_secondwavedeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_secondwavedeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_secondwavedeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_secondwavedeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_secondwavedeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_secondwavedeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_secondwavedeterminanthscm_positive) = (mdr_j_secondwavedeterminanthsc)) /\ ff_column_mdm_cell_mdr_secondwavedeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_secondwavedeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_secondwavedeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_secondwavedeterminanthscm_positive_cell_column_after + (mdr_j_secondwavedeterminanthsc) = (ff_column_mdm_prefix_mdr_secondwavedeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_secondwavedeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_secondwavedeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_secondwavedeterminanthscm_positive_cell_source. ff_h_mdm_mdr_secondwavedeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_secondwavedeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_secondwavedeterminanthscm_positive_cell) * (S (mdr_q_secondwavedeterminanths)) + (ff_column_mdm_cell_mdr_secondwavedeterminanthscm_positive_cell))) * mdr_pc_secondwavedeterminanth)) /\ exists ff_q_mdm_mdr_secondwavedeterminanthscm_positive_cell_source. mdr_pb_secondwavedeterminanth = ff_q_mdm_mdr_secondwavedeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_secondwavedeterminanthscm_positive_cell) * (S (mdr_q_secondwavedeterminanths)) + (ff_column_mdm_cell_mdr_secondwavedeterminanthscm_positive_cell))) * mdr_pc_secondwavedeterminanth) + (ff_value_mdm_prefix_mdr_secondwavedeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_secondwavedeterminanthscm_positive_target. ff_h_mdm_mdr_secondwavedeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_secondwavedeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_secondwavedeterminanthscm_positive)) * mdr_us_secondwavedeterminanthsc)) /\ exists ff_q_mdm_mdr_secondwavedeterminanthscm_positive_target. mdr_up_secondwavedeterminanthsc = ff_q_mdm_mdr_secondwavedeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_secondwavedeterminanthscm_positive)) * mdr_us_secondwavedeterminanthsc) + (ff_value_mdm_prefix_mdr_secondwavedeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_secondwavedeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_secondwavedeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_secondwavedeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_secondwavedeterminanthscm_negative) = ((mdr_q_secondwavedeterminanths) * (mdr_q_secondwavedeterminanths))) -> exists ff_row_mdm_prefix_mdr_secondwavedeterminanthscm_negative ff_column_mdm_prefix_mdr_secondwavedeterminanthscm_negative ff_value_mdm_prefix_mdr_secondwavedeterminanthscm_negative. (ff_index_mdm_prefix_mdr_secondwavedeterminanthscm_negative = (mdr_q_secondwavedeterminanths) * ff_row_mdm_prefix_mdr_secondwavedeterminanthscm_negative + ff_column_mdm_prefix_mdr_secondwavedeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_secondwavedeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_secondwavedeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_secondwavedeterminanthscm_negative) = (mdr_q_secondwavedeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_secondwavedeterminanthscm_negative_cell ff_column_mdm_cell_mdr_secondwavedeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_secondwavedeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_secondwavedeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_secondwavedeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_secondwavedeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_secondwavedeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_secondwavedeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_secondwavedeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_secondwavedeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_secondwavedeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_secondwavedeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_secondwavedeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_secondwavedeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_secondwavedeterminanthscm_negative) = (mdr_j_secondwavedeterminanthsc)) /\ ff_column_mdm_cell_mdr_secondwavedeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_secondwavedeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_secondwavedeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_secondwavedeterminanthscm_negative_cell_column_after + (mdr_j_secondwavedeterminanthsc) = (ff_column_mdm_prefix_mdr_secondwavedeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_secondwavedeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_secondwavedeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_secondwavedeterminanthscm_negative_cell_source. ff_h_mdm_mdr_secondwavedeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_secondwavedeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_secondwavedeterminanthscm_negative_cell) * (S (mdr_q_secondwavedeterminanths)) + (ff_column_mdm_cell_mdr_secondwavedeterminanthscm_negative_cell))) * mdr_nc_secondwavedeterminanth)) /\ exists ff_q_mdm_mdr_secondwavedeterminanthscm_negative_cell_source. mdr_nb_secondwavedeterminanth = ff_q_mdm_mdr_secondwavedeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_secondwavedeterminanthscm_negative_cell) * (S (mdr_q_secondwavedeterminanths)) + (ff_column_mdm_cell_mdr_secondwavedeterminanthscm_negative_cell))) * mdr_nc_secondwavedeterminanth) + (ff_value_mdm_prefix_mdr_secondwavedeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_secondwavedeterminanthscm_negative_target. ff_h_mdm_mdr_secondwavedeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_secondwavedeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_secondwavedeterminanthscm_negative)) * mdr_ut_secondwavedeterminanthsc)) /\ exists ff_q_mdm_mdr_secondwavedeterminanthscm_negative_target. mdr_un_secondwavedeterminanthsc = ff_q_mdm_mdr_secondwavedeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_secondwavedeterminanthscm_negative)) * mdr_ut_secondwavedeterminanthsc) + (ff_value_mdm_prefix_mdr_secondwavedeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_secondwavedeterminanthscp. ff_h_mdr_secondwavedeterminanthscp + S (mdr_p_secondwavedeterminanthsc) = S ((S (mdr_j_secondwavedeterminanthsc)) * mdr_ec_secondwavedeterminanths)) /\ exists ff_q_mdr_secondwavedeterminanthscp. mdr_eb_secondwavedeterminanths = ff_q_mdr_secondwavedeterminanthscp * S ((S (mdr_j_secondwavedeterminanthsc)) * mdr_ec_secondwavedeterminanths) + (mdr_p_secondwavedeterminanthsc))) /\ (((exists ff_h_mdr_secondwavedeterminanthscn. ff_h_mdr_secondwavedeterminanthscn + S (mdr_n_secondwavedeterminanthsc) = S ((S (mdr_j_secondwavedeterminanthsc)) * mdr_fc_secondwavedeterminanths)) /\ exists ff_q_mdr_secondwavedeterminanthscn. mdr_fb_secondwavedeterminanths = ff_q_mdr_secondwavedeterminanthscn * S ((S (mdr_j_secondwavedeterminanthsc)) * mdr_fc_secondwavedeterminanths) + (mdr_n_secondwavedeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_secondwavedeterminanthsf ff_uc_mce_fold_mdr_secondwavedeterminanthsf ff_vb_mce_fold_mdr_secondwavedeterminanthsf ff_vc_mce_fold_mdr_secondwavedeterminanthsf. ((forall ff_index_mce_alternating_mdr_secondwavedeterminanthsf_prefix. (exists ff_gap_mce_mdr_secondwavedeterminanthsf_prefix_index. ff_gap_mce_mdr_secondwavedeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_secondwavedeterminanthsf_prefix) = (S (mdr_q_secondwavedeterminanths))) -> exists ff_ap_mce_alternating_mdr_secondwavedeterminanthsf_prefix ff_an_mce_alternating_mdr_secondwavedeterminanthsf_prefix ff_bp_mce_alternating_mdr_secondwavedeterminanthsf_prefix ff_bn_mce_alternating_mdr_secondwavedeterminanthsf_prefix ff_p_mce_alternating_mdr_secondwavedeterminanthsf_prefix ff_n_mce_alternating_mdr_secondwavedeterminanthsf_prefix. ((((exists ff_h_mce_mdr_secondwavedeterminanthsf_prefix_ap. ff_h_mce_mdr_secondwavedeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_secondwavedeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavedeterminanthsf_prefix)) * mdr_pc_secondwavedeterminanth)) /\ exists ff_q_mce_mdr_secondwavedeterminanthsf_prefix_ap. mdr_pb_secondwavedeterminanth = ff_q_mce_mdr_secondwavedeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_secondwavedeterminanthsf_prefix)) * mdr_pc_secondwavedeterminanth) + (ff_ap_mce_alternating_mdr_secondwavedeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavedeterminanthsf_prefix_an. ff_h_mce_mdr_secondwavedeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_secondwavedeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavedeterminanthsf_prefix)) * mdr_nc_secondwavedeterminanth)) /\ exists ff_q_mce_mdr_secondwavedeterminanthsf_prefix_an. mdr_nb_secondwavedeterminanth = ff_q_mce_mdr_secondwavedeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_secondwavedeterminanthsf_prefix)) * mdr_nc_secondwavedeterminanth) + (ff_an_mce_alternating_mdr_secondwavedeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavedeterminanthsf_prefix_bp. ff_h_mce_mdr_secondwavedeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_secondwavedeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavedeterminanthsf_prefix)) * mdr_ec_secondwavedeterminanths)) /\ exists ff_q_mce_mdr_secondwavedeterminanthsf_prefix_bp. mdr_eb_secondwavedeterminanths = ff_q_mce_mdr_secondwavedeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_secondwavedeterminanthsf_prefix)) * mdr_ec_secondwavedeterminanths) + (ff_bp_mce_alternating_mdr_secondwavedeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavedeterminanthsf_prefix_bn. ff_h_mce_mdr_secondwavedeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_secondwavedeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavedeterminanthsf_prefix)) * mdr_fc_secondwavedeterminanths)) /\ exists ff_q_mce_mdr_secondwavedeterminanthsf_prefix_bn. mdr_fb_secondwavedeterminanths = ff_q_mce_mdr_secondwavedeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_secondwavedeterminanthsf_prefix)) * mdr_fc_secondwavedeterminanths) + (ff_bn_mce_alternating_mdr_secondwavedeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavedeterminanthsf_prefix_positive. ff_h_mce_mdr_secondwavedeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_secondwavedeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavedeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_secondwavedeterminanthsf)) /\ exists ff_q_mce_mdr_secondwavedeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_secondwavedeterminanthsf = ff_q_mce_mdr_secondwavedeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_secondwavedeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_secondwavedeterminanthsf) + (ff_p_mce_alternating_mdr_secondwavedeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_secondwavedeterminanthsf_prefix_negative. ff_h_mce_mdr_secondwavedeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_secondwavedeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_secondwavedeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_secondwavedeterminanthsf)) /\ exists ff_q_mce_mdr_secondwavedeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_secondwavedeterminanthsf = ff_q_mce_mdr_secondwavedeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_secondwavedeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_secondwavedeterminanthsf) + (ff_n_mce_alternating_mdr_secondwavedeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_secondwavedeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_secondwavedeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_secondwavedeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_secondwavedeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_secondwavedeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_secondwavedeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_secondwavedeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_secondwavedeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_secondwavedeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_secondwavedeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_secondwavedeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_secondwavedeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_secondwavedeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_secondwavedeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_secondwavedeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_secondwavedeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_secondwavedeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_secondwavedeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_secondwavedeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_secondwavedeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_secondwavedeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_secondwavedeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_secondwavedeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_secondwavedeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_secondwavedeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_secondwavedeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_secondwavedeterminanthsf_positive ff_v_mce_mdr_secondwavedeterminanthsf_positive. ((((exists ff_h_mce_mdr_secondwavedeterminanthsf_positive_start. ff_h_mce_mdr_secondwavedeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_secondwavedeterminanthsf_positive)) /\ exists ff_q_mce_mdr_secondwavedeterminanthsf_positive_start. ff_u_mce_mdr_secondwavedeterminanthsf_positive = ff_q_mce_mdr_secondwavedeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_secondwavedeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_secondwavedeterminanthsf_positive_terminal. ff_h_mce_mdr_secondwavedeterminanthsf_positive_terminal + S (mdr_p_secondwavedeterminanth) = S ((S ((S (mdr_q_secondwavedeterminanths)))) * ff_v_mce_mdr_secondwavedeterminanthsf_positive)) /\ exists ff_q_mce_mdr_secondwavedeterminanthsf_positive_terminal. ff_u_mce_mdr_secondwavedeterminanthsf_positive = ff_q_mce_mdr_secondwavedeterminanthsf_positive_terminal * S ((S ((S (mdr_q_secondwavedeterminanths)))) * ff_v_mce_mdr_secondwavedeterminanthsf_positive) + (mdr_p_secondwavedeterminanth))) /\ forall ff_i_mce_mdr_secondwavedeterminanthsf_positive. (exists ff_lt_mce_mdr_secondwavedeterminanthsf_positive_bound. ff_lt_mce_mdr_secondwavedeterminanthsf_positive_bound + S ff_i_mce_mdr_secondwavedeterminanthsf_positive = (S (mdr_q_secondwavedeterminanths))) -> exists ff_a_mce_mdr_secondwavedeterminanthsf_positive ff_r_mce_mdr_secondwavedeterminanthsf_positive ff_s_mce_mdr_secondwavedeterminanthsf_positive. ((((exists ff_h_mce_mdr_secondwavedeterminanthsf_positive_summand. ff_h_mce_mdr_secondwavedeterminanthsf_positive_summand + S (ff_a_mce_mdr_secondwavedeterminanthsf_positive) = S ((S (ff_i_mce_mdr_secondwavedeterminanthsf_positive)) * ff_uc_mce_fold_mdr_secondwavedeterminanthsf)) /\ exists ff_q_mce_mdr_secondwavedeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_secondwavedeterminanthsf = ff_q_mce_mdr_secondwavedeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_secondwavedeterminanthsf_positive)) * ff_uc_mce_fold_mdr_secondwavedeterminanthsf) + (ff_a_mce_mdr_secondwavedeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_secondwavedeterminanthsf_positive_partial. ff_h_mce_mdr_secondwavedeterminanthsf_positive_partial + S (ff_r_mce_mdr_secondwavedeterminanthsf_positive) = S ((S (ff_i_mce_mdr_secondwavedeterminanthsf_positive)) * ff_v_mce_mdr_secondwavedeterminanthsf_positive)) /\ exists ff_q_mce_mdr_secondwavedeterminanthsf_positive_partial. ff_u_mce_mdr_secondwavedeterminanthsf_positive = ff_q_mce_mdr_secondwavedeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_secondwavedeterminanthsf_positive)) * ff_v_mce_mdr_secondwavedeterminanthsf_positive) + (ff_r_mce_mdr_secondwavedeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_secondwavedeterminanthsf_positive_successor. ff_h_mce_mdr_secondwavedeterminanthsf_positive_successor + S (ff_s_mce_mdr_secondwavedeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_secondwavedeterminanthsf_positive)) * ff_v_mce_mdr_secondwavedeterminanthsf_positive)) /\ exists ff_q_mce_mdr_secondwavedeterminanthsf_positive_successor. ff_u_mce_mdr_secondwavedeterminanthsf_positive = ff_q_mce_mdr_secondwavedeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_secondwavedeterminanthsf_positive)) * ff_v_mce_mdr_secondwavedeterminanthsf_positive) + (ff_s_mce_mdr_secondwavedeterminanthsf_positive))) /\ ff_s_mce_mdr_secondwavedeterminanthsf_positive = ff_r_mce_mdr_secondwavedeterminanthsf_positive + ff_a_mce_mdr_secondwavedeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_secondwavedeterminanthsf_negative ff_v_mce_mdr_secondwavedeterminanthsf_negative. ((((exists ff_h_mce_mdr_secondwavedeterminanthsf_negative_start. ff_h_mce_mdr_secondwavedeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_secondwavedeterminanthsf_negative)) /\ exists ff_q_mce_mdr_secondwavedeterminanthsf_negative_start. ff_u_mce_mdr_secondwavedeterminanthsf_negative = ff_q_mce_mdr_secondwavedeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_secondwavedeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_secondwavedeterminanthsf_negative_terminal. ff_h_mce_mdr_secondwavedeterminanthsf_negative_terminal + S (mdr_n_secondwavedeterminanth) = S ((S ((S (mdr_q_secondwavedeterminanths)))) * ff_v_mce_mdr_secondwavedeterminanthsf_negative)) /\ exists ff_q_mce_mdr_secondwavedeterminanthsf_negative_terminal. ff_u_mce_mdr_secondwavedeterminanthsf_negative = ff_q_mce_mdr_secondwavedeterminanthsf_negative_terminal * S ((S ((S (mdr_q_secondwavedeterminanths)))) * ff_v_mce_mdr_secondwavedeterminanthsf_negative) + (mdr_n_secondwavedeterminanth))) /\ forall ff_i_mce_mdr_secondwavedeterminanthsf_negative. (exists ff_lt_mce_mdr_secondwavedeterminanthsf_negative_bound. ff_lt_mce_mdr_secondwavedeterminanthsf_negative_bound + S ff_i_mce_mdr_secondwavedeterminanthsf_negative = (S (mdr_q_secondwavedeterminanths))) -> exists ff_a_mce_mdr_secondwavedeterminanthsf_negative ff_r_mce_mdr_secondwavedeterminanthsf_negative ff_s_mce_mdr_secondwavedeterminanthsf_negative. ((((exists ff_h_mce_mdr_secondwavedeterminanthsf_negative_summand. ff_h_mce_mdr_secondwavedeterminanthsf_negative_summand + S (ff_a_mce_mdr_secondwavedeterminanthsf_negative) = S ((S (ff_i_mce_mdr_secondwavedeterminanthsf_negative)) * ff_vc_mce_fold_mdr_secondwavedeterminanthsf)) /\ exists ff_q_mce_mdr_secondwavedeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_secondwavedeterminanthsf = ff_q_mce_mdr_secondwavedeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_secondwavedeterminanthsf_negative)) * ff_vc_mce_fold_mdr_secondwavedeterminanthsf) + (ff_a_mce_mdr_secondwavedeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_secondwavedeterminanthsf_negative_partial. ff_h_mce_mdr_secondwavedeterminanthsf_negative_partial + S (ff_r_mce_mdr_secondwavedeterminanthsf_negative) = S ((S (ff_i_mce_mdr_secondwavedeterminanthsf_negative)) * ff_v_mce_mdr_secondwavedeterminanthsf_negative)) /\ exists ff_q_mce_mdr_secondwavedeterminanthsf_negative_partial. ff_u_mce_mdr_secondwavedeterminanthsf_negative = ff_q_mce_mdr_secondwavedeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_secondwavedeterminanthsf_negative)) * ff_v_mce_mdr_secondwavedeterminanthsf_negative) + (ff_r_mce_mdr_secondwavedeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_secondwavedeterminanthsf_negative_successor. ff_h_mce_mdr_secondwavedeterminanthsf_negative_successor + S (ff_s_mce_mdr_secondwavedeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_secondwavedeterminanthsf_negative)) * ff_v_mce_mdr_secondwavedeterminanthsf_negative)) /\ exists ff_q_mce_mdr_secondwavedeterminanthsf_negative_successor. ff_u_mce_mdr_secondwavedeterminanthsf_negative = ff_q_mce_mdr_secondwavedeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_secondwavedeterminanthsf_negative)) * ff_v_mce_mdr_secondwavedeterminanthsf_negative) + (ff_s_mce_mdr_secondwavedeterminanthsf_negative))) /\ ff_s_mce_mdr_secondwavedeterminanthsf_negative = ff_r_mce_mdr_secondwavedeterminanthsf_negative + ff_a_mce_mdr_secondwavedeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_secondwavedeterminanti. mdr_gap_secondwavedeterminanti + S (mdr_i_secondwavedeterminant) = (mdr_l_secondwavedeterminant)) /\ (exists mdr_z_secondwavedeterminantr. ((exists mdr_a_secondwavedeterminantrc mdr_b_secondwavedeterminantrc mdr_c_secondwavedeterminantrc mdr_e_secondwavedeterminantrc mdr_f_secondwavedeterminantrc. ((mdr_a_secondwavedeterminantrc = ((q) + (mdr_ub_secondwave)) * S ((q) + (mdr_ub_secondwave)) + ((mdr_ub_secondwave) + (mdr_ub_secondwave))) /\ ((mdr_b_secondwavedeterminantrc = ((mdr_uc_secondwave) + (mdr_vb_secondwave)) * S ((mdr_uc_secondwave) + (mdr_vb_secondwave)) + ((mdr_vb_secondwave) + (mdr_vb_secondwave))) /\ ((mdr_c_secondwavedeterminantrc = ((mdr_a_secondwavedeterminantrc) + (mdr_b_secondwavedeterminantrc)) * S ((mdr_a_secondwavedeterminantrc) + (mdr_b_secondwavedeterminantrc)) + ((mdr_b_secondwavedeterminantrc) + (mdr_b_secondwavedeterminantrc))) /\ ((mdr_e_secondwavedeterminantrc = ((p) + (n)) * S ((p) + (n)) + ((n) + (n))) /\ ((mdr_f_secondwavedeterminantrc = ((mdr_vc_secondwave) + (mdr_e_secondwavedeterminantrc)) * S ((mdr_vc_secondwave) + (mdr_e_secondwavedeterminantrc)) + ((mdr_e_secondwavedeterminantrc) + (mdr_e_secondwavedeterminantrc))) /\ ((mdr_z_secondwavedeterminantr) = ((mdr_c_secondwavedeterminantrc) + (mdr_f_secondwavedeterminantrc)) * S ((mdr_c_secondwavedeterminantrc) + (mdr_f_secondwavedeterminantrc)) + ((mdr_f_secondwavedeterminantrc) + (mdr_f_secondwavedeterminantrc))))))))) /\ (((exists ff_h_mdr_secondwavedeterminantrb. ff_h_mdr_secondwavedeterminantrb + S (mdr_z_secondwavedeterminantr) = S ((S (mdr_i_secondwavedeterminant)) * mdr_c_secondwavedeterminant)) /\ exists ff_q_mdr_secondwavedeterminantrb. mdr_b_secondwavedeterminant = ff_q_mdr_secondwavedeterminantrb * S ((S (mdr_i_secondwavedeterminant)) * mdr_c_secondwavedeterminant) + (mdr_z_secondwavedeterminantr)))))))))

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