YES(?, 18*b + 18*a + 15)

Initial complexity problem:
1:	T:
		(1, 1)    evalwisestart(a, b) -> evalwiseentryin(a, b)
		(?, 1)    evalwiseentryin(a, b) -> evalwisereturnin(a, b) [ 0 >= a + 1 ]
		(?, 1)    evalwiseentryin(a, b) -> evalwisereturnin(a, b) [ 0 >= b + 1 ]
		(?, 1)    evalwiseentryin(a, b) -> evalwisebb6in(b, a) [ a >= 0 /\ b >= 0 ]
		(?, 1)    evalwisebb6in(a, b) -> evalwisebb3in(a, b) [ b >= a + 3 ]
		(?, 1)    evalwisebb6in(a, b) -> evalwisebb3in(a, b) [ a >= b + 3 ]
		(?, 1)    evalwisebb6in(a, b) -> evalwisereturnin(a, b) [ a + 2 >= b /\ b + 2 >= a ]
		(?, 1)    evalwisebb3in(a, b) -> evalwisebb4in(a, b) [ a >= b + 1 ]
		(?, 1)    evalwisebb3in(a, b) -> evalwisebb5in(a, b) [ b >= a ]
		(?, 1)    evalwisebb4in(a, b) -> evalwisebb6in(a, b + 1)
		(?, 1)    evalwisebb5in(a, b) -> evalwisebb6in(a + 1, b)
		(?, 1)    evalwisereturnin(a, b) -> evalwisestop(a, b)
	start location:	evalwisestart
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(1, 1)    evalwisestart(a, b) -> evalwiseentryin(a, b)
		(?, 1)    evalwiseentryin(a, b) -> evalwisebb6in(b, a) [ a >= 0 /\ b >= 0 ]
		(?, 1)    evalwisebb6in(a, b) -> evalwisebb3in(a, b) [ b >= a + 3 ]
		(?, 1)    evalwisebb6in(a, b) -> evalwisebb3in(a, b) [ a >= b + 3 ]
		(?, 1)    evalwisebb3in(a, b) -> evalwisebb4in(a, b) [ a >= b + 1 ]
		(?, 1)    evalwisebb3in(a, b) -> evalwisebb5in(a, b) [ b >= a ]
		(?, 1)    evalwisebb4in(a, b) -> evalwisebb6in(a, b + 1)
		(?, 1)    evalwisebb5in(a, b) -> evalwisebb6in(a + 1, b)
	start location:	evalwisestart
	leaf cost:	4

Repeatedly propagating knowledge in problem 2 produces the following problem:
3:	T:
		(1, 1)    evalwisestart(a, b) -> evalwiseentryin(a, b)
		(1, 1)    evalwiseentryin(a, b) -> evalwisebb6in(b, a) [ a >= 0 /\ b >= 0 ]
		(?, 1)    evalwisebb6in(a, b) -> evalwisebb3in(a, b) [ b >= a + 3 ]
		(?, 1)    evalwisebb6in(a, b) -> evalwisebb3in(a, b) [ a >= b + 3 ]
		(?, 1)    evalwisebb3in(a, b) -> evalwisebb4in(a, b) [ a >= b + 1 ]
		(?, 1)    evalwisebb3in(a, b) -> evalwisebb5in(a, b) [ b >= a ]
		(?, 1)    evalwisebb4in(a, b) -> evalwisebb6in(a, b + 1)
		(?, 1)    evalwisebb5in(a, b) -> evalwisebb6in(a + 1, b)
	start location:	evalwisestart
	leaf cost:	4

Applied AI with 'oct' on problem 3 to obtain the following invariants:
  For symbol evalwisebb3in: X_2 >= 0 /\ X_1 + X_2 - 3 >= 0 /\ X_1 >= 0
  For symbol evalwisebb4in: X_1 - X_2 - 1 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 - 3 >= 0 /\ X_1 - 2 >= 0
  For symbol evalwisebb5in: X_2 - 1 >= 0 /\ X_1 + X_2 - 3 >= 0 /\ -X_1 + X_2 >= 0 /\ X_1 >= 0
  For symbol evalwisebb6in: X_2 >= 0 /\ X_1 + X_2 >= 0 /\ X_1 >= 0


