YES(?, 123984*a + 360*a^2 + 530498)

Initial complexity problem:
1:	T:
		(1, 1)    evalwcet2start(a, b) -> evalwcet2entryin(a, b)
		(?, 1)    evalwcet2entryin(a, b) -> evalwcet2bb5in(a, b)
		(?, 1)    evalwcet2bb5in(a, b) -> evalwcet2bb2in(a, 0) [ 4 >= a ]
		(?, 1)    evalwcet2bb5in(a, b) -> evalwcet2returnin(a, b) [ a >= 5 ]
		(?, 1)    evalwcet2bb2in(a, b) -> evalwcet2bb1in(a, b) [ a >= 3 /\ 9 >= b ]
		(?, 1)    evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ 2 >= a ]
		(?, 1)    evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ b >= 10 ]
		(?, 1)    evalwcet2bb1in(a, b) -> evalwcet2bb2in(a, b + 1)
		(?, 1)    evalwcet2bb4in(a, b) -> evalwcet2bb5in(a + 1, b)
		(?, 1)    evalwcet2returnin(a, b) -> evalwcet2stop(a, b)
	start location:	evalwcet2start
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(1, 1)    evalwcet2start(a, b) -> evalwcet2entryin(a, b)
		(?, 1)    evalwcet2entryin(a, b) -> evalwcet2bb5in(a, b)
		(?, 1)    evalwcet2bb5in(a, b) -> evalwcet2bb2in(a, 0) [ 4 >= a ]
		(?, 1)    evalwcet2bb2in(a, b) -> evalwcet2bb1in(a, b) [ a >= 3 /\ 9 >= b ]
		(?, 1)    evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ 2 >= a ]
		(?, 1)    evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ b >= 10 ]
		(?, 1)    evalwcet2bb1in(a, b) -> evalwcet2bb2in(a, b + 1)
		(?, 1)    evalwcet2bb4in(a, b) -> evalwcet2bb5in(a + 1, b)
	start location:	evalwcet2start
	leaf cost:	2

Repeatedly propagating knowledge in problem 2 produces the following problem:
3:	T:
		(1, 1)    evalwcet2start(a, b) -> evalwcet2entryin(a, b)
		(1, 1)    evalwcet2entryin(a, b) -> evalwcet2bb5in(a, b)
		(?, 1)    evalwcet2bb5in(a, b) -> evalwcet2bb2in(a, 0) [ 4 >= a ]
		(?, 1)    evalwcet2bb2in(a, b) -> evalwcet2bb1in(a, b) [ a >= 3 /\ 9 >= b ]
		(?, 1)    evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ 2 >= a ]
		(?, 1)    evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ b >= 10 ]
		(?, 1)    evalwcet2bb1in(a, b) -> evalwcet2bb2in(a, b + 1)
		(?, 1)    evalwcet2bb4in(a, b) -> evalwcet2bb5in(a + 1, b)
	start location:	evalwcet2start
	leaf cost:	2

A polynomial rank function with
	Pol(evalwcet2start) = -3*V_1 + 8
	Pol(evalwcet2entryin) = -3*V_1 + 8
	Pol(evalwcet2bb5in) = -3*V_1 + 8
	Pol(evalwcet2bb2in) = -3*V_1 + 7
	Pol(evalwcet2bb1in) = -3*V_1 + 7
	Pol(evalwcet2bb4in) = -3*V_1 + 6
orients all transitions weakly and the transition
	evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ 2 >= a ]
strictly and produces the following problem:
4:	T:
		(1, 1)          evalwcet2start(a, b) -> evalwcet2entryin(a, b)
		(1, 1)          evalwcet2entryin(a, b) -> evalwcet2bb5in(a, b)
		(?, 1)          evalwcet2bb5in(a, b) -> evalwcet2bb2in(a, 0) [ 4 >= a ]
		(?, 1)          evalwcet2bb2in(a, b) -> evalwcet2bb1in(a, b) [ a >= 3 /\ 9 >= b ]
		(3*a + 8, 1)    evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ 2 >= a ]
		(?, 1)          evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ b >= 10 ]
		(?, 1)          evalwcet2bb1in(a, b) -> evalwcet2bb2in(a, b + 1)
		(?, 1)          evalwcet2bb4in(a, b) -> evalwcet2bb5in(a + 1, b)
	start location:	evalwcet2start
	leaf cost:	2

