(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B C D E F G) (RULES f0(A, B, C, D, E, F, G) -> Com_1(f1(A, B, C, D, E, F, G)) [ A >= 0 /\ 3 >= A /\ B >= 0 /\ 3 >= B /\ 3 >= C /\ D >= 0 /\ 3 >= E /\ E >= 0 ] f1(A, B, C, D, E, F, G) -> Com_1(f2(A, B, C, D, E, D + 1, G)) [ E >= 0 /\ D + E >= 0 /\ -C + E + 3 >= 0 /\ B + E >= 0 /\ -B + E + 3 >= 0 /\ A + E >= 0 /\ -A + E + 3 >= 0 /\ D >= 0 /\ -C + D + 3 >= 0 /\ B + D >= 0 /\ -B + D + 3 >= 0 /\ A + D >= 0 /\ -A + D + 3 >= 0 /\ -C + 3 >= 0 /\ B - C + 3 >= 0 /\ -B - C + 6 >= 0 /\ A - C + 3 >= 0 /\ -A - C + 6 >= 0 /\ -B + 3 >= 0 /\ A - B + 3 >= 0 /\ -A - B + 6 >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B + 3 >= 0 /\ -A + 3 >= 0 /\ A >= 0 /\ B + 1 >= 2*D ] f1(A, B, C, D, E, F, G) -> Com_1(f2(A, B, C, D, E, D - 1, G)) [ E >= 0 /\ D + E >= 0 /\ -C + E + 3 >= 0 /\ B + E >= 0 /\ -B + E + 3 >= 0 /\ A + E >= 0 /\ -A + E + 3 >= 0 /\ D >= 0 /\ -C + D + 3 >= 0 /\ B + D >= 0 /\ -B + D + 3 >= 0 /\ A + D >= 0 /\ -A + D + 3 >= 0 /\ -C + 3 >= 0 /\ B - C + 3 >= 0 /\ -B - C + 6 >= 0 /\ A - C + 3 >= 0 /\ -A - C + 6 >= 0 /\ -B + 3 >= 0 /\ A - B + 3 >= 0 /\ -A - B + 6 >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B + 3 >= 0 /\ -A + 3 >= 0 /\ A >= 0 /\ 2*D >= B + 4 ] f1(A, B, C, D, E, F, G) -> Com_1(f2(A, B, C, D, E, D, G)) [ E >= 0 /\ D + E >= 0 /\ -C + E + 3 >= 0 /\ B + E >= 0 /\ -B + E + 3 >= 0 /\ A + E >= 0 /\ -A + E + 3 >= 0 /\ D >= 0 /\ -C + D + 3 >= 0 /\ B + D >= 0 /\ -B + D + 3 >= 0 /\ A + D >= 0 /\ -A + D + 3 >= 0 /\ -C + 3 >= 0 /\ B - C + 3 >= 0 /\ -B - C + 6 >= 0 /\ A - C + 3 >= 0 /\ -A - C + 6 >= 0 /\ -B + 3 >= 0 /\ A - B + 3 >= 0 /\ -A - B + 6 >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B + 3 >= 0 /\ -A + 3 >= 0 /\ A >= 0 /\ B + 2 = 2*D ] f1(A, B, C, D, E, F, G) -> Com_1(f2(A, B, C, D, E, D, G)) [ E >= 0 /\ D + E >= 0 /\ -C + E + 3 >= 0 /\ B + E >= 0 /\ -B + E + 3 >= 0 /\ A + E >= 0 /\ -A + E + 3 >= 0 /\ D >= 0 /\ -C + D + 3 >= 0 /\ B + D >= 0 /\ -B + D + 3 >= 0 /\ A + D >= 0 /\ -A + D + 3 >= 0 /\ -C + 3 >= 0 /\ B - C + 3 >= 0 /\ -B - C + 6 >= 0 /\ A - C + 3 >= 0 /\ -A - C + 6 >= 0 /\ -B + 3 >= 0 /\ A - B + 3 >= 0 /\ -A - B + 6 >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B + 3 >= 0 /\ -A + 3 >= 0 /\ A >= 0 /\ B + 3 = 2*D ] f2(A, B, C, D, E, F, G) -> Com_1(f3(A, B, C, D, E, F, E + 1)) [ D - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F + 2 >= 0 /\ A + F - 1 >= 0 /\ -A + F + 2 >= 0 /\ E >= 0 /\ D + E >= 0 /\ -C + E + 3 >= 0 /\ B + E >= 0 /\ -B + E + 3 >= 0 /\ A + E >= 0 /\ -A + E + 3 >= 0 /\ D >= 0 /\ -C + D + 3 >= 0 /\ B + D >= 0 /\ -B + D + 3 >= 0 /\ A + D >= 0 /\ -A + D + 3 >= 0 /\ -C + 3 >= 0 /\ B - C + 3 >= 0 /\ -B - C + 6 >= 0 /\ A - C + 3 >= 0 /\ -A - C + 6 >= 0 /\ -B + 3 >= 0 /\ A - B + 3 >= 0 /\ -A - B + 6 >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B + 3 >= 0 /\ -A + 3 >= 0 /\ A >= 0 /\ D + A >= 2*E + 1 ] f2(A, B, C, D, E, F, G) -> Com_1(f3(A, B, C, D, E, F, E - 1)) [ D - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F + 2 >= 0 /\ A + F - 1 >= 0 /\ -A + F + 2 >= 0 /\ E >= 0 /\ D + E >= 0 /\ -C + E + 3 >= 0 /\ B + E >= 0 /\ -B + E + 3 >= 0 /\ A + E >= 0 /\ -A + E + 3 >= 0 /\ D >= 0 /\ -C + D + 3 >= 0 /\ B + D >= 0 /\ -B + D + 3 >= 0 /\ A + D >= 0 /\ -A + D + 3 >= 0 /\ -C + 3 >= 0 /\ B - C + 3 >= 0 /\ -B - C + 6 >= 0 /\ A - C + 3 >= 0 /\ -A - C + 6 >= 0 /\ -B + 3 >= 0 /\ A - B + 3 >= 0 /\ -A - B + 6 >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B + 3 >= 0 /\ -A + 3 >= 0 /\ A >= 0 /\ 2*E >= D + A + 2 ] f2(A, B, C, D, E, F, G) -> Com_1(f3(A, B, C, D, E, F, E)) [ D - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F + 2 >= 0 /\ A + F - 1 >= 0 /\ -A + F + 2 >= 0 /\ E >= 0 /\ D + E >= 0 /\ -C + E + 3 >= 0 /\ B + E >= 0 /\ -B + E + 3 >= 0 /\ A + E >= 0 /\ -A + E + 3 >= 0 /\ D >= 0 /\ -C + D + 3 >= 0 /\ B + D >= 0 /\ -B + D + 3 >= 0 /\ A + D >= 0 /\ -A + D + 3 >= 0 /\ -C + 3 >= 0 /\ B - C + 3 >= 0 /\ -B - C + 6 >= 0 /\ A - C + 3 >= 0 /\ -A - C + 6 >= 0 /\ -B + 3 >= 0 /\ A - B + 3 >= 0 /\ -A - B + 6 >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B + 3 >= 0 /\ -A + 3 >= 0 /\ A >= 0 /\ D + A = 2*E ] f2(A, B, C, D, E, F, G) -> Com_1(f3(A, B, C, D, E, F, E)) [ D - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F + 2 >= 0 /\ A + F - 1 >= 0 /\ -A + F + 2 >= 0 /\ E >= 0 /\ D + E >= 0 /\ -C + E + 3 >= 0 /\ B + E >= 0 /\ -B + E + 3 >= 0 /\ A + E >= 0 /\ -A + E + 3 >= 0 /\ D >= 0 /\ -C + D + 3 >= 0 /\ B + D >= 0 /\ -B + D + 3 >= 0 /\ A + D >= 0 /\ -A + D + 3 >= 0 /\ -C + 3 >= 0 /\ B - C + 3 >= 0 /\ -B - C + 6 >= 0 /\ A - C + 3 >= 0 /\ -A - C + 6 >= 0 /\ -B + 3 >= 0 /\ A - B + 3 >= 0 /\ -A - B + 6 >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B + 3 >= 0 /\ -A + 3 >= 0 /\ A >= 0 /\ D + A + 1 = 2*E ] f3(A, B, C, D, E, F, G) -> Com_1(f1(A, B, C, F, G, F, G)) [ E - G + 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ -E + G + 1 >= 0 /\ D + G >= 0 /\ -C + G + 3 >= 0 /\ B + G >= 0 /\ -B + G + 3 >= 0 /\ A + G >= 0 /\ -A + G + 3 >= 0 /\ D - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F + 2 >= 0 /\ A + F - 1 >= 0 /\ -A + F + 2 >= 0 /\ E >= 0 /\ D + E >= 0 /\ -C + E + 3 >= 0 /\ B + E >= 0 /\ -B + E + 3 >= 0 /\ A + E >= 0 /\ -A + E + 3 >= 0 /\ D >= 0 /\ -C + D + 3 >= 0 /\ B + D >= 0 /\ -B + D + 3 >= 0 /\ A + D >= 0 /\ -A + D + 3 >= 0 /\ -C + 3 >= 0 /\ B - C + 3 >= 0 /\ -B - C + 6 >= 0 /\ A - C + 3 >= 0 /\ -A - C + 6 >= 0 /\ -B + 3 >= 0 /\ A - B + 3 >= 0 /\ -A - B + 6 >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B + 3 >= 0 /\ -A + 3 >= 0 /\ A >= 0 /\ D >= F + 1 ] f3(A, B, C, D, E, F, G) -> Com_1(f1(A, B, C, F, G, F, G)) [ E - G + 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ -E + G + 1 >= 0 /\ D + G >= 0 /\ -C + G + 3 >= 0 /\ B + G >= 0 /\ -B + G + 3 >= 0 /\ A + G >= 0 /\ -A + G + 3 >= 0 /\ D - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F + 2 >= 0 /\ A + F - 1 >= 0 /\ -A + F + 2 >= 0 /\ E >= 0 /\ D + E >= 0 /\ -C + E + 3 >= 0 /\ B + E >= 0 /\ -B + E + 3 >= 0 /\ A + E >= 0 /\ -A + E + 3 >= 0 /\ D >= 0 /\ -C + D + 3 >= 0 /\ B + D >= 0 /\ -B + D + 3 >= 0 /\ A + D >= 0 /\ -A + D + 3 >= 0 /\ -C + 3 >= 0 /\ B - C + 3 >= 0 /\ -B - C + 6 >= 0 /\ A - C + 3 >= 0 /\ -A - C + 6 >= 0 /\ -B + 3 >= 0 /\ A - B + 3 >= 0 /\ -A - B + 6 >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B + 3 >= 0 /\ -A + 3 >= 0 /\ A >= 0 /\ F >= D + 1 ] f3(A, B, C, D, E, F, G) -> Com_1(f1(A, B, C, F, G, F, G)) [ E - G + 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ -E + G + 1 >= 0 /\ D + G >= 0 /\ -C + G + 3 >= 0 /\ B + G >= 0 /\ -B + G + 3 >= 0 /\ A + G >= 0 /\ -A + G + 3 >= 0 /\ D - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F + 2 >= 0 /\ A + F - 1 >= 0 /\ -A + F + 2 >= 0 /\ E >= 0 /\ D + E >= 0 /\ -C + E + 3 >= 0 /\ B + E >= 0 /\ -B + E + 3 >= 0 /\ A + E >= 0 /\ -A + E + 3 >= 0 /\ D >= 0 /\ -C + D + 3 >= 0 /\ B + D >= 0 /\ -B + D + 3 >= 0 /\ A + D >= 0 /\ -A + D + 3 >= 0 /\ -C + 3 >= 0 /\ B - C + 3 >= 0 /\ -B - C + 6 >= 0 /\ A - C + 3 >= 0 /\ -A - C + 6 >= 0 /\ -B + 3 >= 0 /\ A - B + 3 >= 0 /\ -A - B + 6 >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B + 3 >= 0 /\ -A + 3 >= 0 /\ A >= 0 /\ E >= G + 1 ] f3(A, B, C, D, E, F, G) -> Com_1(f1(A, B, C, F, G, F, G)) [ E - G + 1 >= 0 /\ G >= 0 /\ F + G - 1 >= 0 /\ E + G >= 0 /\ -E + G + 1 >= 0 /\ D + G >= 0 /\ -C + G + 3 >= 0 /\ B + G >= 0 /\ -B + G + 3 >= 0 /\ A + G >= 0 /\ -A + G + 3 >= 0 /\ D - F + 1 >= 0 /\ F - 1 >= 0 /\ E + F - 1 >= 0 /\ D + F - 1 >= 0 /\ -D + F + 1 >= 0 /\ -C + F + 2 >= 0 /\ B + F - 1 >= 0 /\ -B + F + 2 >= 0 /\ A + F - 1 >= 0 /\ -A + F + 2 >= 0 /\ E >= 0 /\ D + E >= 0 /\ -C + E + 3 >= 0 /\ B + E >= 0 /\ -B + E + 3 >= 0 /\ A + E >= 0 /\ -A + E + 3 >= 0 /\ D >= 0 /\ -C + D + 3 >= 0 /\ B + D >= 0 /\ -B + D + 3 >= 0 /\ A + D >= 0 /\ -A + D + 3 >= 0 /\ -C + 3 >= 0 /\ B - C + 3 >= 0 /\ -B - C + 6 >= 0 /\ A - C + 3 >= 0 /\ -A - C + 6 >= 0 /\ -B + 3 >= 0 /\ A - B + 3 >= 0 /\ -A - B + 6 >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B + 3 >= 0 /\ -A + 3 >= 0 /\ A >= 0 /\ G >= E + 1 ] )