This yielded the following problem:
4:	T:
		(?, 1)    evalwisebb5in(a, b) -> evalwisebb6in(a + 1, b) [ b - 1 >= 0 /\ a + b - 3 >= 0 /\ -a + b >= 0 /\ a >= 0 ]
		(?, 1)    evalwisebb4in(a, b) -> evalwisebb6in(a, b + 1) [ a - b - 1 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 ]
		(?, 1)    evalwisebb3in(a, b) -> evalwisebb5in(a, b) [ b >= 0 /\ a + b - 3 >= 0 /\ a >= 0 /\ b >= a ]
		(?, 1)    evalwisebb3in(a, b) -> evalwisebb4in(a, b) [ b >= 0 /\ a + b - 3 >= 0 /\ a >= 0 /\ a >= b + 1 ]
		(?, 1)    evalwisebb6in(a, b) -> evalwisebb3in(a, b) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= b + 3 ]
		(?, 1)    evalwisebb6in(a, b) -> evalwisebb3in(a, b) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= a + 3 ]
		(1, 1)    evalwiseentryin(a, b) -> evalwisebb6in(b, a) [ a >= 0 /\ b >= 0 ]
		(1, 1)    evalwisestart(a, b) -> evalwiseentryin(a, b)
	start location:	evalwisestart
	leaf cost:	4

A polynomial rank function with
	Pol(evalwisebb5in) = -3*V_1 + 3*V_2 + 1
	Pol(evalwisebb6in) = -3*V_1 + 3*V_2 + 3
	Pol(evalwisebb3in) = -3*V_1 + 3*V_2 + 2
and size complexities
	S("evalwisestart(a, b) -> evalwiseentryin(a, b)", 0-0) = a
	S("evalwisestart(a, b) -> evalwiseentryin(a, b)", 0-1) = b
	S("evalwiseentryin(a, b) -> evalwisebb6in(b, a) [ a >= 0 /\\ b >= 0 ]", 0-0) = b
	S("evalwiseentryin(a, b) -> evalwisebb6in(b, a) [ a >= 0 /\\ b >= 0 ]", 0-1) = a
	S("evalwisebb6in(a, b) -> evalwisebb3in(a, b) [ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ b >= a + 3 ]", 0-0) = ?
	S("evalwisebb6in(a, b) -> evalwisebb3in(a, b) [ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ b >= a + 3 ]", 0-1) = a
	S("evalwisebb6in(a, b) -> evalwisebb3in(a, b) [ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ a >= b + 3 ]", 0-0) = b
	S("evalwisebb6in(a, b) -> evalwisebb3in(a, b) [ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ a >= b + 3 ]", 0-1) = a + b
	S("evalwisebb3in(a, b) -> evalwisebb4in(a, b) [ b >= 0 /\\ a + b - 3 >= 0 /\\ a >= 0 /\\ a >= b + 1 ]", 0-0) = b
	S("evalwisebb3in(a, b) -> evalwisebb4in(a, b) [ b >= 0 /\\ a + b - 3 >= 0 /\\ a >= 0 /\\ a >= b + 1 ]", 0-1) = a + b
	S("evalwisebb3in(a, b) -> evalwisebb5in(a, b) [ b >= 0 /\\ a + b - 3 >= 0 /\\ a >= 0 /\\ b >= a ]", 0-0) = ?
	S("evalwisebb3in(a, b) -> evalwisebb5in(a, b) [ b >= 0 /\\ a + b - 3 >= 0 /\\ a >= 0 /\\ b >= a ]", 0-1) = a
	S("evalwisebb4in(a, b) -> evalwisebb6in(a, b + 1) [ a - b - 1 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 2 >= 0 ]", 0-0) = b
	S("evalwisebb4in(a, b) -> evalwisebb6in(a, b + 1) [ a - b - 1 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 2 >= 0 ]", 0-1) = b
	S("evalwisebb5in(a, b) -> evalwisebb6in(a + 1, b) [ b - 1 >= 0 /\\ a + b - 3 >= 0 /\\ -a + b >= 0 /\\ a >= 0 ]", 0-0) = ?
	S("evalwisebb5in(a, b) -> evalwisebb6in(a + 1, b) [ b - 1 >= 0 /\\ a + b - 3 >= 0 /\\ -a + b >= 0 /\\ a >= 0 ]", 0-1) = a
