(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS l0)) (VAR A B C D) (RULES l0(A, B, C, D) -> Com_1(l1(0, B, C, D)) l1(A, B, C, D) -> Com_1(l2(A, B, 0, 0)) [ A >= 0 /\ B > 0 ] l2(A, B, C, D) -> Com_1(l2(A, B, C + 1, D + C)) [ D >= 0 /\ C + D >= 0 /\ B + D - 1 >= 0 /\ A + D >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ A >= 0 /\ C < B ] l2(A, B, C, D) -> Com_1(l1(A + D, B - 1, C, D)) [ D >= 0 /\ C + D >= 0 /\ B + D - 1 >= 0 /\ A + D >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C >= 0 /\ B - 1 >= 0 /\ A + B - 1 >= 0 /\ A >= 0 /\ C >= B ] l1(A, B, C, D) -> Com_1(l3(A, B, C, D)) [ A >= 0 /\ B <= 0 ] l3(A, B, C, D) -> Com_1(l3(A - 1, B, C, D)) [ -B >= 0 /\ A - B >= 0 /\ A >= 0 /\ A > 0 ] )