YES Termination: (Ranking Functions Found) ------------ l0: < < a_0 > > l2: < < a_0 >, < -2 + a_0 >, < -1 + b_0 > > l3: < < a_0 > > l4: < < a_0 >, < -2 + a_0 >, < -1 + b_0 > > l5: < < a_0 >, < -2 + a_0 >, < b_0 >, < -1 + i_0 > > l6: < < a_0 >, < -2 + a_0 >, < b_0 >, < i_0 > > l7: < < a_0 >, < -2 + a_0 >, < b_0 >, < i_0 > > l8: < < a_0 >, < -2 + a_0 > > l9: < < a_0 >, < -2 + a_0 >, < b_0 >, < -1 + i_0 > > method 1