orients the transitions
	evalwisebb5in(a, b) -> evalwisebb6in(a + 1, b) [ b - 1 >= 0 /\ a + b - 3 >= 0 /\ -a + b >= 0 /\ a >= 0 ]
	evalwisebb3in(a, b) -> evalwisebb5in(a, b) [ b >= 0 /\ a + b - 3 >= 0 /\ a >= 0 /\ b >= a ]
	evalwisebb6in(a, b) -> evalwisebb3in(a, b) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= a + 3 ]
weakly and the transitions
	evalwisebb6in(a, b) -> evalwisebb3in(a, b) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= a + 3 ]
	evalwisebb5in(a, b) -> evalwisebb6in(a + 1, b) [ b - 1 >= 0 /\ a + b - 3 >= 0 /\ -a + b >= 0 /\ a >= 0 ]
	evalwisebb3in(a, b) -> evalwisebb5in(a, b) [ b >= 0 /\ a + b - 3 >= 0 /\ a >= 0 /\ b >= a ]
strictly and produces the following problem:
5:	T:
		(3*b + 3*a + 3, 1)    evalwisebb5in(a, b) -> evalwisebb6in(a + 1, b) [ b - 1 >= 0 /\ a + b - 3 >= 0 /\ -a + b >= 0 /\ a >= 0 ]
		(?, 1)                evalwisebb4in(a, b) -> evalwisebb6in(a, b + 1) [ a - b - 1 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 ]
		(3*b + 3*a + 3, 1)    evalwisebb3in(a, b) -> evalwisebb5in(a, b) [ b >= 0 /\ a + b - 3 >= 0 /\ a >= 0 /\ b >= a ]
		(?, 1)                evalwisebb3in(a, b) -> evalwisebb4in(a, b) [ b >= 0 /\ a + b - 3 >= 0 /\ a >= 0 /\ a >= b + 1 ]
		(?, 1)                evalwisebb6in(a, b) -> evalwisebb3in(a, b) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= b + 3 ]
		(3*b + 3*a + 3, 1)    evalwisebb6in(a, b) -> evalwisebb3in(a, b) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= a + 3 ]
		(1, 1)                evalwiseentryin(a, b) -> evalwisebb6in(b, a) [ a >= 0 /\ b >= 0 ]
		(1, 1)                evalwisestart(a, b) -> evalwiseentryin(a, b)
	start location:	evalwisestart
	leaf cost:	4

A polynomial rank function with
	Pol(evalwisebb6in) = 3*V_1 - 3*V_2
	Pol(evalwisebb3in) = 3*V_1 - 3*V_2 - 1
	Pol(evalwisebb4in) = 3*V_1 - 3*V_2 - 2
