(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS evalrsdstart))
(VAR A B C)
(RULES
  evalrsdstart(A, B, C) -> Com_1(evalrsdentryin(A, B, C))
  evalrsdentryin(A, B, C) -> Com_1(evalrsdbbin(A, B, C)) [ A >= 0 ]
  evalrsdentryin(A, B, C) -> Com_1(evalrsdreturnin(A, B, C)) [ 0 >= A + 1 ]
  evalrsdbbin(A, B, C) -> Com_1(evalrsdbb4in(A, 2*A, 2*A)) [ A >= 0 ]
  evalrsdbb4in(A, B, C) -> Com_1(evalrsdbb1in(A, B, C)) [ A >= 0 /\ C >= A ]
  evalrsdbb4in(A, B, C) -> Com_1(evalrsdreturnin(A, B, C)) [ A >= 0 /\ A >= C + 1 ]
  evalrsdbb1in(A, B, C) -> Com_1(evalrsdbb2in(A, B, C)) [ C >= 0 /\ A + C >= 0 /\ -A + C >= 0 /\ A >= 0 /\ 0 >= D + 1 ]
  evalrsdbb1in(A, B, C) -> Com_1(evalrsdbb2in(A, B, C)) [ C >= 0 /\ A + C >= 0 /\ -A + C >= 0 /\ A >= 0 /\ D >= 1 ]
  evalrsdbb1in(A, B, C) -> Com_1(evalrsdbb3in(A, B, C)) [ C >= 0 /\ A + C >= 0 /\ -A + C >= 0 /\ A >= 0 ]
  evalrsdbb2in(A, B, C) -> Com_1(evalrsdbb4in(A, B, C - 1)) [ C >= 0 /\ A + C >= 0 /\ -A + C >= 0 /\ A >= 0 ]
  evalrsdbb3in(A, B, C) -> Com_1(evalrsdbb4in(A, B - 1, B - 1)) [ C >= 0 /\ A + C >= 0 /\ -A + C >= 0 /\ A >= 0 ]
  evalrsdreturnin(A, B, C) -> Com_1(evalrsdstop(A, B, C))
)