(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B C D E F G) (RULES f0(A, B, C, D, E, F, G) -> Com_1(f64(5, 18, 0, 0, E, F, G)) f64(A, B, C, D, E, F, G) -> Com_1(f64(A, B, C, C + 1, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 18 >= 0 /\ -B + D + 18 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 18 >= 0 /\ -B - C + 18 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 18 >= 0 /\ -B + C + 18 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 18 >= 0 /\ A - B + 13 >= 0 /\ -A - B + 23 >= 0 /\ B - 18 >= 0 /\ A + B - 23 >= 0 /\ -A + B - 13 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ A >= D + 1 /\ C = D ] f64(A, B, C, D, E, F, G) -> Com_1(f72(A, B, C, 0, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 18 >= 0 /\ -B + D + 18 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 18 >= 0 /\ -B - C + 18 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 18 >= 0 /\ -B + C + 18 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 18 >= 0 /\ A - B + 13 >= 0 /\ -A - B + 23 >= 0 /\ B - 18 >= 0 /\ A + B - 23 >= 0 /\ -A + B - 13 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ D >= A ] f64(A, B, C, D, E, F, G) -> Com_1(f64(A, B, C, D + 1, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 18 >= 0 /\ -B + D + 18 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 18 >= 0 /\ -B - C + 18 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 18 >= 0 /\ -B + C + 18 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 18 >= 0 /\ A - B + 13 >= 0 /\ -A - B + 23 >= 0 /\ B - 18 >= 0 /\ A + B - 23 >= 0 /\ -A + B - 13 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ A >= D + 1 /\ D >= C + 1 ] f72(A, B, C, D, E, F, G) -> Com_1(f86(A, B, C, 0, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 18 >= 0 /\ -B + D + 18 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 18 >= 0 /\ -B - C + 18 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 18 >= 0 /\ -B + C + 18 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 18 >= 0 /\ A - B + 13 >= 0 /\ -A - B + 23 >= 0 /\ B - 18 >= 0 /\ A + B - 23 >= 0 /\ -A + B - 13 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ D >= A ] f72(A, B, C, D, E, F, G) -> Com_1(f75(A, B, C, D, 0, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 18 >= 0 /\ -B + D + 18 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 18 >= 0 /\ -B - C + 18 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 18 >= 0 /\ -B + C + 18 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 18 >= 0 /\ A - B + 13 >= 0 /\ -A - B + 23 >= 0 /\ B - 18 >= 0 /\ A + B - 23 >= 0 /\ -A + B - 13 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ A >= D + 1 ] f86(A, B, C, D, E, F, G) -> Com_1(f96(A, B, C, 0, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 18 >= 0 /\ -B + D + 18 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 18 >= 0 /\ -B - C + 18 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 18 >= 0 /\ -B + C + 18 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 18 >= 0 /\ A - B + 13 >= 0 /\ -A - B + 23 >= 0 /\ B - 18 >= 0 /\ A + B - 23 >= 0 /\ -A + B - 13 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ D >= B ] f86(A, B, C, D, E, F, G) -> Com_1(f86(A, B, C, D + 1, E, H, I)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 18 >= 0 /\ -B + D + 18 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 18 >= 0 /\ -B - C + 18 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 18 >= 0 /\ -B + C + 18 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 18 >= 0 /\ A - B + 13 >= 0 /\ -A - B + 23 >= 0 /\ B - 18 >= 0 /\ A + B - 23 >= 0 /\ -A + B - 13 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ B >= D + 1 ] f86(A, B, C, D, E, F, G) -> Com_1(f92(A, B, C, D, E, H, I)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 18 >= 0 /\ -B + D + 18 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 18 >= 0 /\ -B - C + 18 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 18 >= 0 /\ -B + C + 18 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 18 >= 0 /\ A - B + 13 >= 0 /\ -A - B + 23 >= 0 /\ B - 18 >= 0 /\ A + B - 23 >= 0 /\ -A + B - 13 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ B >= D + 1 ] f75(A, B, C, D, E, F, G) -> Com_1(f72(A, B, C, D + 1, E, F, G)) [ E >= 0 /\ D + E >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ B + E - 18 >= 0 /\ -B + E + 18 >= 0 /\ A + E - 5 >= 0 /\ -A + E + 5 >= 0 /\ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 18 >= 0 /\ -B + D + 18 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 18 >= 0 /\ -B - C + 18 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 18 >= 0 /\ -B + C + 18 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 18 >= 0 /\ A - B + 13 >= 0 /\ -A - B + 23 >= 0 /\ B - 18 >= 0 /\ A + B - 23 >= 0 /\ -A + B - 13 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ E >= B ] f75(A, B, C, D, E, F, G) -> Com_1(f75(A, B, C, D, E + 1, H, I)) [ E >= 0 /\ D + E >= 0 /\ C + E >= 0 /\ -C + E >= 0 /\ B + E - 18 >= 0 /\ -B + E + 18 >= 0 /\ A + E - 5 >= 0 /\ -A + E + 5 >= 0 /\ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 18 >= 0 /\ -B + D + 18 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 18 >= 0 /\ -B - C + 18 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 18 >= 0 /\ -B + C + 18 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 18 >= 0 /\ A - B + 13 >= 0 /\ -A - B + 23 >= 0 /\ B - 18 >= 0 /\ A + B - 23 >= 0 /\ -A + B - 13 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ B >= E + 1 ] f96(A, B, C, D, E, F, G) -> Com_1(f92(A, B, C, D, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 18 >= 0 /\ -B + D + 18 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 18 >= 0 /\ -B - C + 18 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 18 >= 0 /\ -B + C + 18 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 18 >= 0 /\ A - B + 13 >= 0 /\ -A - B + 23 >= 0 /\ B - 18 >= 0 /\ A + B - 23 >= 0 /\ -A + B - 13 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ D >= A ] f96(A, B, C, D, E, F, G) -> Com_1(f96(A, B, C, D + 1, E, F, G)) [ D >= 0 /\ C + D >= 0 /\ -C + D >= 0 /\ B + D - 18 >= 0 /\ -B + D + 18 >= 0 /\ A + D - 5 >= 0 /\ -A + D + 5 >= 0 /\ -C >= 0 /\ B - C - 18 >= 0 /\ -B - C + 18 >= 0 /\ A - C - 5 >= 0 /\ -A - C + 5 >= 0 /\ C >= 0 /\ B + C - 18 >= 0 /\ -B + C + 18 >= 0 /\ A + C - 5 >= 0 /\ -A + C + 5 >= 0 /\ -B + 18 >= 0 /\ A - B + 13 >= 0 /\ -A - B + 23 >= 0 /\ B - 18 >= 0 /\ A + B - 23 >= 0 /\ -A + B - 13 >= 0 /\ -A + 5 >= 0 /\ A - 5 >= 0 /\ A >= D + 1 ] )