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