(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (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) (RULES f0(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f36(A, B, 1, D, E, F, 0, A1, I, J, K, L, M, N, O, P, 0, Z, S, T, U, V, W, Y)) [ Y >= 2 ] f0(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f36(A, B, 1, D, E, F, 0, A1, I, J, K, L, M, N, O, P, 0, Z, S, T, U, V, W, Y)) [ 0 >= Y ] f0(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f15(A, B, 0, D, E, F, 0, Z, I, J, K, L, M, N, O, P, 0, Y, S, T, U, V, W, 1)) f36(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f61(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, 0, R, S, T, U, V, W, X)) [ -G >= 0 /\ C - G - 1 >= 0 /\ Q - G >= 0 /\ -Q - G >= 0 /\ G >= 0 /\ C + G - 1 >= 0 /\ Q + G >= 0 /\ -Q + G >= 0 /\ C - 1 >= 0 /\ Q + C - 1 >= 0 /\ -Q + C - 1 >= 0 /\ -Q >= 0 /\ Q >= 0 /\ C >= H + 1 ] f36(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f45(A, B, C, D, E, F, G, H, Y, Z, A1, B1, B1, N, O, P, Q, R, S, T, U, V, W, X)) [ -G >= 0 /\ C - G - 1 >= 0 /\ Q - G >= 0 /\ -Q - G >= 0 /\ G >= 0 /\ C + G - 1 >= 0 /\ Q + G >= 0 /\ -Q + G >= 0 /\ C - 1 >= 0 /\ Q + C - 1 >= 0 /\ -Q + C - 1 >= 0 /\ -Q >= 0 /\ Q >= 0 /\ H >= C ] 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) -> Com_1(f31(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X)) [ -G >= 0 /\ C - G >= 0 /\ X - G - 1 >= 0 /\ -X - G + 1 >= 0 /\ Q - G >= 0 /\ -Q - G >= 0 /\ G >= 0 /\ C + G >= 0 /\ X + G - 1 >= 0 /\ -X + G + 1 >= 0 /\ Q + G >= 0 /\ -Q + G >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ -X + C + 1 >= 0 /\ Q + C >= 0 /\ -Q + C >= 0 /\ -X + 1 >= 0 /\ Q - X + 1 >= 0 /\ -Q - X + 1 >= 0 /\ X - 1 >= 0 /\ Q + X - 1 >= 0 /\ -Q + X - 1 >= 0 /\ -Q >= 0 /\ Q >= 0 /\ C >= R ] 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) -> Com_1(f15(A, B, C + 1, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, Y, Z, 0, 0, 0, X)) [ -G >= 0 /\ C - G >= 0 /\ X - G - 1 >= 0 /\ -X - G + 1 >= 0 /\ Q - G >= 0 /\ -Q - G >= 0 /\ G >= 0 /\ C + G >= 0 /\ X + G - 1 >= 0 /\ -X + G + 1 >= 0 /\ Q + G >= 0 /\ -Q + G >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ -X + C + 1 >= 0 /\ Q + C >= 0 /\ -Q + C >= 0 /\ -X + 1 >= 0 /\ Q - X + 1 >= 0 /\ -Q - X + 1 >= 0 /\ X - 1 >= 0 /\ Q + X - 1 >= 0 /\ -Q + X - 1 >= 0 /\ -Q >= 0 /\ Q >= 0 /\ R >= C + 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) -> Com_1(f25(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, Y, Z, A1, A1, A1, X)) [ -G >= 0 /\ C - G >= 0 /\ X - G - 1 >= 0 /\ -X - G + 1 >= 0 /\ Q - G >= 0 /\ -Q - G >= 0 /\ G >= 0 /\ C + G >= 0 /\ X + G - 1 >= 0 /\ -X + G + 1 >= 0 /\ Q + G >= 0 /\ -Q + G >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ -X + C + 1 >= 0 /\ Q + C >= 0 /\ -Q + C >= 0 /\ -X + 1 >= 0 /\ Q - X + 1 >= 0 /\ -Q - X + 1 >= 0 /\ X - 1 >= 0 /\ Q + X - 1 >= 0 /\ -Q + X - 1 >= 0 /\ -Q >= 0 /\ Q >= 0 /\ A1 >= 1 /\ R >= C + 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) -> Com_1(f25(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, Y, Z, A1, A1, A1, X)) [ -G >= 0 /\ C - G >= 0 /\ X - G - 1 >= 0 /\ -X - G + 1 >= 0 /\ Q - G >= 0 /\ -Q - G >= 0 /\ G >= 0 /\ C + G >= 0 /\ X + G - 1 >= 0 /\ -X + G + 1 >= 0 /\ Q + G >= 0 /\ -Q + G >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ -X + C + 1 >= 0 /\ Q + C >= 0 /\ -Q + C >= 0 /\ -X + 1 >= 0 /\ Q - X + 1 >= 0 /\ -Q - X + 1 >= 0 /\ X - 1 >= 0 /\ Q + X - 1 >= 0 /\ -Q + X - 1 >= 0 /\ -Q >= 0 /\ Q >= 0 /\ 0 >= A1 + 1 /\ R >= C + 1 ] f31(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f31(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X)) [ -G >= 0 /\ C - G >= 0 /\ X - G - 1 >= 0 /\ -X - G + 1 >= 0 /\ Q - G >= 0 /\ -Q - G >= 0 /\ G >= 0 /\ C + G >= 0 /\ X + G - 1 >= 0 /\ -X + G + 1 >= 0 /\ Q + G >= 0 /\ -Q + G >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ -X + C + 1 >= 0 /\ -R + C >= 0 /\ Q + C >= 0 /\ -Q + C >= 0 /\ -X + 1 >= 0 /\ Q - X + 1 >= 0 /\ -Q - X + 1 >= 0 /\ X - 1 >= 0 /\ Q + X - 1 >= 0 /\ -Q + X - 1 >= 0 /\ -Q >= 0 /\ Q >= 0 ] f25(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f15(A, B, C + 1, Y, 0, 1, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X)) [ -G >= 0 /\ C - G >= 0 /\ X - G - 1 >= 0 /\ -X - G + 1 >= 0 /\ R - G - 1 >= 0 /\ Q - G >= 0 /\ -Q - G >= 0 /\ G >= 0 /\ C + G >= 0 /\ X + G - 1 >= 0 /\ -X + G + 1 >= 0 /\ R + G - 1 >= 0 /\ Q + G >= 0 /\ -Q + G >= 0 /\ R - C - 1 >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ -X + C + 1 >= 0 /\ R + C - 1 >= 0 /\ Q + C >= 0 /\ -Q + C >= 0 /\ -X + 1 >= 0 /\ R - X >= 0 /\ Q - X + 1 >= 0 /\ -Q - X + 1 >= 0 /\ X - 1 >= 0 /\ R + X - 2 >= 0 /\ Q + X - 1 >= 0 /\ -Q + X - 1 >= 0 /\ R - 1 >= 0 /\ Q + R - 1 >= 0 /\ -Q + R - 1 >= 0 /\ -Q >= 0 /\ Q >= 0 /\ B >= A ] f25(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f15(A, B, C + 1, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X)) [ -G >= 0 /\ C - G >= 0 /\ X - G - 1 >= 0 /\ -X - G + 1 >= 0 /\ R - G - 1 >= 0 /\ Q - G >= 0 /\ -Q - G >= 0 /\ G >= 0 /\ C + G >= 0 /\ X + G - 1 >= 0 /\ -X + G + 1 >= 0 /\ R + G - 1 >= 0 /\ Q + G >= 0 /\ -Q + G >= 0 /\ R - C - 1 >= 0 /\ C >= 0 /\ X + C - 1 >= 0 /\ -X + C + 1 >= 0 /\ R + C - 1 >= 0 /\ Q + C >= 0 /\ -Q + C >= 0 /\ -X + 1 >= 0 /\ R - X >= 0 /\ Q - X + 1 >= 0 /\ -Q - X + 1 >= 0 /\ X - 1 >= 0 /\ R + X - 2 >= 0 /\ Q + X - 1 >= 0 /\ -Q + X - 1 >= 0 /\ R - 1 >= 0 /\ Q + R - 1 >= 0 /\ -Q + R - 1 >= 0 /\ -Q >= 0 /\ Q >= 0 /\ A >= B + 1 ] f61(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f61(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X)) [ C - H - 1 >= 0 /\ -G >= 0 /\ C - G - 1 >= 0 /\ Q - G >= 0 /\ -Q - G >= 0 /\ G >= 0 /\ C + G - 1 >= 0 /\ Q + G >= 0 /\ -Q + G >= 0 /\ C - 1 >= 0 /\ Q + C - 1 >= 0 /\ -Q + C - 1 >= 0 /\ -Q >= 0 /\ Q >= 0 ] f45(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f36(A, B, C + 1, D, E, F, G, H, I, J, K, L, 0, 0, O, P, Q, R, S, T, U, V, W, X)) [ H - 1 >= 0 /\ G + H - 1 >= 0 /\ -G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ -C + H >= 0 /\ Q + H - 1 >= 0 /\ -Q + H - 1 >= 0 /\ -G >= 0 /\ C - G - 1 >= 0 /\ Q - G >= 0 /\ -Q - G >= 0 /\ G >= 0 /\ C + G - 1 >= 0 /\ Q + G >= 0 /\ -Q + G >= 0 /\ C - 1 >= 0 /\ Q + C - 1 >= 0 /\ -Q + C - 1 >= 0 /\ -Q >= 0 /\ Q >= 0 /\ M = 0 ] f45(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f46(A, B, C, D, E, F, G, H, I, J, K, L, M, M, O, P, Q, R, S, T, U, V, W, X)) [ H - 1 >= 0 /\ G + H - 1 >= 0 /\ -G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ -C + H >= 0 /\ Q + H - 1 >= 0 /\ -Q + H - 1 >= 0 /\ -G >= 0 /\ C - G - 1 >= 0 /\ Q - G >= 0 /\ -Q - G >= 0 /\ G >= 0 /\ C + G - 1 >= 0 /\ Q + G >= 0 /\ -Q + G >= 0 /\ C - 1 >= 0 /\ Q + C - 1 >= 0 /\ -Q + C - 1 >= 0 /\ -Q >= 0 /\ Q >= 0 /\ M >= 1 ] f45(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f46(A, B, C, D, E, F, G, H, I, J, K, L, M, M, O, P, Q, R, S, T, U, V, W, X)) [ H - 1 >= 0 /\ G + H - 1 >= 0 /\ -G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ -C + H >= 0 /\ Q + H - 1 >= 0 /\ -Q + H - 1 >= 0 /\ -G >= 0 /\ C - G - 1 >= 0 /\ Q - G >= 0 /\ -Q - G >= 0 /\ G >= 0 /\ C + G - 1 >= 0 /\ Q + G >= 0 /\ -Q + G >= 0 /\ C - 1 >= 0 /\ Q + C - 1 >= 0 /\ -Q + C - 1 >= 0 /\ -Q >= 0 /\ Q >= 0 /\ 0 >= M + 1 ] f46(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f45(A, B, C, D, E, F, G, H, I, Y, Z, A1, A1, N, O, B1, Q, R, S, T, U, V, W, X)) [ H - 1 >= 0 /\ G + H - 1 >= 0 /\ -G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ -C + H >= 0 /\ Q + H - 1 >= 0 /\ -Q + H - 1 >= 0 /\ -G >= 0 /\ C - G - 1 >= 0 /\ Q - G >= 0 /\ -Q - G >= 0 /\ G >= 0 /\ C + G - 1 >= 0 /\ Q + G >= 0 /\ -Q + G >= 0 /\ C - 1 >= 0 /\ Q + C - 1 >= 0 /\ -Q + C - 1 >= 0 /\ -Q >= 0 /\ Q >= 0 /\ M - N >= 0 /\ -M + N >= 0 /\ B >= A ] f46(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f36(A, B, C + 1, Y, 0, F, G, H, I, J, K, L, M, N, Z, P, Q, R, S, T, U, V, W, X)) [ H - 1 >= 0 /\ G + H - 1 >= 0 /\ -G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ -C + H >= 0 /\ Q + H - 1 >= 0 /\ -Q + H - 1 >= 0 /\ -G >= 0 /\ C - G - 1 >= 0 /\ Q - G >= 0 /\ -Q - G >= 0 /\ G >= 0 /\ C + G - 1 >= 0 /\ Q + G >= 0 /\ -Q + G >= 0 /\ C - 1 >= 0 /\ Q + C - 1 >= 0 /\ -Q + C - 1 >= 0 /\ -Q >= 0 /\ Q >= 0 /\ M - N >= 0 /\ -M + N >= 0 /\ B >= A ] f46(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X) -> Com_1(f36(A, B, C + 1, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X)) [ H - 1 >= 0 /\ G + H - 1 >= 0 /\ -G + H - 1 >= 0 /\ C + H - 2 >= 0 /\ -C + H >= 0 /\ Q + H - 1 >= 0 /\ -Q + H - 1 >= 0 /\ -G >= 0 /\ C - G - 1 >= 0 /\ Q - G >= 0 /\ -Q - G >= 0 /\ G >= 0 /\ C + G - 1 >= 0 /\ Q + G >= 0 /\ -Q + G >= 0 /\ C - 1 >= 0 /\ Q + C - 1 >= 0 /\ -Q + C - 1 >= 0 /\ -Q >= 0 /\ Q >= 0 /\ M - N >= 0 /\ -M + N >= 0 /\ A >= B + 1 ] )