(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(l1(A + 1, B - 1, C, D)) [ A >= 0 /\ B >= 1 ] l1(A, B, C, D) -> Com_1(l2(A, B, A, D)) [ A >= 0 /\ 0 >= B ] l2(A, B, C, D) -> Com_1(l3(A, B, C, C)) [ A - C >= 0 /\ C >= 0 /\ -B + C >= 0 /\ A + C >= 0 /\ -B >= 0 /\ A - B >= 0 /\ A >= 0 /\ C >= 1 ] l3(A, B, C, D) -> Com_1(l3(A, B, C, D - 1)) [ C - D >= 0 /\ A - D >= 0 /\ A - C >= 0 /\ C - 1 >= 0 /\ -B + C - 1 >= 0 /\ A + C - 2 >= 0 /\ -B >= 0 /\ A - B - 1 >= 0 /\ A - 1 >= 0 /\ D >= 1 /\ C >= 1 ] l3(A, B, C, D) -> Com_1(l2(A, B, C - 1, D)) [ C - D >= 0 /\ A - D >= 0 /\ A - C >= 0 /\ C - 1 >= 0 /\ -B + C - 1 >= 0 /\ A + C - 2 >= 0 /\ -B >= 0 /\ A - B - 1 >= 0 /\ A - 1 >= 0 /\ 0 >= D /\ C >= 1 ] )