(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS f0))
(VAR A B C D E F G H I J K L M N O)
(RULES
  f0(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O) -> Com_1(f1(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O))
  f1(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O) -> Com_1(f7(A - 1, 1, D, D, F, F, Q, P, 0, 1, Q, P, 7, N, O)) [ A >= 1 /\ 7 >= P /\ 7 >= Q /\ 3 >= P /\ P >= 1 /\ Q >= 1 ]
  f1(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O) -> Com_1(f7(A, 1, D, D, F, F, Q, P, 0, 1, Q, P, 7, N, O)) [ 7 >= P /\ 7 >= Q /\ P >= 5 /\ Q >= 1 ]
  f1(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O) -> Com_1(f7(A, 1, D + 1, D + 1, F + 1, F + 1, Q, 4, 1, 1, Q, 4, 7, N, O)) [ 7 >= Q /\ Q >= 1 ]
  f1(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O) -> Com_1(f2(A, 0, D, D, F, F, 3, Q, 0, 0, 3, Q, 2, N, O)) [ 7 >= Q /\ 3 >= Q /\ Q >= 1 ]
  f1(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O) -> Com_1(f2(A, 0, D, D, F, F, 3, Q, 0, 0, 3, Q, 2, N, O)) [ 7 >= Q /\ Q >= 5 ]
  f1(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O) -> Com_1(f2(A, 0, D + 1, D + 1, F + 1, F + 1, 3, 4, 1, 0, 3, 4, 2, N, O))
  f2(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O) -> Com_1(f7(A, 1, D, D, F, F, Q, P, I, 1, Q, P, 7, N, O)) [ -I + 1 >= 0 /\ B - I + 1 >= 0 /\ -B - I + 1 >= 0 /\ M - I - 1 >= 0 /\ -M - I + 3 >= 0 /\ L - I >= 0 /\ -L - I + 8 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 1 >= 0 /\ I >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ M + I - 2 >= 0 /\ -M + I + 2 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 7 >= 0 /\ J + I >= 0 /\ -J + I >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ C - D >= 0 /\ -C + D >= 0 /\ -B >= 0 /\ M - B - 2 >= 0 /\ -M - B + 2 >= 0 /\ L - B - 1 >= 0 /\ -L - B + 7 >= 0 /\ J - B >= 0 /\ -J - B >= 0 /\ B >= 0 /\ M + B - 2 >= 0 /\ -M + B + 2 >= 0 /\ L + B - 1 >= 0 /\ -L + B + 7 >= 0 /\ J + B >= 0 /\ -J + B >= 0 /\ -M + 2 >= 0 /\ L - M + 1 >= 0 /\ -L - M + 9 >= 0 /\ J - M + 2 >= 0 /\ -J - M + 2 >= 0 /\ M - 2 >= 0 /\ L + M - 3 >= 0 /\ -L + M + 5 >= 0 /\ J + M - 2 >= 0 /\ -J + M - 2 >= 0 /\ -L + 7 >= 0 /\ J - L + 7 >= 0 /\ -J - L + 7 >= 0 /\ L - 1 >= 0 /\ J + L - 1 >= 0 /\ -J + L - 1 >= 0 /\ -J >= 0 /\ J >= 0 /\ 7 >= P /\ 7 >= Q /\ 3 >= P /\ P >= 1 /\ Q >= 1 ]
  f2(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O) -> Com_1(f7(A, 1, D, D, F, F, Q, P, I, 1, Q, P, 7, N, O)) [ -I + 1 >= 0 /\ B - I + 1 >= 0 /\ -B - I + 1 >= 0 /\ M - I - 1 >= 0 /\ -M - I + 3 >= 0 /\ L - I >= 0 /\ -L - I + 8 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 1 >= 0 /\ I >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ M + I - 2 >= 0 /\ -M + I + 2 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 7 >= 0 /\ J + I >= 0 /\ -J + I >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ C - D >= 0 /\ -C + D >= 0 /\ -B >= 0 /\ M - B - 2 >= 0 /\ -M - B + 2 >= 0 /\ L - B - 1 >= 0 /\ -L - B + 7 >= 0 /\ J - B >= 0 /\ -J - B >= 0 /\ B >= 0 /\ M + B - 2 >= 0 /\ -M + B + 2 >= 0 /\ L + B - 1 >= 0 /\ -L + B + 7 >= 0 /\ J + B >= 0 /\ -J + B >= 0 /\ -M + 2 >= 0 /\ L - M + 1 >= 0 /\ -L - M + 9 >= 0 /\ J - M + 2 >= 0 /\ -J - M + 2 >= 0 /\ M - 2 >= 0 /\ L + M - 3 >= 0 /\ -L + M + 5 >= 0 /\ J + M - 2 >= 0 /\ -J + M - 2 >= 0 /\ -L + 7 >= 0 /\ J - L + 7 >= 0 /\ -J - L + 7 >= 0 /\ L - 1 >= 0 /\ J + L - 1 >= 0 /\ -J + L - 1 >= 0 /\ -J >= 0 /\ J >= 0 /\ 7 >= P /\ 7 >= Q /\ P >= 5 /\ Q >= 1 ]
  f2(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O) -> Com_1(f7(A, 1, D + 1, D + 1, F + 1, F + 1, Q, 4, 1, 1, Q, 4, 7, N, O)) [ -I + 1 >= 0 /\ B - I + 1 >= 0 /\ -B - I + 1 >= 0 /\ M - I - 1 >= 0 /\ -M - I + 3 >= 0 /\ L - I >= 0 /\ -L - I + 8 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 1 >= 0 /\ I >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ M + I - 2 >= 0 /\ -M + I + 2 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 7 >= 0 /\ J + I >= 0 /\ -J + I >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ C - D >= 0 /\ -C + D >= 0 /\ -B >= 0 /\ M - B - 2 >= 0 /\ -M - B + 2 >= 0 /\ L - B - 1 >= 0 /\ -L - B + 7 >= 0 /\ J - B >= 0 /\ -J - B >= 0 /\ B >= 0 /\ M + B - 2 >= 0 /\ -M + B + 2 >= 0 /\ L + B - 1 >= 0 /\ -L + B + 7 >= 0 /\ J + B >= 0 /\ -J + B >= 0 /\ -M + 2 >= 0 /\ L - M + 1 >= 0 /\ -L - M + 9 >= 0 /\ J - M + 2 >= 0 /\ -J - M + 2 >= 0 /\ M - 2 >= 0 /\ L + M - 3 >= 0 /\ -L + M + 5 >= 0 /\ J + M - 2 >= 0 /\ -J + M - 2 >= 0 /\ -L + 7 >= 0 /\ J - L + 7 >= 0 /\ -J - L + 7 >= 0 /\ L - 1 >= 0 /\ J + L - 1 >= 0 /\ -J + L - 1 >= 0 /\ -J >= 0 /\ J >= 0 /\ 7 >= Q /\ Q >= 1 ]
  f2(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O) -> Com_1(f3(A, 0, D, D, F, F, Q, P, I, 0, Q, P, 3, N, O)) [ -I + 1 >= 0 /\ B - I + 1 >= 0 /\ -B - I + 1 >= 0 /\ M - I - 1 >= 0 /\ -M - I + 3 >= 0 /\ L - I >= 0 /\ -L - I + 8 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 1 >= 0 /\ I >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ M + I - 2 >= 0 /\ -M + I + 2 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 7 >= 0 /\ J + I >= 0 /\ -J + I >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ C - D >= 0 /\ -C + D >= 0 /\ -B >= 0 /\ M - B - 2 >= 0 /\ -M - B + 2 >= 0 /\ L - B - 1 >= 0 /\ -L - B + 7 >= 0 /\ J - B >= 0 /\ -J - B >= 0 /\ B >= 0 /\ M + B - 2 >= 0 /\ -M + B + 2 >= 0 /\ L + B - 1 >= 0 /\ -L + B + 7 >= 0 /\ J + B >= 0 /\ -J + B >= 0 /\ -M + 2 >= 0 /\ L - M + 1 >= 0 /\ -L - M + 9 >= 0 /\ J - M + 2 >= 0 /\ -J - M + 2 >= 0 /\ M - 2 >= 0 /\ L + M - 3 >= 0 /\ -L + M + 5 >= 0 /\ J + M - 2 >= 0 /\ -J + M - 2 >= 0 /\ -L + 7 >= 0 /\ J - L + 7 >= 0 /\ -J - L + 7 >= 0 /\ L - 1 >= 0 /\ J + L - 1 >= 0 /\ -J + L - 1 >= 0 /\ -J >= 0 /\ J >= 0 /\ 7 >= P /\ 7 >= Q /\ 3 >= P /\ P >= 1 /\ Q >= 1 ]
  f2(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O) -> Com_1(f3(A, 0, D, D, F, F, Q, P, I, 0, Q, P, 3, N, O)) [ -I + 1 >= 0 /\ B - I + 1 >= 0 /\ -B - I + 1 >= 0 /\ M - I - 1 >= 0 /\ -M - I + 3 >= 0 /\ L - I >= 0 /\ -L - I + 8 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 1 >= 0 /\ I >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ M + I - 2 >= 0 /\ -M + I + 2 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 7 >= 0 /\ J + I >= 0 /\ -J + I >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ C - D >= 0 /\ -C + D >= 0 /\ -B >= 0 /\ M - B - 2 >= 0 /\ -M - B + 2 >= 0 /\ L - B - 1 >= 0 /\ -L - B + 7 >= 0 /\ J - B >= 0 /\ -J - B >= 0 /\ B >= 0 /\ M + B - 2 >= 0 /\ -M + B + 2 >= 0 /\ L + B - 1 >= 0 /\ -L + B + 7 >= 0 /\ J + B >= 0 /\ -J + B >= 0 /\ -M + 2 >= 0 /\ L - M + 1 >= 0 /\ -L - M + 9 >= 0 /\ J - M + 2 >= 0 /\ -J - M + 2 >= 0 /\ M - 2 >= 0 /\ L + M - 3 >= 0 /\ -L + M + 5 >= 0 /\ J + M - 2 >= 0 /\ -J + M - 2 >= 0 /\ -L + 7 >= 0 /\ J - L + 7 >= 0 /\ -J - L + 7 >= 0 /\ L - 1 >= 0 /\ J + L - 1 >= 0 /\ -J + L - 1 >= 0 /\ -J >= 0 /\ J >= 0 /\ 7 >= P /\ 7 >= Q /\ P >= 5 /\ Q >= 1 ]
  f2(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O) -> Com_1(f3(A, 0, D + 1, D + 1, F + 1, F + 1, Q, 4, 1, 0, Q, 4, 3, N, O)) [ -I + 1 >= 0 /\ B - I + 1 >= 0 /\ -B - I + 1 >= 0 /\ M - I - 1 >= 0 /\ -M - I + 3 >= 0 /\ L - I >= 0 /\ -L - I + 8 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 1 >= 0 /\ I >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ M + I - 2 >= 0 /\ -M + I + 2 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 7 >= 0 /\ J + I >= 0 /\ -J + I >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ C - D >= 0 /\ -C + D >= 0 /\ -B >= 0 /\ M - B - 2 >= 0 /\ -M - B + 2 >= 0 /\ L - B - 1 >= 0 /\ -L - B + 7 >= 0 /\ J - B >= 0 /\ -J - B >= 0 /\ B >= 0 /\ M + B - 2 >= 0 /\ -M + B + 2 >= 0 /\ L + B - 1 >= 0 /\ -L + B + 7 >= 0 /\ J + B >= 0 /\ -J + B >= 0 /\ -M + 2 >= 0 /\ L - M + 1 >= 0 /\ -L - M + 9 >= 0 /\ J - M + 2 >= 0 /\ -J - M + 2 >= 0 /\ M - 2 >= 0 /\ L + M - 3 >= 0 /\ -L + M + 5 >= 0 /\ J + M - 2 >= 0 /\ -J + M - 2 >= 0 /\ -L + 7 >= 0 /\ J - L + 7 >= 0 /\ -J - L + 7 >= 0 /\ L - 1 >= 0 /\ J + L - 1 >= 0 /\ -J + L - 1 >= 0 /\ -J >= 0 /\ J >= 0 /\ 7 >= Q /\ Q >= 1 ]
  f3(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O) -> Com_1(f6(A, 1, D, D, F, F, Q, P, I, 1, Q, P, 6, N, O)) [ -I + 1 >= 0 /\ B - I + 1 >= 0 /\ -B - I + 1 >= 0 /\ M - I - 2 >= 0 /\ -M - I + 4 >= 0 /\ L - I >= 0 /\ -L - I + 8 >= 0 /\ K - I >= 0 /\ -K - I + 8 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 1 >= 0 /\ I >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ M + I - 3 >= 0 /\ -M + I + 3 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 7 >= 0 /\ K + I - 1 >= 0 /\ -K + I + 7 >= 0 /\ J + I >= 0 /\ -J + I >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ C - D >= 0 /\ -C + D >= 0 /\ -B >= 0 /\ M - B - 3 >= 0 /\ -M - B + 3 >= 0 /\ L - B - 1 >= 0 /\ -L - B + 7 >= 0 /\ K - B - 1 >= 0 /\ -K - B + 7 >= 0 /\ J - B >= 0 /\ -J - B >= 0 /\ B >= 0 /\ M + B - 3 >= 0 /\ -M + B + 3 >= 0 /\ L + B - 1 >= 0 /\ -L + B + 7 >= 0 /\ K + B - 1 >= 0 /\ -K + B + 7 >= 0 /\ J + B >= 0 /\ -J + B >= 0 /\ -M + 3 >= 0 /\ L - M + 2 >= 0 /\ -L - M + 10 >= 0 /\ K - M + 2 >= 0 /\ -K - M + 10 >= 0 /\ J - M + 3 >= 0 /\ -J - M + 3 >= 0 /\ M - 3 >= 0 /\ L + M - 4 >= 0 /\ -L + M + 4 >= 0 /\ K + M - 4 >= 0 /\ -K + M + 4 >= 0 /\ J + M - 3 >= 0 /\ -J + M - 3 >= 0 /\ -L + 7 >= 0 /\ K - L + 6 >= 0 /\ -K - L + 14 >= 0 /\ J - L + 7 >= 0 /\ -J - L + 7 >= 0 /\ L - 1 >= 0 /\ K + L - 2 >= 0 /\ -K + L + 6 >= 0 /\ J + L - 1 >= 0 /\ -J + L - 1 >= 0 /\ -K + 7 >= 0 /\ J - K + 7 >= 0 /\ -J - K + 7 >= 0 /\ K - 1 >= 0 /\ J + K - 1 >= 0 /\ -J + K - 1 >= 0 /\ -J >= 0 /\ J >= 0 /\ 7 >= P /\ 7 >= Q /\ 3 >= P /\ P >= 1 /\ Q >= 1 ]
  f3(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O) -> Com_1(f6(A, 1, D, D, F, F, Q, P, I, 1, Q, P, 6, N, O)) [ -I + 1 >= 0 /\ B - I + 1 >= 0 /\ -B - I + 1 >= 0 /\ M - I - 2 >= 0 /\ -M - I + 4 >= 0 /\ L - I >= 0 /\ -L - I + 8 >= 0 /\ K - I >= 0 /\ -K - I + 8 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 1 >= 0 /\ I >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ M + I - 3 >= 0 /\ -M + I + 3 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 7 >= 0 /\ K + I - 1 >= 0 /\ -K + I + 7 >= 0 /\ J + I >= 0 /\ -J + I >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ C - D >= 0 /\ -C + D >= 0 /\ -B >= 0 /\ M - B - 3 >= 0 /\ -M - B + 3 >= 0 /\ L - B - 1 >= 0 /\ -L - B + 7 >= 0 /\ K - B - 1 >= 0 /\ -K - B + 7 >= 0 /\ J - B >= 0 /\ -J - B >= 0 /\ B >= 0 /\ M + B - 3 >= 0 /\ -M + B + 3 >= 0 /\ L + B - 1 >= 0 /\ -L + B + 7 >= 0 /\ K + B - 1 >= 0 /\ -K + B + 7 >= 0 /\ J + B >= 0 /\ -J + B >= 0 /\ -M + 3 >= 0 /\ L - M + 2 >= 0 /\ -L - M + 10 >= 0 /\ K - M + 2 >= 0 /\ -K - M + 10 >= 0 /\ J - M + 3 >= 0 /\ -J - M + 3 >= 0 /\ M - 3 >= 0 /\ L + M - 4 >= 0 /\ -L + M + 4 >= 0 /\ K + M - 4 >= 0 /\ -K + M + 4 >= 0 /\ J + M - 3 >= 0 /\ -J + M - 3 >= 0 /\ -L + 7 >= 0 /\ K - L + 6 >= 0 /\ -K - L + 14 >= 0 /\ J - L + 7 >= 0 /\ -J - L + 7 >= 0 /\ L - 1 >= 0 /\ K + L - 2 >= 0 /\ -K + L + 6 >= 0 /\ J + L - 1 >= 0 /\ -J + L - 1 >= 0 /\ -K + 7 >= 0 /\ J - K + 7 >= 0 /\ -J - K + 7 >= 0 /\ K - 1 >= 0 /\ J + K - 1 >= 0 /\ -J + K - 1 >= 0 /\ -J >= 0 /\ J >= 0 /\ 7 >= P /\ 7 >= Q /\ P >= 5 /\ Q >= 1 ]
  f3(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O) -> Com_1(f6(A, 1, D + 1, D + 1, F + 1, F + 1, Q, 4, 1, 1, Q, 4, 6, N, O)) [ -I + 1 >= 0 /\ B - I + 1 >= 0 /\ -B - I + 1 >= 0 /\ M - I - 2 >= 0 /\ -M - I + 4 >= 0 /\ L - I >= 0 /\ -L - I + 8 >= 0 /\ K - I >= 0 /\ -K - I + 8 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 1 >= 0 /\ I >= 0 /\ B + I >= 0 /\ -B + I >= 0 /\ M + I - 3 >= 0 /\ -M + I + 3 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 7 >= 0 /\ K + I - 1 >= 0 /\ -K + I + 7 >= 0 /\ J + I >= 0 /\ -J + I >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ C - D >= 0 /\ -C + D >= 0 /\ -B >= 0 /\ M - B - 3 >= 0 /\ -M - B + 3 >= 0 /\ L - B - 1 >= 0 /\ -L - B + 7 >= 0 /\ K - B - 1 >= 0 /\ -K - B + 7 >= 0 /\ J - B >= 0 /\ -J - B >= 0 /\ B >= 0 /\ M + B - 3 >= 0 /\ -M + B + 3 >= 0 /\ L + B - 1 >= 0 /\ -L + B + 7 >= 0 /\ K + B - 1 >= 0 /\ -K + B + 7 >= 0 /\ J + B >= 0 /\ -J + B >= 0 /\ -M + 3 >= 0 /\ L - M + 2 >= 0 /\ -L - M + 10 >= 0 /\ K - M + 2 >= 0 /\ -K - M + 10 >= 0 /\ J - M + 3 >= 0 /\ -J - M + 3 >= 0 /\ M - 3 >= 0 /\ L + M - 4 >= 0 /\ -L + M + 4 >= 0 /\ K + M - 4 >= 0 /\ -K + M + 4 >= 0 /\ J + M - 3 >= 0 /\ -J + M - 3 >= 0 /\ -L + 7 >= 0 /\ K - L + 6 >= 0 /\ -K - L + 14 >= 0 /\ J - L + 7 >= 0 /\ -J - L + 7 >= 0 /\ L - 1 >= 0 /\ K + L - 2 >= 0 /\ -K + L + 6 >= 0 /\ J + L - 1 >= 0 /\ -J + L - 1 >= 0 /\ -K + 7 >= 0 /\ J - K + 7 >= 0 /\ -J - K + 7 >= 0 /\ K - 1 >= 0 /\ J + K - 1 >= 0 /\ -J + K - 1 >= 0 /\ -J >= 0 /\ J >= 0 /\ 7 >= Q /\ Q >= 1 ]
  f6(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O) -> Com_1(f4(A, 1, D, D, F, F, Q, 2, 0, 1, Q, 2, 4, N, O)) [ -I + 1 >= 0 /\ B - I >= 0 /\ -B - I + 2 >= 0 /\ M - I - 5 >= 0 /\ -M - I + 7 >= 0 /\ L - I >= 0 /\ -L - I + 8 >= 0 /\ K - I >= 0 /\ -K - I + 8 >= 0 /\ J - I >= 0 /\ -J - I + 2 >= 0 /\ I >= 0 /\ B + I - 1 >= 0 /\ -B + I + 1 >= 0 /\ M + I - 6 >= 0 /\ -M + I + 6 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 7 >= 0 /\ K + I - 1 >= 0 /\ -K + I + 7 >= 0 /\ J + I - 1 >= 0 /\ -J + I + 1 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ C - D >= 0 /\ -C + D >= 0 /\ -B + 1 >= 0 /\ M - B - 5 >= 0 /\ -M - B + 7 >= 0 /\ L - B >= 0 /\ -L - B + 8 >= 0 /\ K - B >= 0 /\ -K - B + 8 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ B - 1 >= 0 /\ M + B - 7 >= 0 /\ -M + B + 5 >= 0 /\ L + B - 2 >= 0 /\ -L + B + 6 >= 0 /\ K + B - 2 >= 0 /\ -K + B + 6 >= 0 /\ J + B - 2 >= 0 /\ -J + B >= 0 /\ -M + 6 >= 0 /\ L - M + 5 >= 0 /\ -L - M + 13 >= 0 /\ K - M + 5 >= 0 /\ -K - M + 13 >= 0 /\ J - M + 5 >= 0 /\ -J - M + 7 >= 0 /\ M - 6 >= 0 /\ L + M - 7 >= 0 /\ -L + M + 1 >= 0 /\ K + M - 7 >= 0 /\ -K + M + 1 >= 0 /\ J + M - 7 >= 0 /\ -J + M - 5 >= 0 /\ -L + 7 >= 0 /\ K - L + 6 >= 0 /\ -K - L + 14 >= 0 /\ J - L + 6 >= 0 /\ -J - L + 8 >= 0 /\ L - 1 >= 0 /\ K + L - 2 >= 0 /\ -K + L + 6 >= 0 /\ J + L - 2 >= 0 /\ -J + L >= 0 /\ -K + 7 >= 0 /\ J - K + 6 >= 0 /\ -J - K + 8 >= 0 /\ K - 1 >= 0 /\ J + K - 2 >= 0 /\ -J + K >= 0 /\ -J + 1 >= 0 /\ J - 1 >= 0 /\ Q >= 1 /\ 7 >= Q ]
  f6(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O) -> Com_1(f4(A, Q, D, D, F, F, P, 7, 1, Q, P, 7, 4, N, O)) [ -I + 1 >= 0 /\ B - I >= 0 /\ -B - I + 2 >= 0 /\ M - I - 5 >= 0 /\ -M - I + 7 >= 0 /\ L - I >= 0 /\ -L - I + 8 >= 0 /\ K - I >= 0 /\ -K - I + 8 >= 0 /\ J - I >= 0 /\ -J - I + 2 >= 0 /\ I >= 0 /\ B + I - 1 >= 0 /\ -B + I + 1 >= 0 /\ M + I - 6 >= 0 /\ -M + I + 6 >= 0 /\ L + I - 1 >= 0 /\ -L + I + 7 >= 0 /\ K + I - 1 >= 0 /\ -K + I + 7 >= 0 /\ J + I - 1 >= 0 /\ -J + I + 1 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ C - D >= 0 /\ -C + D >= 0 /\ -B + 1 >= 0 /\ M - B - 5 >= 0 /\ -M - B + 7 >= 0 /\ L - B >= 0 /\ -L - B + 8 >= 0 /\ K - B >= 0 /\ -K - B + 8 >= 0 /\ J - B >= 0 /\ -J - B + 2 >= 0 /\ B - 1 >= 0 /\ M + B - 7 >= 0 /\ -M + B + 5 >= 0 /\ L + B - 2 >= 0 /\ -L + B + 6 >= 0 /\ K + B - 2 >= 0 /\ -K + B + 6 >= 0 /\ J + B - 2 >= 0 /\ -J + B >= 0 /\ -M + 6 >= 0 /\ L - M + 5 >= 0 /\ -L - M + 13 >= 0 /\ K - M + 5 >= 0 /\ -K - M + 13 >= 0 /\ J - M + 5 >= 0 /\ -J - M + 7 >= 0 /\ M - 6 >= 0 /\ L + M - 7 >= 0 /\ -L + M + 1 >= 0 /\ K + M - 7 >= 0 /\ -K + M + 1 >= 0 /\ J + M - 7 >= 0 /\ -J + M - 5 >= 0 /\ -L + 7 >= 0 /\ K - L + 6 >= 0 /\ -K - L + 14 >= 0 /\ J - L + 6 >= 0 /\ -J - L + 8 >= 0 /\ L - 1 >= 0 /\ K + L - 2 >= 0 /\ -K + L + 6 >= 0 /\ J + L - 2 >= 0 /\ -J + L >= 0 /\ -K + 7 >= 0 /\ J - K + 6 >= 0 /\ -J - K + 8 >= 0 /\ K - 1 >= 0 /\ J + K - 2 >= 0 /\ -J + K >= 0 /\ -J + 1 >= 0 /\ J - 1 >= 0 /\ 7 >= P /\ 1 >= Q /\ Q >= 0 /\ P >= 1 /\ I = 1 ]
  f4(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O) -> Com_1(f2(A, 0, D, D, F, F, Q, P, 1, 0, Q, P, 2, N, O)) [ -I + 1 >= 0 /\ H - I - 2 >= 0 /\ -H - I + 8 >= 0 /\ M - I - 3 >= 0 /\ -M - I + 5 >= 0 /\ L - I - 2 >= 0 /\ -L - I + 8 >= 0 /\ K - I >= 0 /\ -K - I + 8 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ I >= 0 /\ H + I - 2 >= 0 /\ -H + I + 6 >= 0 /\ M + I - 4 >= 0 /\ -M + I + 4 >= 0 /\ L + I - 2 >= 0 /\ -L + I + 6 >= 0 /\ K + I - 1 >= 0 /\ -K + I + 7 >= 0 /\ J + I - 1 >= 0 /\ -J + I + 1 >= 0 /\ -H + 7 >= 0 /\ M - H + 3 >= 0 /\ -M - H + 11 >= 0 /\ L - H >= 0 /\ -L - H + 14 >= 0 /\ K - H + 6 >= 0 /\ -K - H + 14 >= 0 /\ J - H + 7 >= 0 /\ -J - H + 8 >= 0 /\ H - 2 >= 0 /\ M + H - 6 >= 0 /\ -M + H + 2 >= 0 /\ L + H - 4 >= 0 /\ -L + H >= 0 /\ K + H - 3 >= 0 /\ -K + H + 5 >= 0 /\ J + H - 3 >= 0 /\ -J + H - 1 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ C - D >= 0 /\ -C + D >= 0 /\ -M + 4 >= 0 /\ L - M + 2 >= 0 /\ -L - M + 11 >= 0 /\ K - M + 3 >= 0 /\ -K - M + 11 >= 0 /\ J - M + 4 >= 0 /\ -J - M + 5 >= 0 /\ M - 4 >= 0 /\ L + M - 6 >= 0 /\ -L + M + 3 >= 0 /\ K + M - 5 >= 0 /\ -K + M + 3 >= 0 /\ J + M - 4 >= 0 /\ -J + M - 3 >= 0 /\ -L + 7 >= 0 /\ K - L + 6 >= 0 /\ -K - L + 14 >= 0 /\ J - L + 7 >= 0 /\ -J - L + 8 >= 0 /\ L - 2 >= 0 /\ K + L - 3 >= 0 /\ -K + L + 5 >= 0 /\ J + L - 3 >= 0 /\ -J + L - 1 >= 0 /\ -K + 7 >= 0 /\ J - K + 7 >= 0 /\ -J - K + 8 >= 0 /\ K - 1 >= 0 /\ J + K - 1 >= 0 /\ -J + K >= 0 /\ -J + 1 >= 0 /\ J >= 0 /\ N >= 1 /\ N >= F + 1 /\ O >= 1 /\ O >= D + 1 /\ 7 >= P /\ 7 >= Q /\ 3 >= P /\ P >= 1 /\ Q >= 1 /\ I = 1 ]
  f4(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O) -> Com_1(f2(A, 0, D, D, F, F, Q, P, 1, 0, Q, P, 2, N, O)) [ -I + 1 >= 0 /\ H - I - 2 >= 0 /\ -H - I + 8 >= 0 /\ M - I - 3 >= 0 /\ -M - I + 5 >= 0 /\ L - I - 2 >= 0 /\ -L - I + 8 >= 0 /\ K - I >= 0 /\ -K - I + 8 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ I >= 0 /\ H + I - 2 >= 0 /\ -H + I + 6 >= 0 /\ M + I - 4 >= 0 /\ -M + I + 4 >= 0 /\ L + I - 2 >= 0 /\ -L + I + 6 >= 0 /\ K + I - 1 >= 0 /\ -K + I + 7 >= 0 /\ J + I - 1 >= 0 /\ -J + I + 1 >= 0 /\ -H + 7 >= 0 /\ M - H + 3 >= 0 /\ -M - H + 11 >= 0 /\ L - H >= 0 /\ -L - H + 14 >= 0 /\ K - H + 6 >= 0 /\ -K - H + 14 >= 0 /\ J - H + 7 >= 0 /\ -J - H + 8 >= 0 /\ H - 2 >= 0 /\ M + H - 6 >= 0 /\ -M + H + 2 >= 0 /\ L + H - 4 >= 0 /\ -L + H >= 0 /\ K + H - 3 >= 0 /\ -K + H + 5 >= 0 /\ J + H - 3 >= 0 /\ -J + H - 1 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ C - D >= 0 /\ -C + D >= 0 /\ -M + 4 >= 0 /\ L - M + 2 >= 0 /\ -L - M + 11 >= 0 /\ K - M + 3 >= 0 /\ -K - M + 11 >= 0 /\ J - M + 4 >= 0 /\ -J - M + 5 >= 0 /\ M - 4 >= 0 /\ L + M - 6 >= 0 /\ -L + M + 3 >= 0 /\ K + M - 5 >= 0 /\ -K + M + 3 >= 0 /\ J + M - 4 >= 0 /\ -J + M - 3 >= 0 /\ -L + 7 >= 0 /\ K - L + 6 >= 0 /\ -K - L + 14 >= 0 /\ J - L + 7 >= 0 /\ -J - L + 8 >= 0 /\ L - 2 >= 0 /\ K + L - 3 >= 0 /\ -K + L + 5 >= 0 /\ J + L - 3 >= 0 /\ -J + L - 1 >= 0 /\ -K + 7 >= 0 /\ J - K + 7 >= 0 /\ -J - K + 8 >= 0 /\ K - 1 >= 0 /\ J + K - 1 >= 0 /\ -J + K >= 0 /\ -J + 1 >= 0 /\ J >= 0 /\ N >= 1 /\ N >= F + 1 /\ O >= 1 /\ O >= D + 1 /\ 7 >= P /\ 7 >= Q /\ P >= 5 /\ Q >= 1 /\ I = 1 ]
  f4(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O) -> Com_1(f2(A, 0, D + 1, D + 1, F + 1, F + 1, Q, 4, 1, 0, Q, 4, 2, N, O)) [ -I + 1 >= 0 /\ H - I - 2 >= 0 /\ -H - I + 8 >= 0 /\ M - I - 3 >= 0 /\ -M - I + 5 >= 0 /\ L - I - 2 >= 0 /\ -L - I + 8 >= 0 /\ K - I >= 0 /\ -K - I + 8 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ I >= 0 /\ H + I - 2 >= 0 /\ -H + I + 6 >= 0 /\ M + I - 4 >= 0 /\ -M + I + 4 >= 0 /\ L + I - 2 >= 0 /\ -L + I + 6 >= 0 /\ K + I - 1 >= 0 /\ -K + I + 7 >= 0 /\ J + I - 1 >= 0 /\ -J + I + 1 >= 0 /\ -H + 7 >= 0 /\ M - H + 3 >= 0 /\ -M - H + 11 >= 0 /\ L - H >= 0 /\ -L - H + 14 >= 0 /\ K - H + 6 >= 0 /\ -K - H + 14 >= 0 /\ J - H + 7 >= 0 /\ -J - H + 8 >= 0 /\ H - 2 >= 0 /\ M + H - 6 >= 0 /\ -M + H + 2 >= 0 /\ L + H - 4 >= 0 /\ -L + H >= 0 /\ K + H - 3 >= 0 /\ -K + H + 5 >= 0 /\ J + H - 3 >= 0 /\ -J + H - 1 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ C - D >= 0 /\ -C + D >= 0 /\ -M + 4 >= 0 /\ L - M + 2 >= 0 /\ -L - M + 11 >= 0 /\ K - M + 3 >= 0 /\ -K - M + 11 >= 0 /\ J - M + 4 >= 0 /\ -J - M + 5 >= 0 /\ M - 4 >= 0 /\ L + M - 6 >= 0 /\ -L + M + 3 >= 0 /\ K + M - 5 >= 0 /\ -K + M + 3 >= 0 /\ J + M - 4 >= 0 /\ -J + M - 3 >= 0 /\ -L + 7 >= 0 /\ K - L + 6 >= 0 /\ -K - L + 14 >= 0 /\ J - L + 7 >= 0 /\ -J - L + 8 >= 0 /\ L - 2 >= 0 /\ K + L - 3 >= 0 /\ -K + L + 5 >= 0 /\ J + L - 3 >= 0 /\ -J + L - 1 >= 0 /\ -K + 7 >= 0 /\ J - K + 7 >= 0 /\ -J - K + 8 >= 0 /\ K - 1 >= 0 /\ J + K - 1 >= 0 /\ -J + K >= 0 /\ -J + 1 >= 0 /\ J >= 0 /\ N >= F + 2 /\ O >= D + 2 /\ N >= 1 /\ O >= 1 /\ 7 >= Q /\ Q >= 1 ]
  f4(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O) -> Com_1(f7(A, 0, D, D, F, F, Q, P, I, 0, Q, P, 7, N, O)) [ -I + 1 >= 0 /\ H - I - 2 >= 0 /\ -H - I + 8 >= 0 /\ M - I - 3 >= 0 /\ -M - I + 5 >= 0 /\ L - I - 2 >= 0 /\ -L - I + 8 >= 0 /\ K - I >= 0 /\ -K - I + 8 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ I >= 0 /\ H + I - 2 >= 0 /\ -H + I + 6 >= 0 /\ M + I - 4 >= 0 /\ -M + I + 4 >= 0 /\ L + I - 2 >= 0 /\ -L + I + 6 >= 0 /\ K + I - 1 >= 0 /\ -K + I + 7 >= 0 /\ J + I - 1 >= 0 /\ -J + I + 1 >= 0 /\ -H + 7 >= 0 /\ M - H + 3 >= 0 /\ -M - H + 11 >= 0 /\ L - H >= 0 /\ -L - H + 14 >= 0 /\ K - H + 6 >= 0 /\ -K - H + 14 >= 0 /\ J - H + 7 >= 0 /\ -J - H + 8 >= 0 /\ H - 2 >= 0 /\ M + H - 6 >= 0 /\ -M + H + 2 >= 0 /\ L + H - 4 >= 0 /\ -L + H >= 0 /\ K + H - 3 >= 0 /\ -K + H + 5 >= 0 /\ J + H - 3 >= 0 /\ -J + H - 1 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ C - D >= 0 /\ -C + D >= 0 /\ -M + 4 >= 0 /\ L - M + 2 >= 0 /\ -L - M + 11 >= 0 /\ K - M + 3 >= 0 /\ -K - M + 11 >= 0 /\ J - M + 4 >= 0 /\ -J - M + 5 >= 0 /\ M - 4 >= 0 /\ L + M - 6 >= 0 /\ -L + M + 3 >= 0 /\ K + M - 5 >= 0 /\ -K + M + 3 >= 0 /\ J + M - 4 >= 0 /\ -J + M - 3 >= 0 /\ -L + 7 >= 0 /\ K - L + 6 >= 0 /\ -K - L + 14 >= 0 /\ J - L + 7 >= 0 /\ -J - L + 8 >= 0 /\ L - 2 >= 0 /\ K + L - 3 >= 0 /\ -K + L + 5 >= 0 /\ J + L - 3 >= 0 /\ -J + L - 1 >= 0 /\ -K + 7 >= 0 /\ J - K + 7 >= 0 /\ -J - K + 8 >= 0 /\ K - 1 >= 0 /\ J + K - 1 >= 0 /\ -J + K >= 0 /\ -J + 1 >= 0 /\ J >= 0 /\ F >= N /\ D >= O /\ 7 >= P /\ 7 >= Q /\ 3 >= P /\ P >= 1 /\ Q >= 1 ]
  f4(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O) -> Com_1(f7(A, 0, D, D, F, F, Q, P, I, 0, Q, P, 7, N, O)) [ -I + 1 >= 0 /\ H - I - 2 >= 0 /\ -H - I + 8 >= 0 /\ M - I - 3 >= 0 /\ -M - I + 5 >= 0 /\ L - I - 2 >= 0 /\ -L - I + 8 >= 0 /\ K - I >= 0 /\ -K - I + 8 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ I >= 0 /\ H + I - 2 >= 0 /\ -H + I + 6 >= 0 /\ M + I - 4 >= 0 /\ -M + I + 4 >= 0 /\ L + I - 2 >= 0 /\ -L + I + 6 >= 0 /\ K + I - 1 >= 0 /\ -K + I + 7 >= 0 /\ J + I - 1 >= 0 /\ -J + I + 1 >= 0 /\ -H + 7 >= 0 /\ M - H + 3 >= 0 /\ -M - H + 11 >= 0 /\ L - H >= 0 /\ -L - H + 14 >= 0 /\ K - H + 6 >= 0 /\ -K - H + 14 >= 0 /\ J - H + 7 >= 0 /\ -J - H + 8 >= 0 /\ H - 2 >= 0 /\ M + H - 6 >= 0 /\ -M + H + 2 >= 0 /\ L + H - 4 >= 0 /\ -L + H >= 0 /\ K + H - 3 >= 0 /\ -K + H + 5 >= 0 /\ J + H - 3 >= 0 /\ -J + H - 1 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ C - D >= 0 /\ -C + D >= 0 /\ -M + 4 >= 0 /\ L - M + 2 >= 0 /\ -L - M + 11 >= 0 /\ K - M + 3 >= 0 /\ -K - M + 11 >= 0 /\ J - M + 4 >= 0 /\ -J - M + 5 >= 0 /\ M - 4 >= 0 /\ L + M - 6 >= 0 /\ -L + M + 3 >= 0 /\ K + M - 5 >= 0 /\ -K + M + 3 >= 0 /\ J + M - 4 >= 0 /\ -J + M - 3 >= 0 /\ -L + 7 >= 0 /\ K - L + 6 >= 0 /\ -K - L + 14 >= 0 /\ J - L + 7 >= 0 /\ -J - L + 8 >= 0 /\ L - 2 >= 0 /\ K + L - 3 >= 0 /\ -K + L + 5 >= 0 /\ J + L - 3 >= 0 /\ -J + L - 1 >= 0 /\ -K + 7 >= 0 /\ J - K + 7 >= 0 /\ -J - K + 8 >= 0 /\ K - 1 >= 0 /\ J + K - 1 >= 0 /\ -J + K >= 0 /\ -J + 1 >= 0 /\ J >= 0 /\ F >= N /\ D >= O /\ 7 >= P /\ 7 >= Q /\ P >= 5 /\ Q >= 1 ]
  f4(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O) -> Com_1(f7(A, 0, D + 1, D + 1, F + 1, F + 1, Q, 4, 1, 0, Q, 4, 7, N, O)) [ -I + 1 >= 0 /\ H - I - 2 >= 0 /\ -H - I + 8 >= 0 /\ M - I - 3 >= 0 /\ -M - I + 5 >= 0 /\ L - I - 2 >= 0 /\ -L - I + 8 >= 0 /\ K - I >= 0 /\ -K - I + 8 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ I >= 0 /\ H + I - 2 >= 0 /\ -H + I + 6 >= 0 /\ M + I - 4 >= 0 /\ -M + I + 4 >= 0 /\ L + I - 2 >= 0 /\ -L + I + 6 >= 0 /\ K + I - 1 >= 0 /\ -K + I + 7 >= 0 /\ J + I - 1 >= 0 /\ -J + I + 1 >= 0 /\ -H + 7 >= 0 /\ M - H + 3 >= 0 /\ -M - H + 11 >= 0 /\ L - H >= 0 /\ -L - H + 14 >= 0 /\ K - H + 6 >= 0 /\ -K - H + 14 >= 0 /\ J - H + 7 >= 0 /\ -J - H + 8 >= 0 /\ H - 2 >= 0 /\ M + H - 6 >= 0 /\ -M + H + 2 >= 0 /\ L + H - 4 >= 0 /\ -L + H >= 0 /\ K + H - 3 >= 0 /\ -K + H + 5 >= 0 /\ J + H - 3 >= 0 /\ -J + H - 1 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ C - D >= 0 /\ -C + D >= 0 /\ -M + 4 >= 0 /\ L - M + 2 >= 0 /\ -L - M + 11 >= 0 /\ K - M + 3 >= 0 /\ -K - M + 11 >= 0 /\ J - M + 4 >= 0 /\ -J - M + 5 >= 0 /\ M - 4 >= 0 /\ L + M - 6 >= 0 /\ -L + M + 3 >= 0 /\ K + M - 5 >= 0 /\ -K + M + 3 >= 0 /\ J + M - 4 >= 0 /\ -J + M - 3 >= 0 /\ -L + 7 >= 0 /\ K - L + 6 >= 0 /\ -K - L + 14 >= 0 /\ J - L + 7 >= 0 /\ -J - L + 8 >= 0 /\ L - 2 >= 0 /\ K + L - 3 >= 0 /\ -K + L + 5 >= 0 /\ J + L - 3 >= 0 /\ -J + L - 1 >= 0 /\ -K + 7 >= 0 /\ J - K + 7 >= 0 /\ -J - K + 8 >= 0 /\ K - 1 >= 0 /\ J + K - 1 >= 0 /\ -J + K >= 0 /\ -J + 1 >= 0 /\ J >= 0 /\ F + 1 >= N /\ D + 1 >= O /\ 7 >= Q /\ Q >= 1 ]
  f4(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O) -> Com_1(f7(A, 1, D, D, F, F, Q, P, I, 1, Q, P, 7, N, O)) [ -I + 1 >= 0 /\ H - I - 2 >= 0 /\ -H - I + 8 >= 0 /\ M - I - 3 >= 0 /\ -M - I + 5 >= 0 /\ L - I - 2 >= 0 /\ -L - I + 8 >= 0 /\ K - I >= 0 /\ -K - I + 8 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ I >= 0 /\ H + I - 2 >= 0 /\ -H + I + 6 >= 0 /\ M + I - 4 >= 0 /\ -M + I + 4 >= 0 /\ L + I - 2 >= 0 /\ -L + I + 6 >= 0 /\ K + I - 1 >= 0 /\ -K + I + 7 >= 0 /\ J + I - 1 >= 0 /\ -J + I + 1 >= 0 /\ -H + 7 >= 0 /\ M - H + 3 >= 0 /\ -M - H + 11 >= 0 /\ L - H >= 0 /\ -L - H + 14 >= 0 /\ K - H + 6 >= 0 /\ -K - H + 14 >= 0 /\ J - H + 7 >= 0 /\ -J - H + 8 >= 0 /\ H - 2 >= 0 /\ M + H - 6 >= 0 /\ -M + H + 2 >= 0 /\ L + H - 4 >= 0 /\ -L + H >= 0 /\ K + H - 3 >= 0 /\ -K + H + 5 >= 0 /\ J + H - 3 >= 0 /\ -J + H - 1 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ C - D >= 0 /\ -C + D >= 0 /\ -M + 4 >= 0 /\ L - M + 2 >= 0 /\ -L - M + 11 >= 0 /\ K - M + 3 >= 0 /\ -K - M + 11 >= 0 /\ J - M + 4 >= 0 /\ -J - M + 5 >= 0 /\ M - 4 >= 0 /\ L + M - 6 >= 0 /\ -L + M + 3 >= 0 /\ K + M - 5 >= 0 /\ -K + M + 3 >= 0 /\ J + M - 4 >= 0 /\ -J + M - 3 >= 0 /\ -L + 7 >= 0 /\ K - L + 6 >= 0 /\ -K - L + 14 >= 0 /\ J - L + 7 >= 0 /\ -J - L + 8 >= 0 /\ L - 2 >= 0 /\ K + L - 3 >= 0 /\ -K + L + 5 >= 0 /\ J + L - 3 >= 0 /\ -J + L - 1 >= 0 /\ -K + 7 >= 0 /\ J - K + 7 >= 0 /\ -J - K + 8 >= 0 /\ K - 1 >= 0 /\ J + K - 1 >= 0 /\ -J + K >= 0 /\ -J + 1 >= 0 /\ J >= 0 /\ 7 >= P /\ 7 >= Q /\ 3 >= P /\ P >= 1 /\ Q >= 1 ]
  f4(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O) -> Com_1(f7(A, 1, D, D, F, F, Q, P, I, 1, Q, P, 7, N, O)) [ -I + 1 >= 0 /\ H - I - 2 >= 0 /\ -H - I + 8 >= 0 /\ M - I - 3 >= 0 /\ -M - I + 5 >= 0 /\ L - I - 2 >= 0 /\ -L - I + 8 >= 0 /\ K - I >= 0 /\ -K - I + 8 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ I >= 0 /\ H + I - 2 >= 0 /\ -H + I + 6 >= 0 /\ M + I - 4 >= 0 /\ -M + I + 4 >= 0 /\ L + I - 2 >= 0 /\ -L + I + 6 >= 0 /\ K + I - 1 >= 0 /\ -K + I + 7 >= 0 /\ J + I - 1 >= 0 /\ -J + I + 1 >= 0 /\ -H + 7 >= 0 /\ M - H + 3 >= 0 /\ -M - H + 11 >= 0 /\ L - H >= 0 /\ -L - H + 14 >= 0 /\ K - H + 6 >= 0 /\ -K - H + 14 >= 0 /\ J - H + 7 >= 0 /\ -J - H + 8 >= 0 /\ H - 2 >= 0 /\ M + H - 6 >= 0 /\ -M + H + 2 >= 0 /\ L + H - 4 >= 0 /\ -L + H >= 0 /\ K + H - 3 >= 0 /\ -K + H + 5 >= 0 /\ J + H - 3 >= 0 /\ -J + H - 1 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ C - D >= 0 /\ -C + D >= 0 /\ -M + 4 >= 0 /\ L - M + 2 >= 0 /\ -L - M + 11 >= 0 /\ K - M + 3 >= 0 /\ -K - M + 11 >= 0 /\ J - M + 4 >= 0 /\ -J - M + 5 >= 0 /\ M - 4 >= 0 /\ L + M - 6 >= 0 /\ -L + M + 3 >= 0 /\ K + M - 5 >= 0 /\ -K + M + 3 >= 0 /\ J + M - 4 >= 0 /\ -J + M - 3 >= 0 /\ -L + 7 >= 0 /\ K - L + 6 >= 0 /\ -K - L + 14 >= 0 /\ J - L + 7 >= 0 /\ -J - L + 8 >= 0 /\ L - 2 >= 0 /\ K + L - 3 >= 0 /\ -K + L + 5 >= 0 /\ J + L - 3 >= 0 /\ -J + L - 1 >= 0 /\ -K + 7 >= 0 /\ J - K + 7 >= 0 /\ -J - K + 8 >= 0 /\ K - 1 >= 0 /\ J + K - 1 >= 0 /\ -J + K >= 0 /\ -J + 1 >= 0 /\ J >= 0 /\ 7 >= P /\ 7 >= Q /\ P >= 5 /\ Q >= 1 ]
  f4(A, B, C, D, E, F, G, H, I, J, K, L, M, N, O) -> Com_1(f7(A, 1, D + 1, D + 1, F + 1, F + 1, Q, 4, 1, 1, Q, 4, 7, N, O)) [ -I + 1 >= 0 /\ H - I - 2 >= 0 /\ -H - I + 8 >= 0 /\ M - I - 3 >= 0 /\ -M - I + 5 >= 0 /\ L - I - 2 >= 0 /\ -L - I + 8 >= 0 /\ K - I >= 0 /\ -K - I + 8 >= 0 /\ J - I + 1 >= 0 /\ -J - I + 2 >= 0 /\ I >= 0 /\ H + I - 2 >= 0 /\ -H + I + 6 >= 0 /\ M + I - 4 >= 0 /\ -M + I + 4 >= 0 /\ L + I - 2 >= 0 /\ -L + I + 6 >= 0 /\ K + I - 1 >= 0 /\ -K + I + 7 >= 0 /\ J + I - 1 >= 0 /\ -J + I + 1 >= 0 /\ -H + 7 >= 0 /\ M - H + 3 >= 0 /\ -M - H + 11 >= 0 /\ L - H >= 0 /\ -L - H + 14 >= 0 /\ K - H + 6 >= 0 /\ -K - H + 14 >= 0 /\ J - H + 7 >= 0 /\ -J - H + 8 >= 0 /\ H - 2 >= 0 /\ M + H - 6 >= 0 /\ -M + H + 2 >= 0 /\ L + H - 4 >= 0 /\ -L + H >= 0 /\ K + H - 3 >= 0 /\ -K + H + 5 >= 0 /\ J + H - 3 >= 0 /\ -J + H - 1 >= 0 /\ E - F >= 0 /\ -E + F >= 0 /\ C - D >= 0 /\ -C + D >= 0 /\ -M + 4 >= 0 /\ L - M + 2 >= 0 /\ -L - M + 11 >= 0 /\ K - M + 3 >= 0 /\ -K - M + 11 >= 0 /\ J - M + 4 >= 0 /\ -J - M + 5 >= 0 /\ M - 4 >= 0 /\ L + M - 6 >= 0 /\ -L + M + 3 >= 0 /\ K + M - 5 >= 0 /\ -K + M + 3 >= 0 /\ J + M - 4 >= 0 /\ -J + M - 3 >= 0 /\ -L + 7 >= 0 /\ K - L + 6 >= 0 /\ -K - L + 14 >= 0 /\ J - L + 7 >= 0 /\ -J - L + 8 >= 0 /\ L - 2 >= 0 /\ K + L - 3 >= 0 /\ -K + L + 5 >= 0 /\ J + L - 3 >= 0 /\ -J + L - 1 >= 0 /\ -K + 7 >= 0 /\ J - K + 7 >= 0 /\ -J - K + 8 >= 0 /\ K - 1 >= 0 /\ J + K - 1 >= 0 /\ -J + K >= 0 /\ -J + 1 >= 0 /\ J >= 0 /\ 7 >= Q /\ Q >= 1 ]
)