(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS evalrealbubblestart))
(VAR A B C D)
(RULES
  evalrealbubblestart(A, B, C, D) -> Com_1(evalrealbubbleentryin(A, B, C, D))
  evalrealbubbleentryin(A, B, C, D) -> Com_1(evalrealbubblebb7in(A - 1, B, C, D))
  evalrealbubblebb7in(A, B, C, D) -> Com_1(evalrealbubblebb4in(A, 0, 0, D)) [ A >= 1 ]
  evalrealbubblebb7in(A, B, C, D) -> Com_1(evalrealbubblereturnin(A, B, C, D)) [ 0 >= A ]
  evalrealbubblebb4in(A, B, C, D) -> Com_1(evalrealbubblebb1in(A, B, C, D)) [ B - C >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 /\ A >= B + 1 ]
  evalrealbubblebb4in(A, B, C, D) -> Com_1(evalrealbubblebb5in(A, B, C, D)) [ B - C >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 /\ B >= A ]
  evalrealbubblebb1in(A, B, C, D) -> Com_1(evalrealbubblebb2in(A, B, C, D)) [ B - C >= 0 /\ A - C - 1 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 1 >= 0 /\ A - B - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 /\ E >= F + 1 ]
  evalrealbubblebb1in(A, B, C, D) -> Com_1(evalrealbubblebb3in(A, B, C, C)) [ B - C >= 0 /\ A - C - 1 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 1 >= 0 /\ A - B - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 /\ F >= E ]
  evalrealbubblebb2in(A, B, C, D) -> Com_1(evalrealbubblebb3in(A, B, C, 1)) [ B - C >= 0 /\ A - C - 1 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 1 >= 0 /\ A - B - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 ]
  evalrealbubblebb3in(A, B, C, D) -> Com_1(evalrealbubblebb4in(A, B + 1, D, D)) [ C - D + 1 >= 0 /\ B - D + 1 >= 0 /\ A - D >= 0 /\ D >= 0 /\ C + D >= 0 /\ B + D >= 0 /\ A + D - 1 >= 0 /\ B - C >= 0 /\ A - C - 1 >= 0 /\ C >= 0 /\ B + C >= 0 /\ A + C - 1 >= 0 /\ A - B - 1 >= 0 /\ B >= 0 /\ A + B - 1 >= 0 /\ A - 1 >= 0 ]
  evalrealbubblebb5in(A, B, C, D) -> Com_1(evalrealbubblereturnin(A, B, C, D)) [ B - C >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ A - 1 >= 0 /\ C = 0 ]
  evalrealbubblebb5in(A, B, C, D) -> Com_1(evalrealbubblebb6in(A, B, C, D)) [ B - C >= 0 /\ C >= 0 /\ B + C - 1 >= 0 /\ A + C - 1 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ A - 1 >= 0 /\ C >= 1 ]
  evalrealbubblebb6in(A, B, C, D) -> Com_1(evalrealbubblebb7in(A - 1, B, C, D)) [ B - C >= 0 /\ C - 1 >= 0 /\ B + C - 2 >= 0 /\ A + C - 2 >= 0 /\ B - 1 >= 0 /\ A + B - 2 >= 0 /\ -A + B >= 0 /\ A - 1 >= 0 ]
  evalrealbubblereturnin(A, B, C, D) -> Com_1(evalrealbubblestop(A, B, C, D))
)