(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f12)) (VAR A B C D E F) (RULES f12(A, B, C, D, E, F) -> Com_1(f5(4, 0, 0, D, E, F)) f5(A, B, C, D, E, F) -> Com_1(f5(A, B + 1, G, H, E, G)) [ B >= 0 /\ A + B - 4 >= 0 /\ -A + B + 4 >= 0 /\ -A + 4 >= 0 /\ A - 4 >= 0 /\ A >= B + 1 /\ C = 0 ] f5(A, B, C, D, E, F) -> Com_1(f10(A, B, C, C, C, F)) [ B >= 0 /\ A + B - 4 >= 0 /\ -A + B + 4 >= 0 /\ -A + 4 >= 0 /\ A - 4 >= 0 /\ 0 >= C + 1 ] f5(A, B, C, D, E, F) -> Com_1(f10(A, B, C, C, C, F)) [ B >= 0 /\ A + B - 4 >= 0 /\ -A + B + 4 >= 0 /\ -A + 4 >= 0 /\ A - 4 >= 0 /\ C >= 1 ] f5(A, B, C, D, E, F) -> Com_1(f11(A, B, 0, 0, 0, F)) [ B >= 0 /\ A + B - 4 >= 0 /\ -A + B + 4 >= 0 /\ -A + 4 >= 0 /\ A - 4 >= 0 /\ B >= A /\ C = 0 ] )