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