(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS eval0)) (VAR A B C D) (RULES eval0(A, B, C, D) -> Com_1(eval1(B, B, 1, D)) eval1(A, B, C, D) -> Com_1(end(A, B, C, D)) [ -C + 1 >= 0 /\ C - 1 >= 0 /\ A - B >= 0 /\ -A + B >= 0 /\ A >= 101 ] eval1(A, B, C, D) -> Com_1(eval3(A, B, C, D)) [ -C + 1 >= 0 /\ C - 1 >= 0 /\ A - B >= 0 /\ -A + B >= 0 /\ 100 >= A ] eval3(A, B, C, D) -> Com_1(eval3(A + 11, B, C + 1, D)) [ C - 1 >= 0 /\ -B + C + 99 >= 0 /\ -B + 100 >= 0 /\ A - B >= 0 /\ 100 >= A ] eval3(A, B, C, D) -> Com_1(eval5(A, B, C, D)) [ C - 1 >= 0 /\ -B + C + 99 >= 0 /\ -B + 100 >= 0 /\ A - B >= 0 /\ A >= 101 ] eval5(A, B, C, D) -> Com_1(eval7(A - 10, B, C - 1, D)) [ C - 1 >= 0 /\ -B + C + 99 >= 0 /\ A + C - 102 >= 0 /\ -B + 100 >= 0 /\ A - B - 1 >= 0 /\ A - 101 >= 0 /\ C >= 2 ] eval7(A, B, C, D) -> Com_1(eval5(A, B, C, A - 10)) [ C - 1 >= 0 /\ -B + C + 99 >= 0 /\ A + C - 92 >= 0 /\ -B + 100 >= 0 /\ A - B + 9 >= 0 /\ A - 91 >= 0 /\ A >= 101 /\ C = 1 ] eval7(A, B, C, D) -> Com_1(eval9(A, B, C, D)) [ C - 1 >= 0 /\ -B + C + 99 >= 0 /\ A + C - 92 >= 0 /\ -B + 100 >= 0 /\ A - B + 9 >= 0 /\ A - 91 >= 0 /\ 100 >= A ] eval7(A, B, C, D) -> Com_1(eval9(A, B, C, D)) [ C - 1 >= 0 /\ -B + C + 99 >= 0 /\ A + C - 92 >= 0 /\ -B + 100 >= 0 /\ A - B + 9 >= 0 /\ A - 91 >= 0 /\ 2 >= C ] eval7(A, B, C, D) -> Com_1(eval9(A, B, C, D)) [ C - 1 >= 0 /\ -B + C + 99 >= 0 /\ A + C - 92 >= 0 /\ -B + 100 >= 0 /\ A - B + 9 >= 0 /\ A - 91 >= 0 /\ C >= 0 ] eval9(A, B, C, D) -> Com_1(eval11(A - 10, B, C - 1, D)) [ C - 1 >= 0 /\ -B + C + 99 >= 0 /\ A + C - 92 >= 0 /\ -B + 100 >= 0 /\ A - B + 9 >= 0 /\ A - 91 >= 0 /\ A >= 101 ] eval9(A, B, C, D) -> Com_1(eval11(A, B, C, D)) [ C - 1 >= 0 /\ -B + C + 99 >= 0 /\ A + C - 92 >= 0 /\ -B + 100 >= 0 /\ A - B + 9 >= 0 /\ A - 91 >= 0 /\ 100 >= A ] eval11(A, B, C, D) -> Com_1(eval5(A + 11, B, C + 1, D)) [ C >= 0 /\ -B + C + 100 >= 0 /\ A + C - 91 >= 0 /\ -B + 100 >= 0 /\ A - B + 9 >= 0 /\ A - 91 >= 0 ] )