(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS start0)) (VAR A B C D) (RULES start(A, B, C, D) -> Com_1(stop1(A, B, C, D)) [ A - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ B + D >= 0 /\ A + D >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ D = 0 ] start(A, B, C, D) -> Com_1(cont1(A, B, C, D)) [ A - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ B + D >= 0 /\ A + D >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ D >= 1 /\ A >= D ] cont1(A, B, C, D) -> Com_1(stop2(A, B, 1, D - 1)) [ A - D >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ B + D - 1 >= 0 /\ A + D - 2 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 /\ D >= 1 /\ A >= D /\ C = 0 ] cont1(A, B, C, D) -> Com_1(a(A, B, C - 1, D)) [ A - D >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ B + D - 1 >= 0 /\ A + D - 2 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 /\ C >= 1 /\ D >= 1 /\ A >= D ] a(A, B, C, D) -> Com_1(b(A, B, E, D - 1)) [ A - D >= 0 /\ D - 1 >= 0 /\ C + D - 1 >= 0 /\ B + D - 1 >= 0 /\ A + D - 2 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 /\ A >= D /\ D >= 1 ] b(A, B, C, D) -> Com_1(start(A, B, C, D)) [ A - D - 1 >= 0 /\ D >= 0 /\ B + D >= 0 /\ A + D - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 /\ C >= 0 /\ A >= D + 1 ] b(A, B, C, D) -> Com_1(stop3(A, B, C, D)) [ A - D - 1 >= 0 /\ D >= 0 /\ B + D >= 0 /\ A + D - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 /\ 0 >= C + 1 /\ A >= D + 1 ] start0(A, B, C, D) -> Com_1(start(A, B, B, A)) [ A >= 0 /\ B >= 0 ] )