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