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