(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS evalrealshellsortstart)) (VAR A B C D E) (RULES evalrealshellsortstart(A, B, C, D, E) -> Com_1(evalrealshellsortentryin(A, B, C, D, E)) evalrealshellsortentryin(A, B, C, D, E) -> Com_1(evalrealshellsortbb8in(A, 0, C, D, E)) [ A = 0 ] evalrealshellsortentryin(A, B, C, D, E) -> Com_1(evalrealshellsortbb8in(A, F, C, D, E)) [ A >= 1 /\ F >= 0 /\ A >= 2*F /\ 2*F + 1 >= A ] evalrealshellsortentryin(A, B, C, D, E) -> Com_1(evalrealshellsortbb8in(A, F, C, D, E)) [ 0 >= A + 1 /\ 0 >= F /\ 2*F >= A /\ A + 1 >= 2*F ] evalrealshellsortbb8in(A, B, C, D, E) -> Com_1(evalrealshellsortbb6in(A, B, 0, D, E)) [ B >= 1 ] evalrealshellsortbb8in(A, B, C, D, E) -> Com_1(evalrealshellsortreturnin(A, B, C, D, E)) [ 0 >= B ] evalrealshellsortbb6in(A, B, C, D, E) -> Com_1(evalrealshellsortbb1in(A, B, C, D, E)) [ C >= 0 /\ B + C - 1 >= 0 /\ B - 1 >= 0 /\ A >= C + 1 ] evalrealshellsortbb6in(A, B, C, D, E) -> Com_1(evalrealshellsortbb7in(A, B, C, D, E)) [ C >= 0 /\ B + C - 1 >= 0 /\ B - 1 >= 0 /\ C >= A ] evalrealshellsortbb1in(A, B, C, D, E) -> Com_1(evalrealshellsortbb3in(A, B, C, F, C)) [ A - C - 1 >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ A - 1 >= 0 ] evalrealshellsortbb3in(A, B, C, D, E) -> Com_1(evalrealshellsortbb5in(A, B, C, D, E)) [ C - E >= 0 /\ A - E - 1 >= 0 /\ C + E >= 0 /\ B + E - 1 >= 0 /\ A + E - 1 >= 0 /\ A - C - 1 >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ A - 1 >= 0 /\ B >= E + 1 ] evalrealshellsortbb3in(A, B, C, D, E) -> Com_1(evalrealshellsortbb4in(A, B, C, D, E)) [ C - E >= 0 /\ A - E - 1 >= 0 /\ C + E >= 0 /\ B + E - 1 >= 0 /\ A + E - 1 >= 0 /\ A - C - 1 >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ A - 1 >= 0 /\ E >= B ] evalrealshellsortbb4in(A, B, C, D, E) -> Com_1(evalrealshellsortbb2in(A, B, C, D, E)) [ C - E >= 0 /\ A - E - 1 >= 0 /\ E - 1 >= 0 /\ C + E - 2 >= 0 /\ B + E - 2 >= 0 /\ -B + E >= 0 /\ A + E - 3 >= 0 /\ A - C - 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ A + C - 3 >= 0 /\ A - B - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 3 >= 0 /\ A - 2 >= 0 /\ F >= D + 1 ] evalrealshellsortbb4in(A, B, C, D, E) -> Com_1(evalrealshellsortbb5in(A, B, C, D, E)) [ C - E >= 0 /\ A - E - 1 >= 0 /\ E - 1 >= 0 /\ C + E - 2 >= 0 /\ B + E - 2 >= 0 /\ -B + E >= 0 /\ A + E - 3 >= 0 /\ A - C - 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ A + C - 3 >= 0 /\ A - B - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 3 >= 0 /\ A - 2 >= 0 /\ D >= F ] evalrealshellsortbb2in(A, B, C, D, E) -> Com_1(evalrealshellsortbb3in(A, B, C, D, E - B)) [ C - E >= 0 /\ A - E - 1 >= 0 /\ E - 1 >= 0 /\ C + E - 2 >= 0 /\ B + E - 2 >= 0 /\ -B + E >= 0 /\ A + E - 3 >= 0 /\ A - C - 1 >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ -B + C >= 0 /\ A + C - 3 >= 0 /\ A - B - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 3 >= 0 /\ A - 2 >= 0 ] evalrealshellsortbb5in(A, B, C, D, E) -> Com_1(evalrealshellsortbb6in(A, B, C + 1, D, E)) [ C - E >= 0 /\ A - E - 1 >= 0 /\ C + E >= 0 /\ B + E - 1 >= 0 /\ A + E - 1 >= 0 /\ A - C - 1 >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ A - 1 >= 0 ] evalrealshellsortbb7in(A, B, C, D, E) -> Com_1(evalrealshellsortbb8in(A, F, C, D, E)) [ C >= 0 /\ B + C - 1 >= 0 /\ -A + C >= 0 /\ B - 1 >= 0 /\ B >= 1 /\ F >= 0 /\ B >= 2*F /\ 2*F + 1 >= B ] evalrealshellsortreturnin(A, B, C, D, E) -> Com_1(evalrealshellsortstop(A, B, C, D, E)) [ -B >= 0 ] )