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