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