(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B C D) (RULES f0(A, B, C, D) -> Com_1(f10001(B, 1, C, 1)) f0(A, B, C, D) -> Com_1(f10001(B, B, C, 1)) f0(A, B, C, D) -> Com_1(f12(B, 2, C, D)) f0(A, B, C, D) -> Com_1(f110(1, 1, C, D)) f0(A, B, C, D) -> Com_1(f10001(A, 1, C, D)) f0(A, B, C, D) -> Com_1(f2(A, 2, C, D)) f0(A, B, C, D) -> Com_1(f10001(A, B, C, D)) f12(A, B, C, D) -> Com_1(f10001(A, B, C, 1)) [ -B + 2 >= 0 /\ B - 2 >= 0 ] f12(A, B, C, D) -> Com_1(f12(A, B, C, D)) [ -B + 2 >= 0 /\ B - 2 >= 0 ] f110(A, B, C, D) -> Com_1(f10001(A, B, C, 1)) [ -B + 1 >= 0 /\ A - B >= 0 /\ -A - B + 2 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 ] f110(A, B, C, D) -> Com_1(f120(A, 2, C, D)) [ -B + 1 >= 0 /\ A - B >= 0 /\ -A - B + 2 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 ] f2(A, B, C, D) -> Com_1(f1200(B, B, C, D)) [ -B + 2 >= 0 /\ B - 2 >= 0 ] f2(A, B, C, D) -> Com_1(f10001(A, B, C, D)) [ -B + 2 >= 0 /\ B - 2 >= 0 ] f2(A, B, C, D) -> Com_1(f2(A, B, C, D)) [ -B + 2 >= 0 /\ B - 2 >= 0 ] f120(A, B, C, D) -> Com_1(f10001(A, B, C, 1)) [ -B + 2 >= 0 /\ A - B + 1 >= 0 /\ -A - B + 3 >= 0 /\ B - 2 >= 0 /\ A + B - 3 >= 0 /\ -A + B - 1 >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 ] f120(A, B, C, D) -> Com_1(f120(A, B, C, D)) [ -B + 2 >= 0 /\ A - B + 1 >= 0 /\ -A - B + 3 >= 0 /\ B - 2 >= 0 /\ A + B - 3 >= 0 /\ -A + B - 1 >= 0 /\ -A + 1 >= 0 /\ A - 1 >= 0 ] f1200(A, B, C, D) -> Com_1(f10001(A, B, C, 1)) [ -B + 2 >= 0 /\ A - B >= 0 /\ -A - B + 4 >= 0 /\ B - 2 >= 0 /\ A + B - 4 >= 0 /\ -A + B >= 0 /\ -A + 2 >= 0 /\ A - 2 >= 0 ] f1200(A, B, C, D) -> Com_1(f1200(A, B, C, D)) [ -B + 2 >= 0 /\ A - B >= 0 /\ -A - B + 4 >= 0 /\ B - 2 >= 0 /\ A + B - 4 >= 0 /\ -A + B >= 0 /\ -A + 2 >= 0 /\ A - 2 >= 0 ] )