(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B C D E F) (RULES f5(A, B, C, D, E, F) -> Com_1(f7(A, B, C, D, E, F)) [ E >= 0 /\ B + E >= 0 /\ -A + E + 4 >= 0 /\ -A - B + 4 >= 0 /\ B >= 0 /\ -A + B + 4 >= 0 /\ -A + 4 >= 0 /\ 0 >= A ] f5(A, B, C, D, E, F) -> Com_1(f7(A, B, C, D, E, F)) [ E >= 0 /\ B + E >= 0 /\ -A + E + 4 >= 0 /\ -A - B + 4 >= 0 /\ B >= 0 /\ -A + B + 4 >= 0 /\ -A + 4 >= 0 /\ A >= 2 ] f7(A, B, C, D, E, F) -> Com_1(f9(A, 0, C, D, E, F)) [ E >= 0 /\ B + E >= 0 /\ -A + E + 4 >= 0 /\ -A - B + 4 >= 0 /\ B >= 0 /\ -A + B + 4 >= 0 /\ -A + 4 >= 0 /\ B = 0 ] f16(A, B, C, D, E, F) -> Com_1(f5(A, B, C, G, E, F)) [ D - F - 1 >= 0 /\ -E + 2 >= 0 /\ B - E + 2 >= 0 /\ -A - E + 6 >= 0 /\ E - 2 >= 0 /\ B + E - 2 >= 0 /\ -A + E + 2 >= 0 /\ -A - B + 4 >= 0 /\ B >= 0 /\ -A + B + 4 >= 0 /\ -A + 4 >= 0 /\ 255 >= C ] f25(A, B, C, D, E, F) -> Com_1(f5(A, B, C, G, E, F)) [ -D + F - 1 >= 0 /\ -E + 1 >= 0 /\ B - E + 1 >= 0 /\ -A - E + 5 >= 0 /\ E - 1 >= 0 /\ B + E - 1 >= 0 /\ -A + E + 3 >= 0 /\ -A - B + 4 >= 0 /\ B >= 0 /\ -A + B + 4 >= 0 /\ -A + 4 >= 0 /\ C >= 0 ] f0(A, B, C, D, E, F) -> Com_1(f5(4, 0, C, G, 0, F)) f7(A, B, C, D, E, F) -> Com_1(f9(A - 1, B, C, D, E, F)) [ E >= 0 /\ B + E >= 0 /\ -A + E + 4 >= 0 /\ -A - B + 4 >= 0 /\ B >= 0 /\ -A + B + 4 >= 0 /\ -A + 4 >= 0 /\ B >= 1 ] f9(A, B, C, D, E, F) -> Com_1(f16(A, B, C + A, D, 2, F)) [ E >= 0 /\ B + E >= 0 /\ -A + E + 4 >= 0 /\ -A - B + 4 >= 0 /\ B >= 0 /\ -A + B + 4 >= 0 /\ -A + 4 >= 0 /\ 0 >= E /\ D >= F + 1 ] f9(A, B, C, D, E, F) -> Com_1(f16(A, B, C + A, D, 2, F)) [ E >= 0 /\ B + E >= 0 /\ -A + E + 4 >= 0 /\ -A - B + 4 >= 0 /\ B >= 0 /\ -A + B + 4 >= 0 /\ -A + 4 >= 0 /\ E >= 2 /\ D >= F + 1 ] f9(A, B, C, D, E, F) -> Com_1(f16(A, B, C + A, D, 2, F)) [ E >= 0 /\ B + E >= 0 /\ -A + E + 4 >= 0 /\ -A - B + 4 >= 0 /\ B >= 0 /\ -A + B + 4 >= 0 /\ -A + 4 >= 0 /\ B >= 1 /\ D >= F + 1 /\ E = 1 ] f9(A, B, C, D, E, F) -> Com_1(f16(A - 1, 1, C + A - 1, D, 2, F)) [ E >= 0 /\ B + E >= 0 /\ -A + E + 4 >= 0 /\ -A - B + 4 >= 0 /\ B >= 0 /\ -A + B + 4 >= 0 /\ -A + 4 >= 0 /\ D >= F + 1 /\ B = 0 /\ E = 1 ] f9(A, B, C, D, E, F) -> Com_1(f25(A, B, C - A, D, 1, F)) [ E >= 0 /\ B + E >= 0 /\ -A + E + 4 >= 0 /\ -A - B + 4 >= 0 /\ B >= 0 /\ -A + B + 4 >= 0 /\ -A + 4 >= 0 /\ 1 >= E /\ F >= D + 1 ] f9(A, B, C, D, E, F) -> Com_1(f25(A, B, C - A, D, 1, F)) [ E >= 0 /\ B + E >= 0 /\ -A + E + 4 >= 0 /\ -A - B + 4 >= 0 /\ B >= 0 /\ -A + B + 4 >= 0 /\ -A + 4 >= 0 /\ E >= 3 /\ F >= D + 1 ] f9(A, B, C, D, E, F) -> Com_1(f25(A, B, C - A, D, 1, F)) [ E >= 0 /\ B + E >= 0 /\ -A + E + 4 >= 0 /\ -A - B + 4 >= 0 /\ B >= 0 /\ -A + B + 4 >= 0 /\ -A + 4 >= 0 /\ B >= 1 /\ F >= D + 1 /\ E = 2 ] f9(A, B, C, D, E, F) -> Com_1(f25(A - 1, 1, C - A + 1, D, 1, F)) [ E >= 0 /\ B + E >= 0 /\ -A + E + 4 >= 0 /\ -A - B + 4 >= 0 /\ B >= 0 /\ -A + B + 4 >= 0 /\ -A + 4 >= 0 /\ F >= D + 1 /\ B = 0 /\ E = 2 ] f5(A, B, C, D, E, F) -> Com_1(f30(1, B, C, D, E, F)) [ E >= 0 /\ B + E >= 0 /\ -A + E + 4 >= 0 /\ -A - B + 4 >= 0 /\ B >= 0 /\ -A + B + 4 >= 0 /\ -A + 4 >= 0 /\ A = 1 ] f16(A, B, C, D, E, F) -> Com_1(f30(A, B, C, D, E, F)) [ D - F - 1 >= 0 /\ -E + 2 >= 0 /\ B - E + 2 >= 0 /\ -A - E + 6 >= 0 /\ E - 2 >= 0 /\ B + E - 2 >= 0 /\ -A + E + 2 >= 0 /\ -A - B + 4 >= 0 /\ B >= 0 /\ -A + B + 4 >= 0 /\ -A + 4 >= 0 /\ C >= 256 ] f25(A, B, C, D, E, F) -> Com_1(f30(A, B, C, D, E, F)) [ -D + F - 1 >= 0 /\ -E + 1 >= 0 /\ B - E + 1 >= 0 /\ -A - E + 5 >= 0 /\ E - 1 >= 0 /\ B + E - 1 >= 0 /\ -A + E + 3 >= 0 /\ -A - B + 4 >= 0 /\ B >= 0 /\ -A + B + 4 >= 0 /\ -A + 4 >= 0 /\ 0 >= C + 1 ] f9(A, B, C, D, E, F) -> Com_1(f30(A, B, C, D, E, D)) [ E >= 0 /\ B + E >= 0 /\ -A + E + 4 >= 0 /\ -A - B + 4 >= 0 /\ B >= 0 /\ -A + B + 4 >= 0 /\ -A + 4 >= 0 /\ D = F ] )