matrix_rank_selected_nonzero_value_decidable

Exact expanded first-order arithmetic statement

forall pb pc nb nc w rb rc cb cc q. (exists mdr_p_nonzero_value_yes mdr_n_nonzero_value_yes. ((exists mdr_ub_nonzero_value_yesevaluation mdr_uc_nonzero_value_yesevaluation mdr_vb_nonzero_value_yesevaluation mdr_vc_nonzero_value_yesevaluation. ((((forall mdr_i_nonzero_value_yesevaluationmatrixpositive. (exists mdr_gap_nonzero_value_yesevaluationmatrixpositivebound. mdr_gap_nonzero_value_yesevaluationmatrixpositivebound + S (mdr_i_nonzero_value_yesevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_nonzero_value_yesevaluationmatrixpositive. (((exists mdr_r_nonzero_value_yesevaluationmatrixpositivepoint mdr_s_nonzero_value_yesevaluationmatrixpositivepoint mdr_u_nonzero_value_yesevaluationmatrixpositivepoint mdr_v_nonzero_value_yesevaluationmatrixpositivepoint. ((mdr_i_nonzero_value_yesevaluationmatrixpositive = (q) * mdr_r_nonzero_value_yesevaluationmatrixpositivepoint + mdr_s_nonzero_value_yesevaluationmatrixpositivepoint) /\ ((exists mdr_gap_nonzero_value_yesevaluationmatrixpositivepointcolumn. mdr_gap_nonzero_value_yesevaluationmatrixpositivepointcolumn + S (mdr_s_nonzero_value_yesevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_nonzero_value_yesevaluationmatrixpositivepointrow_index. ff_h_mdr_nonzero_value_yesevaluationmatrixpositivepointrow_index + S (mdr_u_nonzero_value_yesevaluationmatrixpositivepoint) = S ((S (mdr_r_nonzero_value_yesevaluationmatrixpositivepoint)) * rc)) /\ exists ff_q_mdr_nonzero_value_yesevaluationmatrixpositivepointrow_index. rb = ff_q_mdr_nonzero_value_yesevaluationmatrixpositivepointrow_index * S ((S (mdr_r_nonzero_value_yesevaluationmatrixpositivepoint)) * rc) + (mdr_u_nonzero_value_yesevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_nonzero_value_yesevaluationmatrixpositivepointcolumn_index. ff_h_mdr_nonzero_value_yesevaluationmatrixpositivepointcolumn_index + S (mdr_v_nonzero_value_yesevaluationmatrixpositivepoint) = S ((S (mdr_s_nonzero_value_yesevaluationmatrixpositivepoint)) * cc)) /\ exists ff_q_mdr_nonzero_value_yesevaluationmatrixpositivepointcolumn_index. cb = ff_q_mdr_nonzero_value_yesevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_nonzero_value_yesevaluationmatrixpositivepoint)) * cc) + (mdr_v_nonzero_value_yesevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_nonzero_value_yesevaluationmatrixpositivepointsource. ff_h_mdr_nonzero_value_yesevaluationmatrixpositivepointsource + S (mdr_a_nonzero_value_yesevaluationmatrixpositive) = S ((S ((mdr_u_nonzero_value_yesevaluationmatrixpositivepoint) * (w) + (mdr_v_nonzero_value_yesevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_nonzero_value_yesevaluationmatrixpositivepointsource. pb = ff_q_mdr_nonzero_value_yesevaluationmatrixpositivepointsource * S ((S ((mdr_u_nonzero_value_yesevaluationmatrixpositivepoint) * (w) + (mdr_v_nonzero_value_yesevaluationmatrixpositivepoint))) * pc) + (mdr_a_nonzero_value_yesevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_nonzero_value_yesevaluationmatrixpositiveoutput. ff_h_mdr_nonzero_value_yesevaluationmatrixpositiveoutput + S (mdr_a_nonzero_value_yesevaluationmatrixpositive) = S ((S (mdr_i_nonzero_value_yesevaluationmatrixpositive)) * mdr_uc_nonzero_value_yesevaluation)) /\ exists ff_q_mdr_nonzero_value_yesevaluationmatrixpositiveoutput. mdr_ub_nonzero_value_yesevaluation = ff_q_mdr_nonzero_value_yesevaluationmatrixpositiveoutput * S ((S (mdr_i_nonzero_value_yesevaluationmatrixpositive)) * mdr_uc_nonzero_value_yesevaluation) + (mdr_a_nonzero_value_yesevaluationmatrixpositive)))))) /\ (forall mdr_i_nonzero_value_yesevaluationmatrixnegative. (exists mdr_gap_nonzero_value_yesevaluationmatrixnegativebound. mdr_gap_nonzero_value_yesevaluationmatrixnegativebound + S (mdr_i_nonzero_value_yesevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_nonzero_value_yesevaluationmatrixnegative. (((exists mdr_r_nonzero_value_yesevaluationmatrixnegativepoint mdr_s_nonzero_value_yesevaluationmatrixnegativepoint mdr_u_nonzero_value_yesevaluationmatrixnegativepoint mdr_v_nonzero_value_yesevaluationmatrixnegativepoint. ((mdr_i_nonzero_value_yesevaluationmatrixnegative = (q) * mdr_r_nonzero_value_yesevaluationmatrixnegativepoint + mdr_s_nonzero_value_yesevaluationmatrixnegativepoint) /\ ((exists mdr_gap_nonzero_value_yesevaluationmatrixnegativepointcolumn. mdr_gap_nonzero_value_yesevaluationmatrixnegativepointcolumn + S (mdr_s_nonzero_value_yesevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_nonzero_value_yesevaluationmatrixnegativepointrow_index. ff_h_mdr_nonzero_value_yesevaluationmatrixnegativepointrow_index + S (mdr_u_nonzero_value_yesevaluationmatrixnegativepoint) = S ((S (mdr_r_nonzero_value_yesevaluationmatrixnegativepoint)) * rc)) /\ exists ff_q_mdr_nonzero_value_yesevaluationmatrixnegativepointrow_index. rb = ff_q_mdr_nonzero_value_yesevaluationmatrixnegativepointrow_index * S ((S (mdr_r_nonzero_value_yesevaluationmatrixnegativepoint)) * rc) + (mdr_u_nonzero_value_yesevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_nonzero_value_yesevaluationmatrixnegativepointcolumn_index. ff_h_mdr_nonzero_value_yesevaluationmatrixnegativepointcolumn_index + S (mdr_v_nonzero_value_yesevaluationmatrixnegativepoint) = S ((S (mdr_s_nonzero_value_yesevaluationmatrixnegativepoint)) * cc)) /\ exists ff_q_mdr_nonzero_value_yesevaluationmatrixnegativepointcolumn_index. cb = ff_q_mdr_nonzero_value_yesevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_nonzero_value_yesevaluationmatrixnegativepoint)) * cc) + (mdr_v_nonzero_value_yesevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_nonzero_value_yesevaluationmatrixnegativepointsource. ff_h_mdr_nonzero_value_yesevaluationmatrixnegativepointsource + S (mdr_a_nonzero_value_yesevaluationmatrixnegative) = S ((S ((mdr_u_nonzero_value_yesevaluationmatrixnegativepoint) * (w) + (mdr_v_nonzero_value_yesevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_nonzero_value_yesevaluationmatrixnegativepointsource. nb = ff_q_mdr_nonzero_value_yesevaluationmatrixnegativepointsource * S ((S ((mdr_u_nonzero_value_yesevaluationmatrixnegativepoint) * (w) + (mdr_v_nonzero_value_yesevaluationmatrixnegativepoint))) * nc) + (mdr_a_nonzero_value_yesevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_nonzero_value_yesevaluationmatrixnegativeoutput. ff_h_mdr_nonzero_value_yesevaluationmatrixnegativeoutput + S (mdr_a_nonzero_value_yesevaluationmatrixnegative) = S ((S (mdr_i_nonzero_value_yesevaluationmatrixnegative)) * mdr_vc_nonzero_value_yesevaluation)) /\ exists ff_q_mdr_nonzero_value_yesevaluationmatrixnegativeoutput. mdr_vb_nonzero_value_yesevaluation = ff_q_mdr_nonzero_value_yesevaluationmatrixnegativeoutput * S ((S (mdr_i_nonzero_value_yesevaluationmatrixnegative)) * mdr_vc_nonzero_value_yesevaluation) + (mdr_a_nonzero_value_yesevaluationmatrixnegative)))))))) /\ (exists mdr_b_nonzero_value_yesevaluationdeterminant mdr_c_nonzero_value_yesevaluationdeterminant mdr_l_nonzero_value_yesevaluationdeterminant mdr_i_nonzero_value_yesevaluationdeterminant. ((forall mdr_i_nonzero_value_yesevaluationdeterminanth. (exists mdr_gap_nonzero_value_yesevaluationdeterminanthi. mdr_gap_nonzero_value_yesevaluationdeterminanthi + S (mdr_i_nonzero_value_yesevaluationdeterminanth) = (mdr_l_nonzero_value_yesevaluationdeterminant)) -> exists mdr_d_nonzero_value_yesevaluationdeterminanth mdr_pb_nonzero_value_yesevaluationdeterminanth mdr_pc_nonzero_value_yesevaluationdeterminanth mdr_nb_nonzero_value_yesevaluationdeterminanth mdr_nc_nonzero_value_yesevaluationdeterminanth mdr_p_nonzero_value_yesevaluationdeterminanth mdr_n_nonzero_value_yesevaluationdeterminanth. ((exists mdr_z_nonzero_value_yesevaluationdeterminanthr. ((exists mdr_a_nonzero_value_yesevaluationdeterminanthrc mdr_b_nonzero_value_yesevaluationdeterminanthrc mdr_c_nonzero_value_yesevaluationdeterminanthrc mdr_e_nonzero_value_yesevaluationdeterminanthrc mdr_f_nonzero_value_yesevaluationdeterminanthrc. ((mdr_a_nonzero_value_yesevaluationdeterminanthrc = ((mdr_d_nonzero_value_yesevaluationdeterminanth) + (mdr_pb_nonzero_value_yesevaluationdeterminanth)) * S ((mdr_d_nonzero_value_yesevaluationdeterminanth) + (mdr_pb_nonzero_value_yesevaluationdeterminanth)) + ((mdr_pb_nonzero_value_yesevaluationdeterminanth) + (mdr_pb_nonzero_value_yesevaluationdeterminanth))) /\ ((mdr_b_nonzero_value_yesevaluationdeterminanthrc = ((mdr_pc_nonzero_value_yesevaluationdeterminanth) + (mdr_nb_nonzero_value_yesevaluationdeterminanth)) * S ((mdr_pc_nonzero_value_yesevaluationdeterminanth) + (mdr_nb_nonzero_value_yesevaluationdeterminanth)) + ((mdr_nb_nonzero_value_yesevaluationdeterminanth) + (mdr_nb_nonzero_value_yesevaluationdeterminanth))) /\ ((mdr_c_nonzero_value_yesevaluationdeterminanthrc = ((mdr_a_nonzero_value_yesevaluationdeterminanthrc) + (mdr_b_nonzero_value_yesevaluationdeterminanthrc)) * S ((mdr_a_nonzero_value_yesevaluationdeterminanthrc) + (mdr_b_nonzero_value_yesevaluationdeterminanthrc)) + ((mdr_b_nonzero_value_yesevaluationdeterminanthrc) + (mdr_b_nonzero_value_yesevaluationdeterminanthrc))) /\ ((mdr_e_nonzero_value_yesevaluationdeterminanthrc = ((mdr_p_nonzero_value_yesevaluationdeterminanth) + (mdr_n_nonzero_value_yesevaluationdeterminanth)) * S ((mdr_p_nonzero_value_yesevaluationdeterminanth) + (mdr_n_nonzero_value_yesevaluationdeterminanth)) + ((mdr_n_nonzero_value_yesevaluationdeterminanth) + (mdr_n_nonzero_value_yesevaluationdeterminanth))) /\ ((mdr_f_nonzero_value_yesevaluationdeterminanthrc = ((mdr_nc_nonzero_value_yesevaluationdeterminanth) + (mdr_e_nonzero_value_yesevaluationdeterminanthrc)) * S ((mdr_nc_nonzero_value_yesevaluationdeterminanth) + (mdr_e_nonzero_value_yesevaluationdeterminanthrc)) + ((mdr_e_nonzero_value_yesevaluationdeterminanthrc) + (mdr_e_nonzero_value_yesevaluationdeterminanthrc))) /\ ((mdr_z_nonzero_value_yesevaluationdeterminanthr) = ((mdr_c_nonzero_value_yesevaluationdeterminanthrc) + (mdr_f_nonzero_value_yesevaluationdeterminanthrc)) * S ((mdr_c_nonzero_value_yesevaluationdeterminanthrc) + (mdr_f_nonzero_value_yesevaluationdeterminanthrc)) + ((mdr_f_nonzero_value_yesevaluationdeterminanthrc) + (mdr_f_nonzero_value_yesevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_nonzero_value_yesevaluationdeterminanthrb. ff_h_mdr_nonzero_value_yesevaluationdeterminanthrb + S (mdr_z_nonzero_value_yesevaluationdeterminanthr) = S ((S (mdr_i_nonzero_value_yesevaluationdeterminanth)) * mdr_c_nonzero_value_yesevaluationdeterminant)) /\ exists ff_q_mdr_nonzero_value_yesevaluationdeterminanthrb. mdr_b_nonzero_value_yesevaluationdeterminant = ff_q_mdr_nonzero_value_yesevaluationdeterminanthrb * S ((S (mdr_i_nonzero_value_yesevaluationdeterminanth)) * mdr_c_nonzero_value_yesevaluationdeterminant) + (mdr_z_nonzero_value_yesevaluationdeterminanthr))))) /\ (((((mdr_d_nonzero_value_yesevaluationdeterminanth) = 0) /\ (((mdr_p_nonzero_value_yesevaluationdeterminanth) = 1) /\ ((mdr_n_nonzero_value_yesevaluationdeterminanth) = 0))) \/ exists mdr_q_nonzero_value_yesevaluationdeterminanths mdr_eb_nonzero_value_yesevaluationdeterminanths mdr_ec_nonzero_value_yesevaluationdeterminanths mdr_fb_nonzero_value_yesevaluationdeterminanths mdr_fc_nonzero_value_yesevaluationdeterminanths. (((mdr_d_nonzero_value_yesevaluationdeterminanth) = S (mdr_q_nonzero_value_yesevaluationdeterminanths)) /\ ((forall mdr_j_nonzero_value_yesevaluationdeterminanthsc. (exists mdr_gap_nonzero_value_yesevaluationdeterminanthscj. mdr_gap_nonzero_value_yesevaluationdeterminanthscj + S (mdr_j_nonzero_value_yesevaluationdeterminanthsc) = (S (mdr_q_nonzero_value_yesevaluationdeterminanths))) -> exists mdr_i_nonzero_value_yesevaluationdeterminanthsc mdr_up_nonzero_value_yesevaluationdeterminanthsc mdr_us_nonzero_value_yesevaluationdeterminanthsc mdr_un_nonzero_value_yesevaluationdeterminanthsc mdr_ut_nonzero_value_yesevaluationdeterminanthsc mdr_p_nonzero_value_yesevaluationdeterminanthsc mdr_n_nonzero_value_yesevaluationdeterminanthsc. ((exists mdr_gap_nonzero_value_yesevaluationdeterminanthsci. mdr_gap_nonzero_value_yesevaluationdeterminanthsci + S (mdr_i_nonzero_value_yesevaluationdeterminanthsc) = (mdr_i_nonzero_value_yesevaluationdeterminanth)) /\ ((exists mdr_z_nonzero_value_yesevaluationdeterminanthscr. ((exists mdr_a_nonzero_value_yesevaluationdeterminanthscrc mdr_b_nonzero_value_yesevaluationdeterminanthscrc mdr_c_nonzero_value_yesevaluationdeterminanthscrc mdr_e_nonzero_value_yesevaluationdeterminanthscrc mdr_f_nonzero_value_yesevaluationdeterminanthscrc. ((mdr_a_nonzero_value_yesevaluationdeterminanthscrc = ((mdr_q_nonzero_value_yesevaluationdeterminanths) + (mdr_up_nonzero_value_yesevaluationdeterminanthsc)) * S ((mdr_q_nonzero_value_yesevaluationdeterminanths) + (mdr_up_nonzero_value_yesevaluationdeterminanthsc)) + ((mdr_up_nonzero_value_yesevaluationdeterminanthsc) + (mdr_up_nonzero_value_yesevaluationdeterminanthsc))) /\ ((mdr_b_nonzero_value_yesevaluationdeterminanthscrc = ((mdr_us_nonzero_value_yesevaluationdeterminanthsc) + (mdr_un_nonzero_value_yesevaluationdeterminanthsc)) * S ((mdr_us_nonzero_value_yesevaluationdeterminanthsc) + (mdr_un_nonzero_value_yesevaluationdeterminanthsc)) + ((mdr_un_nonzero_value_yesevaluationdeterminanthsc) + (mdr_un_nonzero_value_yesevaluationdeterminanthsc))) /\ ((mdr_c_nonzero_value_yesevaluationdeterminanthscrc = ((mdr_a_nonzero_value_yesevaluationdeterminanthscrc) + (mdr_b_nonzero_value_yesevaluationdeterminanthscrc)) * S ((mdr_a_nonzero_value_yesevaluationdeterminanthscrc) + (mdr_b_nonzero_value_yesevaluationdeterminanthscrc)) + ((mdr_b_nonzero_value_yesevaluationdeterminanthscrc) + (mdr_b_nonzero_value_yesevaluationdeterminanthscrc))) /\ ((mdr_e_nonzero_value_yesevaluationdeterminanthscrc = ((mdr_p_nonzero_value_yesevaluationdeterminanthsc) + (mdr_n_nonzero_value_yesevaluationdeterminanthsc)) * S ((mdr_p_nonzero_value_yesevaluationdeterminanthsc) + (mdr_n_nonzero_value_yesevaluationdeterminanthsc)) + ((mdr_n_nonzero_value_yesevaluationdeterminanthsc) + (mdr_n_nonzero_value_yesevaluationdeterminanthsc))) /\ ((mdr_f_nonzero_value_yesevaluationdeterminanthscrc = ((mdr_ut_nonzero_value_yesevaluationdeterminanthsc) + (mdr_e_nonzero_value_yesevaluationdeterminanthscrc)) * S ((mdr_ut_nonzero_value_yesevaluationdeterminanthsc) + (mdr_e_nonzero_value_yesevaluationdeterminanthscrc)) + ((mdr_e_nonzero_value_yesevaluationdeterminanthscrc) + (mdr_e_nonzero_value_yesevaluationdeterminanthscrc))) /\ ((mdr_z_nonzero_value_yesevaluationdeterminanthscr) = ((mdr_c_nonzero_value_yesevaluationdeterminanthscrc) + (mdr_f_nonzero_value_yesevaluationdeterminanthscrc)) * S ((mdr_c_nonzero_value_yesevaluationdeterminanthscrc) + (mdr_f_nonzero_value_yesevaluationdeterminanthscrc)) + ((mdr_f_nonzero_value_yesevaluationdeterminanthscrc) + (mdr_f_nonzero_value_yesevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_nonzero_value_yesevaluationdeterminanthscrb. ff_h_mdr_nonzero_value_yesevaluationdeterminanthscrb + S (mdr_z_nonzero_value_yesevaluationdeterminanthscr) = S ((S (mdr_i_nonzero_value_yesevaluationdeterminanthsc)) * mdr_c_nonzero_value_yesevaluationdeterminant)) /\ exists ff_q_mdr_nonzero_value_yesevaluationdeterminanthscrb. mdr_b_nonzero_value_yesevaluationdeterminant = ff_q_mdr_nonzero_value_yesevaluationdeterminanthscrb * S ((S (mdr_i_nonzero_value_yesevaluationdeterminanthsc)) * mdr_c_nonzero_value_yesevaluationdeterminant) + (mdr_z_nonzero_value_yesevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_positive) = ((mdr_q_nonzero_value_yesevaluationdeterminanths) * (mdr_q_nonzero_value_yesevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_positive = (mdr_q_nonzero_value_yesevaluationdeterminanths) * ff_row_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_positive) = (mdr_q_nonzero_value_yesevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_positive) = (mdr_j_nonzero_value_yesevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_nonzero_value_yesevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_cell) * (S (mdr_q_nonzero_value_yesevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_cell))) * mdr_pc_nonzero_value_yesevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_cell_source. mdr_pb_nonzero_value_yesevaluationdeterminanth = ff_q_mdm_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_cell) * (S (mdr_q_nonzero_value_yesevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_cell))) * mdr_pc_nonzero_value_yesevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_positive)) * mdr_us_nonzero_value_yesevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_target. mdr_up_nonzero_value_yesevaluationdeterminanthsc = ff_q_mdm_mdr_nonzero_value_yesevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_positive)) * mdr_us_nonzero_value_yesevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_negative) = ((mdr_q_nonzero_value_yesevaluationdeterminanths) * (mdr_q_nonzero_value_yesevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_negative = (mdr_q_nonzero_value_yesevaluationdeterminanths) * ff_row_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_negative) = (mdr_q_nonzero_value_yesevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_negative) = (mdr_j_nonzero_value_yesevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_nonzero_value_yesevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_cell) * (S (mdr_q_nonzero_value_yesevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_cell))) * mdr_nc_nonzero_value_yesevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_cell_source. mdr_nb_nonzero_value_yesevaluationdeterminanth = ff_q_mdm_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_cell) * (S (mdr_q_nonzero_value_yesevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_cell))) * mdr_nc_nonzero_value_yesevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_negative)) * mdr_ut_nonzero_value_yesevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_target. mdr_un_nonzero_value_yesevaluationdeterminanthsc = ff_q_mdm_mdr_nonzero_value_yesevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_negative)) * mdr_ut_nonzero_value_yesevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_nonzero_value_yesevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_nonzero_value_yesevaluationdeterminanthscp. ff_h_mdr_nonzero_value_yesevaluationdeterminanthscp + S (mdr_p_nonzero_value_yesevaluationdeterminanthsc) = S ((S (mdr_j_nonzero_value_yesevaluationdeterminanthsc)) * mdr_ec_nonzero_value_yesevaluationdeterminanths)) /\ exists ff_q_mdr_nonzero_value_yesevaluationdeterminanthscp. mdr_eb_nonzero_value_yesevaluationdeterminanths = ff_q_mdr_nonzero_value_yesevaluationdeterminanthscp * S ((S (mdr_j_nonzero_value_yesevaluationdeterminanthsc)) * mdr_ec_nonzero_value_yesevaluationdeterminanths) + (mdr_p_nonzero_value_yesevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_nonzero_value_yesevaluationdeterminanthscn. ff_h_mdr_nonzero_value_yesevaluationdeterminanthscn + S (mdr_n_nonzero_value_yesevaluationdeterminanthsc) = S ((S (mdr_j_nonzero_value_yesevaluationdeterminanthsc)) * mdr_fc_nonzero_value_yesevaluationdeterminanths)) /\ exists ff_q_mdr_nonzero_value_yesevaluationdeterminanthscn. mdr_fb_nonzero_value_yesevaluationdeterminanths = ff_q_mdr_nonzero_value_yesevaluationdeterminanthscn * S ((S (mdr_j_nonzero_value_yesevaluationdeterminanthsc)) * mdr_fc_nonzero_value_yesevaluationdeterminanths) + (mdr_n_nonzero_value_yesevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_nonzero_value_yesevaluationdeterminanthsf ff_uc_mce_fold_mdr_nonzero_value_yesevaluationdeterminanthsf ff_vb_mce_fold_mdr_nonzero_value_yesevaluationdeterminanthsf ff_vc_mce_fold_mdr_nonzero_value_yesevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix) = (S (mdr_q_nonzero_value_yesevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix)) * mdr_pc_nonzero_value_yesevaluationdeterminanth)) /\ exists ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_ap. mdr_pb_nonzero_value_yesevaluationdeterminanth = ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix)) * mdr_pc_nonzero_value_yesevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix)) * mdr_nc_nonzero_value_yesevaluationdeterminanth)) /\ exists ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_an. mdr_nb_nonzero_value_yesevaluationdeterminanth = ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix)) * mdr_nc_nonzero_value_yesevaluationdeterminanth) + (ff_an_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix)) * mdr_ec_nonzero_value_yesevaluationdeterminanths)) /\ exists ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_bp. mdr_eb_nonzero_value_yesevaluationdeterminanths = ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix)) * mdr_ec_nonzero_value_yesevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix)) * mdr_fc_nonzero_value_yesevaluationdeterminanths)) /\ exists ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_bn. mdr_fb_nonzero_value_yesevaluationdeterminanths = ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix)) * mdr_fc_nonzero_value_yesevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_nonzero_value_yesevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_nonzero_value_yesevaluationdeterminanthsf = ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_nonzero_value_yesevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_nonzero_value_yesevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_nonzero_value_yesevaluationdeterminanthsf = ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_nonzero_value_yesevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_nonzero_value_yesevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive ff_v_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive = ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive_terminal + S (mdr_p_nonzero_value_yesevaluationdeterminanth) = S ((S ((S (mdr_q_nonzero_value_yesevaluationdeterminanths)))) * ff_v_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive = ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_nonzero_value_yesevaluationdeterminanths)))) * ff_v_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive) + (mdr_p_nonzero_value_yesevaluationdeterminanth))) /\ forall ff_i_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive = (S (mdr_q_nonzero_value_yesevaluationdeterminanths))) -> exists ff_a_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive ff_r_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive ff_s_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_nonzero_value_yesevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_nonzero_value_yesevaluationdeterminanthsf = ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_nonzero_value_yesevaluationdeterminanthsf) + (ff_a_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive = ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive = ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive = ff_r_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive + ff_a_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative ff_v_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative = ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative_terminal + S (mdr_n_nonzero_value_yesevaluationdeterminanth) = S ((S ((S (mdr_q_nonzero_value_yesevaluationdeterminanths)))) * ff_v_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative = ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_nonzero_value_yesevaluationdeterminanths)))) * ff_v_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative) + (mdr_n_nonzero_value_yesevaluationdeterminanth))) /\ forall ff_i_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative = (S (mdr_q_nonzero_value_yesevaluationdeterminanths))) -> exists ff_a_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative ff_r_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative ff_s_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_nonzero_value_yesevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_nonzero_value_yesevaluationdeterminanthsf = ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_nonzero_value_yesevaluationdeterminanthsf) + (ff_a_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative = ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative = ff_q_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative = ff_r_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative + ff_a_mce_mdr_nonzero_value_yesevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_nonzero_value_yesevaluationdeterminanti. mdr_gap_nonzero_value_yesevaluationdeterminanti + S (mdr_i_nonzero_value_yesevaluationdeterminant) = (mdr_l_nonzero_value_yesevaluationdeterminant)) /\ (exists mdr_z_nonzero_value_yesevaluationdeterminantr. ((exists mdr_a_nonzero_value_yesevaluationdeterminantrc mdr_b_nonzero_value_yesevaluationdeterminantrc mdr_c_nonzero_value_yesevaluationdeterminantrc mdr_e_nonzero_value_yesevaluationdeterminantrc mdr_f_nonzero_value_yesevaluationdeterminantrc. ((mdr_a_nonzero_value_yesevaluationdeterminantrc = ((q) + (mdr_ub_nonzero_value_yesevaluation)) * S ((q) + (mdr_ub_nonzero_value_yesevaluation)) + ((mdr_ub_nonzero_value_yesevaluation) + (mdr_ub_nonzero_value_yesevaluation))) /\ ((mdr_b_nonzero_value_yesevaluationdeterminantrc = ((mdr_uc_nonzero_value_yesevaluation) + (mdr_vb_nonzero_value_yesevaluation)) * S ((mdr_uc_nonzero_value_yesevaluation) + (mdr_vb_nonzero_value_yesevaluation)) + ((mdr_vb_nonzero_value_yesevaluation) + (mdr_vb_nonzero_value_yesevaluation))) /\ ((mdr_c_nonzero_value_yesevaluationdeterminantrc = ((mdr_a_nonzero_value_yesevaluationdeterminantrc) + (mdr_b_nonzero_value_yesevaluationdeterminantrc)) * S ((mdr_a_nonzero_value_yesevaluationdeterminantrc) + (mdr_b_nonzero_value_yesevaluationdeterminantrc)) + ((mdr_b_nonzero_value_yesevaluationdeterminantrc) + (mdr_b_nonzero_value_yesevaluationdeterminantrc))) /\ ((mdr_e_nonzero_value_yesevaluationdeterminantrc = ((mdr_p_nonzero_value_yes) + (mdr_n_nonzero_value_yes)) * S ((mdr_p_nonzero_value_yes) + (mdr_n_nonzero_value_yes)) + ((mdr_n_nonzero_value_yes) + (mdr_n_nonzero_value_yes))) /\ ((mdr_f_nonzero_value_yesevaluationdeterminantrc = ((mdr_vc_nonzero_value_yesevaluation) + (mdr_e_nonzero_value_yesevaluationdeterminantrc)) * S ((mdr_vc_nonzero_value_yesevaluation) + (mdr_e_nonzero_value_yesevaluationdeterminantrc)) + ((mdr_e_nonzero_value_yesevaluationdeterminantrc) + (mdr_e_nonzero_value_yesevaluationdeterminantrc))) /\ ((mdr_z_nonzero_value_yesevaluationdeterminantr) = ((mdr_c_nonzero_value_yesevaluationdeterminantrc) + (mdr_f_nonzero_value_yesevaluationdeterminantrc)) * S ((mdr_c_nonzero_value_yesevaluationdeterminantrc) + (mdr_f_nonzero_value_yesevaluationdeterminantrc)) + ((mdr_f_nonzero_value_yesevaluationdeterminantrc) + (mdr_f_nonzero_value_yesevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_nonzero_value_yesevaluationdeterminantrb. ff_h_mdr_nonzero_value_yesevaluationdeterminantrb + S (mdr_z_nonzero_value_yesevaluationdeterminantr) = S ((S (mdr_i_nonzero_value_yesevaluationdeterminant)) * mdr_c_nonzero_value_yesevaluationdeterminant)) /\ exists ff_q_mdr_nonzero_value_yesevaluationdeterminantrb. mdr_b_nonzero_value_yesevaluationdeterminant = ff_q_mdr_nonzero_value_yesevaluationdeterminantrb * S ((S (mdr_i_nonzero_value_yesevaluationdeterminant)) * mdr_c_nonzero_value_yesevaluationdeterminant) + (mdr_z_nonzero_value_yesevaluationdeterminantr)))))))))) /\ (~(mdr_p_nonzero_value_yes = mdr_n_nonzero_value_yes)))) \/ ~(exists mdr_p_nonzero_value_no mdr_n_nonzero_value_no. ((exists mdr_ub_nonzero_value_noevaluation mdr_uc_nonzero_value_noevaluation mdr_vb_nonzero_value_noevaluation mdr_vc_nonzero_value_noevaluation. ((((forall mdr_i_nonzero_value_noevaluationmatrixpositive. (exists mdr_gap_nonzero_value_noevaluationmatrixpositivebound. mdr_gap_nonzero_value_noevaluationmatrixpositivebound + S (mdr_i_nonzero_value_noevaluationmatrixpositive) = ((q) * (q))) -> exists mdr_a_nonzero_value_noevaluationmatrixpositive. (((exists mdr_r_nonzero_value_noevaluationmatrixpositivepoint mdr_s_nonzero_value_noevaluationmatrixpositivepoint mdr_u_nonzero_value_noevaluationmatrixpositivepoint mdr_v_nonzero_value_noevaluationmatrixpositivepoint. ((mdr_i_nonzero_value_noevaluationmatrixpositive = (q) * mdr_r_nonzero_value_noevaluationmatrixpositivepoint + mdr_s_nonzero_value_noevaluationmatrixpositivepoint) /\ ((exists mdr_gap_nonzero_value_noevaluationmatrixpositivepointcolumn. mdr_gap_nonzero_value_noevaluationmatrixpositivepointcolumn + S (mdr_s_nonzero_value_noevaluationmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_nonzero_value_noevaluationmatrixpositivepointrow_index. ff_h_mdr_nonzero_value_noevaluationmatrixpositivepointrow_index + S (mdr_u_nonzero_value_noevaluationmatrixpositivepoint) = S ((S (mdr_r_nonzero_value_noevaluationmatrixpositivepoint)) * rc)) /\ exists ff_q_mdr_nonzero_value_noevaluationmatrixpositivepointrow_index. rb = ff_q_mdr_nonzero_value_noevaluationmatrixpositivepointrow_index * S ((S (mdr_r_nonzero_value_noevaluationmatrixpositivepoint)) * rc) + (mdr_u_nonzero_value_noevaluationmatrixpositivepoint))) /\ ((((exists ff_h_mdr_nonzero_value_noevaluationmatrixpositivepointcolumn_index. ff_h_mdr_nonzero_value_noevaluationmatrixpositivepointcolumn_index + S (mdr_v_nonzero_value_noevaluationmatrixpositivepoint) = S ((S (mdr_s_nonzero_value_noevaluationmatrixpositivepoint)) * cc)) /\ exists ff_q_mdr_nonzero_value_noevaluationmatrixpositivepointcolumn_index. cb = ff_q_mdr_nonzero_value_noevaluationmatrixpositivepointcolumn_index * S ((S (mdr_s_nonzero_value_noevaluationmatrixpositivepoint)) * cc) + (mdr_v_nonzero_value_noevaluationmatrixpositivepoint))) /\ (((exists ff_h_mdr_nonzero_value_noevaluationmatrixpositivepointsource. ff_h_mdr_nonzero_value_noevaluationmatrixpositivepointsource + S (mdr_a_nonzero_value_noevaluationmatrixpositive) = S ((S ((mdr_u_nonzero_value_noevaluationmatrixpositivepoint) * (w) + (mdr_v_nonzero_value_noevaluationmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_nonzero_value_noevaluationmatrixpositivepointsource. pb = ff_q_mdr_nonzero_value_noevaluationmatrixpositivepointsource * S ((S ((mdr_u_nonzero_value_noevaluationmatrixpositivepoint) * (w) + (mdr_v_nonzero_value_noevaluationmatrixpositivepoint))) * pc) + (mdr_a_nonzero_value_noevaluationmatrixpositive)))))))) /\ (((exists ff_h_mdr_nonzero_value_noevaluationmatrixpositiveoutput. ff_h_mdr_nonzero_value_noevaluationmatrixpositiveoutput + S (mdr_a_nonzero_value_noevaluationmatrixpositive) = S ((S (mdr_i_nonzero_value_noevaluationmatrixpositive)) * mdr_uc_nonzero_value_noevaluation)) /\ exists ff_q_mdr_nonzero_value_noevaluationmatrixpositiveoutput. mdr_ub_nonzero_value_noevaluation = ff_q_mdr_nonzero_value_noevaluationmatrixpositiveoutput * S ((S (mdr_i_nonzero_value_noevaluationmatrixpositive)) * mdr_uc_nonzero_value_noevaluation) + (mdr_a_nonzero_value_noevaluationmatrixpositive)))))) /\ (forall mdr_i_nonzero_value_noevaluationmatrixnegative. (exists mdr_gap_nonzero_value_noevaluationmatrixnegativebound. mdr_gap_nonzero_value_noevaluationmatrixnegativebound + S (mdr_i_nonzero_value_noevaluationmatrixnegative) = ((q) * (q))) -> exists mdr_a_nonzero_value_noevaluationmatrixnegative. (((exists mdr_r_nonzero_value_noevaluationmatrixnegativepoint mdr_s_nonzero_value_noevaluationmatrixnegativepoint mdr_u_nonzero_value_noevaluationmatrixnegativepoint mdr_v_nonzero_value_noevaluationmatrixnegativepoint. ((mdr_i_nonzero_value_noevaluationmatrixnegative = (q) * mdr_r_nonzero_value_noevaluationmatrixnegativepoint + mdr_s_nonzero_value_noevaluationmatrixnegativepoint) /\ ((exists mdr_gap_nonzero_value_noevaluationmatrixnegativepointcolumn. mdr_gap_nonzero_value_noevaluationmatrixnegativepointcolumn + S (mdr_s_nonzero_value_noevaluationmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_nonzero_value_noevaluationmatrixnegativepointrow_index. ff_h_mdr_nonzero_value_noevaluationmatrixnegativepointrow_index + S (mdr_u_nonzero_value_noevaluationmatrixnegativepoint) = S ((S (mdr_r_nonzero_value_noevaluationmatrixnegativepoint)) * rc)) /\ exists ff_q_mdr_nonzero_value_noevaluationmatrixnegativepointrow_index. rb = ff_q_mdr_nonzero_value_noevaluationmatrixnegativepointrow_index * S ((S (mdr_r_nonzero_value_noevaluationmatrixnegativepoint)) * rc) + (mdr_u_nonzero_value_noevaluationmatrixnegativepoint))) /\ ((((exists ff_h_mdr_nonzero_value_noevaluationmatrixnegativepointcolumn_index. ff_h_mdr_nonzero_value_noevaluationmatrixnegativepointcolumn_index + S (mdr_v_nonzero_value_noevaluationmatrixnegativepoint) = S ((S (mdr_s_nonzero_value_noevaluationmatrixnegativepoint)) * cc)) /\ exists ff_q_mdr_nonzero_value_noevaluationmatrixnegativepointcolumn_index. cb = ff_q_mdr_nonzero_value_noevaluationmatrixnegativepointcolumn_index * S ((S (mdr_s_nonzero_value_noevaluationmatrixnegativepoint)) * cc) + (mdr_v_nonzero_value_noevaluationmatrixnegativepoint))) /\ (((exists ff_h_mdr_nonzero_value_noevaluationmatrixnegativepointsource. ff_h_mdr_nonzero_value_noevaluationmatrixnegativepointsource + S (mdr_a_nonzero_value_noevaluationmatrixnegative) = S ((S ((mdr_u_nonzero_value_noevaluationmatrixnegativepoint) * (w) + (mdr_v_nonzero_value_noevaluationmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_nonzero_value_noevaluationmatrixnegativepointsource. nb = ff_q_mdr_nonzero_value_noevaluationmatrixnegativepointsource * S ((S ((mdr_u_nonzero_value_noevaluationmatrixnegativepoint) * (w) + (mdr_v_nonzero_value_noevaluationmatrixnegativepoint))) * nc) + (mdr_a_nonzero_value_noevaluationmatrixnegative)))))))) /\ (((exists ff_h_mdr_nonzero_value_noevaluationmatrixnegativeoutput. ff_h_mdr_nonzero_value_noevaluationmatrixnegativeoutput + S (mdr_a_nonzero_value_noevaluationmatrixnegative) = S ((S (mdr_i_nonzero_value_noevaluationmatrixnegative)) * mdr_vc_nonzero_value_noevaluation)) /\ exists ff_q_mdr_nonzero_value_noevaluationmatrixnegativeoutput. mdr_vb_nonzero_value_noevaluation = ff_q_mdr_nonzero_value_noevaluationmatrixnegativeoutput * S ((S (mdr_i_nonzero_value_noevaluationmatrixnegative)) * mdr_vc_nonzero_value_noevaluation) + (mdr_a_nonzero_value_noevaluationmatrixnegative)))))))) /\ (exists mdr_b_nonzero_value_noevaluationdeterminant mdr_c_nonzero_value_noevaluationdeterminant mdr_l_nonzero_value_noevaluationdeterminant mdr_i_nonzero_value_noevaluationdeterminant. ((forall mdr_i_nonzero_value_noevaluationdeterminanth. (exists mdr_gap_nonzero_value_noevaluationdeterminanthi. mdr_gap_nonzero_value_noevaluationdeterminanthi + S (mdr_i_nonzero_value_noevaluationdeterminanth) = (mdr_l_nonzero_value_noevaluationdeterminant)) -> exists mdr_d_nonzero_value_noevaluationdeterminanth mdr_pb_nonzero_value_noevaluationdeterminanth mdr_pc_nonzero_value_noevaluationdeterminanth mdr_nb_nonzero_value_noevaluationdeterminanth mdr_nc_nonzero_value_noevaluationdeterminanth mdr_p_nonzero_value_noevaluationdeterminanth mdr_n_nonzero_value_noevaluationdeterminanth. ((exists mdr_z_nonzero_value_noevaluationdeterminanthr. ((exists mdr_a_nonzero_value_noevaluationdeterminanthrc mdr_b_nonzero_value_noevaluationdeterminanthrc mdr_c_nonzero_value_noevaluationdeterminanthrc mdr_e_nonzero_value_noevaluationdeterminanthrc mdr_f_nonzero_value_noevaluationdeterminanthrc. ((mdr_a_nonzero_value_noevaluationdeterminanthrc = ((mdr_d_nonzero_value_noevaluationdeterminanth) + (mdr_pb_nonzero_value_noevaluationdeterminanth)) * S ((mdr_d_nonzero_value_noevaluationdeterminanth) + (mdr_pb_nonzero_value_noevaluationdeterminanth)) + ((mdr_pb_nonzero_value_noevaluationdeterminanth) + (mdr_pb_nonzero_value_noevaluationdeterminanth))) /\ ((mdr_b_nonzero_value_noevaluationdeterminanthrc = ((mdr_pc_nonzero_value_noevaluationdeterminanth) + (mdr_nb_nonzero_value_noevaluationdeterminanth)) * S ((mdr_pc_nonzero_value_noevaluationdeterminanth) + (mdr_nb_nonzero_value_noevaluationdeterminanth)) + ((mdr_nb_nonzero_value_noevaluationdeterminanth) + (mdr_nb_nonzero_value_noevaluationdeterminanth))) /\ ((mdr_c_nonzero_value_noevaluationdeterminanthrc = ((mdr_a_nonzero_value_noevaluationdeterminanthrc) + (mdr_b_nonzero_value_noevaluationdeterminanthrc)) * S ((mdr_a_nonzero_value_noevaluationdeterminanthrc) + (mdr_b_nonzero_value_noevaluationdeterminanthrc)) + ((mdr_b_nonzero_value_noevaluationdeterminanthrc) + (mdr_b_nonzero_value_noevaluationdeterminanthrc))) /\ ((mdr_e_nonzero_value_noevaluationdeterminanthrc = ((mdr_p_nonzero_value_noevaluationdeterminanth) + (mdr_n_nonzero_value_noevaluationdeterminanth)) * S ((mdr_p_nonzero_value_noevaluationdeterminanth) + (mdr_n_nonzero_value_noevaluationdeterminanth)) + ((mdr_n_nonzero_value_noevaluationdeterminanth) + (mdr_n_nonzero_value_noevaluationdeterminanth))) /\ ((mdr_f_nonzero_value_noevaluationdeterminanthrc = ((mdr_nc_nonzero_value_noevaluationdeterminanth) + (mdr_e_nonzero_value_noevaluationdeterminanthrc)) * S ((mdr_nc_nonzero_value_noevaluationdeterminanth) + (mdr_e_nonzero_value_noevaluationdeterminanthrc)) + ((mdr_e_nonzero_value_noevaluationdeterminanthrc) + (mdr_e_nonzero_value_noevaluationdeterminanthrc))) /\ ((mdr_z_nonzero_value_noevaluationdeterminanthr) = ((mdr_c_nonzero_value_noevaluationdeterminanthrc) + (mdr_f_nonzero_value_noevaluationdeterminanthrc)) * S ((mdr_c_nonzero_value_noevaluationdeterminanthrc) + (mdr_f_nonzero_value_noevaluationdeterminanthrc)) + ((mdr_f_nonzero_value_noevaluationdeterminanthrc) + (mdr_f_nonzero_value_noevaluationdeterminanthrc))))))))) /\ (((exists ff_h_mdr_nonzero_value_noevaluationdeterminanthrb. ff_h_mdr_nonzero_value_noevaluationdeterminanthrb + S (mdr_z_nonzero_value_noevaluationdeterminanthr) = S ((S (mdr_i_nonzero_value_noevaluationdeterminanth)) * mdr_c_nonzero_value_noevaluationdeterminant)) /\ exists ff_q_mdr_nonzero_value_noevaluationdeterminanthrb. mdr_b_nonzero_value_noevaluationdeterminant = ff_q_mdr_nonzero_value_noevaluationdeterminanthrb * S ((S (mdr_i_nonzero_value_noevaluationdeterminanth)) * mdr_c_nonzero_value_noevaluationdeterminant) + (mdr_z_nonzero_value_noevaluationdeterminanthr))))) /\ (((((mdr_d_nonzero_value_noevaluationdeterminanth) = 0) /\ (((mdr_p_nonzero_value_noevaluationdeterminanth) = 1) /\ ((mdr_n_nonzero_value_noevaluationdeterminanth) = 0))) \/ exists mdr_q_nonzero_value_noevaluationdeterminanths mdr_eb_nonzero_value_noevaluationdeterminanths mdr_ec_nonzero_value_noevaluationdeterminanths mdr_fb_nonzero_value_noevaluationdeterminanths mdr_fc_nonzero_value_noevaluationdeterminanths. (((mdr_d_nonzero_value_noevaluationdeterminanth) = S (mdr_q_nonzero_value_noevaluationdeterminanths)) /\ ((forall mdr_j_nonzero_value_noevaluationdeterminanthsc. (exists mdr_gap_nonzero_value_noevaluationdeterminanthscj. mdr_gap_nonzero_value_noevaluationdeterminanthscj + S (mdr_j_nonzero_value_noevaluationdeterminanthsc) = (S (mdr_q_nonzero_value_noevaluationdeterminanths))) -> exists mdr_i_nonzero_value_noevaluationdeterminanthsc mdr_up_nonzero_value_noevaluationdeterminanthsc mdr_us_nonzero_value_noevaluationdeterminanthsc mdr_un_nonzero_value_noevaluationdeterminanthsc mdr_ut_nonzero_value_noevaluationdeterminanthsc mdr_p_nonzero_value_noevaluationdeterminanthsc mdr_n_nonzero_value_noevaluationdeterminanthsc. ((exists mdr_gap_nonzero_value_noevaluationdeterminanthsci. mdr_gap_nonzero_value_noevaluationdeterminanthsci + S (mdr_i_nonzero_value_noevaluationdeterminanthsc) = (mdr_i_nonzero_value_noevaluationdeterminanth)) /\ ((exists mdr_z_nonzero_value_noevaluationdeterminanthscr. ((exists mdr_a_nonzero_value_noevaluationdeterminanthscrc mdr_b_nonzero_value_noevaluationdeterminanthscrc mdr_c_nonzero_value_noevaluationdeterminanthscrc mdr_e_nonzero_value_noevaluationdeterminanthscrc mdr_f_nonzero_value_noevaluationdeterminanthscrc. ((mdr_a_nonzero_value_noevaluationdeterminanthscrc = ((mdr_q_nonzero_value_noevaluationdeterminanths) + (mdr_up_nonzero_value_noevaluationdeterminanthsc)) * S ((mdr_q_nonzero_value_noevaluationdeterminanths) + (mdr_up_nonzero_value_noevaluationdeterminanthsc)) + ((mdr_up_nonzero_value_noevaluationdeterminanthsc) + (mdr_up_nonzero_value_noevaluationdeterminanthsc))) /\ ((mdr_b_nonzero_value_noevaluationdeterminanthscrc = ((mdr_us_nonzero_value_noevaluationdeterminanthsc) + (mdr_un_nonzero_value_noevaluationdeterminanthsc)) * S ((mdr_us_nonzero_value_noevaluationdeterminanthsc) + (mdr_un_nonzero_value_noevaluationdeterminanthsc)) + ((mdr_un_nonzero_value_noevaluationdeterminanthsc) + (mdr_un_nonzero_value_noevaluationdeterminanthsc))) /\ ((mdr_c_nonzero_value_noevaluationdeterminanthscrc = ((mdr_a_nonzero_value_noevaluationdeterminanthscrc) + (mdr_b_nonzero_value_noevaluationdeterminanthscrc)) * S ((mdr_a_nonzero_value_noevaluationdeterminanthscrc) + (mdr_b_nonzero_value_noevaluationdeterminanthscrc)) + ((mdr_b_nonzero_value_noevaluationdeterminanthscrc) + (mdr_b_nonzero_value_noevaluationdeterminanthscrc))) /\ ((mdr_e_nonzero_value_noevaluationdeterminanthscrc = ((mdr_p_nonzero_value_noevaluationdeterminanthsc) + (mdr_n_nonzero_value_noevaluationdeterminanthsc)) * S ((mdr_p_nonzero_value_noevaluationdeterminanthsc) + (mdr_n_nonzero_value_noevaluationdeterminanthsc)) + ((mdr_n_nonzero_value_noevaluationdeterminanthsc) + (mdr_n_nonzero_value_noevaluationdeterminanthsc))) /\ ((mdr_f_nonzero_value_noevaluationdeterminanthscrc = ((mdr_ut_nonzero_value_noevaluationdeterminanthsc) + (mdr_e_nonzero_value_noevaluationdeterminanthscrc)) * S ((mdr_ut_nonzero_value_noevaluationdeterminanthsc) + (mdr_e_nonzero_value_noevaluationdeterminanthscrc)) + ((mdr_e_nonzero_value_noevaluationdeterminanthscrc) + (mdr_e_nonzero_value_noevaluationdeterminanthscrc))) /\ ((mdr_z_nonzero_value_noevaluationdeterminanthscr) = ((mdr_c_nonzero_value_noevaluationdeterminanthscrc) + (mdr_f_nonzero_value_noevaluationdeterminanthscrc)) * S ((mdr_c_nonzero_value_noevaluationdeterminanthscrc) + (mdr_f_nonzero_value_noevaluationdeterminanthscrc)) + ((mdr_f_nonzero_value_noevaluationdeterminanthscrc) + (mdr_f_nonzero_value_noevaluationdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_nonzero_value_noevaluationdeterminanthscrb. ff_h_mdr_nonzero_value_noevaluationdeterminanthscrb + S (mdr_z_nonzero_value_noevaluationdeterminanthscr) = S ((S (mdr_i_nonzero_value_noevaluationdeterminanthsc)) * mdr_c_nonzero_value_noevaluationdeterminant)) /\ exists ff_q_mdr_nonzero_value_noevaluationdeterminanthscrb. mdr_b_nonzero_value_noevaluationdeterminant = ff_q_mdr_nonzero_value_noevaluationdeterminanthscrb * S ((S (mdr_i_nonzero_value_noevaluationdeterminanthsc)) * mdr_c_nonzero_value_noevaluationdeterminant) + (mdr_z_nonzero_value_noevaluationdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_nonzero_value_noevaluationdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_nonzero_value_noevaluationdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_positive) = ((mdr_q_nonzero_value_noevaluationdeterminanths) * (mdr_q_nonzero_value_noevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_positive ff_column_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_positive ff_value_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_positive = (mdr_q_nonzero_value_noevaluationdeterminanths) * ff_row_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_positive + ff_column_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_nonzero_value_noevaluationdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_nonzero_value_noevaluationdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_positive) = (mdr_q_nonzero_value_noevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_nonzero_value_noevaluationdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_nonzero_value_noevaluationdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_nonzero_value_noevaluationdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_nonzero_value_noevaluationdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_nonzero_value_noevaluationdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_nonzero_value_noevaluationdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_nonzero_value_noevaluationdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_nonzero_value_noevaluationdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_nonzero_value_noevaluationdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_nonzero_value_noevaluationdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_positive) = (mdr_j_nonzero_value_noevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_nonzero_value_noevaluationdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_nonzero_value_noevaluationdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_nonzero_value_noevaluationdeterminanthscm_positive_cell_column_after + (mdr_j_nonzero_value_noevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_nonzero_value_noevaluationdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_nonzero_value_noevaluationdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_nonzero_value_noevaluationdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_nonzero_value_noevaluationdeterminanthscm_positive_cell) * (S (mdr_q_nonzero_value_noevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_nonzero_value_noevaluationdeterminanthscm_positive_cell))) * mdr_pc_nonzero_value_noevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_nonzero_value_noevaluationdeterminanthscm_positive_cell_source. mdr_pb_nonzero_value_noevaluationdeterminanth = ff_q_mdm_mdr_nonzero_value_noevaluationdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_nonzero_value_noevaluationdeterminanthscm_positive_cell) * (S (mdr_q_nonzero_value_noevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_nonzero_value_noevaluationdeterminanthscm_positive_cell))) * mdr_pc_nonzero_value_noevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_nonzero_value_noevaluationdeterminanthscm_positive_target. ff_h_mdm_mdr_nonzero_value_noevaluationdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_positive)) * mdr_us_nonzero_value_noevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_nonzero_value_noevaluationdeterminanthscm_positive_target. mdr_up_nonzero_value_noevaluationdeterminanthsc = ff_q_mdm_mdr_nonzero_value_noevaluationdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_positive)) * mdr_us_nonzero_value_noevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_nonzero_value_noevaluationdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_nonzero_value_noevaluationdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_negative) = ((mdr_q_nonzero_value_noevaluationdeterminanths) * (mdr_q_nonzero_value_noevaluationdeterminanths))) -> exists ff_row_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_negative ff_column_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_negative ff_value_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_negative = (mdr_q_nonzero_value_noevaluationdeterminanths) * ff_row_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_negative + ff_column_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_nonzero_value_noevaluationdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_nonzero_value_noevaluationdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_negative) = (mdr_q_nonzero_value_noevaluationdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_nonzero_value_noevaluationdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_nonzero_value_noevaluationdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_nonzero_value_noevaluationdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_nonzero_value_noevaluationdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_nonzero_value_noevaluationdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_nonzero_value_noevaluationdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_nonzero_value_noevaluationdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_nonzero_value_noevaluationdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_nonzero_value_noevaluationdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_nonzero_value_noevaluationdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_negative) = (mdr_j_nonzero_value_noevaluationdeterminanthsc)) /\ ff_column_mdm_cell_mdr_nonzero_value_noevaluationdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_nonzero_value_noevaluationdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_nonzero_value_noevaluationdeterminanthscm_negative_cell_column_after + (mdr_j_nonzero_value_noevaluationdeterminanthsc) = (ff_column_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_nonzero_value_noevaluationdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_nonzero_value_noevaluationdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_nonzero_value_noevaluationdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_nonzero_value_noevaluationdeterminanthscm_negative_cell) * (S (mdr_q_nonzero_value_noevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_nonzero_value_noevaluationdeterminanthscm_negative_cell))) * mdr_nc_nonzero_value_noevaluationdeterminanth)) /\ exists ff_q_mdm_mdr_nonzero_value_noevaluationdeterminanthscm_negative_cell_source. mdr_nb_nonzero_value_noevaluationdeterminanth = ff_q_mdm_mdr_nonzero_value_noevaluationdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_nonzero_value_noevaluationdeterminanthscm_negative_cell) * (S (mdr_q_nonzero_value_noevaluationdeterminanths)) + (ff_column_mdm_cell_mdr_nonzero_value_noevaluationdeterminanthscm_negative_cell))) * mdr_nc_nonzero_value_noevaluationdeterminanth) + (ff_value_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_nonzero_value_noevaluationdeterminanthscm_negative_target. ff_h_mdm_mdr_nonzero_value_noevaluationdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_negative)) * mdr_ut_nonzero_value_noevaluationdeterminanthsc)) /\ exists ff_q_mdm_mdr_nonzero_value_noevaluationdeterminanthscm_negative_target. mdr_un_nonzero_value_noevaluationdeterminanthsc = ff_q_mdm_mdr_nonzero_value_noevaluationdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_negative)) * mdr_ut_nonzero_value_noevaluationdeterminanthsc) + (ff_value_mdm_prefix_mdr_nonzero_value_noevaluationdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_nonzero_value_noevaluationdeterminanthscp. ff_h_mdr_nonzero_value_noevaluationdeterminanthscp + S (mdr_p_nonzero_value_noevaluationdeterminanthsc) = S ((S (mdr_j_nonzero_value_noevaluationdeterminanthsc)) * mdr_ec_nonzero_value_noevaluationdeterminanths)) /\ exists ff_q_mdr_nonzero_value_noevaluationdeterminanthscp. mdr_eb_nonzero_value_noevaluationdeterminanths = ff_q_mdr_nonzero_value_noevaluationdeterminanthscp * S ((S (mdr_j_nonzero_value_noevaluationdeterminanthsc)) * mdr_ec_nonzero_value_noevaluationdeterminanths) + (mdr_p_nonzero_value_noevaluationdeterminanthsc))) /\ (((exists ff_h_mdr_nonzero_value_noevaluationdeterminanthscn. ff_h_mdr_nonzero_value_noevaluationdeterminanthscn + S (mdr_n_nonzero_value_noevaluationdeterminanthsc) = S ((S (mdr_j_nonzero_value_noevaluationdeterminanthsc)) * mdr_fc_nonzero_value_noevaluationdeterminanths)) /\ exists ff_q_mdr_nonzero_value_noevaluationdeterminanthscn. mdr_fb_nonzero_value_noevaluationdeterminanths = ff_q_mdr_nonzero_value_noevaluationdeterminanthscn * S ((S (mdr_j_nonzero_value_noevaluationdeterminanthsc)) * mdr_fc_nonzero_value_noevaluationdeterminanths) + (mdr_n_nonzero_value_noevaluationdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_nonzero_value_noevaluationdeterminanthsf ff_uc_mce_fold_mdr_nonzero_value_noevaluationdeterminanthsf ff_vb_mce_fold_mdr_nonzero_value_noevaluationdeterminanthsf ff_vc_mce_fold_mdr_nonzero_value_noevaluationdeterminanthsf. ((forall ff_index_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix. (exists ff_gap_mce_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_index. ff_gap_mce_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix) = (S (mdr_q_nonzero_value_noevaluationdeterminanths))) -> exists ff_ap_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix ff_an_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix ff_bp_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix ff_bn_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix ff_p_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix ff_n_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_ap. ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix)) * mdr_pc_nonzero_value_noevaluationdeterminanth)) /\ exists ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_ap. mdr_pb_nonzero_value_noevaluationdeterminanth = ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix)) * mdr_pc_nonzero_value_noevaluationdeterminanth) + (ff_ap_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_an. ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix)) * mdr_nc_nonzero_value_noevaluationdeterminanth)) /\ exists ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_an. mdr_nb_nonzero_value_noevaluationdeterminanth = ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix)) * mdr_nc_nonzero_value_noevaluationdeterminanth) + (ff_an_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_bp. ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix)) * mdr_ec_nonzero_value_noevaluationdeterminanths)) /\ exists ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_bp. mdr_eb_nonzero_value_noevaluationdeterminanths = ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix)) * mdr_ec_nonzero_value_noevaluationdeterminanths) + (ff_bp_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_bn. ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix)) * mdr_fc_nonzero_value_noevaluationdeterminanths)) /\ exists ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_bn. mdr_fb_nonzero_value_noevaluationdeterminanths = ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix)) * mdr_fc_nonzero_value_noevaluationdeterminanths) + (ff_bn_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_positive. ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_nonzero_value_noevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_nonzero_value_noevaluationdeterminanthsf = ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_nonzero_value_noevaluationdeterminanthsf) + (ff_p_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_negative. ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_nonzero_value_noevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_nonzero_value_noevaluationdeterminanthsf = ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_nonzero_value_noevaluationdeterminanthsf) + (ff_n_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_nonzero_value_noevaluationdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_nonzero_value_noevaluationdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive ff_v_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive_start. ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive_start. ff_u_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive = ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive_terminal. ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive_terminal + S (mdr_p_nonzero_value_noevaluationdeterminanth) = S ((S ((S (mdr_q_nonzero_value_noevaluationdeterminanths)))) * ff_v_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive_terminal. ff_u_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive = ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_nonzero_value_noevaluationdeterminanths)))) * ff_v_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive) + (mdr_p_nonzero_value_noevaluationdeterminanth))) /\ forall ff_i_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive. (exists ff_lt_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive_bound. ff_lt_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive_bound + S ff_i_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive = (S (mdr_q_nonzero_value_noevaluationdeterminanths))) -> exists ff_a_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive ff_r_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive ff_s_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive. ((((exists ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive_summand. ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive_summand + S (ff_a_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_nonzero_value_noevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_nonzero_value_noevaluationdeterminanthsf = ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_nonzero_value_noevaluationdeterminanthsf) + (ff_a_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive_partial. ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive_partial + S (ff_r_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive_partial. ff_u_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive = ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive) + (ff_r_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive_successor. ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive_successor + S (ff_s_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive_successor. ff_u_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive = ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive)) * ff_v_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive) + (ff_s_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive))) /\ ff_s_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive = ff_r_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive + ff_a_mce_mdr_nonzero_value_noevaluationdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative ff_v_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative_start. ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative_start. ff_u_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative = ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative_terminal. ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative_terminal + S (mdr_n_nonzero_value_noevaluationdeterminanth) = S ((S ((S (mdr_q_nonzero_value_noevaluationdeterminanths)))) * ff_v_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative_terminal. ff_u_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative = ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_nonzero_value_noevaluationdeterminanths)))) * ff_v_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative) + (mdr_n_nonzero_value_noevaluationdeterminanth))) /\ forall ff_i_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative. (exists ff_lt_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative_bound. ff_lt_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative_bound + S ff_i_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative = (S (mdr_q_nonzero_value_noevaluationdeterminanths))) -> exists ff_a_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative ff_r_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative ff_s_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative. ((((exists ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative_summand. ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative_summand + S (ff_a_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_nonzero_value_noevaluationdeterminanthsf)) /\ exists ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_nonzero_value_noevaluationdeterminanthsf = ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_nonzero_value_noevaluationdeterminanthsf) + (ff_a_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative_partial. ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative_partial + S (ff_r_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative_partial. ff_u_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative = ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative) + (ff_r_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative_successor. ff_h_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative_successor + S (ff_s_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative_successor. ff_u_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative = ff_q_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative)) * ff_v_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative) + (ff_s_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative))) /\ ff_s_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative = ff_r_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative + ff_a_mce_mdr_nonzero_value_noevaluationdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_nonzero_value_noevaluationdeterminanti. mdr_gap_nonzero_value_noevaluationdeterminanti + S (mdr_i_nonzero_value_noevaluationdeterminant) = (mdr_l_nonzero_value_noevaluationdeterminant)) /\ (exists mdr_z_nonzero_value_noevaluationdeterminantr. ((exists mdr_a_nonzero_value_noevaluationdeterminantrc mdr_b_nonzero_value_noevaluationdeterminantrc mdr_c_nonzero_value_noevaluationdeterminantrc mdr_e_nonzero_value_noevaluationdeterminantrc mdr_f_nonzero_value_noevaluationdeterminantrc. ((mdr_a_nonzero_value_noevaluationdeterminantrc = ((q) + (mdr_ub_nonzero_value_noevaluation)) * S ((q) + (mdr_ub_nonzero_value_noevaluation)) + ((mdr_ub_nonzero_value_noevaluation) + (mdr_ub_nonzero_value_noevaluation))) /\ ((mdr_b_nonzero_value_noevaluationdeterminantrc = ((mdr_uc_nonzero_value_noevaluation) + (mdr_vb_nonzero_value_noevaluation)) * S ((mdr_uc_nonzero_value_noevaluation) + (mdr_vb_nonzero_value_noevaluation)) + ((mdr_vb_nonzero_value_noevaluation) + (mdr_vb_nonzero_value_noevaluation))) /\ ((mdr_c_nonzero_value_noevaluationdeterminantrc = ((mdr_a_nonzero_value_noevaluationdeterminantrc) + (mdr_b_nonzero_value_noevaluationdeterminantrc)) * S ((mdr_a_nonzero_value_noevaluationdeterminantrc) + (mdr_b_nonzero_value_noevaluationdeterminantrc)) + ((mdr_b_nonzero_value_noevaluationdeterminantrc) + (mdr_b_nonzero_value_noevaluationdeterminantrc))) /\ ((mdr_e_nonzero_value_noevaluationdeterminantrc = ((mdr_p_nonzero_value_no) + (mdr_n_nonzero_value_no)) * S ((mdr_p_nonzero_value_no) + (mdr_n_nonzero_value_no)) + ((mdr_n_nonzero_value_no) + (mdr_n_nonzero_value_no))) /\ ((mdr_f_nonzero_value_noevaluationdeterminantrc = ((mdr_vc_nonzero_value_noevaluation) + (mdr_e_nonzero_value_noevaluationdeterminantrc)) * S ((mdr_vc_nonzero_value_noevaluation) + (mdr_e_nonzero_value_noevaluationdeterminantrc)) + ((mdr_e_nonzero_value_noevaluationdeterminantrc) + (mdr_e_nonzero_value_noevaluationdeterminantrc))) /\ ((mdr_z_nonzero_value_noevaluationdeterminantr) = ((mdr_c_nonzero_value_noevaluationdeterminantrc) + (mdr_f_nonzero_value_noevaluationdeterminantrc)) * S ((mdr_c_nonzero_value_noevaluationdeterminantrc) + (mdr_f_nonzero_value_noevaluationdeterminantrc)) + ((mdr_f_nonzero_value_noevaluationdeterminantrc) + (mdr_f_nonzero_value_noevaluationdeterminantrc))))))))) /\ (((exists ff_h_mdr_nonzero_value_noevaluationdeterminantrb. ff_h_mdr_nonzero_value_noevaluationdeterminantrb + S (mdr_z_nonzero_value_noevaluationdeterminantr) = S ((S (mdr_i_nonzero_value_noevaluationdeterminant)) * mdr_c_nonzero_value_noevaluationdeterminant)) /\ exists ff_q_mdr_nonzero_value_noevaluationdeterminantrb. mdr_b_nonzero_value_noevaluationdeterminant = ff_q_mdr_nonzero_value_noevaluationdeterminantrb * S ((S (mdr_i_nonzero_value_noevaluationdeterminant)) * mdr_c_nonzero_value_noevaluationdeterminant) + (mdr_z_nonzero_value_noevaluationdeterminantr)))))))))) /\ (~(mdr_p_nonzero_value_no = mdr_n_nonzero_value_no))))