(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS evalEx1start)) (VAR A B C D) (RULES evalEx1start(A, B, C, D) -> Com_1(evalEx1entryin(A, B, C, D)) evalEx1entryin(A, B, C, D) -> Com_1(evalEx1bb6in(0, A, C, D)) evalEx1bb6in(A, B, C, D) -> Com_1(evalEx1bbin(A, B, C, D)) [ A >= 0 /\ B >= A + 1 ] evalEx1bb6in(A, B, C, D) -> Com_1(evalEx1returnin(A, B, C, D)) [ A >= 0 /\ A >= B ] evalEx1bbin(A, B, C, D) -> Com_1(evalEx1bb4in(A, B, A + 1, B)) [ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 ] evalEx1bb4in(A, B, C, D) -> Com_1(evalEx1bb1in(A, B, C, D)) [ B - D >= 0 /\ D - 1 >= 0 /\ C + D - 2 >= 0 /\ -C + D >= 0 /\ B + D - 2 >= 0 /\ A + D - 1 >= 0 /\ -A + D - 1 >= 0 /\ B - C >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ A + C - 1 >= 0 /\ -A + C - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ D >= C + 1 ] evalEx1bb4in(A, B, C, D) -> Com_1(evalEx1bb5in(A, B, C, D)) [ B - D >= 0 /\ D - 1 >= 0 /\ C + D - 2 >= 0 /\ -C + D >= 0 /\ B + D - 2 >= 0 /\ A + D - 1 >= 0 /\ -A + D - 1 >= 0 /\ B - C >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ A + C - 1 >= 0 /\ -A + C - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ C >= D ] evalEx1bb1in(A, B, C, D) -> Com_1(evalEx1bb4in(A, B, C, D - 1)) [ B - D >= 0 /\ D - 2 >= 0 /\ C + D - 3 >= 0 /\ -C + D - 1 >= 0 /\ B + D - 4 >= 0 /\ A + D - 2 >= 0 /\ -A + D - 2 >= 0 /\ B - C - 1 >= 0 /\ C - 1 >= 0 /\ B + C - 3 >= 0 /\ A + C - 1 >= 0 /\ -A + C - 1 >= 0 /\ B - 2 >= 0 /\ A + B - 2 >= 0 /\ -A + B - 2 >= 0 /\ A >= 0 /\ 0 >= E + 1 ] evalEx1bb1in(A, B, C, D) -> Com_1(evalEx1bb4in(A, B, C, D - 1)) [ B - D >= 0 /\ D - 2 >= 0 /\ C + D - 3 >= 0 /\ -C + D - 1 >= 0 /\ B + D - 4 >= 0 /\ A + D - 2 >= 0 /\ -A + D - 2 >= 0 /\ B - C - 1 >= 0 /\ C - 1 >= 0 /\ B + C - 3 >= 0 /\ A + C - 1 >= 0 /\ -A + C - 1 >= 0 /\ B - 2 >= 0 /\ A + B - 2 >= 0 /\ -A + B - 2 >= 0 /\ A >= 0 /\ E >= 1 ] evalEx1bb1in(A, B, C, D) -> Com_1(evalEx1bb4in(A, B, C + 1, D)) [ B - D >= 0 /\ D - 2 >= 0 /\ C + D - 3 >= 0 /\ -C + D - 1 >= 0 /\ B + D - 4 >= 0 /\ A + D - 2 >= 0 /\ -A + D - 2 >= 0 /\ B - C - 1 >= 0 /\ C - 1 >= 0 /\ B + C - 3 >= 0 /\ A + C - 1 >= 0 /\ -A + C - 1 >= 0 /\ B - 2 >= 0 /\ A + B - 2 >= 0 /\ -A + B - 2 >= 0 /\ A >= 0 ] evalEx1bb5in(A, B, C, D) -> Com_1(evalEx1bb6in(A + 1, D, C, D)) [ C - D >= 0 /\ B - D >= 0 /\ D - 1 >= 0 /\ C + D - 2 >= 0 /\ -C + D >= 0 /\ B + D - 2 >= 0 /\ A + D - 1 >= 0 /\ -A + D - 1 >= 0 /\ B - C >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ A + C - 1 >= 0 /\ -A + C - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 ] evalEx1returnin(A, B, C, D) -> Com_1(evalEx1stop(A, B, C, D)) [ A - B >= 0 /\ A >= 0 ] )