(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS eval_abc_start))
(VAR v_3 v_i_0 v_j_0 v_m v_n)
(RULES
  eval_abc_start(v_3, v_i_0, v_j_0, v_m, v_n) -> Com_1(eval_abc_bb0_in(v_3, v_i_0, v_j_0, v_m, v_n))
  eval_abc_bb0_in(v_3, v_i_0, v_j_0, v_m, v_n) -> Com_1(eval_abc_0(v_3, v_i_0, v_j_0, v_m, v_n))
  eval_abc_0(v_3, v_i_0, v_j_0, v_m, v_n) -> Com_1(eval_abc_1(v_3, v_i_0, v_j_0, v_m, v_n))
  eval_abc_1(v_3, v_i_0, v_j_0, v_m, v_n) -> Com_1(eval_abc_2(v_3, v_i_0, v_j_0, v_m, v_n))
  eval_abc_2(v_3, v_i_0, v_j_0, v_m, v_n) -> Com_1(eval_abc_3(v_3, v_i_0, v_j_0, v_m, v_n))
  eval_abc_3(v_3, v_i_0, v_j_0, v_m, v_n) -> Com_1(eval_abc_4(v_3, v_i_0, v_j_0, v_m, v_n))
  eval_abc_4(v_3, v_i_0, v_j_0, v_m, v_n) -> Com_1(eval_abc_5(v_3, v_i_0, v_j_0, v_m, v_n))
  eval_abc_5(v_3, v_i_0, v_j_0, v_m, v_n) -> Com_1(eval_abc_bb1_in(v_3, v_n, v_j_0, v_m, v_n))
  eval_abc_bb1_in(v_3, v_i_0, v_j_0, v_m, v_n) -> Com_1(eval_abc_bb2_in(v_3, v_i_0, v_m, v_m, v_n)) [ -v_i_0 + v_n >= 0 /\ v_i_0 >= 1 ]
  eval_abc_bb1_in(v_3, v_i_0, v_j_0, v_m, v_n) -> Com_1(eval_abc_bb5_in(v_3, v_i_0, v_j_0, v_m, v_n)) [ -v_i_0 + v_n >= 0 /\ v_i_0 < 1 ]
  eval_abc_bb2_in(v_3, v_i_0, v_j_0, v_m, v_n) -> Com_1(eval_abc_bb3_in(v_3, v_i_0, v_j_0, v_m, v_n)) [ v_n - 1 >= 0 /\ v_i_0 + v_n - 2 >= 0 /\ -v_i_0 + v_n >= 0 /\ -v_j_0 + v_m >= 0 /\ v_i_0 - 1 >= 0 /\ v_j_0 >= 1 ]
  eval_abc_bb2_in(v_3, v_i_0, v_j_0, v_m, v_n) -> Com_1(eval_abc_bb4_in(v_3, v_i_0, v_j_0, v_m, v_n)) [ v_n - 1 >= 0 /\ v_i_0 + v_n - 2 >= 0 /\ -v_i_0 + v_n >= 0 /\ -v_j_0 + v_m >= 0 /\ v_i_0 - 1 >= 0 /\ v_j_0 < 1 ]
  eval_abc_bb3_in(v_3, v_i_0, v_j_0, v_m, v_n) -> Com_1(eval_abc_bb2_in(v_3, v_i_0, v_j_0 - 1, v_m, v_n)) [ v_n - 1 >= 0 /\ v_m + v_n - 2 >= 0 /\ v_j_0 + v_n - 2 >= 0 /\ v_i_0 + v_n - 2 >= 0 /\ -v_i_0 + v_n >= 0 /\ v_m - 1 >= 0 /\ v_j_0 + v_m - 2 >= 0 /\ -v_j_0 + v_m >= 0 /\ v_i_0 + v_m - 2 >= 0 /\ v_j_0 - 1 >= 0 /\ v_i_0 + v_j_0 - 2 >= 0 /\ v_i_0 - 1 >= 0 ]
  eval_abc_bb4_in(v_3, v_i_0, v_j_0, v_m, v_n) -> Com_1(eval_abc_9(v_i_0 - 1, v_i_0, v_j_0, v_m, v_n)) [ v_n - 1 >= 0 /\ -v_j_0 + v_n - 1 >= 0 /\ v_i_0 + v_n - 2 >= 0 /\ -v_i_0 + v_n >= 0 /\ -v_j_0 + v_m >= 0 /\ -v_j_0 >= 0 /\ v_i_0 - v_j_0 - 1 >= 0 /\ v_i_0 - 1 >= 0 ]
  eval_abc_9(v_3, v_i_0, v_j_0, v_m, v_n) -> Com_1(eval_abc_10(v_3, v_i_0, v_j_0, v_m, v_n)) [ v_n - 1 >= 0 /\ -v_j_0 + v_n - 1 >= 0 /\ v_i_0 + v_n - 2 >= 0 /\ -v_i_0 + v_n >= 0 /\ v_3 + v_n - 1 >= 0 /\ -v_3 + v_n - 1 >= 0 /\ -v_j_0 + v_m >= 0 /\ -v_j_0 >= 0 /\ v_i_0 - v_j_0 - 1 >= 0 /\ v_3 - v_j_0 >= 0 /\ v_3 - v_i_0 + 1 >= 0 /\ v_i_0 - 1 >= 0 /\ v_3 + v_i_0 - 1 >= 0 /\ -v_3 + v_i_0 - 1 >= 0 /\ v_3 >= 0 ]
  eval_abc_10(v_3, v_i_0, v_j_0, v_m, v_n) -> Com_1(eval_abc_bb1_in(v_3, v_3, v_j_0, v_m, v_n)) [ v_n - 1 >= 0 /\ -v_j_0 + v_n - 1 >= 0 /\ v_i_0 + v_n - 2 >= 0 /\ -v_i_0 + v_n >= 0 /\ v_3 + v_n - 1 >= 0 /\ -v_3 + v_n - 1 >= 0 /\ -v_j_0 + v_m >= 0 /\ -v_j_0 >= 0 /\ v_i_0 - v_j_0 - 1 >= 0 /\ v_3 - v_j_0 >= 0 /\ v_3 - v_i_0 + 1 >= 0 /\ v_i_0 - 1 >= 0 /\ v_3 + v_i_0 - 1 >= 0 /\ -v_3 + v_i_0 - 1 >= 0 /\ v_3 >= 0 ]
  eval_abc_bb5_in(v_3, v_i_0, v_j_0, v_m, v_n) -> Com_1(eval_abc_stop(v_3, v_i_0, v_j_0, v_m, v_n)) [ -v_i_0 + v_n >= 0 /\ -v_i_0 >= 0 ]
)