(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS evalrealselectstart)) (VAR A B C) (RULES evalrealselectstart(A, B, C) -> Com_1(evalrealselectentryin(A, B, C)) evalrealselectentryin(A, B, C) -> Com_1(evalrealselectbb6in(0, B, C)) evalrealselectbb6in(A, B, C) -> Com_1(evalrealselectbbin(A, B, C)) [ A >= 0 /\ B >= A + 2 ] evalrealselectbb6in(A, B, C) -> Com_1(evalrealselectreturnin(A, B, C)) [ A >= 0 /\ A + 1 >= B ] evalrealselectbbin(A, B, C) -> Com_1(evalrealselectbb4in(A, B, A + 1)) [ B - 2 >= 0 /\ A + B - 2 >= 0 /\ -A + B - 2 >= 0 /\ A >= 0 ] evalrealselectbb4in(A, B, C) -> Com_1(evalrealselectbb1in(A, B, C)) [ 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 /\ B >= C + 1 ] evalrealselectbb4in(A, B, C) -> Com_1(evalrealselectbb5in(A, B, C)) [ 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 /\ C >= B ] evalrealselectbb1in(A, B, C) -> Com_1(evalrealselectbb4in(A, B, C + 1)) [ 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 /\ D >= E + 1 ] evalrealselectbb1in(A, B, C) -> Com_1(evalrealselectbb4in(A, B, C + 1)) [ 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 >= D ] evalrealselectbb5in(A, B, C) -> Com_1(evalrealselectbb6in(A + 1, B, C)) [ C - 2 >= 0 /\ B + C - 4 >= 0 /\ -B + C >= 0 /\ A + C - 2 >= 0 /\ -A + C - 2 >= 0 /\ B - 2 >= 0 /\ A + B - 2 >= 0 /\ -A + B - 2 >= 0 /\ A >= 0 ] evalrealselectreturnin(A, B, C) -> Com_1(evalrealselectstop(A, B, C)) [ A - B + 1 >= 0 /\ A >= 0 ] )