(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS evalfstart))
(VAR A B C)
(RULES
  evalfstart(A,B) -> Com_1(evalfentryin(A,B))
  evalfentryin(A,B) -> Com_1(evalfbb3in(B,A)) :|: A >= 1 && B >= A + 1
  evalfbb3in(A,B) -> Com_1(evalfreturnin(A,B)) :|: 0 >= A
  evalfbb3in(A,B) -> Com_1(evalfbb4in(A,B)) :|: A >= 1
  evalfbb4in(A,B) -> Com_1(evalfbbin(A,B)) :|: 0 >= C + 1
  evalfbb4in(A,B) -> Com_1(evalfbbin(A,B)) :|: C >= 1
  evalfbb4in(A,B) -> Com_1(evalfreturnin(A,B))
  evalfbbin(A,B) -> Com_1(evalfbb1in(A,B)) :|: B >= A + 1
  evalfbbin(A,B) -> Com_1(evalfbb2in(A,B)) :|: A >= B
  evalfbb1in(A,B) -> Com_1(evalfbb3in(A + 1,B))
  evalfbb2in(A,B) -> Com_1(evalfbb3in(A - B,B))
  evalfreturnin(A,B) -> Com_1(evalfstop(A,B))
)