A polynomial rank function with
	Pol(evalwcet2start) = -3*V_1 + 13
	Pol(evalwcet2entryin) = -3*V_1 + 13
	Pol(evalwcet2bb5in) = -3*V_1 + 13
	Pol(evalwcet2bb2in) = -3*V_1 + 12
	Pol(evalwcet2bb1in) = -3*V_1 + 12
	Pol(evalwcet2bb4in) = -3*V_1 + 11
orients all transitions weakly and the transition
	evalwcet2bb5in(a, b) -> evalwcet2bb2in(a, 0) [ 4 >= a ]
strictly and produces the following problem:
5:	T:
		(1, 1)           evalwcet2start(a, b) -> evalwcet2entryin(a, b)
		(1, 1)           evalwcet2entryin(a, b) -> evalwcet2bb5in(a, b)
		(3*a + 13, 1)    evalwcet2bb5in(a, b) -> evalwcet2bb2in(a, 0) [ 4 >= a ]
		(?, 1)           evalwcet2bb2in(a, b) -> evalwcet2bb1in(a, b) [ a >= 3 /\ 9 >= b ]
		(3*a + 8, 1)     evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ 2 >= a ]
		(?, 1)           evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ b >= 10 ]
		(?, 1)           evalwcet2bb1in(a, b) -> evalwcet2bb2in(a, b + 1)
		(?, 1)           evalwcet2bb4in(a, b) -> evalwcet2bb5in(a + 1, b)
	start location:	evalwcet2start
	leaf cost:	2

A polynomial rank function with
	Pol(evalwcet2bb4in) = 1
	Pol(evalwcet2bb5in) = 0
	Pol(evalwcet2bb2in) = 2
	Pol(evalwcet2bb1in) = 2
and size complexities
	S("evalwcet2bb4in(a, b) -> evalwcet2bb5in(a + 1, b)", 0-0) = ?
	S("evalwcet2bb4in(a, b) -> evalwcet2bb5in(a + 1, b)", 0-1) = ?
	S("evalwcet2bb1in(a, b) -> evalwcet2bb2in(a, b + 1)", 0-0) = ?
	S("evalwcet2bb1in(a, b) -> evalwcet2bb2in(a, b + 1)", 0-1) = ?
	S("evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ b >= 10 ]", 0-0) = ?
	S("evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ b >= 10 ]", 0-1) = ?
	S("evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ 2 >= a ]", 0-0) = ?
	S("evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ 2 >= a ]", 0-1) = ?
	S("evalwcet2bb2in(a, b) -> evalwcet2bb1in(a, b) [ a >= 3 /\\ 9 >= b ]", 0-0) = ?
	S("evalwcet2bb2in(a, b) -> evalwcet2bb1in(a, b) [ a >= 3 /\\ 9 >= b ]", 0-1) = ?
	S("evalwcet2bb5in(a, b) -> evalwcet2bb2in(a, 0) [ 4 >= a ]", 0-0) = ?
	S("evalwcet2bb5in(a, b) -> evalwcet2bb2in(a, 0) [ 4 >= a ]", 0-1) = 0
	S("evalwcet2entryin(a, b) -> evalwcet2bb5in(a, b)", 0-0) = a
	S("evalwcet2entryin(a, b) -> evalwcet2bb5in(a, b)", 0-1) = b
	S("evalwcet2start(a, b) -> evalwcet2entryin(a, b)", 0-0) = a
	S("evalwcet2start(a, b) -> evalwcet2entryin(a, b)", 0-1) = b
orients the transitions
	evalwcet2bb4in(a, b) -> evalwcet2bb5in(a + 1, b)
	evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ b >= 10 ]
	evalwcet2bb2in(a, b) -> evalwcet2bb1in(a, b) [ a >= 3 /\ 9 >= b ]
	evalwcet2bb1in(a, b) -> evalwcet2bb2in(a, b + 1)
weakly and the transition
	evalwcet2bb4in(a, b) -> evalwcet2bb5in(a + 1, b)
