(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B C D E F G H I) (RULES f0(A, B, C, D, E, F, G, H, I) -> Com_1(f9(0, 1, 1, 0, 0, J, G, H, I)) [ J >= 1 ] f9(A, B, C, D, E, F, G, H, I) -> Com_1(f20(A, B, C - 1, D, D, 0, A - 2, 1, A - 2)) [ E >= 0 /\ D + E >= 0 /\ B + E - 1 >= 0 /\ A + E >= 0 /\ D >= 0 /\ B + D - 1 >= 0 /\ A + D >= 0 /\ B - C >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ A >= 3 /\ C >= 1 /\ D = E /\ F = 0 ] f9(A, B, C, D, E, F, G, H, I) -> Com_1(f20(A, B, C - 1, D, D, 0, A, 0, A)) [ E >= 0 /\ D + E >= 0 /\ B + E - 1 >= 0 /\ A + E >= 0 /\ D >= 0 /\ B + D - 1 >= 0 /\ A + D >= 0 /\ B - C >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ 2 >= A /\ C >= 1 /\ D = E /\ F = 0 ] f9(A, B, C, D, E, F, G, H, I) -> Com_1(f20(0, B + 1, B + 1, D, D, J, G, H, I)) [ E >= 0 /\ D + E >= 0 /\ B + E - 1 >= 0 /\ A + E >= 0 /\ D >= 0 /\ B + D - 1 >= 0 /\ A + D >= 0 /\ B - C >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ J >= 1 /\ A >= 3 /\ 0 >= C /\ D = E /\ F = 0 ] f9(A, B, C, D, E, F, G, H, I) -> Com_1(f20(A + 1, B + 1, B + 1, D, D, J, G, H, I)) [ E >= 0 /\ D + E >= 0 /\ B + E - 1 >= 0 /\ A + E >= 0 /\ D >= 0 /\ B + D - 1 >= 0 /\ A + D >= 0 /\ B - C >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ J >= 1 /\ 2 >= A /\ 0 >= C /\ D = E /\ F = 0 ] f9(A, B, C, D, E, F, G, H, I) -> Com_1(f20(A, B, C, D, D, F - 1, G, J, K)) [ E >= 0 /\ D + E >= 0 /\ B + E - 1 >= 0 /\ A + E >= 0 /\ D >= 0 /\ B + D - 1 >= 0 /\ A + D >= 0 /\ B - C >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ 0 >= F + 1 /\ D = E ] f9(A, B, C, D, E, F, G, H, I) -> Com_1(f20(A, B, C, D, D, F - 1, G, J, K)) [ E >= 0 /\ D + E >= 0 /\ B + E - 1 >= 0 /\ A + E >= 0 /\ D >= 0 /\ B + D - 1 >= 0 /\ A + D >= 0 /\ B - C >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ F >= 1 /\ D = E ] f20(A, B, C, D, E, F, G, H, I) -> Com_1(f32(A, B, C, 0, E, F, G, H, 0)) [ D - E >= 0 /\ E >= 0 /\ D + E >= 0 /\ -D + E >= 0 /\ B + E - 1 >= 0 /\ A + E >= 0 /\ D >= 0 /\ B + D - 1 >= 0 /\ A + D >= 0 /\ B - C >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ I = 0 ] f20(A, B, C, D, E, F, G, H, I) -> Com_1(f32(A, B, C, 1, E, F, G, H, I)) [ D - E >= 0 /\ E >= 0 /\ D + E >= 0 /\ -D + E >= 0 /\ B + E - 1 >= 0 /\ A + E >= 0 /\ D >= 0 /\ B + D - 1 >= 0 /\ A + D >= 0 /\ B - C >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ 0 >= I + 1 ] f20(A, B, C, D, E, F, G, H, I) -> Com_1(f32(A, B, C, 1, E, F, G, H, I)) [ D - E >= 0 /\ E >= 0 /\ D + E >= 0 /\ -D + E >= 0 /\ B + E - 1 >= 0 /\ A + E >= 0 /\ D >= 0 /\ B + D - 1 >= 0 /\ A + D >= 0 /\ B - C >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ I >= 1 ] f32(A, B, C, D, E, F, G, H, I) -> Com_1(f9(A, B, C, D, 0, F, G, 0, I)) [ E >= 0 /\ D + E >= 0 /\ -D + E + 1 >= 0 /\ B + E - 1 >= 0 /\ A + E >= 0 /\ -D + 1 >= 0 /\ B - D >= 0 /\ A - D + 1 >= 0 /\ D >= 0 /\ B + D - 1 >= 0 /\ A + D >= 0 /\ B - C >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ H = 0 ] f32(A, B, C, D, E, F, G, H, I) -> Com_1(f9(A, B, C, D, 1, F, G, H, I)) [ E >= 0 /\ D + E >= 0 /\ -D + E + 1 >= 0 /\ B + E - 1 >= 0 /\ A + E >= 0 /\ -D + 1 >= 0 /\ B - D >= 0 /\ A - D + 1 >= 0 /\ D >= 0 /\ B + D - 1 >= 0 /\ A + D >= 0 /\ B - C >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ 0 >= H + 1 ] f32(A, B, C, D, E, F, G, H, I) -> Com_1(f9(A, B, C, D, 1, F, G, H, I)) [ E >= 0 /\ D + E >= 0 /\ -D + E + 1 >= 0 /\ B + E - 1 >= 0 /\ A + E >= 0 /\ -D + 1 >= 0 /\ B - D >= 0 /\ A - D + 1 >= 0 /\ D >= 0 /\ B + D - 1 >= 0 /\ A + D >= 0 /\ B - C >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ H >= 1 ] f9(A, B, C, D, E, F, G, H, I) -> Com_1(f38(A, B, C, D, E, F, G, H, I)) [ E >= 0 /\ D + E >= 0 /\ B + E - 1 >= 0 /\ A + E >= 0 /\ D >= 0 /\ B + D - 1 >= 0 /\ A + D >= 0 /\ B - C >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ E >= D + 1 ] f9(A, B, C, D, E, F, G, H, I) -> Com_1(f38(A, B, C, D, E, F, G, H, I)) [ E >= 0 /\ D + E >= 0 /\ B + E - 1 >= 0 /\ A + E >= 0 /\ D >= 0 /\ B + D - 1 >= 0 /\ A + D >= 0 /\ B - C >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ D >= E + 1 ] )