(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, B, C1, E1, B, G, G, A, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1)) [ C - 2 >= 0 /\ B1 + C - 4 >= 0 /\ S + C - 4 >= 0 /\ -S + C >= 0 /\ J + C - 4 >= 0 /\ B1 - 2 >= 0 /\ S + B1 - 4 >= 0 /\ -S + B1 >= 0 /\ J + B1 - 4 >= 0 /\ -S + 2 >= 0 /\ J - S >= 0 /\ S - 2 >= 0 /\ J + S - 4 >= 0 /\ J - 2 >= 0 /\ A >= 0 /\ C1 >= 2 /\ 0 >= D1 + 1 /\ 0 >= E1 + 1 /\ 0 >= B + 1 ] 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, B, C1, E1, B, G, G, A, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1)) [ C - 2 >= 0 /\ B1 + C - 4 >= 0 /\ S + C - 4 >= 0 /\ -S + C >= 0 /\ J + C - 4 >= 0 /\ B1 - 2 >= 0 /\ S + B1 - 4 >= 0 /\ -S + B1 >= 0 /\ J + B1 - 4 >= 0 /\ -S + 2 >= 0 /\ J - S >= 0 /\ S - 2 >= 0 /\ J + S - 4 >= 0 /\ J - 2 >= 0 /\ A >= 0 /\ C1 >= 2 /\ 0 >= D1 + 1 /\ 0 >= E1 + 1 /\ B >= 1 ] 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, B, C1, E1, B, G, G, A, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1)) [ C - 2 >= 0 /\ B1 + C - 4 >= 0 /\ S + C - 4 >= 0 /\ -S + C >= 0 /\ J + C - 4 >= 0 /\ B1 - 2 >= 0 /\ S + B1 - 4 >= 0 /\ -S + B1 >= 0 /\ J + B1 - 4 >= 0 /\ -S + 2 >= 0 /\ J - S >= 0 /\ S - 2 >= 0 /\ J + S - 4 >= 0 /\ J - 2 >= 0 /\ A >= 0 /\ C1 >= 2 /\ 0 >= D1 + 1 /\ E1 >= 1 /\ 0 >= B + 1 ] 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, B, C1, E1, B, G, G, A, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1)) [ C - 2 >= 0 /\ B1 + C - 4 >= 0 /\ S + C - 4 >= 0 /\ -S + C >= 0 /\ J + C - 4 >= 0 /\ B1 - 2 >= 0 /\ S + B1 - 4 >= 0 /\ -S + B1 >= 0 /\ J + B1 - 4 >= 0 /\ -S + 2 >= 0 /\ J - S >= 0 /\ S - 2 >= 0 /\ J + S - 4 >= 0 /\ J - 2 >= 0 /\ A >= 0 /\ C1 >= 2 /\ 0 >= D1 + 1 /\ E1 >= 1 /\ B >= 1 ] 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, B, C1, E1, B, G, G, A, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1)) [ C - 2 >= 0 /\ B1 + C - 4 >= 0 /\ S + C - 4 >= 0 /\ -S + C >= 0 /\ J + C - 4 >= 0 /\ B1 - 2 >= 0 /\ S + B1 - 4 >= 0 /\ -S + B1 >= 0 /\ J + B1 - 4 >= 0 /\ -S + 2 >= 0 /\ J - S >= 0 /\ S - 2 >= 0 /\ J + S - 4 >= 0 /\ J - 2 >= 0 /\ A >= 0 /\ C1 >= 2 /\ D1 >= 1 /\ 0 >= E1 + 1 /\ 0 >= B + 1 ] 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, B, C1, E1, B, G, G, A, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1)) [ C - 2 >= 0 /\ B1 + C - 4 >= 0 /\ S + C - 4 >= 0 /\ -S + C >= 0 /\ J + C - 4 >= 0 /\ B1 - 2 >= 0 /\ S + B1 - 4 >= 0 /\ -S + B1 >= 0 /\ J + B1 - 4 >= 0 /\ -S + 2 >= 0 /\ J - S >= 0 /\ S - 2 >= 0 /\ J + S - 4 >= 0 /\ J - 2 >= 0 /\ A >= 0 /\ C1 >= 2 /\ D1 >= 1 /\ 0 >= E1 + 1 /\ B >= 1 ] 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, B, C1, E1, B, G, G, A, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1)) [ C - 2 >= 0 /\ B1 + C - 4 >= 0 /\ S + C - 4 >= 0 /\ -S + C >= 0 /\ J + C - 4 >= 0 /\ B1 - 2 >= 0 /\ S + B1 - 4 >= 0 /\ -S + B1 >= 0 /\ J + B1 - 4 >= 0 /\ -S + 2 >= 0 /\ J - S >= 0 /\ S - 2 >= 0 /\ J + S - 4 >= 0 /\ J - 2 >= 0 /\ A >= 0 /\ C1 >= 2 /\ D1 >= 1 /\ E1 >= 1 /\ 0 >= B + 1 ] 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, B, C1, E1, B, G, G, A, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, A1, B1)) [ C - 2 >= 0 /\ B1 + C - 4 >= 0 /\ S + C - 4 >= 0 /\ -S + C >= 0 /\ J + C - 4 >= 0 /\ B1 - 2 >= 0 /\ S + B1 - 4 >= 0 /\ -S + B1 >= 0 /\ J + B1 - 4 >= 0 /\ -S + 2 >= 0 /\ J - S >= 0 /\ S - 2 >= 0 /\ J + S - 4 >= 0 /\ J - 2 >= 0 /\ A >= 0 /\ C1 >= 2 /\ D1 >= 1 /\ E1 >= 1 /\ B >= 1 ] 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, E1, 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, B, C1, D, E, F, G, H, C1, 2, D1, F1, D1, N, O, E1, D1, 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, 0, C1, 0, E, F, G, H, N1, L1, O1, R1, Q1, N, O, M1, P1, R, S, E1, D1, 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, K, C1, E1, E, F, G, H, G1, F1, K1, N1, M1, N, O, P, L1, R, S, T, U, V, W, X, O1, P1, A1, D1)) [ 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 /\ D1 >= C1 /\ C1 >= 2 /\ 0 >= K + 1 /\ 0 >= E1 + 1 ] 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, K, C1, E1, E, F, G, H, G1, F1, K1, N1, M1, N, O, P, L1, R, S, T, U, V, W, X, O1, P1, A1, D1)) [ 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 /\ D1 >= C1 /\ C1 >= 2 /\ 0 >= K + 1 /\ E1 >= 1 ] 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, K, C1, E1, E, F, G, H, G1, F1, K1, N1, M1, N, O, P, L1, R, S, T, U, V, W, X, O1, P1, A1, D1)) [ 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 /\ D1 >= C1 /\ C1 >= 2 /\ K >= 1 /\ 0 >= E1 + 1 ] 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, K, C1, E1, E, F, G, H, G1, F1, K1, N1, M1, N, O, P, L1, R, S, T, U, V, W, X, O1, P1, A1, D1)) [ 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 /\ D1 >= C1 /\ C1 >= 2 /\ K >= 1 /\ E1 >= 1 ] )