(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS evalsipmabubblestart)) (VAR A B) (RULES evalsipmabubblestart(A, B) -> Com_1(evalsipmabubbleentryin(A, B)) evalsipmabubbleentryin(A, B) -> Com_1(evalsipmabubblebb6in(A, B)) evalsipmabubblebb6in(A, B) -> Com_1(evalsipmabubblebb4in(A, 0)) [ A >= 0 ] evalsipmabubblebb6in(A, B) -> Com_1(evalsipmabubblereturnin(A, B)) [ 0 >= A + 1 ] evalsipmabubblebb4in(A, B) -> Com_1(evalsipmabubblebb1in(A, B)) [ A - B >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ A >= B + 1 ] evalsipmabubblebb4in(A, B) -> Com_1(evalsipmabubblebb5in(A, B)) [ A - B >= 0 /\ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ B >= A ] evalsipmabubblebb1in(A, B) -> Com_1(evalsipmabubblebb2in(A, B)) [ A - B - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 /\ C >= D + 1 ] evalsipmabubblebb1in(A, B) -> Com_1(evalsipmabubblebb3in(A, B)) [ A - B - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 /\ D >= C ] evalsipmabubblebb2in(A, B) -> Com_1(evalsipmabubblebb3in(A, B)) [ A - B - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 ] evalsipmabubblebb3in(A, B) -> Com_1(evalsipmabubblebb4in(A, B + 1)) [ A - B - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 ] evalsipmabubblebb5in(A, B) -> Com_1(evalsipmabubblebb6in(A - 1, B)) [ A - B >= 0 /\ B >= 0 /\ A + B >= 0 /\ -A + B >= 0 /\ A >= 0 ] evalsipmabubblereturnin(A, B) -> Com_1(evalsipmabubblestop(A, B)) [ -A - 1 >= 0 ] )