strictly and produces the following problem:
6:	T:
		(1, 1)           evalwcet2start(a, b) -> evalwcet2entryin(a, b)
		(1, 1)           evalwcet2entryin(a, b) -> evalwcet2bb5in(a, b)
		(3*a + 13, 1)    evalwcet2bb5in(a, b) -> evalwcet2bb2in(a, 0) [ 4 >= a ]
		(?, 1)           evalwcet2bb2in(a, b) -> evalwcet2bb1in(a, b) [ a >= 3 /\ 9 >= b ]
		(3*a + 8, 1)     evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ 2 >= a ]
		(?, 1)           evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ b >= 10 ]
		(?, 1)           evalwcet2bb1in(a, b) -> evalwcet2bb2in(a, b + 1)
		(9*a + 34, 1)    evalwcet2bb4in(a, b) -> evalwcet2bb5in(a + 1, b)
	start location:	evalwcet2start
	leaf cost:	2

A polynomial rank function with
	Pol(evalwcet2bb2in) = 1
	Pol(evalwcet2bb4in) = 0
	Pol(evalwcet2bb1in) = 1
and size complexities
	S("evalwcet2bb4in(a, b) -> evalwcet2bb5in(a + 1, b)", 0-0) = 10*a + 3400
	S("evalwcet2bb4in(a, b) -> evalwcet2bb5in(a + 1, b)", 0-1) = ?
	S("evalwcet2bb1in(a, b) -> evalwcet2bb2in(a, b + 1)", 0-0) = 10*a + 3400
	S("evalwcet2bb1in(a, b) -> evalwcet2bb2in(a, b + 1)", 0-1) = ?
	S("evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ b >= 10 ]", 0-0) = 10*a + 3400
	S("evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ b >= 10 ]", 0-1) = ?
	S("evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ 2 >= a ]", 0-0) = 10*a + 3400
	S("evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ 2 >= a ]", 0-1) = ?
	S("evalwcet2bb2in(a, b) -> evalwcet2bb1in(a, b) [ a >= 3 /\\ 9 >= b ]", 0-0) = 10*a + 3400
	S("evalwcet2bb2in(a, b) -> evalwcet2bb1in(a, b) [ a >= 3 /\\ 9 >= b ]", 0-1) = ?
	S("evalwcet2bb5in(a, b) -> evalwcet2bb2in(a, 0) [ 4 >= a ]", 0-0) = 10*a + 3400
	S("evalwcet2bb5in(a, b) -> evalwcet2bb2in(a, 0) [ 4 >= a ]", 0-1) = 0
	S("evalwcet2entryin(a, b) -> evalwcet2bb5in(a, b)", 0-0) = a
	S("evalwcet2entryin(a, b) -> evalwcet2bb5in(a, b)", 0-1) = b
	S("evalwcet2start(a, b) -> evalwcet2entryin(a, b)", 0-0) = a
	S("evalwcet2start(a, b) -> evalwcet2entryin(a, b)", 0-1) = b
orients the transitions
	evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ b >= 10 ]
	evalwcet2bb2in(a, b) -> evalwcet2bb1in(a, b) [ a >= 3 /\ 9 >= b ]
	evalwcet2bb1in(a, b) -> evalwcet2bb2in(a, b + 1)
weakly and the transition
	evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ b >= 10 ]
strictly and produces the following problem:
7:	T:
		(1, 1)           evalwcet2start(a, b) -> evalwcet2entryin(a, b)
		(1, 1)           evalwcet2entryin(a, b) -> evalwcet2bb5in(a, b)
		(3*a + 13, 1)    evalwcet2bb5in(a, b) -> evalwcet2bb2in(a, 0) [ 4 >= a ]
		(?, 1)           evalwcet2bb2in(a, b) -> evalwcet2bb1in(a, b) [ a >= 3 /\ 9 >= b ]
		(3*a + 8, 1)     evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ 2 >= a ]
		(3*a + 13, 1)    evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ b >= 10 ]
		(?, 1)           evalwcet2bb1in(a, b) -> evalwcet2bb2in(a, b + 1)
		(9*a + 34, 1)    evalwcet2bb4in(a, b) -> evalwcet2bb5in(a + 1, b)
	start location:	evalwcet2start
	leaf cost:	2

A polynomial rank function with
	Pol(evalwcet2bb2in) = 6*V_1 - 2*V_2 + 1
	Pol(evalwcet2bb1in) = 6*V_1 - 2*V_2
