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