(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS evalwisestart))
(VAR A B)
(RULES
  evalwisestart(A, B) -> Com_1(evalwiseentryin(A, B))
  evalwiseentryin(A, B) -> Com_1(evalwisereturnin(A, B)) [ 0 >= A + 1 ]
  evalwiseentryin(A, B) -> Com_1(evalwisereturnin(A, B)) [ 0 >= B + 1 ]
  evalwiseentryin(A, B) -> Com_1(evalwisebb6in(B, A)) [ A >= 0 /\ B >= 0 ]
  evalwisebb6in(A, B) -> Com_1(evalwisebb3in(A, B)) [ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ B >= A + 3 ]
  evalwisebb6in(A, B) -> Com_1(evalwisebb3in(A, B)) [ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ A >= B + 3 ]
  evalwisebb6in(A, B) -> Com_1(evalwisereturnin(A, B)) [ B >= 0 /\ A + B >= 0 /\ A >= 0 /\ A + 2 >= B /\ B + 2 >= A ]
  evalwisebb3in(A, B) -> Com_1(evalwisebb4in(A, B)) [ B >= 0 /\ A + B - 3 >= 0 /\ A >= 0 /\ A >= B + 1 ]
  evalwisebb3in(A, B) -> Com_1(evalwisebb5in(A, B)) [ B >= 0 /\ A + B - 3 >= 0 /\ A >= 0 /\ B >= A ]
  evalwisebb4in(A, B) -> Com_1(evalwisebb6in(A, B + 1)) [ A - B - 1 >= 0 /\ B >= 0 /\ A + B - 3 >= 0 /\ A - 2 >= 0 ]
  evalwisebb5in(A, B) -> Com_1(evalwisebb6in(A + 1, B)) [ B - 1 >= 0 /\ A + B - 3 >= 0 /\ -A + B >= 0 /\ A >= 0 ]
  evalwisereturnin(A, B) -> Com_1(evalwisestop(A, B))
)