(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS start)) (VAR A) (RULES start(A) -> Com_1(eval(A)) eval(A) -> Com_1(eval(2*C - 1)) [ 2*C >= 2*B /\ 2*B + 1 >= 2*C /\ 2*C >= 1 /\ A = 2*C ] )