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