(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS evalDis2start)) (VAR A B C) (RULES evalDis2start(A, B, C) -> Com_1(evalDis2entryin(A, B, C)) evalDis2entryin(A, B, C) -> Com_1(evalDis2bb3in(B, C, A)) evalDis2bb3in(A, B, C) -> Com_1(evalDis2bbin(A, B, C)) [ A >= C + 1 ] evalDis2bb3in(A, B, C) -> Com_1(evalDis2returnin(A, B, C)) [ C >= A ] evalDis2bbin(A, B, C) -> Com_1(evalDis2bb1in(A, B, C)) [ A - C - 1 >= 0 /\ B >= C + 1 ] evalDis2bbin(A, B, C) -> Com_1(evalDis2bb2in(A, B, C)) [ A - C - 1 >= 0 /\ C >= B ] evalDis2bb1in(A, B, C) -> Com_1(evalDis2bb3in(A, B, C + 1)) [ B - C - 1 >= 0 /\ A - C - 1 >= 0 ] evalDis2bb2in(A, B, C) -> Com_1(evalDis2bb3in(A, B + 1, C)) [ A - C - 1 >= 0 /\ -B + C >= 0 /\ A - B - 1 >= 0 ] evalDis2returnin(A, B, C) -> Com_1(evalDis2stop(A, B, C)) [ -A + C >= 0 ] )