(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS evalwcet1start)) (VAR A B C D) (RULES evalwcet1start(A, B, C, D) -> Com_1(evalwcet1entryin(A, B, C, D)) evalwcet1entryin(A, B, C, D) -> Com_1(evalwcet1bbin(A, 0, A, D)) [ A >= 1 ] evalwcet1entryin(A, B, C, D) -> Com_1(evalwcet1returnin(A, B, C, D)) [ 0 >= A ] evalwcet1bbin(A, B, C, D) -> Com_1(evalwcet1bb1in(A, B, C, D)) [ A - C >= 0 /\ C - 1 >= 0 /\ B + C - 1 >= 0 /\ A + C - 2 >= 0 /\ A - B - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 /\ 0 >= E + 1 ] evalwcet1bbin(A, B, C, D) -> Com_1(evalwcet1bb1in(A, B, C, D)) [ A - C >= 0 /\ C - 1 >= 0 /\ B + C - 1 >= 0 /\ A + C - 2 >= 0 /\ A - B - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 /\ E >= 1 ] evalwcet1bbin(A, B, C, D) -> Com_1(evalwcet1bb4in(A, B, C, D)) [ A - C >= 0 /\ C - 1 >= 0 /\ B + C - 1 >= 0 /\ A + C - 2 >= 0 /\ A - B - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 ] evalwcet1bb1in(A, B, C, D) -> Com_1(evalwcet1bb6in(A, B, C, 0)) [ A - C >= 0 /\ C - 1 >= 0 /\ B + C - 1 >= 0 /\ A + C - 2 >= 0 /\ A - B - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 /\ B + 1 >= A ] evalwcet1bb1in(A, B, C, D) -> Com_1(evalwcet1bb6in(A, B, C, B + 1)) [ A - C >= 0 /\ C - 1 >= 0 /\ B + C - 1 >= 0 /\ A + C - 2 >= 0 /\ A - B - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 /\ A >= B + 2 ] evalwcet1bb4in(A, B, C, D) -> Com_1(evalwcet1bb5in(A, B, C, D)) [ A - C >= 0 /\ C - 1 >= 0 /\ B + C - 1 >= 0 /\ A + C - 2 >= 0 /\ A - B - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 /\ 1 >= B ] evalwcet1bb4in(A, B, C, D) -> Com_1(evalwcet1bb6in(A, B, C, B - 1)) [ A - C >= 0 /\ C - 1 >= 0 /\ B + C - 1 >= 0 /\ A + C - 2 >= 0 /\ A - B - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 /\ B >= 2 ] evalwcet1bb5in(A, B, C, D) -> Com_1(evalwcet1bb6in(A, B, C, 0)) [ A - C >= 0 /\ C - 1 >= 0 /\ B + C - 1 >= 0 /\ -B + C >= 0 /\ A + C - 2 >= 0 /\ -B + 1 >= 0 /\ A - B - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 ] evalwcet1bb6in(A, B, C, D) -> Com_1(evalwcet1bbin(A, D, C - 1, D)) [ B - D + 1 >= 0 /\ A - D - 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ A + D - 1 >= 0 /\ A - C >= 0 /\ C - 1 >= 0 /\ B + C - 1 >= 0 /\ A + C - 2 >= 0 /\ A - B - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 /\ C >= 2 ] evalwcet1bb6in(A, B, C, D) -> Com_1(evalwcet1returnin(A, B, C, D)) [ B - D + 1 >= 0 /\ A - D - 1 >= 0 /\ D >= 0 /\ C + D - 1 >= 0 /\ B + D >= 0 /\ A + D - 1 >= 0 /\ A - C >= 0 /\ C - 1 >= 0 /\ B + C - 1 >= 0 /\ A + C - 2 >= 0 /\ A - B - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 /\ 1 >= C ] evalwcet1returnin(A, B, C, D) -> Com_1(evalwcet1stop(A, B, C, D)) )