(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B C D E F) (RULES f0(A, B, C, D, E, F) -> Com_1(f10(G, 0, C, D, 0, G)) f10(A, B, C, D, E, F) -> Com_1(f25(A, B, C, D, E, F)) [ -E >= 0 /\ B - E >= 0 /\ -B - E >= 0 /\ E >= 0 /\ B + E >= 0 /\ -B + E >= 0 /\ -B >= 0 /\ B >= 0 /\ A >= 1 ] f10(A, B, C, D, E, F) -> Com_1(f16(A, 0, G, G, E, F)) [ -E >= 0 /\ B - E >= 0 /\ -B - E >= 0 /\ E >= 0 /\ B + E >= 0 /\ -B + E >= 0 /\ -B >= 0 /\ B >= 0 /\ 0 >= A ] f25(A, B, C, D, E, F) -> Com_1(f25(A, B, C, D, E, F)) [ -E >= 0 /\ B - E >= 0 /\ -B - E >= 0 /\ A - E - 1 >= 0 /\ E >= 0 /\ B + E >= 0 /\ -B + E >= 0 /\ A + E - 1 >= 0 /\ -B >= 0 /\ A - B - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 ] f16(A, B, C, D, E, F) -> Com_1(f10(G, B, C, D, 0, G)) [ -E >= 0 /\ B - E >= 0 /\ -B - E >= 0 /\ -A - E >= 0 /\ E >= 0 /\ B + E >= 0 /\ -B + E >= 0 /\ -A + E >= 0 /\ -B >= 0 /\ -A - B >= 0 /\ B >= 0 /\ -A + B >= 0 /\ -A >= 0 /\ 0 >= D ] f16(A, B, C, D, E, F) -> Com_1(f16(A, B, C, D, E, F)) [ -E >= 0 /\ B - E >= 0 /\ -B - E >= 0 /\ -A - E >= 0 /\ E >= 0 /\ B + E >= 0 /\ -B + E >= 0 /\ -A + E >= 0 /\ -B >= 0 /\ -A - B >= 0 /\ B >= 0 /\ -A + B >= 0 /\ -A >= 0 /\ D >= 1 ] )