YES


Termination: (Ranking Functions Found)
------------
n_eval_main_4___10: < < -1 + v_x_P0 > >
n_eval_main_4___15: < < v_10 > >
n_eval_main_4___17: < < v_8 > >
n_eval_main_4___2: < < -1 + v_y_P0 > >
n_eval_main_4___20: < < v_8 > >
n_eval_main_4___23: < < -1 + v_8 > >
n_eval_main_4___29: < < v_12 > >
n_eval_main_4___4: < < v_8 > >
n_eval_main_4___44: < < v_10 > >
n_eval_main_4___46: < < v_x_P0 > >
n_eval_main_4___49: < < v_x_P0 > >
n_eval_main_4___52: < < -1 + v_x_P0 > >
n_eval_main_4___7: < < v_x_P0 > >
n_eval_main_4___71: < < -1 + v_y_P0 > >
n_eval_main_4___75: < < -1 + v_y_P0 > >
n_eval_main_4___79: < < -v_11 > >
n_eval_main_bb1_in___11: < < v_y_P0 > >
n_eval_main_bb1_in___12: < < v_8 > >
n_eval_main_bb1_in___18: < < v_8 > >
n_eval_main_bb1_in___21: < < v_x_P0 > >
n_eval_main_bb1_in___24: < < 1 + v_10 > >
n_eval_main_bb1_in___25: < < v_8 > >
n_eval_main_bb1_in___47: < < v_x_P0 > >
n_eval_main_bb1_in___5: < < v_x_P0 > >
n_eval_main_bb1_in___50: < < v_x_P0 > >
n_eval_main_bb1_in___53: < < 1 + v_10 > >
n_eval_main_bb1_in___54: < < v_8 > >
n_eval_main_bb1_in___72: < < -1 + v_12 > >
n_eval_main_bb1_in___76: < < v_12 > >
n_eval_main_bb1_in___8: < < v_x_P0 > >
n_eval_main_bb1_in___80: < < v_12 > >
n_eval_main_bb1_in___81: < < -v_x_P0 > >
n_eval_main_bb3_in___1: < < -1 + v_10 > >
n_eval_main_bb3_in___14: < < v_10 > >
n_eval_main_bb3_in___16: < < v_x_P0 > >
n_eval_main_bb3_in___19: < < v_8 > >
n_eval_main_bb3_in___22: < < -1 + v_8 > >
n_eval_main_bb3_in___3: < < v_x_P0 > >
n_eval_main_bb3_in___43: < < v_10 > >
n_eval_main_bb3_in___45: < < v_8 > >
n_eval_main_bb3_in___48: < < v_8 > >
n_eval_main_bb3_in___51: < < -1 + v_8 > >
n_eval_main_bb3_in___6: < < v_8 > >
n_eval_main_bb3_in___9: < < -1 + v_8 > >
n_eval_main_bb6_in___27: < < v_12 > >
n_eval_main_bb6_in___69: < < -1 + v_y_P0 > >
n_eval_main_bb6_in___73: < < -1 + v_12 > >
n_eval_main_bb6_in___77: < < -v_x_P0 > >
n_n_eval_main_bb1_in___18___6: < < v_8 >, < v_x_P0 >, < v_8 >, < v_8 > >
n_n_eval_main_bb1_in___21___3: < < v_8 >, < v_10 > >
n_n_eval_main_bb1_in___21___5: < < v_8 >, < v_x_P0 >, < v_x_P0 >, < v_10 + v_8 -v_9 > >
n_n_eval_main_bb1_in___47___6: < < v_x_P0 >, < v_8 >, < v_8 >, < v_8 > >
n_n_eval_main_bb1_in___50___3: < < v_8 >, < v_10 > >
n_n_eval_main_bb1_in___50___5: < < v_x_P0 >, < v_8 >, < v_8 >, < v_10 + v_8 -v_9 > >
n_n_eval_main_bb1_in___5___6: < < v_x_P0 >, < v_x_P0 >, < v_x_P0 >, < v_x_P0 > >
n_n_eval_main_bb1_in___72___1: < < -v_11 > >
n_n_eval_main_bb1_in___81___1: < < -v_x_P0 > >
n_n_eval_main_bb1_in___8___3: < < v_8 >, < v_10 > >
n_n_eval_main_bb1_in___8___5: < < v_8 >, < v_8 >, < v_8 >, < -1 + v_8 > >
n_n_eval_main_bb3_in___16___7: < < v_8 >, < v_8 >, < v_8 >, < v_8 > >
n_n_eval_main_bb3_in___19___2: < < v_8 >, < -1 + v_10 > >
n_n_eval_main_bb3_in___19___4: < < v_x_P0 >, < v_8 >, < v_x_P0 >, < -1 + v_x_P0 > >
n_n_eval_main_bb3_in___3___7: < < v_x_P0 >, < v_8 >, < v_x_P0 >, < v_8 > >
n_n_eval_main_bb3_in___45___7: < < v_8 >, < v_8 >, < v_8 >, < v_x_P0 > >
n_n_eval_main_bb3_in___48___2: < < v_8 >, < -1 + v_y_P0 > >
n_n_eval_main_bb3_in___48___4: < < v_8 >, < v_8 >, < v_8 >, < -1 + v_8 > >
n_n_eval_main_bb3_in___6___2: < < v_x_P0 >, < -1 + v_y_P0 > >
n_n_eval_main_bb3_in___6___4: < < v_x_P0 >, < v_8 >, < v_x_P0 >, < -1 + v_8 > >
n_n_eval_main_bb6_in___69___2: < < -1 -v_x_P0 > >


method 1