(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS eval_abc_start))
(VAR v_2 v_6 v_7 v_i_0 v_i_0_sink v_j_0 v_l_0 v_m)
(RULES
  eval_abc_start(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m) -> Com_1(eval_abc_bb0_in(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m))
  eval_abc_bb0_in(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m) -> Com_1(eval_abc_0(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m))
  eval_abc_0(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m) -> Com_1(eval_abc_1(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m))
  eval_abc_1(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m) -> Com_1(eval_abc_2(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m))
  eval_abc_2(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m) -> Com_1(eval_abc_3(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m))
  eval_abc_3(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m) -> Com_1(eval_abc_4(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m))
  eval_abc_4(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m) -> Com_1(eval_abc_5(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m))
  eval_abc_5(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m) -> Com_1(eval_abc_6(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m))
  eval_abc_6(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m) -> Com_1(eval_abc_bb1_in(v_2, v_6, v_7, 1, v_i_0_sink, v_j_0, v_l_0, v_m))
  eval_abc_bb1_in(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m) -> Com_1(eval_abc_bb2_in(v_2, v_6, v_7, v_i_0, v_i_0_sink, 1, v_l_0, v_m)) [ v_i_0 - 1 >= 0 /\ v_i_0 <= v_m ]
  eval_abc_bb1_in(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m) -> Com_1(eval_abc_bb8_in(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m)) [ v_i_0 - 1 >= 0 /\ v_i_0 > v_m ]
  eval_abc_bb2_in(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m) -> Com_1(eval_abc_bb3_in(v_2, v_6, v_7, v_i_0, v_i_0, v_j_0, v_l_0, v_m)) [ v_m - 1 >= 0 /\ v_j_0 + v_m - 2 >= 0 /\ -v_j_0 + v_m + 1 >= 0 /\ v_i_0 + v_m - 2 >= 0 /\ -v_i_0 + v_m >= 0 /\ v_i_0 - v_j_0 + 1 >= 0 /\ v_j_0 - 1 >= 0 /\ v_i_0 + v_j_0 - 2 >= 0 /\ v_i_0 - 1 >= 0 /\ v_j_0 <= v_i_0 ]
  eval_abc_bb2_in(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m) -> Com_1(eval_abc_bb7_in(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m)) [ v_m - 1 >= 0 /\ v_j_0 + v_m - 2 >= 0 /\ -v_j_0 + v_m + 1 >= 0 /\ v_i_0 + v_m - 2 >= 0 /\ -v_i_0 + v_m >= 0 /\ v_i_0 - v_j_0 + 1 >= 0 /\ v_j_0 - 1 >= 0 /\ v_i_0 + v_j_0 - 2 >= 0 /\ v_i_0 - 1 >= 0 /\ v_j_0 > v_i_0 ]
  eval_abc_bb3_in(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m) -> Com_1(eval_abc_bb4_in(v_i_0_sink + 1, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, 1, v_m)) [ v_m - 1 >= 0 /\ v_j_0 + v_m - 2 >= 0 /\ -v_j_0 + v_m >= 0 /\ v_i_0_sink + v_m - 2 >= 0 /\ -v_i_0_sink + v_m >= 0 /\ v_i_0 + v_m - 2 >= 0 /\ -v_i_0 + v_m >= 0 /\ v_i_0_sink - v_j_0 >= 0 /\ v_i_0 - v_j_0 >= 0 /\ v_j_0 - 1 >= 0 /\ v_i_0_sink + v_j_0 - 2 >= 0 /\ v_i_0 + v_j_0 - 2 >= 0 /\ v_i_0_sink - 1 >= 0 /\ v_i_0 + v_i_0_sink - 2 >= 0 /\ -v_i_0 + v_i_0_sink >= 0 /\ v_i_0 - 1 >= 0 /\ v_i_0_sink + 1 <= v_m ]
  eval_abc_bb3_in(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m) -> Com_1(eval_abc_bb6_in(v_i_0_sink + 1, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m)) [ v_m - 1 >= 0 /\ v_j_0 + v_m - 2 >= 0 /\ -v_j_0 + v_m >= 0 /\ v_i_0_sink + v_m - 2 >= 0 /\ -v_i_0_sink + v_m >= 0 /\ v_i_0 + v_m - 2 >= 0 /\ -v_i_0 + v_m >= 0 /\ v_i_0_sink - v_j_0 >= 0 /\ v_i_0 - v_j_0 >= 0 /\ v_j_0 - 1 >= 0 /\ v_i_0_sink + v_j_0 - 2 >= 0 /\ v_i_0 + v_j_0 - 2 >= 0 /\ v_i_0_sink - 1 >= 0 /\ v_i_0 + v_i_0_sink - 2 >= 0 /\ -v_i_0 + v_i_0_sink >= 0 /\ v_i_0 - 1 >= 0 /\ v_i_0_sink + 1 > v_m ]
  eval_abc_bb4_in(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m) -> Com_1(eval_abc_bb5_in(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m)) [ v_m - 2 >= 0 /\ v_l_0 + v_m - 3 >= 0 /\ v_j_0 + v_m - 3 >= 0 /\ -v_j_0 + v_m - 1 >= 0 /\ v_i_0_sink + v_m - 3 >= 0 /\ -v_i_0_sink + v_m - 1 >= 0 /\ v_i_0 + v_m - 3 >= 0 /\ -v_i_0 + v_m - 1 >= 0 /\ v_2 + v_m - 4 >= 0 /\ -v_2 + v_m >= 0 /\ v_l_0 - 1 >= 0 /\ v_j_0 + v_l_0 - 2 >= 0 /\ v_i_0_sink + v_l_0 - 2 >= 0 /\ v_i_0 + v_l_0 - 2 >= 0 /\ v_2 + v_l_0 - 3 >= 0 /\ v_i_0_sink - v_j_0 >= 0 /\ v_i_0 - v_j_0 >= 0 /\ v_2 - v_j_0 - 1 >= 0 /\ v_j_0 - 1 >= 0 /\ v_i_0_sink + v_j_0 - 2 >= 0 /\ v_i_0 + v_j_0 - 2 >= 0 /\ v_2 + v_j_0 - 3 >= 0 /\ v_2 - v_i_0_sink - 1 >= 0 /\ v_i_0_sink - 1 >= 0 /\ v_i_0 + v_i_0_sink - 2 >= 0 /\ -v_i_0 + v_i_0_sink >= 0 /\ v_2 + v_i_0_sink - 3 >= 0 /\ -v_2 + v_i_0_sink + 1 >= 0 /\ v_2 - v_i_0 - 1 >= 0 /\ v_i_0 - 1 >= 0 /\ v_2 + v_i_0 - 3 >= 0 /\ v_2 - 2 >= 0 /\ v_l_0 <= v_2 ]
  eval_abc_bb4_in(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m) -> Com_1(eval_abc_bb3_in(v_2, v_6, v_7, v_i_0, v_2, v_j_0, v_l_0, v_m)) [ v_m - 2 >= 0 /\ v_l_0 + v_m - 3 >= 0 /\ v_j_0 + v_m - 3 >= 0 /\ -v_j_0 + v_m - 1 >= 0 /\ v_i_0_sink + v_m - 3 >= 0 /\ -v_i_0_sink + v_m - 1 >= 0 /\ v_i_0 + v_m - 3 >= 0 /\ -v_i_0 + v_m - 1 >= 0 /\ v_2 + v_m - 4 >= 0 /\ -v_2 + v_m >= 0 /\ v_l_0 - 1 >= 0 /\ v_j_0 + v_l_0 - 2 >= 0 /\ v_i_0_sink + v_l_0 - 2 >= 0 /\ v_i_0 + v_l_0 - 2 >= 0 /\ v_2 + v_l_0 - 3 >= 0 /\ v_i_0_sink - v_j_0 >= 0 /\ v_i_0 - v_j_0 >= 0 /\ v_2 - v_j_0 - 1 >= 0 /\ v_j_0 - 1 >= 0 /\ v_i_0_sink + v_j_0 - 2 >= 0 /\ v_i_0 + v_j_0 - 2 >= 0 /\ v_2 + v_j_0 - 3 >= 0 /\ v_2 - v_i_0_sink - 1 >= 0 /\ v_i_0_sink - 1 >= 0 /\ v_i_0 + v_i_0_sink - 2 >= 0 /\ -v_i_0 + v_i_0_sink >= 0 /\ v_2 + v_i_0_sink - 3 >= 0 /\ -v_2 + v_i_0_sink + 1 >= 0 /\ v_2 - v_i_0 - 1 >= 0 /\ v_i_0 - 1 >= 0 /\ v_2 + v_i_0 - 3 >= 0 /\ v_2 - 2 >= 0 /\ v_l_0 > v_2 ]
  eval_abc_bb5_in(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m) -> Com_1(eval_abc_bb4_in(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0 + 1, v_m)) [ v_m - 2 >= 0 /\ v_l_0 + v_m - 3 >= 0 /\ -v_l_0 + v_m >= 0 /\ v_j_0 + v_m - 3 >= 0 /\ -v_j_0 + v_m - 1 >= 0 /\ v_i_0_sink + v_m - 3 >= 0 /\ -v_i_0_sink + v_m - 1 >= 0 /\ v_i_0 + v_m - 3 >= 0 /\ -v_i_0 + v_m - 1 >= 0 /\ v_2 + v_m - 4 >= 0 /\ -v_2 + v_m >= 0 /\ v_i_0_sink - v_l_0 + 1 >= 0 /\ v_2 - v_l_0 >= 0 /\ v_l_0 - 1 >= 0 /\ v_j_0 + v_l_0 - 2 >= 0 /\ v_i_0_sink + v_l_0 - 2 >= 0 /\ v_i_0 + v_l_0 - 2 >= 0 /\ v_2 + v_l_0 - 3 >= 0 /\ v_i_0_sink - v_j_0 >= 0 /\ v_i_0 - v_j_0 >= 0 /\ v_2 - v_j_0 - 1 >= 0 /\ v_j_0 - 1 >= 0 /\ v_i_0_sink + v_j_0 - 2 >= 0 /\ v_i_0 + v_j_0 - 2 >= 0 /\ v_2 + v_j_0 - 3 >= 0 /\ v_2 - v_i_0_sink - 1 >= 0 /\ v_i_0_sink - 1 >= 0 /\ v_i_0 + v_i_0_sink - 2 >= 0 /\ -v_i_0 + v_i_0_sink >= 0 /\ v_2 + v_i_0_sink - 3 >= 0 /\ -v_2 + v_i_0_sink + 1 >= 0 /\ v_2 - v_i_0 - 1 >= 0 /\ v_i_0 - 1 >= 0 /\ v_2 + v_i_0 - 3 >= 0 /\ v_2 - 2 >= 0 ]
  eval_abc_bb6_in(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m) -> Com_1(eval_abc_12(v_2, v_j_0 + 1, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m)) [ v_i_0_sink - v_m >= 0 /\ v_2 - v_m - 1 >= 0 /\ v_m - 1 >= 0 /\ v_j_0 + v_m - 2 >= 0 /\ -v_j_0 + v_m >= 0 /\ v_i_0_sink + v_m - 2 >= 0 /\ -v_i_0_sink + v_m >= 0 /\ v_i_0 + v_m - 2 >= 0 /\ -v_i_0 + v_m >= 0 /\ v_2 + v_m - 3 >= 0 /\ -v_2 + v_m + 1 >= 0 /\ v_i_0_sink - v_j_0 >= 0 /\ v_i_0 - v_j_0 >= 0 /\ v_2 - v_j_0 - 1 >= 0 /\ v_j_0 - 1 >= 0 /\ v_i_0_sink + v_j_0 - 2 >= 0 /\ v_i_0 + v_j_0 - 2 >= 0 /\ v_2 + v_j_0 - 3 >= 0 /\ v_2 - v_i_0_sink - 1 >= 0 /\ v_i_0_sink - 1 >= 0 /\ v_i_0 + v_i_0_sink - 2 >= 0 /\ -v_i_0 + v_i_0_sink >= 0 /\ v_2 + v_i_0_sink - 3 >= 0 /\ -v_2 + v_i_0_sink + 1 >= 0 /\ v_2 - v_i_0 - 1 >= 0 /\ v_i_0 - 1 >= 0 /\ v_2 + v_i_0 - 3 >= 0 /\ v_2 - 2 >= 0 ]
  eval_abc_12(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m) -> Com_1(eval_abc_13(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m)) [ v_i_0_sink - v_m >= 0 /\ v_2 - v_m - 1 >= 0 /\ v_m - 1 >= 0 /\ v_j_0 + v_m - 2 >= 0 /\ -v_j_0 + v_m >= 0 /\ v_i_0_sink + v_m - 2 >= 0 /\ -v_i_0_sink + v_m >= 0 /\ v_i_0 + v_m - 2 >= 0 /\ -v_i_0 + v_m >= 0 /\ v_6 + v_m - 3 >= 0 /\ -v_6 + v_m + 1 >= 0 /\ v_2 + v_m - 3 >= 0 /\ -v_2 + v_m + 1 >= 0 /\ v_i_0_sink - v_j_0 >= 0 /\ v_i_0 - v_j_0 >= 0 /\ v_6 - v_j_0 - 1 >= 0 /\ v_2 - v_j_0 - 1 >= 0 /\ v_j_0 - 1 >= 0 /\ v_i_0_sink + v_j_0 - 2 >= 0 /\ v_i_0 + v_j_0 - 2 >= 0 /\ v_6 + v_j_0 - 3 >= 0 /\ -v_6 + v_j_0 + 1 >= 0 /\ v_2 + v_j_0 - 3 >= 0 /\ v_2 - v_i_0_sink - 1 >= 0 /\ v_i_0_sink - 1 >= 0 /\ v_i_0 + v_i_0_sink - 2 >= 0 /\ -v_i_0 + v_i_0_sink >= 0 /\ v_6 + v_i_0_sink - 3 >= 0 /\ -v_6 + v_i_0_sink + 1 >= 0 /\ v_2 + v_i_0_sink - 3 >= 0 /\ -v_2 + v_i_0_sink + 1 >= 0 /\ v_2 - v_i_0 - 1 >= 0 /\ v_i_0 - 1 >= 0 /\ v_6 + v_i_0 - 3 >= 0 /\ -v_6 + v_i_0 + 1 >= 0 /\ v_2 + v_i_0 - 3 >= 0 /\ v_2 - v_6 >= 0 /\ v_6 - 2 >= 0 /\ v_2 + v_6 - 4 >= 0 /\ v_2 - 2 >= 0 ]
  eval_abc_13(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m) -> Com_1(eval_abc_bb2_in(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_6, v_l_0, v_m)) [ v_i_0_sink - v_m >= 0 /\ v_2 - v_m - 1 >= 0 /\ v_m - 1 >= 0 /\ v_j_0 + v_m - 2 >= 0 /\ -v_j_0 + v_m >= 0 /\ v_i_0_sink + v_m - 2 >= 0 /\ -v_i_0_sink + v_m >= 0 /\ v_i_0 + v_m - 2 >= 0 /\ -v_i_0 + v_m >= 0 /\ v_6 + v_m - 3 >= 0 /\ -v_6 + v_m + 1 >= 0 /\ v_2 + v_m - 3 >= 0 /\ -v_2 + v_m + 1 >= 0 /\ v_i_0_sink - v_j_0 >= 0 /\ v_i_0 - v_j_0 >= 0 /\ v_6 - v_j_0 - 1 >= 0 /\ v_2 - v_j_0 - 1 >= 0 /\ v_j_0 - 1 >= 0 /\ v_i_0_sink + v_j_0 - 2 >= 0 /\ v_i_0 + v_j_0 - 2 >= 0 /\ v_6 + v_j_0 - 3 >= 0 /\ -v_6 + v_j_0 + 1 >= 0 /\ v_2 + v_j_0 - 3 >= 0 /\ v_2 - v_i_0_sink - 1 >= 0 /\ v_i_0_sink - 1 >= 0 /\ v_i_0 + v_i_0_sink - 2 >= 0 /\ -v_i_0 + v_i_0_sink >= 0 /\ v_6 + v_i_0_sink - 3 >= 0 /\ -v_6 + v_i_0_sink + 1 >= 0 /\ v_2 + v_i_0_sink - 3 >= 0 /\ -v_2 + v_i_0_sink + 1 >= 0 /\ v_2 - v_i_0 - 1 >= 0 /\ v_i_0 - 1 >= 0 /\ v_6 + v_i_0 - 3 >= 0 /\ -v_6 + v_i_0 + 1 >= 0 /\ v_2 + v_i_0 - 3 >= 0 /\ v_2 - v_6 >= 0 /\ v_6 - 2 >= 0 /\ v_2 + v_6 - 4 >= 0 /\ v_2 - 2 >= 0 ]
  eval_abc_bb7_in(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m) -> Com_1(eval_abc_15(v_2, v_6, v_i_0 + 1, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m)) [ v_m - 1 >= 0 /\ v_j_0 + v_m - 3 >= 0 /\ -v_j_0 + v_m + 1 >= 0 /\ v_i_0 + v_m - 2 >= 0 /\ -v_i_0 + v_m >= 0 /\ v_i_0 - v_j_0 + 1 >= 0 /\ v_j_0 - 2 >= 0 /\ v_i_0 + v_j_0 - 3 >= 0 /\ -v_i_0 + v_j_0 - 1 >= 0 /\ v_i_0 - 1 >= 0 ]
  eval_abc_15(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m) -> Com_1(eval_abc_16(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m)) [ v_m - 1 >= 0 /\ v_j_0 + v_m - 3 >= 0 /\ -v_j_0 + v_m + 1 >= 0 /\ v_i_0 + v_m - 2 >= 0 /\ -v_i_0 + v_m >= 0 /\ v_7 + v_m - 3 >= 0 /\ -v_7 + v_m + 1 >= 0 /\ v_i_0 - v_j_0 + 1 >= 0 /\ v_7 - v_j_0 >= 0 /\ v_j_0 - 2 >= 0 /\ v_i_0 + v_j_0 - 3 >= 0 /\ -v_i_0 + v_j_0 - 1 >= 0 /\ v_7 + v_j_0 - 4 >= 0 /\ -v_7 + v_j_0 >= 0 /\ v_7 - v_i_0 - 1 >= 0 /\ v_i_0 - 1 >= 0 /\ v_7 + v_i_0 - 3 >= 0 /\ -v_7 + v_i_0 + 1 >= 0 /\ v_7 - 2 >= 0 ]
  eval_abc_16(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m) -> Com_1(eval_abc_bb1_in(v_2, v_6, v_7, v_7, v_i_0_sink, v_j_0, v_l_0, v_m)) [ v_m - 1 >= 0 /\ v_j_0 + v_m - 3 >= 0 /\ -v_j_0 + v_m + 1 >= 0 /\ v_i_0 + v_m - 2 >= 0 /\ -v_i_0 + v_m >= 0 /\ v_7 + v_m - 3 >= 0 /\ -v_7 + v_m + 1 >= 0 /\ v_i_0 - v_j_0 + 1 >= 0 /\ v_7 - v_j_0 >= 0 /\ v_j_0 - 2 >= 0 /\ v_i_0 + v_j_0 - 3 >= 0 /\ -v_i_0 + v_j_0 - 1 >= 0 /\ v_7 + v_j_0 - 4 >= 0 /\ -v_7 + v_j_0 >= 0 /\ v_7 - v_i_0 - 1 >= 0 /\ v_i_0 - 1 >= 0 /\ v_7 + v_i_0 - 3 >= 0 /\ -v_7 + v_i_0 + 1 >= 0 /\ v_7 - 2 >= 0 ]
  eval_abc_bb8_in(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m) -> Com_1(eval_abc_stop(v_2, v_6, v_7, v_i_0, v_i_0_sink, v_j_0, v_l_0, v_m)) [ v_i_0 - v_m - 1 >= 0 /\ v_i_0 - 1 >= 0 ]
)