(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B C D) (RULES f0(A, B, C, D) -> Com_1(f6(0, 0, C, D)) f6(A, B, C, D) -> Com_1(f6(A, B + 1, C, D)) [ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ C >= B + 1 ] f6(A, B, C, D) -> Com_1(f6(A + 2, B + 1, C, D)) [ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ C >= B + 1 ] f15(A, B, C, D) -> Com_1(f19(C + 1, B, C, 1)) [ B - C >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ A = C + 1 ] f15(A, B, C, D) -> Com_1(f19(A, B, C, 0)) [ B - C >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ C >= A ] f15(A, B, C, D) -> Com_1(f19(A, B, C, 0)) [ B - C >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ A >= C + 2 ] f6(A, B, C, D) -> Com_1(f15(A, B, C, D)) [ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ B >= C /\ C >= A + 1 ] f6(A, B, C, D) -> Com_1(f15(A, B, C, D)) [ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ A >= C + 1 /\ B >= C ] f6(A, B, C, D) -> Com_1(f19(A, B, A, 1)) [ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ B >= C /\ A = C ] )