(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS evalNestedLoopstart))
(VAR A B C D E F G H)
(RULES
  evalNestedLoopstart(A, B, C, D, E, F, G, H) -> Com_1(evalNestedLoopentryin(A, B, C, D, E, F, G, H))
  evalNestedLoopentryin(A, B, C, D, E, F, G, H) -> Com_1(evalNestedLoopbb9in(A, B, C, 0, E, F, G, H)) [ A >= 0 /\ B >= 0 /\ C >= 0 ]
  evalNestedLoopbb9in(A, B, C, D, E, F, G, H) -> Com_1(evalNestedLoopreturnin(A, B, C, D, E, F, G, H)) [ D >= 0 /\ C + D >= 0 /\ B + D >= 0 /\ A + D >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ D >= A ]
  evalNestedLoopbb9in(A, B, C, D, E, F, G, H) -> Com_1(evalNestedLoopbb10in(A, B, C, D, E, F, G, H)) [ D >= 0 /\ C + D >= 0 /\ B + D >= 0 /\ A + D >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ A >= D + 1 ]
  evalNestedLoopbb10in(A, B, C, D, E, F, G, H) -> Com_1(evalNestedLoopbb6in(A, B, C, D, 0, D, G, H)) [ A - D - 1 >= 0 /\ D >= 0 /\ C + D >= 0 /\ B + D >= 0 /\ A + D - 1 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 /\ 0 >= I + 1 ]
  evalNestedLoopbb10in(A, B, C, D, E, F, G, H) -> Com_1(evalNestedLoopbb6in(A, B, C, D, 0, D, G, H)) [ A - D - 1 >= 0 /\ D >= 0 /\ C + D >= 0 /\ B + D >= 0 /\ A + D - 1 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 /\ I >= 1 ]
  evalNestedLoopbb10in(A, B, C, D, E, F, G, H) -> Com_1(evalNestedLoopreturnin(A, B, C, D, E, F, G, H)) [ A - D - 1 >= 0 /\ D >= 0 /\ C + D >= 0 /\ B + D >= 0 /\ A + D - 1 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 ]
  evalNestedLoopbb6in(A, B, C, D, E, F, G, H) -> Com_1(evalNestedLoopbb8in(A, B, C, D, E, F, G, H)) [ F >= 0 /\ E + F >= 0 /\ D + F >= 0 /\ -D + F >= 0 /\ C + F >= 0 /\ B + F >= 0 /\ A + F - 1 >= 0 /\ B - E >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E >= 0 /\ B + E >= 0 /\ A + E - 1 >= 0 /\ A - D - 1 >= 0 /\ D >= 0 /\ C + D >= 0 /\ B + D >= 0 /\ A + D - 1 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 /\ E >= B ]
  evalNestedLoopbb6in(A, B, C, D, E, F, G, H) -> Com_1(evalNestedLoopbb7in(A, B, C, D, E, F, G, H)) [ F >= 0 /\ E + F >= 0 /\ D + F >= 0 /\ -D + F >= 0 /\ C + F >= 0 /\ B + F >= 0 /\ A + F - 1 >= 0 /\ B - E >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E >= 0 /\ B + E >= 0 /\ A + E - 1 >= 0 /\ A - D - 1 >= 0 /\ D >= 0 /\ C + D >= 0 /\ B + D >= 0 /\ A + D - 1 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 /\ B >= E + 1 ]
  evalNestedLoopbb7in(A, B, C, D, E, F, G, H) -> Com_1(evalNestedLoopbb1in(A, B, C, D, E, F, G, H)) [ F >= 0 /\ E + F >= 0 /\ D + F >= 0 /\ -D + F >= 0 /\ C + F >= 0 /\ B + F - 1 >= 0 /\ A + F - 1 >= 0 /\ B - E - 1 >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E >= 0 /\ B + E - 1 >= 0 /\ A + E - 1 >= 0 /\ A - D - 1 >= 0 /\ D >= 0 /\ C + D >= 0 /\ B + D - 1 >= 0 /\ A + D - 1 >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ A - 1 >= 0 /\ 0 >= I + 1 ]
  evalNestedLoopbb7in(A, B, C, D, E, F, G, H) -> Com_1(evalNestedLoopbb1in(A, B, C, D, E, F, G, H)) [ F >= 0 /\ E + F >= 0 /\ D + F >= 0 /\ -D + F >= 0 /\ C + F >= 0 /\ B + F - 1 >= 0 /\ A + F - 1 >= 0 /\ B - E - 1 >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E >= 0 /\ B + E - 1 >= 0 /\ A + E - 1 >= 0 /\ A - D - 1 >= 0 /\ D >= 0 /\ C + D >= 0 /\ B + D - 1 >= 0 /\ A + D - 1 >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ A - 1 >= 0 /\ I >= 1 ]
  evalNestedLoopbb7in(A, B, C, D, E, F, G, H) -> Com_1(evalNestedLoopbb8in(A, B, C, D, E, F, G, H)) [ F >= 0 /\ E + F >= 0 /\ D + F >= 0 /\ -D + F >= 0 /\ C + F >= 0 /\ B + F - 1 >= 0 /\ A + F - 1 >= 0 /\ B - E - 1 >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E >= 0 /\ B + E - 1 >= 0 /\ A + E - 1 >= 0 /\ A - D - 1 >= 0 /\ D >= 0 /\ C + D >= 0 /\ B + D - 1 >= 0 /\ A + D - 1 >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ A - 1 >= 0 ]
  evalNestedLoopbb1in(A, B, C, D, E, F, G, H) -> Com_1(evalNestedLoopbb3in(A, B, C, D, E, F, E + 1, F)) [ F >= 0 /\ E + F >= 0 /\ D + F >= 0 /\ -D + F >= 0 /\ C + F >= 0 /\ B + F - 1 >= 0 /\ A + F - 1 >= 0 /\ B - E - 1 >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E >= 0 /\ B + E - 1 >= 0 /\ A + E - 1 >= 0 /\ A - D - 1 >= 0 /\ D >= 0 /\ C + D >= 0 /\ B + D - 1 >= 0 /\ A + D - 1 >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ A - 1 >= 0 ]
  evalNestedLoopbb3in(A, B, C, D, E, F, G, H) -> Com_1(evalNestedLoopbb6in(A, B, C, D, G, H, G, H)) [ H >= 0 /\ G + H - 1 >= 0 /\ F + H >= 0 /\ -F + H >= 0 /\ E + H >= 0 /\ D + H >= 0 /\ -D + H >= 0 /\ C + H >= 0 /\ B + H - 1 >= 0 /\ A + H - 1 >= 0 /\ E - G + 1 >= 0 /\ B - G >= 0 /\ G - 1 >= 0 /\ F + G - 1 >= 0 /\ E + G - 1 >= 0 /\ -E + G - 1 >= 0 /\ D + G - 1 >= 0 /\ C + G - 1 >= 0 /\ B + G - 2 >= 0 /\ A + G - 2 >= 0 /\ F >= 0 /\ E + F >= 0 /\ D + F >= 0 /\ -D + F >= 0 /\ C + F >= 0 /\ B + F - 1 >= 0 /\ A + F - 1 >= 0 /\ B - E - 1 >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E >= 0 /\ B + E - 1 >= 0 /\ A + E - 1 >= 0 /\ A - D - 1 >= 0 /\ D >= 0 /\ C + D >= 0 /\ B + D - 1 >= 0 /\ A + D - 1 >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ A - 1 >= 0 /\ H >= C ]
  evalNestedLoopbb3in(A, B, C, D, E, F, G, H) -> Com_1(evalNestedLoopbb4in(A, B, C, D, E, F, G, H)) [ H >= 0 /\ G + H - 1 >= 0 /\ F + H >= 0 /\ -F + H >= 0 /\ E + H >= 0 /\ D + H >= 0 /\ -D + H >= 0 /\ C + H >= 0 /\ B + H - 1 >= 0 /\ A + H - 1 >= 0 /\ E - G + 1 >= 0 /\ B - G >= 0 /\ G - 1 >= 0 /\ F + G - 1 >= 0 /\ E + G - 1 >= 0 /\ -E + G - 1 >= 0 /\ D + G - 1 >= 0 /\ C + G - 1 >= 0 /\ B + G - 2 >= 0 /\ A + G - 2 >= 0 /\ F >= 0 /\ E + F >= 0 /\ D + F >= 0 /\ -D + F >= 0 /\ C + F >= 0 /\ B + F - 1 >= 0 /\ A + F - 1 >= 0 /\ B - E - 1 >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E >= 0 /\ B + E - 1 >= 0 /\ A + E - 1 >= 0 /\ A - D - 1 >= 0 /\ D >= 0 /\ C + D >= 0 /\ B + D - 1 >= 0 /\ A + D - 1 >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ A - 1 >= 0 /\ C >= H + 1 ]
  evalNestedLoopbb4in(A, B, C, D, E, F, G, H) -> Com_1(evalNestedLoopbb2in(A, B, C, D, E, F, G, H)) [ C - H - 1 >= 0 /\ H >= 0 /\ G + H - 1 >= 0 /\ F + H >= 0 /\ -F + H >= 0 /\ E + H >= 0 /\ D + H >= 0 /\ -D + H >= 0 /\ C + H - 1 >= 0 /\ B + H - 1 >= 0 /\ A + H - 1 >= 0 /\ E - G + 1 >= 0 /\ B - G >= 0 /\ G - 1 >= 0 /\ F + G - 1 >= 0 /\ E + G - 1 >= 0 /\ -E + G - 1 >= 0 /\ D + G - 1 >= 0 /\ C + G - 2 >= 0 /\ B + G - 2 >= 0 /\ A + G - 2 >= 0 /\ C - F - 1 >= 0 /\ F >= 0 /\ E + F >= 0 /\ D + F >= 0 /\ -D + F >= 0 /\ C + F - 1 >= 0 /\ B + F - 1 >= 0 /\ A + F - 1 >= 0 /\ B - E - 1 >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E - 1 >= 0 /\ A + E - 1 >= 0 /\ C - D - 1 >= 0 /\ A - D - 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D - 1 >= 0 /\ A + D - 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ A + C - 2 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ A - 1 >= 0 /\ 0 >= I + 1 ]
  evalNestedLoopbb4in(A, B, C, D, E, F, G, H) -> Com_1(evalNestedLoopbb2in(A, B, C, D, E, F, G, H)) [ C - H - 1 >= 0 /\ H >= 0 /\ G + H - 1 >= 0 /\ F + H >= 0 /\ -F + H >= 0 /\ E + H >= 0 /\ D + H >= 0 /\ -D + H >= 0 /\ C + H - 1 >= 0 /\ B + H - 1 >= 0 /\ A + H - 1 >= 0 /\ E - G + 1 >= 0 /\ B - G >= 0 /\ G - 1 >= 0 /\ F + G - 1 >= 0 /\ E + G - 1 >= 0 /\ -E + G - 1 >= 0 /\ D + G - 1 >= 0 /\ C + G - 2 >= 0 /\ B + G - 2 >= 0 /\ A + G - 2 >= 0 /\ C - F - 1 >= 0 /\ F >= 0 /\ E + F >= 0 /\ D + F >= 0 /\ -D + F >= 0 /\ C + F - 1 >= 0 /\ B + F - 1 >= 0 /\ A + F - 1 >= 0 /\ B - E - 1 >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E - 1 >= 0 /\ A + E - 1 >= 0 /\ C - D - 1 >= 0 /\ A - D - 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D - 1 >= 0 /\ A + D - 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ A + C - 2 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ A - 1 >= 0 /\ I >= 1 ]
  evalNestedLoopbb4in(A, B, C, D, E, F, G, H) -> Com_1(evalNestedLoopbb6in(A, B, C, D, G, H, G, H)) [ C - H - 1 >= 0 /\ H >= 0 /\ G + H - 1 >= 0 /\ F + H >= 0 /\ -F + H >= 0 /\ E + H >= 0 /\ D + H >= 0 /\ -D + H >= 0 /\ C + H - 1 >= 0 /\ B + H - 1 >= 0 /\ A + H - 1 >= 0 /\ E - G + 1 >= 0 /\ B - G >= 0 /\ G - 1 >= 0 /\ F + G - 1 >= 0 /\ E + G - 1 >= 0 /\ -E + G - 1 >= 0 /\ D + G - 1 >= 0 /\ C + G - 2 >= 0 /\ B + G - 2 >= 0 /\ A + G - 2 >= 0 /\ C - F - 1 >= 0 /\ F >= 0 /\ E + F >= 0 /\ D + F >= 0 /\ -D + F >= 0 /\ C + F - 1 >= 0 /\ B + F - 1 >= 0 /\ A + F - 1 >= 0 /\ B - E - 1 >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E - 1 >= 0 /\ A + E - 1 >= 0 /\ C - D - 1 >= 0 /\ A - D - 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D - 1 >= 0 /\ A + D - 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ A + C - 2 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ A - 1 >= 0 ]
  evalNestedLoopbb2in(A, B, C, D, E, F, G, H) -> Com_1(evalNestedLoopbb3in(A, B, C, D, E, F, G, H + 1)) [ C - H - 1 >= 0 /\ H >= 0 /\ G + H - 1 >= 0 /\ F + H >= 0 /\ -F + H >= 0 /\ E + H >= 0 /\ D + H >= 0 /\ -D + H >= 0 /\ C + H - 1 >= 0 /\ B + H - 1 >= 0 /\ A + H - 1 >= 0 /\ E - G + 1 >= 0 /\ B - G >= 0 /\ G - 1 >= 0 /\ F + G - 1 >= 0 /\ E + G - 1 >= 0 /\ -E + G - 1 >= 0 /\ D + G - 1 >= 0 /\ C + G - 2 >= 0 /\ B + G - 2 >= 0 /\ A + G - 2 >= 0 /\ C - F - 1 >= 0 /\ F >= 0 /\ E + F >= 0 /\ D + F >= 0 /\ -D + F >= 0 /\ C + F - 1 >= 0 /\ B + F - 1 >= 0 /\ A + F - 1 >= 0 /\ B - E - 1 >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E - 1 >= 0 /\ B + E - 1 >= 0 /\ A + E - 1 >= 0 /\ C - D - 1 >= 0 /\ A - D - 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D - 1 >= 0 /\ A + D - 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ A + C - 2 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ A - 1 >= 0 ]
  evalNestedLoopbb8in(A, B, C, D, E, F, G, H) -> Com_1(evalNestedLoopbb9in(A, B, C, F + 1, E, F, G, H)) [ F >= 0 /\ E + F >= 0 /\ D + F >= 0 /\ -D + F >= 0 /\ C + F >= 0 /\ B + F >= 0 /\ A + F - 1 >= 0 /\ B - E >= 0 /\ E >= 0 /\ D + E >= 0 /\ C + E >= 0 /\ B + E >= 0 /\ A + E - 1 >= 0 /\ A - D - 1 >= 0 /\ D >= 0 /\ C + D >= 0 /\ B + D >= 0 /\ A + D - 1 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 ]
  evalNestedLoopreturnin(A, B, C, D, E, F, G, H) -> Com_1(evalNestedLoopstop(A, B, C, D, E, F, G, H)) [ D >= 0 /\ C + D >= 0 /\ B + D >= 0 /\ A + D >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 ]
)