(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS start)) (VAR A B C) (RULES eval(A) -> Com_1(eval(2*C - 1)) :|: 2*C >= 2*B && 1 + 2*B >= 2*C && 2*C >= 1 && A = 2*C start(A) -> Com_1(eval(A)) )