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