and size complexities
	S("evalwisestart(a, b) -> evalwiseentryin(a, b)", 0-0) = a
	S("evalwisestart(a, b) -> evalwiseentryin(a, b)", 0-1) = b
	S("evalwiseentryin(a, b) -> evalwisebb6in(b, a) [ a >= 0 /\\ b >= 0 ]", 0-0) = b
	S("evalwiseentryin(a, b) -> evalwisebb6in(b, a) [ a >= 0 /\\ b >= 0 ]", 0-1) = a
	S("evalwisebb6in(a, b) -> evalwisebb3in(a, b) [ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ b >= a + 3 ]", 0-0) = 4*a + 4*b + 48
	S("evalwisebb6in(a, b) -> evalwisebb3in(a, b) [ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ b >= a + 3 ]", 0-1) = a
	S("evalwisebb6in(a, b) -> evalwisebb3in(a, b) [ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ a >= b + 3 ]", 0-0) = b
	S("evalwisebb6in(a, b) -> evalwisebb3in(a, b) [ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ a >= b + 3 ]", 0-1) = a + b
	S("evalwisebb3in(a, b) -> evalwisebb4in(a, b) [ b >= 0 /\\ a + b - 3 >= 0 /\\ a >= 0 /\\ a >= b + 1 ]", 0-0) = b
	S("evalwisebb3in(a, b) -> evalwisebb4in(a, b) [ b >= 0 /\\ a + b - 3 >= 0 /\\ a >= 0 /\\ a >= b + 1 ]", 0-1) = a + b
	S("evalwisebb3in(a, b) -> evalwisebb5in(a, b) [ b >= 0 /\\ a + b - 3 >= 0 /\\ a >= 0 /\\ b >= a ]", 0-0) = 4*a + 4*b + 48
	S("evalwisebb3in(a, b) -> evalwisebb5in(a, b) [ b >= 0 /\\ a + b - 3 >= 0 /\\ a >= 0 /\\ b >= a ]", 0-1) = a
	S("evalwisebb4in(a, b) -> evalwisebb6in(a, b + 1) [ a - b - 1 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 2 >= 0 ]", 0-0) = b
	S("evalwisebb4in(a, b) -> evalwisebb6in(a, b + 1) [ a - b - 1 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 2 >= 0 ]", 0-1) = b
	S("evalwisebb5in(a, b) -> evalwisebb6in(a + 1, b) [ b - 1 >= 0 /\\ a + b - 3 >= 0 /\\ -a + b >= 0 /\\ a >= 0 ]", 0-0) = 4*a + 4*b + 48
	S("evalwisebb5in(a, b) -> evalwisebb6in(a + 1, b) [ b - 1 >= 0 /\\ a + b - 3 >= 0 /\\ -a + b >= 0 /\\ a >= 0 ]", 0-1) = a
orients the transitions
	evalwisebb6in(a, b) -> evalwisebb3in(a, b) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= b + 3 ]
	evalwisebb4in(a, b) -> evalwisebb6in(a, b + 1) [ a - b - 1 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 ]
	evalwisebb3in(a, b) -> evalwisebb4in(a, b) [ b >= 0 /\ a + b - 3 >= 0 /\ a >= 0 /\ a >= b + 1 ]
weakly and the transitions
	evalwisebb6in(a, b) -> evalwisebb3in(a, b) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= b + 3 ]
	evalwisebb4in(a, b) -> evalwisebb6in(a, b + 1) [ a - b - 1 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 ]
	evalwisebb3in(a, b) -> evalwisebb4in(a, b) [ b >= 0 /\ a + b - 3 >= 0 /\ a >= 0 /\ a >= b + 1 ]
strictly and produces the following problem:
6:	T:
		(3*b + 3*a + 3, 1)    evalwisebb5in(a, b) -> evalwisebb6in(a + 1, b) [ b - 1 >= 0 /\ a + b - 3 >= 0 /\ -a + b >= 0 /\ a >= 0 ]
		(3*b + 3*a, 1)        evalwisebb4in(a, b) -> evalwisebb6in(a, b + 1) [ a - b - 1 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 ]
		(3*b + 3*a + 3, 1)    evalwisebb3in(a, b) -> evalwisebb5in(a, b) [ b >= 0 /\ a + b - 3 >= 0 /\ a >= 0 /\ b >= a ]
		(3*b + 3*a, 1)        evalwisebb3in(a, b) -> evalwisebb4in(a, b) [ b >= 0 /\ a + b - 3 >= 0 /\ a >= 0 /\ a >= b + 1 ]
		(3*b + 3*a, 1)        evalwisebb6in(a, b) -> evalwisebb3in(a, b) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= b + 3 ]
		(3*b + 3*a + 3, 1)    evalwisebb6in(a, b) -> evalwisebb3in(a, b) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ b >= a + 3 ]
		(1, 1)                evalwiseentryin(a, b) -> evalwisebb6in(b, a) [ a >= 0 /\ b >= 0 ]
		(1, 1)                evalwisestart(a, b) -> evalwiseentryin(a, b)
	start location:	evalwisestart
	leaf cost:	4

Complexity upper bound 18*b + 18*a + 15

Time: 0.441 sec (SMT: 0.416 sec)