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