YES Termination: (Ranking Functions Found) ------------ l0: < < x0_0 -x2_0, 0 > > l1: < < x0_0 -x2_0, x0_0 -x2_0 > > l10: < < x0_0 -x4_0, 0 >, < x0_0 -x4_0 -x5_0, 0 >, < x4_0 + x5_0 -x7_0, 0 > > l11: < < x0_0 -x4_0, 0 >, < x0_0 -x4_0 -x5_0, 0 >, < x4_0 + x5_0 -x7_0, x4_0 + x5_0 -x7_0 > > l12: < < x0_0 -x4_0, 0 >, < x0_0 -x4_0 -x5_0, 0 >, < x4_0 + x5_0 -x6_0, 0 > > l13: < < x0_0 -x4_0, 0 >, < x0_0 -x4_0 -x5_0, 0 >, < x4_0 + x5_0 -x6_0, x4_0 + x5_0 -x6_0 > > l14: < < x0_0 -x4_0, 0 >, < x0_0 -x4_0 -x5_0, 0 >, < x4_0 + x5_0 -x6_0, 0 > > l16: < < x0_0 -x4_0, 0 >, < x0_0 -x4_0 -x5_0, 0 > > l17: < < x0_0 -x4_0, 0 >, < x0_0 -x4_0 -x5_0, 0 >, < x4_0 + x5_0 -x6_0, 0 > > l18: < < x0_0 -x4_0, 0 > > l19: < < x0_0 -x4_0, x0_0 -x4_0 > > l2: < < x0_0 -x1_0, 0 > > l20: < < x0_0 -x4_0, 0 >, < x0_0 -x4_0 -x5_0, 0 > > l23: < < 1 + x0_0 -x3_0, 0 > > l3: < < x0_0 -x1_0, x0_0 -x1_0 > > l4: < < x0_0 -x1_0, 0 >, < 1 + x0_0 -x2_0, 0 > > l5: < < x0_0 -x1_0, 0 >, < 1 + x0_0 -x2_0, 1 + x0_0 -x2_0 > > l6: < < 1 + x0_0 -x3_0, 1 + x0_0 -x3_0 > > l7: < < x0_0 -x1_0, 0 > > l8: < < x0_0 -x4_0, 0 >, < x0_0 -x4_0 -x5_0, 0 > > l9: < < x0_0 -x4_0, 0 >, < x0_0 -x4_0 -x5_0, x0_0 -x4_0 -x5_0 > > method 1