(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f17)) (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 M1 N1 O1 P1 Q1 R1 S1 T1 U1 V1 W1) (RULES f17(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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f0(A2, D2, C2, I2, H2, F, G, H, I, Y1, F2, 0, J2, Z1, N2, O2, P2, Q2, R2, S2, T2, W2, X2, X, Y, K2, A1, B1, C1, C3, E1, B3, Y2, Z2, A3, D3, K1, L1, X1, G2, O1, P1, E2, B2, S1, T1, U1, M2, L2)) [ 0 >= U2 /\ 0 >= Y1 /\ 0 >= V2 ] f17(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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f15(Y1, 2, A2, C2, A2, F, G, H, I, Y1, 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, X1, A2, D2, P1, Q1, R1, S1, T1, U1, V1, W1)) [ Y1 >= 2 ] 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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f13(Y1, C2, A2, H2, G2, F, G, H, I, X1, E2, I2, I2, K2, B2, 0, N2, O2, P2, Q2, R2, S2, 0, X, Y, C, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, F2, O1, P1, D2, J2, Z1, T2, M2, V1, W1)) [ B - 2 >= 0 /\ J + B - 4 >= 0 /\ J - 2 >= 0 /\ L2 >= 2 /\ Z1 >= L2 /\ X1 >= 2 /\ B >= A /\ B >= 0 /\ P1 >= 0 /\ M2 >= 1 /\ C >= 1 /\ I2 >= 1 ] 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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f13(Y1, C2, A2, H2, G2, F, G, H, I, X1, E2, I2, I2, K2, B2, 0, N2, O2, P2, Q2, R2, S2, 0, X, Y, C, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, F2, O1, P1, D2, J2, Z1, T2, M2, V1, W1)) [ B - 2 >= 0 /\ J + B - 4 >= 0 /\ J - 2 >= 0 /\ L2 >= 2 /\ Z1 >= L2 /\ X1 >= 2 /\ B >= A /\ B >= 0 /\ P1 >= 0 /\ M2 >= 1 /\ C >= 1 /\ 0 >= I2 + 1 ] 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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f13(Y1, C2, A2, H2, G2, F, G, H, I, X1, E2, I2, I2, K2, B2, 0, N2, O2, P2, Q2, R2, S2, 0, X, Y, C, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, F2, O1, P1, D2, J2, Z1, T2, M2, V1, W1)) [ B - 2 >= 0 /\ J + B - 4 >= 0 /\ J - 2 >= 0 /\ L2 >= 2 /\ Z1 >= L2 /\ X1 >= 2 /\ B >= A /\ B >= 0 /\ P1 >= 0 /\ M2 >= 1 /\ 0 >= C + 1 /\ I2 >= 1 ] 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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f13(Y1, C2, A2, H2, G2, F, G, H, I, X1, E2, I2, I2, K2, B2, 0, N2, O2, P2, Q2, R2, S2, 0, X, Y, C, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, F2, O1, P1, D2, J2, Z1, T2, M2, V1, W1)) [ B - 2 >= 0 /\ J + B - 4 >= 0 /\ J - 2 >= 0 /\ L2 >= 2 /\ Z1 >= L2 /\ X1 >= 2 /\ B >= A /\ B >= 0 /\ P1 >= 0 /\ M2 >= 1 /\ 0 >= C + 1 /\ 0 >= I2 + 1 ] 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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f13(Y1, C2, A2, H2, G2, F, G, H, I, X1, E2, I2, I2, K2, B2, 0, N2, O2, P2, Q2, R2, S2, 0, X, Y, C, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, F2, O1, P1, D2, J2, Z1, T2, M2, V1, W1)) [ B - 2 >= 0 /\ J + B - 4 >= 0 /\ J - 2 >= 0 /\ L2 >= 2 /\ Z1 >= L2 /\ X1 >= 2 /\ B >= A /\ B >= 0 /\ P1 >= 0 /\ 0 >= M2 + 1 /\ C >= 1 /\ I2 >= 1 ] 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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f13(Y1, C2, A2, H2, G2, F, G, H, I, X1, E2, I2, I2, K2, B2, 0, N2, O2, P2, Q2, R2, S2, 0, X, Y, C, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, F2, O1, P1, D2, J2, Z1, T2, M2, V1, W1)) [ B - 2 >= 0 /\ J + B - 4 >= 0 /\ J - 2 >= 0 /\ L2 >= 2 /\ Z1 >= L2 /\ X1 >= 2 /\ B >= A /\ B >= 0 /\ P1 >= 0 /\ 0 >= M2 + 1 /\ C >= 1 /\ 0 >= I2 + 1 ] 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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f13(Y1, C2, A2, H2, G2, F, G, H, I, X1, E2, I2, I2, K2, B2, 0, N2, O2, P2, Q2, R2, S2, 0, X, Y, C, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, F2, O1, P1, D2, J2, Z1, T2, M2, V1, W1)) [ B - 2 >= 0 /\ J + B - 4 >= 0 /\ J - 2 >= 0 /\ L2 >= 2 /\ Z1 >= L2 /\ X1 >= 2 /\ B >= A /\ B >= 0 /\ P1 >= 0 /\ 0 >= M2 + 1 /\ 0 >= C + 1 /\ I2 >= 1 ] 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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f13(Y1, C2, A2, H2, G2, F, G, H, I, X1, E2, I2, I2, K2, B2, 0, N2, O2, P2, Q2, R2, S2, 0, X, Y, C, A1, B1, C1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, F2, O1, P1, D2, J2, Z1, T2, M2, V1, W1)) [ B - 2 >= 0 /\ J + B - 4 >= 0 /\ J - 2 >= 0 /\ L2 >= 2 /\ Z1 >= L2 /\ X1 >= 2 /\ B >= A /\ B >= 0 /\ P1 >= 0 /\ 0 >= M2 + 1 /\ 0 >= C + 1 /\ 0 >= I2 + 1 ] 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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f15(A, B + 1, D, X1, D, Y1, B, 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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1)) [ B - 2 >= 0 /\ J + B - 4 >= 0 /\ J - 2 >= 0 /\ A >= B + 1 /\ B >= 0 ] f13(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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f13(A, B, C, D, E, F, G, H + 1, I - 1, X1, Y1, A2, A2, C2, D2, 0, E2, F2, G2, H2, I2, J2, 0, K2, Z, Z, B2, H + 1, I - 1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1)) [ S1 - 2 >= 0 /\ P1 + S1 - 2 >= 0 /\ W + S1 - 2 >= 0 /\ -W + S1 - 2 >= 0 /\ P + S1 - 2 >= 0 /\ -P + S1 - 2 >= 0 /\ J + S1 - 4 >= 0 /\ P1 >= 0 /\ W + P1 >= 0 /\ -W + P1 >= 0 /\ P + P1 >= 0 /\ -P + P1 >= 0 /\ J + P1 - 2 >= 0 /\ -W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ J - W - 2 >= 0 /\ W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ J + W - 2 >= 0 /\ -P >= 0 /\ J - P - 2 >= 0 /\ P >= 0 /\ J + P - 2 >= 0 /\ J - 2 >= 0 /\ H >= 0 /\ I >= 0 /\ X1 >= 2 /\ Z1 >= 1 /\ A2 >= 1 /\ B2 >= 1 ] f13(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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f13(A, B, C, D, E, F, G, H + 1, I - 1, X1, Y1, A2, A2, C2, D2, 0, E2, F2, G2, H2, I2, J2, 0, K2, Z, Z, B2, H + 1, I - 1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1)) [ S1 - 2 >= 0 /\ P1 + S1 - 2 >= 0 /\ W + S1 - 2 >= 0 /\ -W + S1 - 2 >= 0 /\ P + S1 - 2 >= 0 /\ -P + S1 - 2 >= 0 /\ J + S1 - 4 >= 0 /\ P1 >= 0 /\ W + P1 >= 0 /\ -W + P1 >= 0 /\ P + P1 >= 0 /\ -P + P1 >= 0 /\ J + P1 - 2 >= 0 /\ -W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ J - W - 2 >= 0 /\ W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ J + W - 2 >= 0 /\ -P >= 0 /\ J - P - 2 >= 0 /\ P >= 0 /\ J + P - 2 >= 0 /\ J - 2 >= 0 /\ H >= 0 /\ I >= 0 /\ X1 >= 2 /\ Z1 >= 1 /\ A2 >= 1 /\ 0 >= B2 + 1 ] f13(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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f13(A, B, C, D, E, F, G, H + 1, I - 1, X1, Y1, A2, A2, C2, D2, 0, E2, F2, G2, H2, I2, J2, 0, K2, Z, Z, B2, H + 1, I - 1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1)) [ S1 - 2 >= 0 /\ P1 + S1 - 2 >= 0 /\ W + S1 - 2 >= 0 /\ -W + S1 - 2 >= 0 /\ P + S1 - 2 >= 0 /\ -P + S1 - 2 >= 0 /\ J + S1 - 4 >= 0 /\ P1 >= 0 /\ W + P1 >= 0 /\ -W + P1 >= 0 /\ P + P1 >= 0 /\ -P + P1 >= 0 /\ J + P1 - 2 >= 0 /\ -W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ J - W - 2 >= 0 /\ W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ J + W - 2 >= 0 /\ -P >= 0 /\ J - P - 2 >= 0 /\ P >= 0 /\ J + P - 2 >= 0 /\ J - 2 >= 0 /\ H >= 0 /\ I >= 0 /\ X1 >= 2 /\ Z1 >= 1 /\ 0 >= A2 + 1 /\ B2 >= 1 ] f13(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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f13(A, B, C, D, E, F, G, H + 1, I - 1, X1, Y1, A2, A2, C2, D2, 0, E2, F2, G2, H2, I2, J2, 0, K2, Z, Z, B2, H + 1, I - 1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1)) [ S1 - 2 >= 0 /\ P1 + S1 - 2 >= 0 /\ W + S1 - 2 >= 0 /\ -W + S1 - 2 >= 0 /\ P + S1 - 2 >= 0 /\ -P + S1 - 2 >= 0 /\ J + S1 - 4 >= 0 /\ P1 >= 0 /\ W + P1 >= 0 /\ -W + P1 >= 0 /\ P + P1 >= 0 /\ -P + P1 >= 0 /\ J + P1 - 2 >= 0 /\ -W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ J - W - 2 >= 0 /\ W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ J + W - 2 >= 0 /\ -P >= 0 /\ J - P - 2 >= 0 /\ P >= 0 /\ J + P - 2 >= 0 /\ J - 2 >= 0 /\ H >= 0 /\ I >= 0 /\ X1 >= 2 /\ Z1 >= 1 /\ 0 >= A2 + 1 /\ 0 >= B2 + 1 ] f13(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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f13(A, B, C, D, E, F, G, H + 1, I - 1, X1, Y1, A2, A2, C2, D2, 0, E2, F2, G2, H2, I2, J2, 0, K2, Z, Z, B2, H + 1, I - 1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1)) [ S1 - 2 >= 0 /\ P1 + S1 - 2 >= 0 /\ W + S1 - 2 >= 0 /\ -W + S1 - 2 >= 0 /\ P + S1 - 2 >= 0 /\ -P + S1 - 2 >= 0 /\ J + S1 - 4 >= 0 /\ P1 >= 0 /\ W + P1 >= 0 /\ -W + P1 >= 0 /\ P + P1 >= 0 /\ -P + P1 >= 0 /\ J + P1 - 2 >= 0 /\ -W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ J - W - 2 >= 0 /\ W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ J + W - 2 >= 0 /\ -P >= 0 /\ J - P - 2 >= 0 /\ P >= 0 /\ J + P - 2 >= 0 /\ J - 2 >= 0 /\ H >= 0 /\ I >= 0 /\ X1 >= 2 /\ 0 >= Z1 + 1 /\ A2 >= 1 /\ B2 >= 1 ] f13(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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f13(A, B, C, D, E, F, G, H + 1, I - 1, X1, Y1, A2, A2, C2, D2, 0, E2, F2, G2, H2, I2, J2, 0, K2, Z, Z, B2, H + 1, I - 1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1)) [ S1 - 2 >= 0 /\ P1 + S1 - 2 >= 0 /\ W + S1 - 2 >= 0 /\ -W + S1 - 2 >= 0 /\ P + S1 - 2 >= 0 /\ -P + S1 - 2 >= 0 /\ J + S1 - 4 >= 0 /\ P1 >= 0 /\ W + P1 >= 0 /\ -W + P1 >= 0 /\ P + P1 >= 0 /\ -P + P1 >= 0 /\ J + P1 - 2 >= 0 /\ -W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ J - W - 2 >= 0 /\ W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ J + W - 2 >= 0 /\ -P >= 0 /\ J - P - 2 >= 0 /\ P >= 0 /\ J + P - 2 >= 0 /\ J - 2 >= 0 /\ H >= 0 /\ I >= 0 /\ X1 >= 2 /\ 0 >= Z1 + 1 /\ A2 >= 1 /\ 0 >= B2 + 1 ] f13(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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f13(A, B, C, D, E, F, G, H + 1, I - 1, X1, Y1, A2, A2, C2, D2, 0, E2, F2, G2, H2, I2, J2, 0, K2, Z, Z, B2, H + 1, I - 1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1)) [ S1 - 2 >= 0 /\ P1 + S1 - 2 >= 0 /\ W + S1 - 2 >= 0 /\ -W + S1 - 2 >= 0 /\ P + S1 - 2 >= 0 /\ -P + S1 - 2 >= 0 /\ J + S1 - 4 >= 0 /\ P1 >= 0 /\ W + P1 >= 0 /\ -W + P1 >= 0 /\ P + P1 >= 0 /\ -P + P1 >= 0 /\ J + P1 - 2 >= 0 /\ -W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ J - W - 2 >= 0 /\ W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ J + W - 2 >= 0 /\ -P >= 0 /\ J - P - 2 >= 0 /\ P >= 0 /\ J + P - 2 >= 0 /\ J - 2 >= 0 /\ H >= 0 /\ I >= 0 /\ X1 >= 2 /\ 0 >= Z1 + 1 /\ 0 >= A2 + 1 /\ B2 >= 1 ] f13(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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f13(A, B, C, D, E, F, G, H + 1, I - 1, X1, Y1, A2, A2, C2, D2, 0, E2, F2, G2, H2, I2, J2, 0, K2, Z, Z, B2, H + 1, I - 1, D1, E1, F1, G1, H1, I1, J1, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1)) [ S1 - 2 >= 0 /\ P1 + S1 - 2 >= 0 /\ W + S1 - 2 >= 0 /\ -W + S1 - 2 >= 0 /\ P + S1 - 2 >= 0 /\ -P + S1 - 2 >= 0 /\ J + S1 - 4 >= 0 /\ P1 >= 0 /\ W + P1 >= 0 /\ -W + P1 >= 0 /\ P + P1 >= 0 /\ -P + P1 >= 0 /\ J + P1 - 2 >= 0 /\ -W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ J - W - 2 >= 0 /\ W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ J + W - 2 >= 0 /\ -P >= 0 /\ J - P - 2 >= 0 /\ P >= 0 /\ J + P - 2 >= 0 /\ J - 2 >= 0 /\ H >= 0 /\ I >= 0 /\ X1 >= 2 /\ 0 >= Z1 + 1 /\ 0 >= A2 + 1 /\ 0 >= B2 + 1 ] f13(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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f10(A, B, C, D, E, F, G, K1 + 1, I, X1, Y1, L, A2, E2, F2, G2, H2, I2, J2, K2, B2, O2, P2, X, Y, C2, A1, B1, C1, L, K1, 0, L, 0, L, L, K1, L1, M1, N1, O1, P1, Q1, D2, S1, T1, U1, Z1, N2)) [ S1 - 2 >= 0 /\ P1 + S1 - 2 >= 0 /\ W + S1 - 2 >= 0 /\ -W + S1 - 2 >= 0 /\ P + S1 - 2 >= 0 /\ -P + S1 - 2 >= 0 /\ J + S1 - 4 >= 0 /\ P1 >= 0 /\ W + P1 >= 0 /\ -W + P1 >= 0 /\ P + P1 >= 0 /\ -P + P1 >= 0 /\ J + P1 - 2 >= 0 /\ -W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ J - W - 2 >= 0 /\ W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ J + W - 2 >= 0 /\ -P >= 0 /\ J - P - 2 >= 0 /\ P >= 0 /\ J + P - 2 >= 0 /\ J - 2 >= 0 /\ Q2 >= 2 /\ X1 >= 2 /\ I >= 0 /\ H >= 0 /\ L >= 1 /\ Z = 0 ] f13(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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f10(A, B, C, D, E, F, G, K1 + 1, I, X1, Y1, L, A2, E2, F2, G2, H2, I2, J2, K2, B2, O2, P2, X, Y, C2, A1, B1, C1, L, K1, 0, L, 0, L, L, K1, L1, M1, N1, O1, P1, Q1, D2, S1, T1, U1, Z1, N2)) [ S1 - 2 >= 0 /\ P1 + S1 - 2 >= 0 /\ W + S1 - 2 >= 0 /\ -W + S1 - 2 >= 0 /\ P + S1 - 2 >= 0 /\ -P + S1 - 2 >= 0 /\ J + S1 - 4 >= 0 /\ P1 >= 0 /\ W + P1 >= 0 /\ -W + P1 >= 0 /\ P + P1 >= 0 /\ -P + P1 >= 0 /\ J + P1 - 2 >= 0 /\ -W >= 0 /\ P - W >= 0 /\ -P - W >= 0 /\ J - W - 2 >= 0 /\ W >= 0 /\ P + W >= 0 /\ -P + W >= 0 /\ J + W - 2 >= 0 /\ -P >= 0 /\ J - P - 2 >= 0 /\ P >= 0 /\ J + P - 2 >= 0 /\ J - 2 >= 0 /\ Q2 >= 2 /\ X1 >= 2 /\ I >= 0 /\ H >= 0 /\ 0 >= L + 1 /\ Z = 0 ] f10(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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f10(A, B, C, D, E, F, G, H, I, X1, K, Y1, M, N, O, P, Q, R, S, T, U, V, W, A2, Y, Z, A1, B1, C1, D1, E1, 0, Y1, 0, Y1, D1, K1 - 1, K1 - 1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1)) [ I >= 0 /\ S1 + I - 2 >= 0 /\ P1 + I >= 0 /\ H1 + I >= 0 /\ -H1 + I >= 0 /\ F1 + I >= 0 /\ -F1 + I >= 0 /\ J + I - 2 >= 0 /\ E1 - H + 1 >= 0 /\ -K1 + H - 1 >= 0 /\ -E1 + H - 1 >= 0 /\ S1 - 2 >= 0 /\ P1 + S1 - 2 >= 0 /\ H1 + S1 - 2 >= 0 /\ -H1 + S1 - 2 >= 0 /\ F1 + S1 - 2 >= 0 /\ -F1 + S1 - 2 >= 0 /\ J + S1 - 4 >= 0 /\ P1 >= 0 /\ H1 + P1 >= 0 /\ -H1 + P1 >= 0 /\ F1 + P1 >= 0 /\ -F1 + P1 >= 0 /\ J + P1 - 2 >= 0 /\ E1 - K1 >= 0 /\ D1 - J1 >= 0 /\ -D1 + J1 >= 0 /\ -H1 >= 0 /\ F1 - H1 >= 0 /\ -F1 - H1 >= 0 /\ J - H1 - 2 >= 0 /\ H1 >= 0 /\ F1 + H1 >= 0 /\ -F1 + H1 >= 0 /\ J + H1 - 2 >= 0 /\ -F1 >= 0 /\ J - F1 - 2 >= 0 /\ F1 >= 0 /\ J + F1 - 2 >= 0 /\ J - 2 >= 0 /\ D1 >= C2 + 1 /\ K1 >= 0 /\ X1 >= 2 /\ C2 >= Y1 + 1 /\ 0 >= Y1 + 1 /\ F1 = 0 ] f10(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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f10(A, B, C, D, E, F, G, H, I, X1, K, Y1, M, N, O, P, Q, R, S, T, U, V, W, A2, Y, Z, A1, B1, C1, D1, E1, 0, Y1, 0, Y1, D1, K1 - 1, K1 - 1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1)) [ I >= 0 /\ S1 + I - 2 >= 0 /\ P1 + I >= 0 /\ H1 + I >= 0 /\ -H1 + I >= 0 /\ F1 + I >= 0 /\ -F1 + I >= 0 /\ J + I - 2 >= 0 /\ E1 - H + 1 >= 0 /\ -K1 + H - 1 >= 0 /\ -E1 + H - 1 >= 0 /\ S1 - 2 >= 0 /\ P1 + S1 - 2 >= 0 /\ H1 + S1 - 2 >= 0 /\ -H1 + S1 - 2 >= 0 /\ F1 + S1 - 2 >= 0 /\ -F1 + S1 - 2 >= 0 /\ J + S1 - 4 >= 0 /\ P1 >= 0 /\ H1 + P1 >= 0 /\ -H1 + P1 >= 0 /\ F1 + P1 >= 0 /\ -F1 + P1 >= 0 /\ J + P1 - 2 >= 0 /\ E1 - K1 >= 0 /\ D1 - J1 >= 0 /\ -D1 + J1 >= 0 /\ -H1 >= 0 /\ F1 - H1 >= 0 /\ -F1 - H1 >= 0 /\ J - H1 - 2 >= 0 /\ H1 >= 0 /\ F1 + H1 >= 0 /\ -F1 + H1 >= 0 /\ J + H1 - 2 >= 0 /\ -F1 >= 0 /\ J - F1 - 2 >= 0 /\ F1 >= 0 /\ J + F1 - 2 >= 0 /\ J - 2 >= 0 /\ D1 >= C2 + 1 /\ K1 >= 0 /\ X1 >= 2 /\ Y1 >= C2 + 1 /\ Y1 >= 1 /\ F1 = 0 ] f10(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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f10(A, B, C, D, E, F, G, H, I, X1, K, Y1, M, N, O, P, Q, R, S, T, U, V, W, A2, Y, Z, A1, B1, C1, D1, E1, 0, Y1, 0, Y1, D1, K1 - 1, K1 - 1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1)) [ I >= 0 /\ S1 + I - 2 >= 0 /\ P1 + I >= 0 /\ H1 + I >= 0 /\ -H1 + I >= 0 /\ F1 + I >= 0 /\ -F1 + I >= 0 /\ J + I - 2 >= 0 /\ E1 - H + 1 >= 0 /\ -K1 + H - 1 >= 0 /\ -E1 + H - 1 >= 0 /\ S1 - 2 >= 0 /\ P1 + S1 - 2 >= 0 /\ H1 + S1 - 2 >= 0 /\ -H1 + S1 - 2 >= 0 /\ F1 + S1 - 2 >= 0 /\ -F1 + S1 - 2 >= 0 /\ J + S1 - 4 >= 0 /\ P1 >= 0 /\ H1 + P1 >= 0 /\ -H1 + P1 >= 0 /\ F1 + P1 >= 0 /\ -F1 + P1 >= 0 /\ J + P1 - 2 >= 0 /\ E1 - K1 >= 0 /\ D1 - J1 >= 0 /\ -D1 + J1 >= 0 /\ -H1 >= 0 /\ F1 - H1 >= 0 /\ -F1 - H1 >= 0 /\ J - H1 - 2 >= 0 /\ H1 >= 0 /\ F1 + H1 >= 0 /\ -F1 + H1 >= 0 /\ J + H1 - 2 >= 0 /\ -F1 >= 0 /\ J - F1 - 2 >= 0 /\ F1 >= 0 /\ J + F1 - 2 >= 0 /\ J - 2 >= 0 /\ D1 >= C2 + 1 /\ K1 >= 0 /\ X1 >= 2 /\ Y1 >= C2 + 1 /\ 0 >= Y1 + 1 /\ F1 = 0 ] f10(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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f10(A, B, C, D, E, F, G, H, I, X1, K, Y1, M, N, O, P, Q, R, S, T, U, V, W, A2, Y, Z, A1, B1, C1, D1, E1, 0, Y1, 0, Y1, D1, K1 - 1, K1 - 1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1)) [ I >= 0 /\ S1 + I - 2 >= 0 /\ P1 + I >= 0 /\ H1 + I >= 0 /\ -H1 + I >= 0 /\ F1 + I >= 0 /\ -F1 + I >= 0 /\ J + I - 2 >= 0 /\ E1 - H + 1 >= 0 /\ -K1 + H - 1 >= 0 /\ -E1 + H - 1 >= 0 /\ S1 - 2 >= 0 /\ P1 + S1 - 2 >= 0 /\ H1 + S1 - 2 >= 0 /\ -H1 + S1 - 2 >= 0 /\ F1 + S1 - 2 >= 0 /\ -F1 + S1 - 2 >= 0 /\ J + S1 - 4 >= 0 /\ P1 >= 0 /\ H1 + P1 >= 0 /\ -H1 + P1 >= 0 /\ F1 + P1 >= 0 /\ -F1 + P1 >= 0 /\ J + P1 - 2 >= 0 /\ E1 - K1 >= 0 /\ D1 - J1 >= 0 /\ -D1 + J1 >= 0 /\ -H1 >= 0 /\ F1 - H1 >= 0 /\ -F1 - H1 >= 0 /\ J - H1 - 2 >= 0 /\ H1 >= 0 /\ F1 + H1 >= 0 /\ -F1 + H1 >= 0 /\ J + H1 - 2 >= 0 /\ -F1 >= 0 /\ J - F1 - 2 >= 0 /\ F1 >= 0 /\ J + F1 - 2 >= 0 /\ J - 2 >= 0 /\ C2 >= D1 + 1 /\ K1 >= 0 /\ X1 >= 2 /\ C2 >= Y1 + 1 /\ Y1 >= 1 /\ F1 = 0 ] f10(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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f10(A, B, C, D, E, F, G, H, I, X1, K, Y1, M, N, O, P, Q, R, S, T, U, V, W, A2, Y, Z, A1, B1, C1, D1, E1, 0, Y1, 0, Y1, D1, K1 - 1, K1 - 1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1)) [ I >= 0 /\ S1 + I - 2 >= 0 /\ P1 + I >= 0 /\ H1 + I >= 0 /\ -H1 + I >= 0 /\ F1 + I >= 0 /\ -F1 + I >= 0 /\ J + I - 2 >= 0 /\ E1 - H + 1 >= 0 /\ -K1 + H - 1 >= 0 /\ -E1 + H - 1 >= 0 /\ S1 - 2 >= 0 /\ P1 + S1 - 2 >= 0 /\ H1 + S1 - 2 >= 0 /\ -H1 + S1 - 2 >= 0 /\ F1 + S1 - 2 >= 0 /\ -F1 + S1 - 2 >= 0 /\ J + S1 - 4 >= 0 /\ P1 >= 0 /\ H1 + P1 >= 0 /\ -H1 + P1 >= 0 /\ F1 + P1 >= 0 /\ -F1 + P1 >= 0 /\ J + P1 - 2 >= 0 /\ E1 - K1 >= 0 /\ D1 - J1 >= 0 /\ -D1 + J1 >= 0 /\ -H1 >= 0 /\ F1 - H1 >= 0 /\ -F1 - H1 >= 0 /\ J - H1 - 2 >= 0 /\ H1 >= 0 /\ F1 + H1 >= 0 /\ -F1 + H1 >= 0 /\ J + H1 - 2 >= 0 /\ -F1 >= 0 /\ J - F1 - 2 >= 0 /\ F1 >= 0 /\ J + F1 - 2 >= 0 /\ J - 2 >= 0 /\ C2 >= D1 + 1 /\ K1 >= 0 /\ X1 >= 2 /\ C2 >= Y1 + 1 /\ 0 >= Y1 + 1 /\ F1 = 0 ] f10(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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f10(A, B, C, D, E, F, G, H, I, X1, K, Y1, M, N, O, P, Q, R, S, T, U, V, W, A2, Y, Z, A1, B1, C1, D1, E1, 0, Y1, 0, Y1, D1, K1 - 1, K1 - 1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1)) [ I >= 0 /\ S1 + I - 2 >= 0 /\ P1 + I >= 0 /\ H1 + I >= 0 /\ -H1 + I >= 0 /\ F1 + I >= 0 /\ -F1 + I >= 0 /\ J + I - 2 >= 0 /\ E1 - H + 1 >= 0 /\ -K1 + H - 1 >= 0 /\ -E1 + H - 1 >= 0 /\ S1 - 2 >= 0 /\ P1 + S1 - 2 >= 0 /\ H1 + S1 - 2 >= 0 /\ -H1 + S1 - 2 >= 0 /\ F1 + S1 - 2 >= 0 /\ -F1 + S1 - 2 >= 0 /\ J + S1 - 4 >= 0 /\ P1 >= 0 /\ H1 + P1 >= 0 /\ -H1 + P1 >= 0 /\ F1 + P1 >= 0 /\ -F1 + P1 >= 0 /\ J + P1 - 2 >= 0 /\ E1 - K1 >= 0 /\ D1 - J1 >= 0 /\ -D1 + J1 >= 0 /\ -H1 >= 0 /\ F1 - H1 >= 0 /\ -F1 - H1 >= 0 /\ J - H1 - 2 >= 0 /\ H1 >= 0 /\ F1 + H1 >= 0 /\ -F1 + H1 >= 0 /\ J + H1 - 2 >= 0 /\ -F1 >= 0 /\ J - F1 - 2 >= 0 /\ F1 >= 0 /\ J + F1 - 2 >= 0 /\ J - 2 >= 0 /\ C2 >= D1 + 1 /\ K1 >= 0 /\ X1 >= 2 /\ Y1 >= C2 + 1 /\ Y1 >= 1 /\ F1 = 0 ] f10(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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f10(A, B, C, D, E, F, G, H, I, X1, K, Y1, M, N, O, P, Q, R, S, T, U, V, W, A2, Y, Z, A1, B1, C1, D1, E1, 0, Y1, 0, Y1, D1, K1 - 1, K1 - 1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1)) [ I >= 0 /\ S1 + I - 2 >= 0 /\ P1 + I >= 0 /\ H1 + I >= 0 /\ -H1 + I >= 0 /\ F1 + I >= 0 /\ -F1 + I >= 0 /\ J + I - 2 >= 0 /\ E1 - H + 1 >= 0 /\ -K1 + H - 1 >= 0 /\ -E1 + H - 1 >= 0 /\ S1 - 2 >= 0 /\ P1 + S1 - 2 >= 0 /\ H1 + S1 - 2 >= 0 /\ -H1 + S1 - 2 >= 0 /\ F1 + S1 - 2 >= 0 /\ -F1 + S1 - 2 >= 0 /\ J + S1 - 4 >= 0 /\ P1 >= 0 /\ H1 + P1 >= 0 /\ -H1 + P1 >= 0 /\ F1 + P1 >= 0 /\ -F1 + P1 >= 0 /\ J + P1 - 2 >= 0 /\ E1 - K1 >= 0 /\ D1 - J1 >= 0 /\ -D1 + J1 >= 0 /\ -H1 >= 0 /\ F1 - H1 >= 0 /\ -F1 - H1 >= 0 /\ J - H1 - 2 >= 0 /\ H1 >= 0 /\ F1 + H1 >= 0 /\ -F1 + H1 >= 0 /\ J + H1 - 2 >= 0 /\ -F1 >= 0 /\ J - F1 - 2 >= 0 /\ F1 >= 0 /\ J + F1 - 2 >= 0 /\ J - 2 >= 0 /\ C2 >= D1 + 1 /\ K1 >= 0 /\ X1 >= 2 /\ Y1 >= C2 + 1 /\ 0 >= Y1 + 1 /\ F1 = 0 ] f10(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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f10(A, B, C, D, E, F, G, H, I, X1, K, Y1, M, N, O, P, Q, R, S, T, U, V, W, A2, Y, Z, A1, B1, C1, D1, E1, 0, Y1, 0, Y1, D1, K1 - 1, K1 - 1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1)) [ I >= 0 /\ S1 + I - 2 >= 0 /\ P1 + I >= 0 /\ H1 + I >= 0 /\ -H1 + I >= 0 /\ F1 + I >= 0 /\ -F1 + I >= 0 /\ J + I - 2 >= 0 /\ E1 - H + 1 >= 0 /\ -K1 + H - 1 >= 0 /\ -E1 + H - 1 >= 0 /\ S1 - 2 >= 0 /\ P1 + S1 - 2 >= 0 /\ H1 + S1 - 2 >= 0 /\ -H1 + S1 - 2 >= 0 /\ F1 + S1 - 2 >= 0 /\ -F1 + S1 - 2 >= 0 /\ J + S1 - 4 >= 0 /\ P1 >= 0 /\ H1 + P1 >= 0 /\ -H1 + P1 >= 0 /\ F1 + P1 >= 0 /\ -F1 + P1 >= 0 /\ J + P1 - 2 >= 0 /\ E1 - K1 >= 0 /\ D1 - J1 >= 0 /\ -D1 + J1 >= 0 /\ -H1 >= 0 /\ F1 - H1 >= 0 /\ -F1 - H1 >= 0 /\ J - H1 - 2 >= 0 /\ H1 >= 0 /\ F1 + H1 >= 0 /\ -F1 + H1 >= 0 /\ J + H1 - 2 >= 0 /\ -F1 >= 0 /\ J - F1 - 2 >= 0 /\ F1 >= 0 /\ J + F1 - 2 >= 0 /\ J - 2 >= 0 /\ D1 >= C2 + 1 /\ K1 >= 0 /\ X1 >= 2 /\ C2 >= Y1 + 1 /\ Y1 >= 1 /\ F1 = 0 ] f10(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, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1) -> Com_1(f0(A, B, C, D, E, F, G, H, I, X1, Y1, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1, C1, F2, E1, E2, A2, C2, D2, G2, K1, L1, M1, N1, O1, P1, Q1, R1, S1, T1, U1, V1, W1)) [ I >= 0 /\ S1 + I - 2 >= 0 /\ P1 + I >= 0 /\ H1 + I >= 0 /\ -H1 + I >= 0 /\ F1 + I >= 0 /\ -F1 + I >= 0 /\ J + I - 2 >= 0 /\ E1 - H + 1 >= 0 /\ -K1 + H - 1 >= 0 /\ -E1 + H - 1 >= 0 /\ S1 - 2 >= 0 /\ P1 + S1 - 2 >= 0 /\ H1 + S1 - 2 >= 0 /\ -H1 + S1 - 2 >= 0 /\ F1 + S1 - 2 >= 0 /\ -F1 + S1 - 2 >= 0 /\ J + S1 - 4 >= 0 /\ P1 >= 0 /\ H1 + P1 >= 0 /\ -H1 + P1 >= 0 /\ F1 + P1 >= 0 /\ -F1 + P1 >= 0 /\ J + P1 - 2 >= 0 /\ E1 - K1 >= 0 /\ D1 - J1 >= 0 /\ -D1 + J1 >= 0 /\ -H1 >= 0 /\ F1 - H1 >= 0 /\ -F1 - H1 >= 0 /\ J - H1 - 2 >= 0 /\ H1 >= 0 /\ F1 + H1 >= 0 /\ -F1 + H1 >= 0 /\ J + H1 - 2 >= 0 /\ -F1 >= 0 /\ J - F1 - 2 >= 0 /\ F1 >= 0 /\ J + F1 - 2 >= 0 /\ J - 2 >= 0 /\ X1 >= 2 /\ K1 >= 0 /\ F1 = D1 ] )