and size complexities
	S("evalwcet2bb4in(a, b) -> evalwcet2bb5in(a + 1, b)", 0-0) = 10*a + 3400
	S("evalwcet2bb4in(a, b) -> evalwcet2bb5in(a + 1, b)", 0-1) = ?
	S("evalwcet2bb1in(a, b) -> evalwcet2bb2in(a, b + 1)", 0-0) = 10*a + 3400
	S("evalwcet2bb1in(a, b) -> evalwcet2bb2in(a, b + 1)", 0-1) = ?
	S("evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ b >= 10 ]", 0-0) = 10*a + 3400
	S("evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ b >= 10 ]", 0-1) = ?
	S("evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ 2 >= a ]", 0-0) = 10*a + 3400
	S("evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ 2 >= a ]", 0-1) = ?
	S("evalwcet2bb2in(a, b) -> evalwcet2bb1in(a, b) [ a >= 3 /\\ 9 >= b ]", 0-0) = 10*a + 3400
	S("evalwcet2bb2in(a, b) -> evalwcet2bb1in(a, b) [ a >= 3 /\\ 9 >= b ]", 0-1) = ?
	S("evalwcet2bb5in(a, b) -> evalwcet2bb2in(a, 0) [ 4 >= a ]", 0-0) = 10*a + 3400
	S("evalwcet2bb5in(a, b) -> evalwcet2bb2in(a, 0) [ 4 >= a ]", 0-1) = 0
	S("evalwcet2entryin(a, b) -> evalwcet2bb5in(a, b)", 0-0) = a
	S("evalwcet2entryin(a, b) -> evalwcet2bb5in(a, b)", 0-1) = b
	S("evalwcet2start(a, b) -> evalwcet2entryin(a, b)", 0-0) = a
	S("evalwcet2start(a, b) -> evalwcet2entryin(a, b)", 0-1) = b
orients the transitions
	evalwcet2bb2in(a, b) -> evalwcet2bb1in(a, b) [ a >= 3 /\ 9 >= b ]
	evalwcet2bb1in(a, b) -> evalwcet2bb2in(a, b + 1)
weakly and the transition
	evalwcet2bb2in(a, b) -> evalwcet2bb1in(a, b) [ a >= 3 /\ 9 >= b ]
strictly and produces the following problem:
8:	T:
		(1, 1)                             evalwcet2start(a, b) -> evalwcet2entryin(a, b)
		(1, 1)                             evalwcet2entryin(a, b) -> evalwcet2bb5in(a, b)
		(3*a + 13, 1)                      evalwcet2bb5in(a, b) -> evalwcet2bb2in(a, 0) [ 4 >= a ]
		(180*a^2 + 61983*a + 265213, 1)    evalwcet2bb2in(a, b) -> evalwcet2bb1in(a, b) [ a >= 3 /\ 9 >= b ]
		(3*a + 8, 1)                       evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ 2 >= a ]
		(3*a + 13, 1)                      evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ b >= 10 ]
		(?, 1)                             evalwcet2bb1in(a, b) -> evalwcet2bb2in(a, b + 1)
		(9*a + 34, 1)                      evalwcet2bb4in(a, b) -> evalwcet2bb5in(a + 1, b)
	start location:	evalwcet2start
	leaf cost:	2

Repeatedly propagating knowledge in problem 8 produces the following problem:
9:	T:
		(1, 1)                             evalwcet2start(a, b) -> evalwcet2entryin(a, b)
		(1, 1)                             evalwcet2entryin(a, b) -> evalwcet2bb5in(a, b)
		(3*a + 13, 1)                      evalwcet2bb5in(a, b) -> evalwcet2bb2in(a, 0) [ 4 >= a ]
		(180*a^2 + 61983*a + 265213, 1)    evalwcet2bb2in(a, b) -> evalwcet2bb1in(a, b) [ a >= 3 /\ 9 >= b ]
		(3*a + 8, 1)                       evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ 2 >= a ]
		(3*a + 13, 1)                      evalwcet2bb2in(a, b) -> evalwcet2bb4in(a, b) [ b >= 10 ]
		(180*a^2 + 61983*a + 265213, 1)    evalwcet2bb1in(a, b) -> evalwcet2bb2in(a, b + 1)
		(9*a + 34, 1)                      evalwcet2bb4in(a, b) -> evalwcet2bb5in(a + 1, b)
	start location:	evalwcet2start
	leaf cost:	2

Complexity upper bound 123984*a + 360*a^2 + 530498

Time: 0.198 sec (SMT: 0.185 sec)