(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS start0)) (VAR A B C D) (RULES start(A, B, C, D) -> Com_1(lbl41(E, B, C, D)) [ C - D >= 0 /\ -C + D >= 0 /\ A - B >= 0 /\ -A + B >= 0 /\ A = B /\ C = D ] lbl41(A, B, C, D) -> Com_1(stop(A, B, A, D)) [ C - D >= 0 /\ -C + D >= 0 /\ C = D ] start0(A, B, C, D) -> Com_1(start(B, B, D, D)) )