(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f9)) (VAR A B C D E F G H I J K L M N O P Q R S T U V W X Y Z A1 B1 C1 D1 E1 F1 G1 H1 I1 J1 K1) (RULES f9(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1) -> Com_1(f10(S1, 0, C, L1, 0, F, G, H, I, J, K, L, M, N, O, P, Q1, X1, A2, Z1, U, V, Y1, B2, C2, Z, R1, B1, M1, N1, O1, P1, D2, H1, I1, T1, K1)) [ 0 >= U1 /\ 0 >= V1 /\ 0 >= L1 /\ 0 >= W1 ] f9(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1) -> Com_1(f1(2, B, C, L1, E, F, G, H, I, J, K, L, M, N, O, P, L1, O1, P1, O1, U, V, O1, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, N1, M1)) [ L1 >= 2 ] f1(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1) -> Com_1(f16(H, R, 0, L1, R, F, G, H, I, J, K, L, M, N, O, P, N1, O1, R1, M1, U, V, P1, S1, T1, Q1, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1)) [ Q - 2 >= 0 /\ A + Q - 4 >= 0 /\ -A + Q >= 0 /\ A - 2 >= 0 /\ A >= Q /\ A >= 0 /\ L1 >= 2 /\ R >= 1 /\ Q1 >= L1 /\ H >= L1 /\ C = 0 ] f1(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1) -> Com_1(f16(H, R, 0, L1, R, F, G, H, I, J, K, L, M, N, O, P, N1, O1, R1, M1, U, V, P1, S1, T1, Q1, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1)) [ Q - 2 >= 0 /\ A + Q - 4 >= 0 /\ -A + Q >= 0 /\ A - 2 >= 0 /\ A >= Q /\ A >= 0 /\ L1 >= 2 /\ 0 >= R + 1 /\ Q1 >= L1 /\ H >= L1 /\ C = 0 ] f1(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1) -> Com_1(f1(A + 1, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, S, L1, S, N1, A, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1)) [ Q - 2 >= 0 /\ A + Q - 4 >= 0 /\ -A + Q >= 0 /\ A - 2 >= 0 /\ Q >= A + 1 /\ A >= 0 ] f16(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1) -> Com_1(f16(A, B, C + 1, L1, N1, O1, G, H - 1, I, J, K, L, B, P1, C + 1, H - 1, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1)) [ A - H >= 0 /\ C + H - 2 >= 0 /\ D - 2 >= 0 /\ C + D - 2 >= 0 /\ Z + D - 4 >= 0 /\ A + D - 4 >= 0 /\ C >= 0 /\ Z + C - 2 >= 0 /\ A + C - 2 >= 0 /\ Z - 2 >= 0 /\ A + Z - 4 >= 0 /\ A - 2 >= 0 /\ H >= 0 /\ L1 >= 2 /\ M1 >= 1 /\ N1 >= 1 /\ P1 >= 1 ] f16(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1) -> Com_1(f16(A, B, C + 1, L1, N1, O1, G, H - 1, I, J, K, L, B, P1, C + 1, H - 1, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1)) [ A - H >= 0 /\ C + H - 2 >= 0 /\ D - 2 >= 0 /\ C + D - 2 >= 0 /\ Z + D - 4 >= 0 /\ A + D - 4 >= 0 /\ C >= 0 /\ Z + C - 2 >= 0 /\ A + C - 2 >= 0 /\ Z - 2 >= 0 /\ A + Z - 4 >= 0 /\ A - 2 >= 0 /\ H >= 0 /\ L1 >= 2 /\ M1 >= 1 /\ N1 >= 1 /\ 0 >= P1 + 1 ] f16(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1) -> Com_1(f16(A, B, C + 1, L1, N1, O1, G, H - 1, I, J, K, L, B, P1, C + 1, H - 1, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1)) [ A - H >= 0 /\ C + H - 2 >= 0 /\ D - 2 >= 0 /\ C + D - 2 >= 0 /\ Z + D - 4 >= 0 /\ A + D - 4 >= 0 /\ C >= 0 /\ Z + C - 2 >= 0 /\ A + C - 2 >= 0 /\ Z - 2 >= 0 /\ A + Z - 4 >= 0 /\ A - 2 >= 0 /\ H >= 0 /\ L1 >= 2 /\ M1 >= 1 /\ 0 >= N1 + 1 /\ P1 >= 1 ] f16(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1) -> Com_1(f16(A, B, C + 1, L1, N1, O1, G, H - 1, I, J, K, L, B, P1, C + 1, H - 1, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1)) [ A - H >= 0 /\ C + H - 2 >= 0 /\ D - 2 >= 0 /\ C + D - 2 >= 0 /\ Z + D - 4 >= 0 /\ A + D - 4 >= 0 /\ C >= 0 /\ Z + C - 2 >= 0 /\ A + C - 2 >= 0 /\ Z - 2 >= 0 /\ A + Z - 4 >= 0 /\ A - 2 >= 0 /\ H >= 0 /\ L1 >= 2 /\ M1 >= 1 /\ 0 >= N1 + 1 /\ 0 >= P1 + 1 ] f16(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1) -> Com_1(f16(A, B, C + 1, L1, N1, O1, G, H - 1, I, J, K, L, B, P1, C + 1, H - 1, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1)) [ A - H >= 0 /\ C + H - 2 >= 0 /\ D - 2 >= 0 /\ C + D - 2 >= 0 /\ Z + D - 4 >= 0 /\ A + D - 4 >= 0 /\ C >= 0 /\ Z + C - 2 >= 0 /\ A + C - 2 >= 0 /\ Z - 2 >= 0 /\ A + Z - 4 >= 0 /\ A - 2 >= 0 /\ H >= 0 /\ L1 >= 2 /\ 0 >= M1 + 1 /\ N1 >= 1 /\ P1 >= 1 ] f16(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1) -> Com_1(f16(A, B, C + 1, L1, N1, O1, G, H - 1, I, J, K, L, B, P1, C + 1, H - 1, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1)) [ A - H >= 0 /\ C + H - 2 >= 0 /\ D - 2 >= 0 /\ C + D - 2 >= 0 /\ Z + D - 4 >= 0 /\ A + D - 4 >= 0 /\ C >= 0 /\ Z + C - 2 >= 0 /\ A + C - 2 >= 0 /\ Z - 2 >= 0 /\ A + Z - 4 >= 0 /\ A - 2 >= 0 /\ H >= 0 /\ L1 >= 2 /\ 0 >= M1 + 1 /\ N1 >= 1 /\ 0 >= P1 + 1 ] f16(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1) -> Com_1(f16(A, B, C + 1, L1, N1, O1, G, H - 1, I, J, K, L, B, P1, C + 1, H - 1, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1)) [ A - H >= 0 /\ C + H - 2 >= 0 /\ D - 2 >= 0 /\ C + D - 2 >= 0 /\ Z + D - 4 >= 0 /\ A + D - 4 >= 0 /\ C >= 0 /\ Z + C - 2 >= 0 /\ A + C - 2 >= 0 /\ Z - 2 >= 0 /\ A + Z - 4 >= 0 /\ A - 2 >= 0 /\ H >= 0 /\ L1 >= 2 /\ 0 >= M1 + 1 /\ 0 >= N1 + 1 /\ P1 >= 1 ] f16(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1) -> Com_1(f16(A, B, C + 1, L1, N1, O1, G, H - 1, I, J, K, L, B, P1, C + 1, H - 1, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1)) [ A - H >= 0 /\ C + H - 2 >= 0 /\ D - 2 >= 0 /\ C + D - 2 >= 0 /\ Z + D - 4 >= 0 /\ A + D - 4 >= 0 /\ C >= 0 /\ Z + C - 2 >= 0 /\ A + C - 2 >= 0 /\ Z - 2 >= 0 /\ A + Z - 4 >= 0 /\ A - 2 >= 0 /\ H >= 0 /\ L1 >= 2 /\ 0 >= M1 + 1 /\ 0 >= N1 + 1 /\ 0 >= P1 + 1 ] f16(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1) -> Com_1(f8(A, 0, H1 + 1, L1, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, E, H1, 0, E, 0, E, E, H1, I1, J1, K1)) [ A - H >= 0 /\ C + H - 2 >= 0 /\ D - 2 >= 0 /\ C + D - 2 >= 0 /\ Z + D - 4 >= 0 /\ A + D - 4 >= 0 /\ C >= 0 /\ Z + C - 2 >= 0 /\ A + C - 2 >= 0 /\ Z - 2 >= 0 /\ A + Z - 4 >= 0 /\ A - 2 >= 0 /\ N1 >= 2 /\ E >= 1 /\ L1 >= 2 /\ H >= 0 /\ B = 0 ] f16(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1) -> Com_1(f8(A, 0, H1 + 1, L1, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, E, H1, 0, E, 0, E, E, H1, I1, J1, K1)) [ A - H >= 0 /\ C + H - 2 >= 0 /\ D - 2 >= 0 /\ C + D - 2 >= 0 /\ Z + D - 4 >= 0 /\ A + D - 4 >= 0 /\ C >= 0 /\ Z + C - 2 >= 0 /\ A + C - 2 >= 0 /\ Z - 2 >= 0 /\ A + Z - 4 >= 0 /\ A - 2 >= 0 /\ N1 >= 2 /\ 0 >= E + 1 /\ L1 >= 2 /\ H >= 0 /\ B = 0 ] f8(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1) -> Com_1(f8(A, 0, C, L1, N1, O1, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, 0, N1, 0, N1, A1, H1 - 1, H1 - 1, J1, K1)) [ A - H >= 0 /\ H >= 0 /\ D + H - 2 >= 0 /\ E1 + H >= 0 /\ -E1 + H >= 0 /\ C1 + H >= 0 /\ -C1 + H >= 0 /\ Z + H - 2 >= 0 /\ B + H >= 0 /\ -B + H >= 0 /\ A + H - 2 >= 0 /\ D - 2 >= 0 /\ E1 + D - 2 >= 0 /\ -E1 + D - 2 >= 0 /\ C1 + D - 2 >= 0 /\ -C1 + D - 2 >= 0 /\ Z + D - 4 >= 0 /\ B + D - 2 >= 0 /\ -B + D - 2 >= 0 /\ A + D - 4 >= 0 /\ C - H1 - 1 >= 0 /\ B1 - H1 >= 0 /\ A1 - G1 >= 0 /\ -A1 + G1 >= 0 /\ -E1 >= 0 /\ C1 - E1 >= 0 /\ -C1 - E1 >= 0 /\ Z - E1 - 2 >= 0 /\ B - E1 >= 0 /\ -B - E1 >= 0 /\ A - E1 - 2 >= 0 /\ E1 >= 0 /\ C1 + E1 >= 0 /\ -C1 + E1 >= 0 /\ Z + E1 - 2 >= 0 /\ B + E1 >= 0 /\ -B + E1 >= 0 /\ A + E1 - 2 >= 0 /\ B1 - C + 1 >= 0 /\ -B1 + C - 1 >= 0 /\ -C1 >= 0 /\ Z - C1 - 2 >= 0 /\ B - C1 >= 0 /\ -B - C1 >= 0 /\ A - C1 - 2 >= 0 /\ C1 >= 0 /\ Z + C1 - 2 >= 0 /\ B + C1 >= 0 /\ -B + C1 >= 0 /\ A + C1 - 2 >= 0 /\ Z - 2 >= 0 /\ B + Z - 2 >= 0 /\ -B + Z - 2 >= 0 /\ A + Z - 4 >= 0 /\ -B >= 0 /\ A - B - 2 >= 0 /\ B >= 0 /\ A + B - 2 >= 0 /\ A - 2 >= 0 /\ A1 >= P1 + 1 /\ H1 >= 0 /\ L1 >= 2 /\ P1 >= N1 + 1 /\ 0 >= N1 + 1 /\ C1 = 0 ] f8(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1) -> Com_1(f8(A, 0, C, L1, N1, O1, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, 0, N1, 0, N1, A1, H1 - 1, H1 - 1, J1, K1)) [ A - H >= 0 /\ H >= 0 /\ D + H - 2 >= 0 /\ E1 + H >= 0 /\ -E1 + H >= 0 /\ C1 + H >= 0 /\ -C1 + H >= 0 /\ Z + H - 2 >= 0 /\ B + H >= 0 /\ -B + H >= 0 /\ A + H - 2 >= 0 /\ D - 2 >= 0 /\ E1 + D - 2 >= 0 /\ -E1 + D - 2 >= 0 /\ C1 + D - 2 >= 0 /\ -C1 + D - 2 >= 0 /\ Z + D - 4 >= 0 /\ B + D - 2 >= 0 /\ -B + D - 2 >= 0 /\ A + D - 4 >= 0 /\ C - H1 - 1 >= 0 /\ B1 - H1 >= 0 /\ A1 - G1 >= 0 /\ -A1 + G1 >= 0 /\ -E1 >= 0 /\ C1 - E1 >= 0 /\ -C1 - E1 >= 0 /\ Z - E1 - 2 >= 0 /\ B - E1 >= 0 /\ -B - E1 >= 0 /\ A - E1 - 2 >= 0 /\ E1 >= 0 /\ C1 + E1 >= 0 /\ -C1 + E1 >= 0 /\ Z + E1 - 2 >= 0 /\ B + E1 >= 0 /\ -B + E1 >= 0 /\ A + E1 - 2 >= 0 /\ B1 - C + 1 >= 0 /\ -B1 + C - 1 >= 0 /\ -C1 >= 0 /\ Z - C1 - 2 >= 0 /\ B - C1 >= 0 /\ -B - C1 >= 0 /\ A - C1 - 2 >= 0 /\ C1 >= 0 /\ Z + C1 - 2 >= 0 /\ B + C1 >= 0 /\ -B + C1 >= 0 /\ A + C1 - 2 >= 0 /\ Z - 2 >= 0 /\ B + Z - 2 >= 0 /\ -B + Z - 2 >= 0 /\ A + Z - 4 >= 0 /\ -B >= 0 /\ A - B - 2 >= 0 /\ B >= 0 /\ A + B - 2 >= 0 /\ A - 2 >= 0 /\ A1 >= P1 + 1 /\ H1 >= 0 /\ L1 >= 2 /\ N1 >= P1 + 1 /\ N1 >= 1 /\ C1 = 0 ] f8(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1) -> Com_1(f8(A, 0, C, L1, N1, O1, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, 0, N1, 0, N1, A1, H1 - 1, H1 - 1, J1, K1)) [ A - H >= 0 /\ H >= 0 /\ D + H - 2 >= 0 /\ E1 + H >= 0 /\ -E1 + H >= 0 /\ C1 + H >= 0 /\ -C1 + H >= 0 /\ Z + H - 2 >= 0 /\ B + H >= 0 /\ -B + H >= 0 /\ A + H - 2 >= 0 /\ D - 2 >= 0 /\ E1 + D - 2 >= 0 /\ -E1 + D - 2 >= 0 /\ C1 + D - 2 >= 0 /\ -C1 + D - 2 >= 0 /\ Z + D - 4 >= 0 /\ B + D - 2 >= 0 /\ -B + D - 2 >= 0 /\ A + D - 4 >= 0 /\ C - H1 - 1 >= 0 /\ B1 - H1 >= 0 /\ A1 - G1 >= 0 /\ -A1 + G1 >= 0 /\ -E1 >= 0 /\ C1 - E1 >= 0 /\ -C1 - E1 >= 0 /\ Z - E1 - 2 >= 0 /\ B - E1 >= 0 /\ -B - E1 >= 0 /\ A - E1 - 2 >= 0 /\ E1 >= 0 /\ C1 + E1 >= 0 /\ -C1 + E1 >= 0 /\ Z + E1 - 2 >= 0 /\ B + E1 >= 0 /\ -B + E1 >= 0 /\ A + E1 - 2 >= 0 /\ B1 - C + 1 >= 0 /\ -B1 + C - 1 >= 0 /\ -C1 >= 0 /\ Z - C1 - 2 >= 0 /\ B - C1 >= 0 /\ -B - C1 >= 0 /\ A - C1 - 2 >= 0 /\ C1 >= 0 /\ Z + C1 - 2 >= 0 /\ B + C1 >= 0 /\ -B + C1 >= 0 /\ A + C1 - 2 >= 0 /\ Z - 2 >= 0 /\ B + Z - 2 >= 0 /\ -B + Z - 2 >= 0 /\ A + Z - 4 >= 0 /\ -B >= 0 /\ A - B - 2 >= 0 /\ B >= 0 /\ A + B - 2 >= 0 /\ A - 2 >= 0 /\ A1 >= P1 + 1 /\ H1 >= 0 /\ L1 >= 2 /\ N1 >= P1 + 1 /\ 0 >= N1 + 1 /\ C1 = 0 ] f8(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1) -> Com_1(f8(A, 0, C, L1, N1, O1, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, 0, N1, 0, N1, A1, H1 - 1, H1 - 1, J1, K1)) [ A - H >= 0 /\ H >= 0 /\ D + H - 2 >= 0 /\ E1 + H >= 0 /\ -E1 + H >= 0 /\ C1 + H >= 0 /\ -C1 + H >= 0 /\ Z + H - 2 >= 0 /\ B + H >= 0 /\ -B + H >= 0 /\ A + H - 2 >= 0 /\ D - 2 >= 0 /\ E1 + D - 2 >= 0 /\ -E1 + D - 2 >= 0 /\ C1 + D - 2 >= 0 /\ -C1 + D - 2 >= 0 /\ Z + D - 4 >= 0 /\ B + D - 2 >= 0 /\ -B + D - 2 >= 0 /\ A + D - 4 >= 0 /\ C - H1 - 1 >= 0 /\ B1 - H1 >= 0 /\ A1 - G1 >= 0 /\ -A1 + G1 >= 0 /\ -E1 >= 0 /\ C1 - E1 >= 0 /\ -C1 - E1 >= 0 /\ Z - E1 - 2 >= 0 /\ B - E1 >= 0 /\ -B - E1 >= 0 /\ A - E1 - 2 >= 0 /\ E1 >= 0 /\ C1 + E1 >= 0 /\ -C1 + E1 >= 0 /\ Z + E1 - 2 >= 0 /\ B + E1 >= 0 /\ -B + E1 >= 0 /\ A + E1 - 2 >= 0 /\ B1 - C + 1 >= 0 /\ -B1 + C - 1 >= 0 /\ -C1 >= 0 /\ Z - C1 - 2 >= 0 /\ B - C1 >= 0 /\ -B - C1 >= 0 /\ A - C1 - 2 >= 0 /\ C1 >= 0 /\ Z + C1 - 2 >= 0 /\ B + C1 >= 0 /\ -B + C1 >= 0 /\ A + C1 - 2 >= 0 /\ Z - 2 >= 0 /\ B + Z - 2 >= 0 /\ -B + Z - 2 >= 0 /\ A + Z - 4 >= 0 /\ -B >= 0 /\ A - B - 2 >= 0 /\ B >= 0 /\ A + B - 2 >= 0 /\ A - 2 >= 0 /\ P1 >= A1 + 1 /\ H1 >= 0 /\ L1 >= 2 /\ P1 >= N1 + 1 /\ N1 >= 1 /\ C1 = 0 ] f8(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1) -> Com_1(f8(A, 0, C, L1, N1, O1, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, 0, N1, 0, N1, A1, H1 - 1, H1 - 1, J1, K1)) [ A - H >= 0 /\ H >= 0 /\ D + H - 2 >= 0 /\ E1 + H >= 0 /\ -E1 + H >= 0 /\ C1 + H >= 0 /\ -C1 + H >= 0 /\ Z + H - 2 >= 0 /\ B + H >= 0 /\ -B + H >= 0 /\ A + H - 2 >= 0 /\ D - 2 >= 0 /\ E1 + D - 2 >= 0 /\ -E1 + D - 2 >= 0 /\ C1 + D - 2 >= 0 /\ -C1 + D - 2 >= 0 /\ Z + D - 4 >= 0 /\ B + D - 2 >= 0 /\ -B + D - 2 >= 0 /\ A + D - 4 >= 0 /\ C - H1 - 1 >= 0 /\ B1 - H1 >= 0 /\ A1 - G1 >= 0 /\ -A1 + G1 >= 0 /\ -E1 >= 0 /\ C1 - E1 >= 0 /\ -C1 - E1 >= 0 /\ Z - E1 - 2 >= 0 /\ B - E1 >= 0 /\ -B - E1 >= 0 /\ A - E1 - 2 >= 0 /\ E1 >= 0 /\ C1 + E1 >= 0 /\ -C1 + E1 >= 0 /\ Z + E1 - 2 >= 0 /\ B + E1 >= 0 /\ -B + E1 >= 0 /\ A + E1 - 2 >= 0 /\ B1 - C + 1 >= 0 /\ -B1 + C - 1 >= 0 /\ -C1 >= 0 /\ Z - C1 - 2 >= 0 /\ B - C1 >= 0 /\ -B - C1 >= 0 /\ A - C1 - 2 >= 0 /\ C1 >= 0 /\ Z + C1 - 2 >= 0 /\ B + C1 >= 0 /\ -B + C1 >= 0 /\ A + C1 - 2 >= 0 /\ Z - 2 >= 0 /\ B + Z - 2 >= 0 /\ -B + Z - 2 >= 0 /\ A + Z - 4 >= 0 /\ -B >= 0 /\ A - B - 2 >= 0 /\ B >= 0 /\ A + B - 2 >= 0 /\ A - 2 >= 0 /\ P1 >= A1 + 1 /\ H1 >= 0 /\ L1 >= 2 /\ P1 >= N1 + 1 /\ 0 >= N1 + 1 /\ C1 = 0 ] f8(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1) -> Com_1(f8(A, 0, C, L1, N1, O1, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, 0, N1, 0, N1, A1, H1 - 1, H1 - 1, J1, K1)) [ A - H >= 0 /\ H >= 0 /\ D + H - 2 >= 0 /\ E1 + H >= 0 /\ -E1 + H >= 0 /\ C1 + H >= 0 /\ -C1 + H >= 0 /\ Z + H - 2 >= 0 /\ B + H >= 0 /\ -B + H >= 0 /\ A + H - 2 >= 0 /\ D - 2 >= 0 /\ E1 + D - 2 >= 0 /\ -E1 + D - 2 >= 0 /\ C1 + D - 2 >= 0 /\ -C1 + D - 2 >= 0 /\ Z + D - 4 >= 0 /\ B + D - 2 >= 0 /\ -B + D - 2 >= 0 /\ A + D - 4 >= 0 /\ C - H1 - 1 >= 0 /\ B1 - H1 >= 0 /\ A1 - G1 >= 0 /\ -A1 + G1 >= 0 /\ -E1 >= 0 /\ C1 - E1 >= 0 /\ -C1 - E1 >= 0 /\ Z - E1 - 2 >= 0 /\ B - E1 >= 0 /\ -B - E1 >= 0 /\ A - E1 - 2 >= 0 /\ E1 >= 0 /\ C1 + E1 >= 0 /\ -C1 + E1 >= 0 /\ Z + E1 - 2 >= 0 /\ B + E1 >= 0 /\ -B + E1 >= 0 /\ A + E1 - 2 >= 0 /\ B1 - C + 1 >= 0 /\ -B1 + C - 1 >= 0 /\ -C1 >= 0 /\ Z - C1 - 2 >= 0 /\ B - C1 >= 0 /\ -B - C1 >= 0 /\ A - C1 - 2 >= 0 /\ C1 >= 0 /\ Z + C1 - 2 >= 0 /\ B + C1 >= 0 /\ -B + C1 >= 0 /\ A + C1 - 2 >= 0 /\ Z - 2 >= 0 /\ B + Z - 2 >= 0 /\ -B + Z - 2 >= 0 /\ A + Z - 4 >= 0 /\ -B >= 0 /\ A - B - 2 >= 0 /\ B >= 0 /\ A + B - 2 >= 0 /\ A - 2 >= 0 /\ P1 >= A1 + 1 /\ H1 >= 0 /\ L1 >= 2 /\ N1 >= P1 + 1 /\ N1 >= 1 /\ C1 = 0 ] f8(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1) -> Com_1(f8(A, 0, C, L1, N1, O1, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, 0, N1, 0, N1, A1, H1 - 1, H1 - 1, J1, K1)) [ A - H >= 0 /\ H >= 0 /\ D + H - 2 >= 0 /\ E1 + H >= 0 /\ -E1 + H >= 0 /\ C1 + H >= 0 /\ -C1 + H >= 0 /\ Z + H - 2 >= 0 /\ B + H >= 0 /\ -B + H >= 0 /\ A + H - 2 >= 0 /\ D - 2 >= 0 /\ E1 + D - 2 >= 0 /\ -E1 + D - 2 >= 0 /\ C1 + D - 2 >= 0 /\ -C1 + D - 2 >= 0 /\ Z + D - 4 >= 0 /\ B + D - 2 >= 0 /\ -B + D - 2 >= 0 /\ A + D - 4 >= 0 /\ C - H1 - 1 >= 0 /\ B1 - H1 >= 0 /\ A1 - G1 >= 0 /\ -A1 + G1 >= 0 /\ -E1 >= 0 /\ C1 - E1 >= 0 /\ -C1 - E1 >= 0 /\ Z - E1 - 2 >= 0 /\ B - E1 >= 0 /\ -B - E1 >= 0 /\ A - E1 - 2 >= 0 /\ E1 >= 0 /\ C1 + E1 >= 0 /\ -C1 + E1 >= 0 /\ Z + E1 - 2 >= 0 /\ B + E1 >= 0 /\ -B + E1 >= 0 /\ A + E1 - 2 >= 0 /\ B1 - C + 1 >= 0 /\ -B1 + C - 1 >= 0 /\ -C1 >= 0 /\ Z - C1 - 2 >= 0 /\ B - C1 >= 0 /\ -B - C1 >= 0 /\ A - C1 - 2 >= 0 /\ C1 >= 0 /\ Z + C1 - 2 >= 0 /\ B + C1 >= 0 /\ -B + C1 >= 0 /\ A + C1 - 2 >= 0 /\ Z - 2 >= 0 /\ B + Z - 2 >= 0 /\ -B + Z - 2 >= 0 /\ A + Z - 4 >= 0 /\ -B >= 0 /\ A - B - 2 >= 0 /\ B >= 0 /\ A + B - 2 >= 0 /\ A - 2 >= 0 /\ P1 >= A1 + 1 /\ H1 >= 0 /\ L1 >= 2 /\ N1 >= P1 + 1 /\ 0 >= N1 + 1 /\ C1 = 0 ] f8(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1) -> Com_1(f8(A, 0, C, L1, N1, O1, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, 0, N1, 0, N1, A1, H1 - 1, H1 - 1, J1, K1)) [ A - H >= 0 /\ H >= 0 /\ D + H - 2 >= 0 /\ E1 + H >= 0 /\ -E1 + H >= 0 /\ C1 + H >= 0 /\ -C1 + H >= 0 /\ Z + H - 2 >= 0 /\ B + H >= 0 /\ -B + H >= 0 /\ A + H - 2 >= 0 /\ D - 2 >= 0 /\ E1 + D - 2 >= 0 /\ -E1 + D - 2 >= 0 /\ C1 + D - 2 >= 0 /\ -C1 + D - 2 >= 0 /\ Z + D - 4 >= 0 /\ B + D - 2 >= 0 /\ -B + D - 2 >= 0 /\ A + D - 4 >= 0 /\ C - H1 - 1 >= 0 /\ B1 - H1 >= 0 /\ A1 - G1 >= 0 /\ -A1 + G1 >= 0 /\ -E1 >= 0 /\ C1 - E1 >= 0 /\ -C1 - E1 >= 0 /\ Z - E1 - 2 >= 0 /\ B - E1 >= 0 /\ -B - E1 >= 0 /\ A - E1 - 2 >= 0 /\ E1 >= 0 /\ C1 + E1 >= 0 /\ -C1 + E1 >= 0 /\ Z + E1 - 2 >= 0 /\ B + E1 >= 0 /\ -B + E1 >= 0 /\ A + E1 - 2 >= 0 /\ B1 - C + 1 >= 0 /\ -B1 + C - 1 >= 0 /\ -C1 >= 0 /\ Z - C1 - 2 >= 0 /\ B - C1 >= 0 /\ -B - C1 >= 0 /\ A - C1 - 2 >= 0 /\ C1 >= 0 /\ Z + C1 - 2 >= 0 /\ B + C1 >= 0 /\ -B + C1 >= 0 /\ A + C1 - 2 >= 0 /\ Z - 2 >= 0 /\ B + Z - 2 >= 0 /\ -B + Z - 2 >= 0 /\ A + Z - 4 >= 0 /\ -B >= 0 /\ A - B - 2 >= 0 /\ B >= 0 /\ A + B - 2 >= 0 /\ A - 2 >= 0 /\ A1 >= P1 + 1 /\ H1 >= 0 /\ L1 >= 2 /\ P1 >= N1 + 1 /\ N1 >= 1 /\ C1 = 0 ] f8(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1) -> Com_1(f10(A, B, C, L1, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, S1, Z, R1, B1, M1, N1, O1, P1, T1, H1, I1, J1, K1)) [ A - H >= 0 /\ H >= 0 /\ D + H - 2 >= 0 /\ E1 + H >= 0 /\ -E1 + H >= 0 /\ C1 + H >= 0 /\ -C1 + H >= 0 /\ Z + H - 2 >= 0 /\ B + H >= 0 /\ -B + H >= 0 /\ A + H - 2 >= 0 /\ D - 2 >= 0 /\ E1 + D - 2 >= 0 /\ -E1 + D - 2 >= 0 /\ C1 + D - 2 >= 0 /\ -C1 + D - 2 >= 0 /\ Z + D - 4 >= 0 /\ B + D - 2 >= 0 /\ -B + D - 2 >= 0 /\ A + D - 4 >= 0 /\ C - H1 - 1 >= 0 /\ B1 - H1 >= 0 /\ A1 - G1 >= 0 /\ -A1 + G1 >= 0 /\ -E1 >= 0 /\ C1 - E1 >= 0 /\ -C1 - E1 >= 0 /\ Z - E1 - 2 >= 0 /\ B - E1 >= 0 /\ -B - E1 >= 0 /\ A - E1 - 2 >= 0 /\ E1 >= 0 /\ C1 + E1 >= 0 /\ -C1 + E1 >= 0 /\ Z + E1 - 2 >= 0 /\ B + E1 >= 0 /\ -B + E1 >= 0 /\ A + E1 - 2 >= 0 /\ B1 - C + 1 >= 0 /\ -B1 + C - 1 >= 0 /\ -C1 >= 0 /\ Z - C1 - 2 >= 0 /\ B - C1 >= 0 /\ -B - C1 >= 0 /\ A - C1 - 2 >= 0 /\ C1 >= 0 /\ Z + C1 - 2 >= 0 /\ B + C1 >= 0 /\ -B + C1 >= 0 /\ A + C1 - 2 >= 0 /\ Z - 2 >= 0 /\ B + Z - 2 >= 0 /\ -B + Z - 2 >= 0 /\ A + Z - 4 >= 0 /\ -B >= 0 /\ A - B - 2 >= 0 /\ B >= 0 /\ A + B - 2 >= 0 /\ A - 2 >= 0 /\ L1 >= 2 /\ H1 >= 0 /\ C1 = A1 ] )