(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 >= 1 ] 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 /\ B >= C + 1 ] 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 ] )