(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 ]
  evalnestedLoopentryin(A, B, C, D, E, F, G, H) -> Com_1(evalnestedLoopreturnin(A, B, C, D, E, F, G, H)) [ 0 >= A + 1 ]
  evalnestedLoopentryin(A, B, C, D, E, F, G, H) -> Com_1(evalnestedLoopreturnin(A, B, C, D, E, F, G, H)) [ 0 >= B + 1 ]
  evalnestedLoopentryin(A, B, C, D, E, F, G, H) -> Com_1(evalnestedLoopreturnin(A, B, C, D, E, F, G, H)) [ 0 >= C + 1 ]
  evalnestedLoopbb9in(A, B, C, D, E, F, G, H) -> Com_1(evalnestedLoopbb7in(A, B, C, D, 0, D, 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 ]
  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 ]
  evalnestedLoopbb7in(A, B, C, D, E, F, G, H) -> Com_1(evalnestedLoopbb4in(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(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 ]
  evalnestedLoopbb4in(A, B, C, D, E, F, G, H) -> Com_1(evalnestedLoopbb6in(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 ]
  evalnestedLoopbb6in(A, B, C, D, E, F, G, H) -> Com_1(evalnestedLoopbb5in(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 ]
  evalnestedLoopbb6in(A, B, C, D, E, F, G, H) -> Com_1(evalnestedLoopbb7in(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 ]
  evalnestedLoopbb5in(A, B, C, D, E, F, G, H) -> Com_1(evalnestedLoopbb6in(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 /\ -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))
)