(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS evalcyclicstart))
(VAR A B C)
(RULES
  evalcyclicstart(A, B, C) -> Com_1(evalcyclicentryin(A, B, C))
  evalcyclicentryin(A, B, C) -> Com_1(evalcyclicbb3in(A, B, A + 1)) [ A >= 0 /\ B >= A + 1 ]
  evalcyclicbb3in(A, B, C) -> Com_1(evalcyclicreturnin(A, B, C)) [ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ C = A ]
  evalcyclicbb3in(A, B, C) -> Com_1(evalcyclicbb4in(A, B, C)) [ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ A >= C + 1 ]
  evalcyclicbb3in(A, B, C) -> Com_1(evalcyclicbb4in(A, B, C)) [ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ C >= A + 1 ]
  evalcyclicbb4in(A, B, C) -> Com_1(evalcyclicbbin(A, B, C)) [ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ 0 >= D + 1 ]
  evalcyclicbb4in(A, B, C) -> Com_1(evalcyclicbbin(A, B, C)) [ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ D >= 1 ]
  evalcyclicbb4in(A, B, C) -> Com_1(evalcyclicreturnin(A, B, C)) [ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 ]
  evalcyclicbbin(A, B, C) -> Com_1(evalcyclicbb3in(A, B, C + 1)) [ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ B >= C ]
  evalcyclicbbin(A, B, C) -> Com_1(evalcyclicbb3in(A, B, 0)) [ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 /\ C >= B + 1 ]
  evalcyclicreturnin(A, B, C) -> Com_1(evalcyclicstop(A, B, C)) [ B - 1 >= 0 /\ A + B - 1 >= 0 /\ -A + B - 1 >= 0 /\ A >= 0 ]
)