(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS evalDis1start)) (VAR A B C D) (RULES evalDis1start(A, B, C, D) -> Com_1(evalDis1entryin(A, B, C, D)) evalDis1entryin(A, B, C, D) -> Com_1(evalDis1bb3in(B, A, D, C)) evalDis1bb3in(A, B, C, D) -> Com_1(evalDis1bbin(A, B, C, D)) [ A >= B + 1 ] evalDis1bb3in(A, B, C, D) -> Com_1(evalDis1returnin(A, B, C, D)) [ B >= A ] evalDis1bbin(A, B, C, D) -> Com_1(evalDis1bb1in(A, B, C, D)) [ A - B - 1 >= 0 /\ C >= D + 1 ] evalDis1bbin(A, B, C, D) -> Com_1(evalDis1bb2in(A, B, C, D)) [ A - B - 1 >= 0 /\ D >= C ] evalDis1bb1in(A, B, C, D) -> Com_1(evalDis1bb3in(A, B, C, D + 1)) [ C - D - 1 >= 0 /\ A - B - 1 >= 0 ] evalDis1bb2in(A, B, C, D) -> Com_1(evalDis1bb3in(A, B + 1, C, D)) [ -C + D >= 0 /\ A - B - 1 >= 0 ] evalDis1returnin(A, B, C, D) -> Com_1(evalDis1stop(A, B, C, D)) [ -A + B >= 0 ] )