(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f0)) (VAR A B C) (RULES f0(A, B, C) -> Com_1(f154(0, 2, 0)) f154(A, B, C) -> Com_1(f154(A + C, B, C + 1)) [ C >= 0 /\ B + C - 2 >= 0 /\ -B + C + 2 >= 0 /\ A + C >= 0 /\ -B + 2 >= 0 /\ A - B + 2 >= 0 /\ B - 2 >= 0 /\ A + B - 2 >= 0 /\ A >= 0 /\ 2 >= C ] f160(A, B, C) -> Com_1(f160(A + C, B, C + 1)) [ C >= 0 /\ B + C - 2 >= 0 /\ -B + C + 2 >= 0 /\ A + C >= 0 /\ -B + 2 >= 0 /\ A - B + 2 >= 0 /\ B - 2 >= 0 /\ A + B - 2 >= 0 /\ A >= 0 /\ 3 >= C ] f166(A, B, C) -> Com_1(f166(A + C, B, C + 1)) [ C >= 0 /\ B + C - 2 >= 0 /\ -B + C + 2 >= 0 /\ A + C >= 0 /\ -B + 2 >= 0 /\ A - B + 2 >= 0 /\ B - 2 >= 0 /\ A + B - 2 >= 0 /\ A >= 0 /\ 2 >= C ] f172(A, B, C) -> Com_1(f172(A + C, B, C + 1)) [ C >= 0 /\ B + C - 2 >= 0 /\ -B + C + 2 >= 0 /\ A + C >= 0 /\ -B + 2 >= 0 /\ A - B + 2 >= 0 /\ B - 2 >= 0 /\ A + B - 2 >= 0 /\ A >= 0 /\ 3 >= C ] f180(A, B, C) -> Com_1(f180(A + C, B, C + 1)) [ A - C + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 3 >= 0 /\ -B + C + 1 >= 0 /\ A + C - 1 >= 0 /\ -B + 2 >= 0 /\ A - B + 2 >= 0 /\ B - 2 >= 0 /\ A + B - 2 >= 0 /\ A >= 0 /\ 1 >= C ] f186(A, B, C) -> Com_1(f186(A + C, B, C + 1)) [ A - C >= 0 /\ C - 1 >= 0 /\ B + C - 3 >= 0 /\ -B + C + 1 >= 0 /\ A + C - 2 >= 0 /\ -B + 2 >= 0 /\ A - B + 1 >= 0 /\ B - 2 >= 0 /\ A + B - 3 >= 0 /\ A - 1 >= 0 /\ 2 >= C ] f192(A, B, C) -> Com_1(f192(A + C, B, C + 1)) [ A - C - 2 >= 0 /\ C - 1 >= 0 /\ B + C - 3 >= 0 /\ -B + C + 1 >= 0 /\ A + C - 4 >= 0 /\ -B + 2 >= 0 /\ A - B - 1 >= 0 /\ B - 2 >= 0 /\ A + B - 5 >= 0 /\ A - 3 >= 0 /\ 1 >= C ] f198(A, B, C) -> Com_1(f198(A + C, B, C + 1)) [ A - C - 3 >= 0 /\ C - 1 >= 0 /\ B + C - 3 >= 0 /\ -B + C + 1 >= 0 /\ A + C - 5 >= 0 /\ -B + 2 >= 0 /\ A - B - 2 >= 0 /\ B - 2 >= 0 /\ A + B - 6 >= 0 /\ A - 4 >= 0 /\ 2 >= C ] f206(A, B, C) -> Com_1(f206(A + C, B, C + 1)) [ C + 3 >= 0 /\ B + C + 1 >= 0 /\ -B + C + 5 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 3 ] f212(A, B, C) -> Com_1(f212(A + C, B, C + 1)) [ C + 3 >= 0 /\ B + C + 1 >= 0 /\ -B + C + 5 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 2 ] f218(A, B, C) -> Com_1(f218(A + C, B, C + 1)) [ C + 3 >= 0 /\ B + C + 1 >= 0 /\ -B + C + 5 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 3 ] f224(A, B, C) -> Com_1(f224(A + C, B, C + 1)) [ C + 3 >= 0 /\ B + C + 1 >= 0 /\ -B + C + 5 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 2 ] f232(A, B, C) -> Com_1(f232(A + C, B, C + 1)) [ C + 4 >= 0 /\ B + C + 2 >= 0 /\ -B + C + 6 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 2 ] f238(A, B, C) -> Com_1(f238(A + C, B, C + 1)) [ C + 4 >= 0 /\ B + C + 2 >= 0 /\ -B + C + 6 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 1 ] f244(A, B, C) -> Com_1(f244(A + C, B, C + 1)) [ C + 4 >= 0 /\ B + C + 2 >= 0 /\ -B + C + 6 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 2 ] f250(A, B, C) -> Com_1(f250(A + C, B, C + 1)) [ C + 4 >= 0 /\ B + C + 2 >= 0 /\ -B + C + 6 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 1 ] f258(A, B, C) -> Com_1(f258(A + C, B, C + 1)) [ C + 5 >= 0 /\ B + C + 3 >= 0 /\ -B + C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 1 ] f264(A, B, C) -> Com_1(f264(A + C, B, C + 1)) [ C + 5 >= 0 /\ B + C + 3 >= 0 /\ -B + C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C ] f270(A, B, C) -> Com_1(f270(A + C, B, C + 1)) [ C + 5 >= 0 /\ B + C + 3 >= 0 /\ -B + C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 1 ] f276(A, B, C) -> Com_1(f276(A + C, B, C + 1)) [ C + 5 >= 0 /\ B + C + 3 >= 0 /\ -B + C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C ] f284(A, B, C) -> Com_1(f284(A + C, B, C + 1)) [ C + 6 >= 0 /\ B + C + 4 >= 0 /\ -B + C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 3 >= C ] f290(A, B, C) -> Com_1(f290(A + C, B, C + 1)) [ C + 6 >= 0 /\ B + C + 4 >= 0 /\ -B + C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 4 >= C ] f296(A, B, C) -> Com_1(f296(A + C, B, C + 1)) [ C + 6 >= 0 /\ B + C + 4 >= 0 /\ -B + C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 3 >= C ] f302(A, B, C) -> Com_1(f302(A + C, B, C + 1)) [ C + 6 >= 0 /\ B + C + 4 >= 0 /\ -B + C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 4 >= C ] f310(A, B, C) -> Com_1(f310(A + C, B, C + B)) [ C >= 0 /\ B + C - 2 >= 0 /\ -B + C + 2 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 2 >= C ] f316(A, B, C) -> Com_1(f316(A + C, B, C + B)) [ C >= 0 /\ B + C - 2 >= 0 /\ -B + C + 2 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 3 >= C ] f322(A, B, C) -> Com_1(f322(A + C, B, C + B)) [ C >= 0 /\ B + C - 2 >= 0 /\ -B + C + 2 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 2 >= C ] f328(A, B, C) -> Com_1(f328(A + C, B, C + B)) [ C >= 0 /\ B + C - 2 >= 0 /\ -B + C + 2 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 3 >= C ] f336(A, B, C) -> Com_1(f336(A + C, B, C + B)) [ C - 1 >= 0 /\ B + C - 3 >= 0 /\ -B + C + 1 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 1 >= C ] f342(A, B, C) -> Com_1(f342(A + C, B, C + B)) [ C - 1 >= 0 /\ B + C - 3 >= 0 /\ -B + C + 1 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 2 >= C ] f348(A, B, C) -> Com_1(f348(A + C, B, C + B)) [ C - 1 >= 0 /\ B + C - 3 >= 0 /\ -B + C + 1 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 1 >= C ] f354(A, B, C) -> Com_1(f354(A + C, B, C + B)) [ C - 1 >= 0 /\ B + C - 3 >= 0 /\ -B + C + 1 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 2 >= C ] f362(A, B, C) -> Com_1(f362(A + C, B, C + B)) [ C + 3 >= 0 /\ B + C + 1 >= 0 /\ -B + C + 5 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 3 ] f368(A, B, C) -> Com_1(f368(A + C, B, C + B)) [ C + 3 >= 0 /\ B + C + 1 >= 0 /\ -B + C + 5 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 2 ] f374(A, B, C) -> Com_1(f374(A + C, B, C + B)) [ C + 3 >= 0 /\ B + C + 1 >= 0 /\ -B + C + 5 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 3 ] f380(A, B, C) -> Com_1(f380(A + C, B, C + B)) [ C + 3 >= 0 /\ B + C + 1 >= 0 /\ -B + C + 5 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 2 ] f388(A, B, C) -> Com_1(f388(A + C, B, C + B)) [ C + 4 >= 0 /\ B + C + 2 >= 0 /\ -B + C + 6 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 2 ] f394(A, B, C) -> Com_1(f394(A + C, B, C + B)) [ C + 4 >= 0 /\ B + C + 2 >= 0 /\ -B + C + 6 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 1 ] f400(A, B, C) -> Com_1(f400(A + C, B, C + B)) [ C + 4 >= 0 /\ B + C + 2 >= 0 /\ -B + C + 6 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 2 ] f406(A, B, C) -> Com_1(f406(A + C, B, C + B)) [ C + 4 >= 0 /\ B + C + 2 >= 0 /\ -B + C + 6 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 1 ] f414(A, B, C) -> Com_1(f414(A + C, B, C + B)) [ C + 5 >= 0 /\ B + C + 3 >= 0 /\ -B + C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 1 ] f420(A, B, C) -> Com_1(f420(A + C, B, C + B)) [ C + 5 >= 0 /\ B + C + 3 >= 0 /\ -B + C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C ] f426(A, B, C) -> Com_1(f426(A + C, B, C + B)) [ C + 5 >= 0 /\ B + C + 3 >= 0 /\ -B + C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 1 ] f432(A, B, C) -> Com_1(f432(A + C, B, C + B)) [ C + 5 >= 0 /\ B + C + 3 >= 0 /\ -B + C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C ] f440(A, B, C) -> Com_1(f440(A + C, B, C + B)) [ C + 6 >= 0 /\ B + C + 4 >= 0 /\ -B + C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 3 >= C ] f446(A, B, C) -> Com_1(f446(A + C, B, C + B)) [ C + 6 >= 0 /\ B + C + 4 >= 0 /\ -B + C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 4 >= C ] f452(A, B, C) -> Com_1(f452(A + C, B, C + B)) [ C + 6 >= 0 /\ B + C + 4 >= 0 /\ -B + C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 3 >= C ] f458(A, B, C) -> Com_1(f458(A + C, B, C + B)) [ C + 6 >= 0 /\ B + C + 4 >= 0 /\ -B + C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 4 >= C ] f466(A, B, C) -> Com_1(f466(A + C, B, C - 1)) [ -C + 5 >= 0 /\ B - C + 3 >= 0 /\ -B - C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 3 ] f472(A, B, C) -> Com_1(f472(A + C, B, C - 1)) [ -C + 5 >= 0 /\ B - C + 3 >= 0 /\ -B - C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 2 ] f478(A, B, C) -> Com_1(f478(A + C, B, C - 1)) [ -C + 5 >= 0 /\ B - C + 3 >= 0 /\ -B - C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 3 ] f484(A, B, C) -> Com_1(f484(A + C, B, C - 1)) [ -C + 5 >= 0 /\ B - C + 3 >= 0 /\ -B - C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 2 ] f492(A, B, C) -> Com_1(f492(A + C, B, C - 1)) [ -C + 6 >= 0 /\ B - C + 4 >= 0 /\ -B - C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 2 ] f498(A, B, C) -> Com_1(f498(A + C, B, C - 1)) [ -C + 6 >= 0 /\ B - C + 4 >= 0 /\ -B - C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 1 ] f504(A, B, C) -> Com_1(f504(A + C, B, C - 1)) [ -C + 6 >= 0 /\ B - C + 4 >= 0 /\ -B - C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 2 ] f510(A, B, C) -> Com_1(f510(A + C, B, C - 1)) [ -C + 6 >= 0 /\ B - C + 4 >= 0 /\ -B - C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 1 ] f518(A, B, C) -> Com_1(f518(A + C, B, C - 1)) [ -C + 7 >= 0 /\ B - C + 5 >= 0 /\ -B - C + 9 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 1 ] f524(A, B, C) -> Com_1(f524(A + C, B, C - 1)) [ -C + 7 >= 0 /\ B - C + 5 >= 0 /\ -B - C + 9 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 0 ] f530(A, B, C) -> Com_1(f530(A + C, B, C - 1)) [ -C + 7 >= 0 /\ B - C + 5 >= 0 /\ -B - C + 9 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 1 ] f536(A, B, C) -> Com_1(f536(A + C, B, C - 1)) [ -C + 7 >= 0 /\ B - C + 5 >= 0 /\ -B - C + 9 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 0 ] f544(A, B, C) -> Com_1(f544(A + C, B, C - 1)) [ -C + 8 >= 0 /\ B - C + 6 >= 0 /\ -B - C + 10 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 0 ] f550(A, B, C) -> Com_1(f550(A + C, B, C - 1)) [ -C + 8 >= 0 /\ B - C + 6 >= 0 /\ -B - C + 10 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 1 >= 0 ] f556(A, B, C) -> Com_1(f556(A + C, B, C - 1)) [ -C + 8 >= 0 /\ B - C + 6 >= 0 /\ -B - C + 10 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 0 ] f562(A, B, C) -> Com_1(f562(A + C, B, C - 1)) [ -C + 8 >= 0 /\ B - C + 6 >= 0 /\ -B - C + 10 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 1 >= 0 ] f570(A, B, C) -> Com_1(f570(A + C, B, C - 1)) [ -C + 9 >= 0 /\ B - C + 7 >= 0 /\ -B - C + 11 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 1 >= 0 ] f576(A, B, C) -> Com_1(f576(A + C, B, C - 1)) [ -C + 9 >= 0 /\ B - C + 7 >= 0 /\ -B - C + 11 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 2 >= 0 ] f582(A, B, C) -> Com_1(f582(A + C, B, C - 1)) [ -C + 9 >= 0 /\ B - C + 7 >= 0 /\ -B - C + 11 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 1 >= 0 ] f588(A, B, C) -> Com_1(f588(A + C, B, C - 1)) [ -C + 9 >= 0 /\ B - C + 7 >= 0 /\ -B - C + 11 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 2 >= 0 ] f596(A, B, C) -> Com_1(f596(A + C, B, C - 1)) [ -C >= 0 /\ B - C - 2 >= 0 /\ -B - C + 2 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 2 >= 0 ] f602(A, B, C) -> Com_1(f602(A + C, B, C - 1)) [ -C >= 0 /\ B - C - 2 >= 0 /\ -B - C + 2 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 3 >= 0 ] f608(A, B, C) -> Com_1(f608(A + C, B, C - 1)) [ -C >= 0 /\ B - C - 2 >= 0 /\ -B - C + 2 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 2 >= 0 ] f614(A, B, C) -> Com_1(f614(A + C, B, C - 1)) [ -C >= 0 /\ B - C - 2 >= 0 /\ -B - C + 2 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 3 >= 0 ] f622(A, B, C) -> Com_1(f622(A + C, B, C - 1)) [ -C - 1 >= 0 /\ B - C - 3 >= 0 /\ -B - C + 1 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 4 >= 0 ] f628(A, B, C) -> Com_1(f628(A + C, B, C - 1)) [ -C - 1 >= 0 /\ B - C - 3 >= 0 /\ -B - C + 1 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 5 >= 0 ] f634(A, B, C) -> Com_1(f634(A + C, B, C - 1)) [ -C - 1 >= 0 /\ B - C - 3 >= 0 /\ -B - C + 1 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 4 >= 0 ] f640(A, B, C) -> Com_1(f640(A + C, B, C - 1)) [ -C - 1 >= 0 /\ B - C - 3 >= 0 /\ -B - C + 1 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 5 >= 0 ] f648(A, B, C) -> Com_1(f648(A + C, B, C - 1)) [ -C - 2 >= 0 /\ B - C - 4 >= 0 /\ -B - C >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 6 >= 0 ] f654(A, B, C) -> Com_1(f654(A + C, B, C - 1)) [ -C - 2 >= 0 /\ B - C - 4 >= 0 /\ -B - C >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 7 >= 0 ] f660(A, B, C) -> Com_1(f660(A + C, B, C - 1)) [ -C - 2 >= 0 /\ B - C - 4 >= 0 /\ -B - C >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 6 >= 0 ] f666(A, B, C) -> Com_1(f666(A + C, B, C - 1)) [ -C - 2 >= 0 /\ B - C - 4 >= 0 /\ -B - C >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 7 >= 0 ] f674(A, B, C) -> Com_1(f674(A + C, B, C - 1)) [ -C + 16 >= 0 /\ B - C + 14 >= 0 /\ -B - C + 18 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 7 >= 0 ] f680(A, B, C) -> Com_1(f680(A + C, B, C - 1)) [ -C + 16 >= 0 /\ B - C + 14 >= 0 /\ -B - C + 18 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 8 >= 0 ] f686(A, B, C) -> Com_1(f686(A + C, B, C - 1)) [ -C + 16 >= 0 /\ B - C + 14 >= 0 /\ -B - C + 18 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 7 >= 0 ] f692(A, B, C) -> Com_1(f692(A + C, B, C - 1)) [ -C + 16 >= 0 /\ B - C + 14 >= 0 /\ -B - C + 18 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 8 >= 0 ] f700(A, B, C) -> Com_1(f700(A + C, B, C - B)) [ -C + 5 >= 0 /\ B - C + 3 >= 0 /\ -B - C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 3 ] f706(A, B, C) -> Com_1(f706(A + C, B, C - B)) [ -C + 5 >= 0 /\ B - C + 3 >= 0 /\ -B - C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 2 ] f712(A, B, C) -> Com_1(f712(A + C, B, C - B)) [ -C + 5 >= 0 /\ B - C + 3 >= 0 /\ -B - C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 3 ] f718(A, B, C) -> Com_1(f718(A + C, B, C - B)) [ -C + 5 >= 0 /\ B - C + 3 >= 0 /\ -B - C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 2 ] f726(A, B, C) -> Com_1(f726(A + C, B, C - B)) [ -C + 6 >= 0 /\ B - C + 4 >= 0 /\ -B - C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 2 ] f732(A, B, C) -> Com_1(f732(A + C, B, C - B)) [ -C + 6 >= 0 /\ B - C + 4 >= 0 /\ -B - C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 1 ] f738(A, B, C) -> Com_1(f738(A + C, B, C - B)) [ -C + 6 >= 0 /\ B - C + 4 >= 0 /\ -B - C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 2 ] f744(A, B, C) -> Com_1(f744(A + C, B, C - B)) [ -C + 6 >= 0 /\ B - C + 4 >= 0 /\ -B - C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 1 ] f752(A, B, C) -> Com_1(f752(A + C, B, C - B)) [ -C + 7 >= 0 /\ B - C + 5 >= 0 /\ -B - C + 9 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 1 ] f758(A, B, C) -> Com_1(f758(A + C, B, C - B)) [ -C + 7 >= 0 /\ B - C + 5 >= 0 /\ -B - C + 9 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 0 ] f764(A, B, C) -> Com_1(f764(A + C, B, C - B)) [ -C + 7 >= 0 /\ B - C + 5 >= 0 /\ -B - C + 9 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 1 ] f770(A, B, C) -> Com_1(f770(A + C, B, C - B)) [ -C + 7 >= 0 /\ B - C + 5 >= 0 /\ -B - C + 9 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 0 ] f778(A, B, C) -> Com_1(f778(A + C, B, C - B)) [ -C + 8 >= 0 /\ B - C + 6 >= 0 /\ -B - C + 10 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 0 ] f784(A, B, C) -> Com_1(f784(A + C, B, C - B)) [ -C + 8 >= 0 /\ B - C + 6 >= 0 /\ -B - C + 10 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 1 >= 0 ] f790(A, B, C) -> Com_1(f790(A + C, B, C - B)) [ -C + 8 >= 0 /\ B - C + 6 >= 0 /\ -B - C + 10 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 0 ] f796(A, B, C) -> Com_1(f796(A + C, B, C - B)) [ -C + 8 >= 0 /\ B - C + 6 >= 0 /\ -B - C + 10 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 1 >= 0 ] f804(A, B, C) -> Com_1(f804(A + C, B, C - B)) [ -C + 9 >= 0 /\ B - C + 7 >= 0 /\ -B - C + 11 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 1 >= 0 ] f810(A, B, C) -> Com_1(f810(A + C, B, C - B)) [ -C + 9 >= 0 /\ B - C + 7 >= 0 /\ -B - C + 11 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 2 >= 0 ] f816(A, B, C) -> Com_1(f816(A + C, B, C - B)) [ -C + 9 >= 0 /\ B - C + 7 >= 0 /\ -B - C + 11 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 1 >= 0 ] f822(A, B, C) -> Com_1(f822(A + C, B, C - B)) [ -C + 9 >= 0 /\ B - C + 7 >= 0 /\ -B - C + 11 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 2 >= 0 ] f830(A, B, C) -> Com_1(f830(A + C, B, C - B)) [ -C >= 0 /\ B - C - 2 >= 0 /\ -B - C + 2 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 2 >= 0 ] f836(A, B, C) -> Com_1(f836(A + C, B, C - B)) [ -C >= 0 /\ B - C - 2 >= 0 /\ -B - C + 2 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 3 >= 0 ] f842(A, B, C) -> Com_1(f842(A + C, B, C - B)) [ -C >= 0 /\ B - C - 2 >= 0 /\ -B - C + 2 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 2 >= 0 ] f848(A, B, C) -> Com_1(f848(A + C, B, C - B)) [ -C >= 0 /\ B - C - 2 >= 0 /\ -B - C + 2 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 3 >= 0 ] f856(A, B, C) -> Com_1(f856(A + C, B, C - B)) [ -C - 1 >= 0 /\ B - C - 3 >= 0 /\ -B - C + 1 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 4 >= 0 ] f862(A, B, C) -> Com_1(f862(A + C, B, C - B)) [ -C - 1 >= 0 /\ B - C - 3 >= 0 /\ -B - C + 1 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 5 >= 0 ] f868(A, B, C) -> Com_1(f868(A + C, B, C - B)) [ -C - 1 >= 0 /\ B - C - 3 >= 0 /\ -B - C + 1 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 4 >= 0 ] f874(A, B, C) -> Com_1(f874(A + C, B, C - B)) [ -C - 1 >= 0 /\ B - C - 3 >= 0 /\ -B - C + 1 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 5 >= 0 ] f882(A, B, C) -> Com_1(f882(A + C, B, C - B)) [ -C - 2 >= 0 /\ B - C - 4 >= 0 /\ -B - C >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 6 >= 0 ] f888(A, B, C) -> Com_1(f888(A + C, B, C - B)) [ -C - 2 >= 0 /\ B - C - 4 >= 0 /\ -B - C >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 7 >= 0 ] f894(A, B, C) -> Com_1(f894(A + C, B, C - B)) [ -C - 2 >= 0 /\ B - C - 4 >= 0 /\ -B - C >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 6 >= 0 ] f900(A, B, C) -> Com_1(f900(A + C, B, C - B)) [ -C - 2 >= 0 /\ B - C - 4 >= 0 /\ -B - C >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 7 >= 0 ] f908(A, B, C) -> Com_1(f908(A + C, B, C - B)) [ -C + 16 >= 0 /\ B - C + 14 >= 0 /\ -B - C + 18 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 7 >= 0 ] f914(A, B, C) -> Com_1(f914(A + C, B, C - B)) [ -C + 16 >= 0 /\ B - C + 14 >= 0 /\ -B - C + 18 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 8 >= 0 ] f920(A, B, C) -> Com_1(f920(A + C, B, C - B)) [ -C + 16 >= 0 /\ B - C + 14 >= 0 /\ -B - C + 18 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 7 >= 0 ] f926(A, B, C) -> Com_1(f926(A + C, B, C - B)) [ -C + 16 >= 0 /\ B - C + 14 >= 0 /\ -B - C + 18 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 8 >= 0 ] f926(A, B, C) -> Com_1(f934(A, B, C)) [ -C + 16 >= 0 /\ B - C + 14 >= 0 /\ -B - C + 18 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 9 ] f920(A, B, C) -> Com_1(f926(A, B, 16)) [ -C + 16 >= 0 /\ B - C + 14 >= 0 /\ -B - C + 18 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 8 ] f914(A, B, C) -> Com_1(f920(A, B, 16)) [ -C + 16 >= 0 /\ B - C + 14 >= 0 /\ -B - C + 18 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 9 ] f908(A, B, C) -> Com_1(f914(A, B, 16)) [ -C + 16 >= 0 /\ B - C + 14 >= 0 /\ -B - C + 18 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 8 ] f900(A, B, C) -> Com_1(f908(A, B, 16)) [ -C - 2 >= 0 /\ B - C - 4 >= 0 /\ -B - C >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 8 ] f894(A, B, C) -> Com_1(f900(A, B, -2)) [ -C - 2 >= 0 /\ B - C - 4 >= 0 /\ -B - C >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 7 ] f888(A, B, C) -> Com_1(f894(A, B, -2)) [ -C - 2 >= 0 /\ B - C - 4 >= 0 /\ -B - C >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 8 ] f882(A, B, C) -> Com_1(f888(A, B, -2)) [ -C - 2 >= 0 /\ B - C - 4 >= 0 /\ -B - C >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 7 ] f874(A, B, C) -> Com_1(f882(A, B, -2)) [ -C - 1 >= 0 /\ B - C - 3 >= 0 /\ -B - C + 1 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 6 ] f868(A, B, C) -> Com_1(f874(A, B, -1)) [ -C - 1 >= 0 /\ B - C - 3 >= 0 /\ -B - C + 1 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 5 ] f862(A, B, C) -> Com_1(f868(A, B, -1)) [ -C - 1 >= 0 /\ B - C - 3 >= 0 /\ -B - C + 1 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 6 ] f856(A, B, C) -> Com_1(f862(A, B, -1)) [ -C - 1 >= 0 /\ B - C - 3 >= 0 /\ -B - C + 1 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 5 ] f848(A, B, C) -> Com_1(f856(A, B, -1)) [ -C >= 0 /\ B - C - 2 >= 0 /\ -B - C + 2 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 4 ] f842(A, B, C) -> Com_1(f848(A, B, 0)) [ -C >= 0 /\ B - C - 2 >= 0 /\ -B - C + 2 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 3 ] f836(A, B, C) -> Com_1(f842(A, B, 0)) [ -C >= 0 /\ B - C - 2 >= 0 /\ -B - C + 2 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 4 ] f830(A, B, C) -> Com_1(f836(A, B, 0)) [ -C >= 0 /\ B - C - 2 >= 0 /\ -B - C + 2 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 3 ] f822(A, B, C) -> Com_1(f830(A, B, 0)) [ -C + 9 >= 0 /\ B - C + 7 >= 0 /\ -B - C + 11 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 3 ] f816(A, B, C) -> Com_1(f822(A, B, 9)) [ -C + 9 >= 0 /\ B - C + 7 >= 0 /\ -B - C + 11 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 2 ] f810(A, B, C) -> Com_1(f816(A, B, 9)) [ -C + 9 >= 0 /\ B - C + 7 >= 0 /\ -B - C + 11 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 3 ] f804(A, B, C) -> Com_1(f810(A, B, 9)) [ -C + 9 >= 0 /\ B - C + 7 >= 0 /\ -B - C + 11 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 2 ] f796(A, B, C) -> Com_1(f804(A, B, 9)) [ -C + 8 >= 0 /\ B - C + 6 >= 0 /\ -B - C + 10 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 2 ] f790(A, B, C) -> Com_1(f796(A, B, 8)) [ -C + 8 >= 0 /\ B - C + 6 >= 0 /\ -B - C + 10 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 1 ] f784(A, B, C) -> Com_1(f790(A, B, 8)) [ -C + 8 >= 0 /\ B - C + 6 >= 0 /\ -B - C + 10 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 2 ] f778(A, B, C) -> Com_1(f784(A, B, 8)) [ -C + 8 >= 0 /\ B - C + 6 >= 0 /\ -B - C + 10 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 1 ] f770(A, B, C) -> Com_1(f778(A, B, 8)) [ -C + 7 >= 0 /\ B - C + 5 >= 0 /\ -B - C + 9 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 1 ] f764(A, B, C) -> Com_1(f770(A, B, 7)) [ -C + 7 >= 0 /\ B - C + 5 >= 0 /\ -B - C + 9 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C ] f758(A, B, C) -> Com_1(f764(A, B, 7)) [ -C + 7 >= 0 /\ B - C + 5 >= 0 /\ -B - C + 9 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 1 ] f752(A, B, C) -> Com_1(f758(A, B, 7)) [ -C + 7 >= 0 /\ B - C + 5 >= 0 /\ -B - C + 9 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C ] f744(A, B, C) -> Com_1(f752(A, B, 7)) [ -C + 6 >= 0 /\ B - C + 4 >= 0 /\ -B - C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C ] f738(A, B, C) -> Com_1(f744(A, B, 6)) [ -C + 6 >= 0 /\ B - C + 4 >= 0 /\ -B - C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 1 >= C ] f732(A, B, C) -> Com_1(f738(A, B, 6)) [ -C + 6 >= 0 /\ B - C + 4 >= 0 /\ -B - C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C ] f726(A, B, C) -> Com_1(f732(A, B, 6)) [ -C + 6 >= 0 /\ B - C + 4 >= 0 /\ -B - C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 1 >= C ] f718(A, B, C) -> Com_1(f726(A, B, 6)) [ -C + 5 >= 0 /\ B - C + 3 >= 0 /\ -B - C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 1 >= C ] f712(A, B, C) -> Com_1(f718(A, B, 5)) [ -C + 5 >= 0 /\ B - C + 3 >= 0 /\ -B - C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 2 >= C ] f706(A, B, C) -> Com_1(f712(A, B, 5)) [ -C + 5 >= 0 /\ B - C + 3 >= 0 /\ -B - C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 1 >= C ] f700(A, B, C) -> Com_1(f706(A, B, 5)) [ -C + 5 >= 0 /\ B - C + 3 >= 0 /\ -B - C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 2 >= C ] f692(A, B, C) -> Com_1(f700(A, B, 5)) [ -C + 16 >= 0 /\ B - C + 14 >= 0 /\ -B - C + 18 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 9 ] f686(A, B, C) -> Com_1(f692(A, B, 16)) [ -C + 16 >= 0 /\ B - C + 14 >= 0 /\ -B - C + 18 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 8 ] f680(A, B, C) -> Com_1(f686(A, B, 16)) [ -C + 16 >= 0 /\ B - C + 14 >= 0 /\ -B - C + 18 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 9 ] f674(A, B, C) -> Com_1(f680(A, B, 16)) [ -C + 16 >= 0 /\ B - C + 14 >= 0 /\ -B - C + 18 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 8 ] f666(A, B, C) -> Com_1(f674(A, B, 16)) [ -C - 2 >= 0 /\ B - C - 4 >= 0 /\ -B - C >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 8 ] f660(A, B, C) -> Com_1(f666(A, B, -2)) [ -C - 2 >= 0 /\ B - C - 4 >= 0 /\ -B - C >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 7 ] f654(A, B, C) -> Com_1(f660(A, B, -2)) [ -C - 2 >= 0 /\ B - C - 4 >= 0 /\ -B - C >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 8 ] f648(A, B, C) -> Com_1(f654(A, B, -2)) [ -C - 2 >= 0 /\ B - C - 4 >= 0 /\ -B - C >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 7 ] f640(A, B, C) -> Com_1(f648(A, B, -2)) [ -C - 1 >= 0 /\ B - C - 3 >= 0 /\ -B - C + 1 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 6 ] f634(A, B, C) -> Com_1(f640(A, B, -1)) [ -C - 1 >= 0 /\ B - C - 3 >= 0 /\ -B - C + 1 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 5 ] f628(A, B, C) -> Com_1(f634(A, B, -1)) [ -C - 1 >= 0 /\ B - C - 3 >= 0 /\ -B - C + 1 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 6 ] f622(A, B, C) -> Com_1(f628(A, B, -1)) [ -C - 1 >= 0 /\ B - C - 3 >= 0 /\ -B - C + 1 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 5 ] f614(A, B, C) -> Com_1(f622(A, B, -1)) [ -C >= 0 /\ B - C - 2 >= 0 /\ -B - C + 2 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 4 ] f608(A, B, C) -> Com_1(f614(A, B, 0)) [ -C >= 0 /\ B - C - 2 >= 0 /\ -B - C + 2 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 3 ] f602(A, B, C) -> Com_1(f608(A, B, 0)) [ -C >= 0 /\ B - C - 2 >= 0 /\ -B - C + 2 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 4 ] f596(A, B, C) -> Com_1(f602(A, B, 0)) [ -C >= 0 /\ B - C - 2 >= 0 /\ -B - C + 2 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 3 ] f588(A, B, C) -> Com_1(f596(A, B, 0)) [ -C + 9 >= 0 /\ B - C + 7 >= 0 /\ -B - C + 11 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 3 ] f582(A, B, C) -> Com_1(f588(A, B, 9)) [ -C + 9 >= 0 /\ B - C + 7 >= 0 /\ -B - C + 11 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 2 ] f576(A, B, C) -> Com_1(f582(A, B, 9)) [ -C + 9 >= 0 /\ B - C + 7 >= 0 /\ -B - C + 11 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 3 ] f570(A, B, C) -> Com_1(f576(A, B, 9)) [ -C + 9 >= 0 /\ B - C + 7 >= 0 /\ -B - C + 11 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 2 ] f562(A, B, C) -> Com_1(f570(A, B, 9)) [ -C + 8 >= 0 /\ B - C + 6 >= 0 /\ -B - C + 10 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 2 ] f556(A, B, C) -> Com_1(f562(A, B, 8)) [ -C + 8 >= 0 /\ B - C + 6 >= 0 /\ -B - C + 10 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 1 ] f550(A, B, C) -> Com_1(f556(A, B, 8)) [ -C + 8 >= 0 /\ B - C + 6 >= 0 /\ -B - C + 10 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 2 ] f544(A, B, C) -> Com_1(f550(A, B, 8)) [ -C + 8 >= 0 /\ B - C + 6 >= 0 /\ -B - C + 10 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 1 ] f536(A, B, C) -> Com_1(f544(A, B, 8)) [ -C + 7 >= 0 /\ B - C + 5 >= 0 /\ -B - C + 9 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 1 ] f530(A, B, C) -> Com_1(f536(A, B, 7)) [ -C + 7 >= 0 /\ B - C + 5 >= 0 /\ -B - C + 9 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C ] f524(A, B, C) -> Com_1(f530(A, B, 7)) [ -C + 7 >= 0 /\ B - C + 5 >= 0 /\ -B - C + 9 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C + 1 ] f518(A, B, C) -> Com_1(f524(A, B, 7)) [ -C + 7 >= 0 /\ B - C + 5 >= 0 /\ -B - C + 9 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C ] f510(A, B, C) -> Com_1(f518(A, B, 7)) [ -C + 6 >= 0 /\ B - C + 4 >= 0 /\ -B - C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C ] f504(A, B, C) -> Com_1(f510(A, B, 6)) [ -C + 6 >= 0 /\ B - C + 4 >= 0 /\ -B - C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 1 >= C ] f498(A, B, C) -> Com_1(f504(A, B, 6)) [ -C + 6 >= 0 /\ B - C + 4 >= 0 /\ -B - C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 0 >= C ] f492(A, B, C) -> Com_1(f498(A, B, 6)) [ -C + 6 >= 0 /\ B - C + 4 >= 0 /\ -B - C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 1 >= C ] f484(A, B, C) -> Com_1(f492(A, B, 6)) [ -C + 5 >= 0 /\ B - C + 3 >= 0 /\ -B - C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 1 >= C ] f478(A, B, C) -> Com_1(f484(A, B, 5)) [ -C + 5 >= 0 /\ B - C + 3 >= 0 /\ -B - C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 2 >= C ] f472(A, B, C) -> Com_1(f478(A, B, 5)) [ -C + 5 >= 0 /\ B - C + 3 >= 0 /\ -B - C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 1 >= C ] f466(A, B, C) -> Com_1(f472(A, B, 5)) [ -C + 5 >= 0 /\ B - C + 3 >= 0 /\ -B - C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ 2 >= C ] f458(A, B, C) -> Com_1(f466(A, B, 5)) [ C + 6 >= 0 /\ B + C + 4 >= 0 /\ -B + C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 5 ] f452(A, B, C) -> Com_1(f458(A, B, -6)) [ C + 6 >= 0 /\ B + C + 4 >= 0 /\ -B + C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 4 ] f446(A, B, C) -> Com_1(f452(A, B, -6)) [ C + 6 >= 0 /\ B + C + 4 >= 0 /\ -B + C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 5 ] f440(A, B, C) -> Com_1(f446(A, B, -6)) [ C + 6 >= 0 /\ B + C + 4 >= 0 /\ -B + C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 4 ] f432(A, B, C) -> Com_1(f440(A, B, -6)) [ C + 5 >= 0 /\ B + C + 3 >= 0 /\ -B + C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 1 ] f426(A, B, C) -> Com_1(f432(A, B, -5)) [ C + 5 >= 0 /\ B + C + 3 >= 0 /\ -B + C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 0 ] f420(A, B, C) -> Com_1(f426(A, B, -5)) [ C + 5 >= 0 /\ B + C + 3 >= 0 /\ -B + C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 1 ] f414(A, B, C) -> Com_1(f420(A, B, -5)) [ C + 5 >= 0 /\ B + C + 3 >= 0 /\ -B + C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 0 ] f406(A, B, C) -> Com_1(f414(A, B, -5)) [ C + 4 >= 0 /\ B + C + 2 >= 0 /\ -B + C + 6 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 0 ] f400(A, B, C) -> Com_1(f406(A, B, -4)) [ C + 4 >= 0 /\ B + C + 2 >= 0 /\ -B + C + 6 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 1 >= 0 ] f394(A, B, C) -> Com_1(f400(A, B, -4)) [ C + 4 >= 0 /\ B + C + 2 >= 0 /\ -B + C + 6 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 0 ] f388(A, B, C) -> Com_1(f394(A, B, -4)) [ C + 4 >= 0 /\ B + C + 2 >= 0 /\ -B + C + 6 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 1 >= 0 ] f380(A, B, C) -> Com_1(f388(A, B, -4)) [ C + 3 >= 0 /\ B + C + 1 >= 0 /\ -B + C + 5 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 1 >= 0 ] f374(A, B, C) -> Com_1(f380(A, B, -3)) [ C + 3 >= 0 /\ B + C + 1 >= 0 /\ -B + C + 5 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 2 >= 0 ] f368(A, B, C) -> Com_1(f374(A, B, -3)) [ C + 3 >= 0 /\ B + C + 1 >= 0 /\ -B + C + 5 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 1 >= 0 ] f362(A, B, C) -> Com_1(f368(A, B, -3)) [ C + 3 >= 0 /\ B + C + 1 >= 0 /\ -B + C + 5 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 2 >= 0 ] f354(A, B, C) -> Com_1(f362(A, B, -3)) [ C - 1 >= 0 /\ B + C - 3 >= 0 /\ -B + C + 1 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 3 ] f348(A, B, C) -> Com_1(f354(A, B, 1)) [ C - 1 >= 0 /\ B + C - 3 >= 0 /\ -B + C + 1 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 2 ] f342(A, B, C) -> Com_1(f348(A, B, 1)) [ C - 1 >= 0 /\ B + C - 3 >= 0 /\ -B + C + 1 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 3 ] f336(A, B, C) -> Com_1(f342(A, B, 1)) [ C - 1 >= 0 /\ B + C - 3 >= 0 /\ -B + C + 1 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 2 ] f328(A, B, C) -> Com_1(f336(A, B, 1)) [ C >= 0 /\ B + C - 2 >= 0 /\ -B + C + 2 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 4 ] f322(A, B, C) -> Com_1(f328(A, B, 0)) [ C >= 0 /\ B + C - 2 >= 0 /\ -B + C + 2 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 3 ] f316(A, B, C) -> Com_1(f322(A, B, 0)) [ C >= 0 /\ B + C - 2 >= 0 /\ -B + C + 2 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 4 ] f310(A, B, C) -> Com_1(f316(A, B, 0)) [ C >= 0 /\ B + C - 2 >= 0 /\ -B + C + 2 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 3 ] f302(A, B, C) -> Com_1(f310(A, B, 0)) [ C + 6 >= 0 /\ B + C + 4 >= 0 /\ -B + C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 5 ] f296(A, B, C) -> Com_1(f302(A, B, -6)) [ C + 6 >= 0 /\ B + C + 4 >= 0 /\ -B + C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 4 ] f290(A, B, C) -> Com_1(f296(A, B, -6)) [ C + 6 >= 0 /\ B + C + 4 >= 0 /\ -B + C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 5 ] f284(A, B, C) -> Com_1(f290(A, B, -6)) [ C + 6 >= 0 /\ B + C + 4 >= 0 /\ -B + C + 8 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 4 ] f276(A, B, C) -> Com_1(f284(A, B, -6)) [ C + 5 >= 0 /\ B + C + 3 >= 0 /\ -B + C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 1 ] f270(A, B, C) -> Com_1(f276(A, B, -5)) [ C + 5 >= 0 /\ B + C + 3 >= 0 /\ -B + C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 0 ] f264(A, B, C) -> Com_1(f270(A, B, -5)) [ C + 5 >= 0 /\ B + C + 3 >= 0 /\ -B + C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 1 ] f258(A, B, C) -> Com_1(f264(A, B, -5)) [ C + 5 >= 0 /\ B + C + 3 >= 0 /\ -B + C + 7 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 0 ] f250(A, B, C) -> Com_1(f258(A, B, -5)) [ C + 4 >= 0 /\ B + C + 2 >= 0 /\ -B + C + 6 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 0 ] f244(A, B, C) -> Com_1(f250(A, B, -4)) [ C + 4 >= 0 /\ B + C + 2 >= 0 /\ -B + C + 6 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 1 >= 0 ] f238(A, B, C) -> Com_1(f244(A, B, -4)) [ C + 4 >= 0 /\ B + C + 2 >= 0 /\ -B + C + 6 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C >= 0 ] f232(A, B, C) -> Com_1(f238(A, B, -4)) [ C + 4 >= 0 /\ B + C + 2 >= 0 /\ -B + C + 6 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 1 >= 0 ] f224(A, B, C) -> Com_1(f232(A, B, -4)) [ C + 3 >= 0 /\ B + C + 1 >= 0 /\ -B + C + 5 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 1 >= 0 ] f218(A, B, C) -> Com_1(f224(A, B, -3)) [ C + 3 >= 0 /\ B + C + 1 >= 0 /\ -B + C + 5 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 2 >= 0 ] f212(A, B, C) -> Com_1(f218(A, B, -3)) [ C + 3 >= 0 /\ B + C + 1 >= 0 /\ -B + C + 5 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 1 >= 0 ] f206(A, B, C) -> Com_1(f212(A, B, -3)) [ C + 3 >= 0 /\ B + C + 1 >= 0 /\ -B + C + 5 >= 0 /\ -B + 2 >= 0 /\ B - 2 >= 0 /\ C + 2 >= 0 ] f198(A, B, C) -> Com_1(f206(A, B, -3)) [ A - C - 3 >= 0 /\ C - 1 >= 0 /\ B + C - 3 >= 0 /\ -B + C + 1 >= 0 /\ A + C - 5 >= 0 /\ -B + 2 >= 0 /\ A - B - 2 >= 0 /\ B - 2 >= 0 /\ A + B - 6 >= 0 /\ A - 4 >= 0 /\ C >= 3 ] f192(A, B, C) -> Com_1(f198(A, B, 1)) [ A - C - 2 >= 0 /\ C - 1 >= 0 /\ B + C - 3 >= 0 /\ -B + C + 1 >= 0 /\ A + C - 4 >= 0 /\ -B + 2 >= 0 /\ A - B - 1 >= 0 /\ B - 2 >= 0 /\ A + B - 5 >= 0 /\ A - 3 >= 0 /\ C >= 2 ] f186(A, B, C) -> Com_1(f192(A, B, 1)) [ A - C >= 0 /\ C - 1 >= 0 /\ B + C - 3 >= 0 /\ -B + C + 1 >= 0 /\ A + C - 2 >= 0 /\ -B + 2 >= 0 /\ A - B + 1 >= 0 /\ B - 2 >= 0 /\ A + B - 3 >= 0 /\ A - 1 >= 0 /\ C >= 3 ] f180(A, B, C) -> Com_1(f186(A, B, 1)) [ A - C + 1 >= 0 /\ C - 1 >= 0 /\ B + C - 3 >= 0 /\ -B + C + 1 >= 0 /\ A + C - 1 >= 0 /\ -B + 2 >= 0 /\ A - B + 2 >= 0 /\ B - 2 >= 0 /\ A + B - 2 >= 0 /\ A >= 0 /\ C >= 2 ] f172(A, B, C) -> Com_1(f180(A, B, 1)) [ C >= 0 /\ B + C - 2 >= 0 /\ -B + C + 2 >= 0 /\ A + C >= 0 /\ -B + 2 >= 0 /\ A - B + 2 >= 0 /\ B - 2 >= 0 /\ A + B - 2 >= 0 /\ A >= 0 /\ C >= 4 ] f166(A, B, C) -> Com_1(f172(A, B, 0)) [ C >= 0 /\ B + C - 2 >= 0 /\ -B + C + 2 >= 0 /\ A + C >= 0 /\ -B + 2 >= 0 /\ A - B + 2 >= 0 /\ B - 2 >= 0 /\ A + B - 2 >= 0 /\ A >= 0 /\ C >= 3 ] f160(A, B, C) -> Com_1(f166(A, B, 0)) [ C >= 0 /\ B + C - 2 >= 0 /\ -B + C + 2 >= 0 /\ A + C >= 0 /\ -B + 2 >= 0 /\ A - B + 2 >= 0 /\ B - 2 >= 0 /\ A + B - 2 >= 0 /\ A >= 0 /\ C >= 4 ] f154(A, B, C) -> Com_1(f160(A, B, 0)) [ C >= 0 /\ B + C - 2 >= 0 /\ -B + C + 2 >= 0 /\ A + C >= 0 /\ -B + 2 >= 0 /\ A - B + 2 >= 0 /\ B - 2 >= 0 /\ A + B - 2 >= 0 /\ A >= 0 /\ C >= 3 ] )