YES(?, 20*d + 12*c + 17)

Initial complexity problem:
1:	T:
		(1, 1)    evalSimpleSingle2start(a, b, c, d) -> evalSimpleSingle2entryin(a, b, c, d)
		(?, 1)    evalSimpleSingle2entryin(a, b, c, d) -> evalSimpleSingle2bb4in(0, 0, c, d)
		(?, 1)    evalSimpleSingle2bb4in(a, b, c, d) -> evalSimpleSingle2bbin(a, b, c, d) [ 0 >= e + 1 ]
		(?, 1)    evalSimpleSingle2bb4in(a, b, c, d) -> evalSimpleSingle2bbin(a, b, c, d) [ e >= 1 ]
		(?, 1)    evalSimpleSingle2bb4in(a, b, c, d) -> evalSimpleSingle2returnin(a, b, c, d)
		(?, 1)    evalSimpleSingle2bbin(a, b, c, d) -> evalSimpleSingle2bb1in(a, b, c, d) [ c >= b + 1 ]
		(?, 1)    evalSimpleSingle2bbin(a, b, c, d) -> evalSimpleSingle2bb2in(a, b, c, d) [ b >= c ]
		(?, 1)    evalSimpleSingle2bb1in(a, b, c, d) -> evalSimpleSingle2bb4in(a + 1, b + 1, c, d)
		(?, 1)    evalSimpleSingle2bb2in(a, b, c, d) -> evalSimpleSingle2bb3in(a, b, c, d) [ d >= a + 1 ]
		(?, 1)    evalSimpleSingle2bb2in(a, b, c, d) -> evalSimpleSingle2returnin(a, b, c, d) [ a >= d ]
		(?, 1)    evalSimpleSingle2bb3in(a, b, c, d) -> evalSimpleSingle2bb4in(a + 1, b + 1, c, d)
		(?, 1)    evalSimpleSingle2returnin(a, b, c, d) -> evalSimpleSingle2stop(a, b, c, d)
	start location:	evalSimpleSingle2start
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(1, 1)    evalSimpleSingle2start(a, b, c, d) -> evalSimpleSingle2entryin(a, b, c, d)
		(?, 1)    evalSimpleSingle2entryin(a, b, c, d) -> evalSimpleSingle2bb4in(0, 0, c, d)
		(?, 1)    evalSimpleSingle2bb4in(a, b, c, d) -> evalSimpleSingle2bbin(a, b, c, d) [ 0 >= e + 1 ]
		(?, 1)    evalSimpleSingle2bb4in(a, b, c, d) -> evalSimpleSingle2bbin(a, b, c, d) [ e >= 1 ]
		(?, 1)    evalSimpleSingle2bbin(a, b, c, d) -> evalSimpleSingle2bb1in(a, b, c, d) [ c >= b + 1 ]
		(?, 1)    evalSimpleSingle2bbin(a, b, c, d) -> evalSimpleSingle2bb2in(a, b, c, d) [ b >= c ]
		(?, 1)    evalSimpleSingle2bb1in(a, b, c, d) -> evalSimpleSingle2bb4in(a + 1, b + 1, c, d)
		(?, 1)    evalSimpleSingle2bb2in(a, b, c, d) -> evalSimpleSingle2bb3in(a, b, c, d) [ d >= a + 1 ]
		(?, 1)    evalSimpleSingle2bb3in(a, b, c, d) -> evalSimpleSingle2bb4in(a + 1, b + 1, c, d)
	start location:	evalSimpleSingle2start
	leaf cost:	3

Repeatedly propagating knowledge in problem 2 produces the following problem:
3:	T:
		(1, 1)    evalSimpleSingle2start(a, b, c, d) -> evalSimpleSingle2entryin(a, b, c, d)
		(1, 1)    evalSimpleSingle2entryin(a, b, c, d) -> evalSimpleSingle2bb4in(0, 0, c, d)
		(?, 1)    evalSimpleSingle2bb4in(a, b, c, d) -> evalSimpleSingle2bbin(a, b, c, d) [ 0 >= e + 1 ]
		(?, 1)    evalSimpleSingle2bb4in(a, b, c, d) -> evalSimpleSingle2bbin(a, b, c, d) [ e >= 1 ]
		(?, 1)    evalSimpleSingle2bbin(a, b, c, d) -> evalSimpleSingle2bb1in(a, b, c, d) [ c >= b + 1 ]
		(?, 1)    evalSimpleSingle2bbin(a, b, c, d) -> evalSimpleSingle2bb2in(a, b, c, d) [ b >= c ]
		(?, 1)    evalSimpleSingle2bb1in(a, b, c, d) -> evalSimpleSingle2bb4in(a + 1, b + 1, c, d)
		(?, 1)    evalSimpleSingle2bb2in(a, b, c, d) -> evalSimpleSingle2bb3in(a, b, c, d) [ d >= a + 1 ]
		(?, 1)    evalSimpleSingle2bb3in(a, b, c, d) -> evalSimpleSingle2bb4in(a + 1, b + 1, c, d)
	start location:	evalSimpleSingle2start
	leaf cost:	3

A polynomial rank function with
	Pol(evalSimpleSingle2start) = 4*V_4 - 1
	Pol(evalSimpleSingle2entryin) = 4*V_4 - 1
	Pol(evalSimpleSingle2bb4in) = -4*V_1 + 4*V_4 - 1
	Pol(evalSimpleSingle2bbin) = -4*V_1 + 4*V_4 - 2
	Pol(evalSimpleSingle2bb1in) = -4*V_1 + 4*V_4 - 4
	Pol(evalSimpleSingle2bb2in) = -4*V_1 + 4*V_4 - 3
	Pol(evalSimpleSingle2bb3in) = -4*V_1 + 4*V_4 - 4
orients all transitions weakly and the transition
	evalSimpleSingle2bb2in(a, b, c, d) -> evalSimpleSingle2bb3in(a, b, c, d) [ d >= a + 1 ]
strictly and produces the following problem:
4:	T:
		(1, 1)          evalSimpleSingle2start(a, b, c, d) -> evalSimpleSingle2entryin(a, b, c, d)
		(1, 1)          evalSimpleSingle2entryin(a, b, c, d) -> evalSimpleSingle2bb4in(0, 0, c, d)
		(?, 1)          evalSimpleSingle2bb4in(a, b, c, d) -> evalSimpleSingle2bbin(a, b, c, d) [ 0 >= e + 1 ]
		(?, 1)          evalSimpleSingle2bb4in(a, b, c, d) -> evalSimpleSingle2bbin(a, b, c, d) [ e >= 1 ]
		(?, 1)          evalSimpleSingle2bbin(a, b, c, d) -> evalSimpleSingle2bb1in(a, b, c, d) [ c >= b + 1 ]
		(?, 1)          evalSimpleSingle2bbin(a, b, c, d) -> evalSimpleSingle2bb2in(a, b, c, d) [ b >= c ]
		(?, 1)          evalSimpleSingle2bb1in(a, b, c, d) -> evalSimpleSingle2bb4in(a + 1, b + 1, c, d)
		(4*d + 1, 1)    evalSimpleSingle2bb2in(a, b, c, d) -> evalSimpleSingle2bb3in(a, b, c, d) [ d >= a + 1 ]
		(?, 1)          evalSimpleSingle2bb3in(a, b, c, d) -> evalSimpleSingle2bb4in(a + 1, b + 1, c, d)
	start location:	evalSimpleSingle2start
	leaf cost:	3

Repeatedly propagating knowledge in problem 4 produces the following problem:
5:	T:
		(1, 1)          evalSimpleSingle2start(a, b, c, d) -> evalSimpleSingle2entryin(a, b, c, d)
		(1, 1)          evalSimpleSingle2entryin(a, b, c, d) -> evalSimpleSingle2bb4in(0, 0, c, d)
		(?, 1)          evalSimpleSingle2bb4in(a, b, c, d) -> evalSimpleSingle2bbin(a, b, c, d) [ 0 >= e + 1 ]
		(?, 1)          evalSimpleSingle2bb4in(a, b, c, d) -> evalSimpleSingle2bbin(a, b, c, d) [ e >= 1 ]
		(?, 1)          evalSimpleSingle2bbin(a, b, c, d) -> evalSimpleSingle2bb1in(a, b, c, d) [ c >= b + 1 ]
		(?, 1)          evalSimpleSingle2bbin(a, b, c, d) -> evalSimpleSingle2bb2in(a, b, c, d) [ b >= c ]
		(?, 1)          evalSimpleSingle2bb1in(a, b, c, d) -> evalSimpleSingle2bb4in(a + 1, b + 1, c, d)
		(4*d + 1, 1)    evalSimpleSingle2bb2in(a, b, c, d) -> evalSimpleSingle2bb3in(a, b, c, d) [ d >= a + 1 ]
		(4*d + 1, 1)    evalSimpleSingle2bb3in(a, b, c, d) -> evalSimpleSingle2bb4in(a + 1, b + 1, c, d)
	start location:	evalSimpleSingle2start
	leaf cost:	3

A polynomial rank function with
	Pol(evalSimpleSingle2bbin) = 1
	Pol(evalSimpleSingle2bb2in) = 0
	Pol(evalSimpleSingle2bb1in) = 1
	Pol(evalSimpleSingle2bb4in) = 1
and size complexities
	S("evalSimpleSingle2bb3in(a, b, c, d) -> evalSimpleSingle2bb4in(a + 1, b + 1, c, d)", 0-0) = ?
	S("evalSimpleSingle2bb3in(a, b, c, d) -> evalSimpleSingle2bb4in(a + 1, b + 1, c, d)", 0-1) = ?
	S("evalSimpleSingle2bb3in(a, b, c, d) -> evalSimpleSingle2bb4in(a + 1, b + 1, c, d)", 0-2) = c
	S("evalSimpleSingle2bb3in(a, b, c, d) -> evalSimpleSingle2bb4in(a + 1, b + 1, c, d)", 0-3) = d
	S("evalSimpleSingle2bb2in(a, b, c, d) -> evalSimpleSingle2bb3in(a, b, c, d) [ d >= a + 1 ]", 0-0) = ?
	S("evalSimpleSingle2bb2in(a, b, c, d) -> evalSimpleSingle2bb3in(a, b, c, d) [ d >= a + 1 ]", 0-1) = ?
	S("evalSimpleSingle2bb2in(a, b, c, d) -> evalSimpleSingle2bb3in(a, b, c, d) [ d >= a + 1 ]", 0-2) = c
	S("evalSimpleSingle2bb2in(a, b, c, d) -> evalSimpleSingle2bb3in(a, b, c, d) [ d >= a + 1 ]", 0-3) = d
	S("evalSimpleSingle2bb1in(a, b, c, d) -> evalSimpleSingle2bb4in(a + 1, b + 1, c, d)", 0-0) = ?
	S("evalSimpleSingle2bb1in(a, b, c, d) -> evalSimpleSingle2bb4in(a + 1, b + 1, c, d)", 0-1) = ?
	S("evalSimpleSingle2bb1in(a, b, c, d) -> evalSimpleSingle2bb4in(a + 1, b + 1, c, d)", 0-2) = c
	S("evalSimpleSingle2bb1in(a, b, c, d) -> evalSimpleSingle2bb4in(a + 1, b + 1, c, d)", 0-3) = d
	S("evalSimpleSingle2bbin(a, b, c, d) -> evalSimpleSingle2bb2in(a, b, c, d) [ b >= c ]", 0-0) = ?
	S("evalSimpleSingle2bbin(a, b, c, d) -> evalSimpleSingle2bb2in(a, b, c, d) [ b >= c ]", 0-1) = ?
	S("evalSimpleSingle2bbin(a, b, c, d) -> evalSimpleSingle2bb2in(a, b, c, d) [ b >= c ]", 0-2) = c
	S("evalSimpleSingle2bbin(a, b, c, d) -> evalSimpleSingle2bb2in(a, b, c, d) [ b >= c ]", 0-3) = d
	S("evalSimpleSingle2bbin(a, b, c, d) -> evalSimpleSingle2bb1in(a, b, c, d) [ c >= b + 1 ]", 0-0) = ?
	S("evalSimpleSingle2bbin(a, b, c, d) -> evalSimpleSingle2bb1in(a, b, c, d) [ c >= b + 1 ]", 0-1) = ?
	S("evalSimpleSingle2bbin(a, b, c, d) -> evalSimpleSingle2bb1in(a, b, c, d) [ c >= b + 1 ]", 0-2) = c
	S("evalSimpleSingle2bbin(a, b, c, d) -> evalSimpleSingle2bb1in(a, b, c, d) [ c >= b + 1 ]", 0-3) = d
	S("evalSimpleSingle2bb4in(a, b, c, d) -> evalSimpleSingle2bbin(a, b, c, d) [ e >= 1 ]", 0-0) = ?
	S("evalSimpleSingle2bb4in(a, b, c, d) -> evalSimpleSingle2bbin(a, b, c, d) [ e >= 1 ]", 0-1) = ?
	S("evalSimpleSingle2bb4in(a, b, c, d) -> evalSimpleSingle2bbin(a, b, c, d) [ e >= 1 ]", 0-2) = c
	S("evalSimpleSingle2bb4in(a, b, c, d) -> evalSimpleSingle2bbin(a, b, c, d) [ e >= 1 ]", 0-3) = d
	S("evalSimpleSingle2bb4in(a, b, c, d) -> evalSimpleSingle2bbin(a, b, c, d) [ 0 >= e + 1 ]", 0-0) = ?
	S("evalSimpleSingle2bb4in(a, b, c, d) -> evalSimpleSingle2bbin(a, b, c, d) [ 0 >= e + 1 ]", 0-1) = ?
	S("evalSimpleSingle2bb4in(a, b, c, d) -> evalSimpleSingle2bbin(a, b, c, d) [ 0 >= e + 1 ]", 0-2) = c
	S("evalSimpleSingle2bb4in(a, b, c, d) -> evalSimpleSingle2bbin(a, b, c, d) [ 0 >= e + 1 ]", 0-3) = d
	S("evalSimpleSingle2entryin(a, b, c, d) -> evalSimpleSingle2bb4in(0, 0, c, d)", 0-0) = 0
	S("evalSimpleSingle2entryin(a, b, c, d) -> evalSimpleSingle2bb4in(0, 0, c, d)", 0-1) = 0
	S("evalSimpleSingle2entryin(a, b, c, d) -> evalSimpleSingle2bb4in(0, 0, c, d)", 0-2) = c
	S("evalSimpleSingle2entryin(a, b, c, d) -> evalSimpleSingle2bb4in(0, 0, c, d)", 0-3) = d
	S("evalSimpleSingle2start(a, b, c, d) -> evalSimpleSingle2entryin(a, b, c, d)", 0-0) = a
	S("evalSimpleSingle2start(a, b, c, d) -> evalSimpleSingle2entryin(a, b, c, d)", 0-1) = b
	S("evalSimpleSingle2start(a, b, c, d) -> evalSimpleSingle2entryin(a, b, c, d)", 0-2) = c
	S("evalSimpleSingle2start(a, b, c, d) -> evalSimpleSingle2entryin(a, b, c, d)", 0-3) = d
orients the transitions
	evalSimpleSingle2bbin(a, b, c, d) -> evalSimpleSingle2bb2in(a, b, c, d) [ b >= c ]
	evalSimpleSingle2bbin(a, b, c, d) -> evalSimpleSingle2bb1in(a, b, c, d) [ c >= b + 1 ]
	evalSimpleSingle2bb4in(a, b, c, d) -> evalSimpleSingle2bbin(a, b, c, d) [ e >= 1 ]
	evalSimpleSingle2bb4in(a, b, c, d) -> evalSimpleSingle2bbin(a, b, c, d) [ 0 >= e + 1 ]
	evalSimpleSingle2bb1in(a, b, c, d) -> evalSimpleSingle2bb4in(a + 1, b + 1, c, d)
weakly and the transition
	evalSimpleSingle2bbin(a, b, c, d) -> evalSimpleSingle2bb2in(a, b, c, d) [ b >= c ]
strictly and produces the following problem:
6:	T:
		(1, 1)          evalSimpleSingle2start(a, b, c, d) -> evalSimpleSingle2entryin(a, b, c, d)
		(1, 1)          evalSimpleSingle2entryin(a, b, c, d) -> evalSimpleSingle2bb4in(0, 0, c, d)
		(?, 1)          evalSimpleSingle2bb4in(a, b, c, d) -> evalSimpleSingle2bbin(a, b, c, d) [ 0 >= e + 1 ]
		(?, 1)          evalSimpleSingle2bb4in(a, b, c, d) -> evalSimpleSingle2bbin(a, b, c, d) [ e >= 1 ]
		(?, 1)          evalSimpleSingle2bbin(a, b, c, d) -> evalSimpleSingle2bb1in(a, b, c, d) [ c >= b + 1 ]
		(4*d + 2, 1)    evalSimpleSingle2bbin(a, b, c, d) -> evalSimpleSingle2bb2in(a, b, c, d) [ b >= c ]
		(?, 1)          evalSimpleSingle2bb1in(a, b, c, d) -> evalSimpleSingle2bb4in(a + 1, b + 1, c, d)
		(4*d + 1, 1)    evalSimpleSingle2bb2in(a, b, c, d) -> evalSimpleSingle2bb3in(a, b, c, d) [ d >= a + 1 ]
		(4*d + 1, 1)    evalSimpleSingle2bb3in(a, b, c, d) -> evalSimpleSingle2bb4in(a + 1, b + 1, c, d)
	start location:	evalSimpleSingle2start
	leaf cost:	3

A polynomial rank function with
	Pol(evalSimpleSingle2start) = 3*V_3 - 1
	Pol(evalSimpleSingle2entryin) = 3*V_3 - 1
	Pol(evalSimpleSingle2bb4in) = -3*V_2 + 3*V_3 - 1
	Pol(evalSimpleSingle2bbin) = -3*V_2 + 3*V_3 - 2
	Pol(evalSimpleSingle2bb1in) = -3*V_2 + 3*V_3 - 3
	Pol(evalSimpleSingle2bb2in) = -3*V_2 + 3*V_3 - 4
	Pol(evalSimpleSingle2bb3in) = -3*V_2 + 3*V_3 - 4
orients all transitions weakly and the transition
	evalSimpleSingle2bbin(a, b, c, d) -> evalSimpleSingle2bb1in(a, b, c, d) [ c >= b + 1 ]
strictly and produces the following problem:
7:	T:
		(1, 1)          evalSimpleSingle2start(a, b, c, d) -> evalSimpleSingle2entryin(a, b, c, d)
		(1, 1)          evalSimpleSingle2entryin(a, b, c, d) -> evalSimpleSingle2bb4in(0, 0, c, d)
		(?, 1)          evalSimpleSingle2bb4in(a, b, c, d) -> evalSimpleSingle2bbin(a, b, c, d) [ 0 >= e + 1 ]
		(?, 1)          evalSimpleSingle2bb4in(a, b, c, d) -> evalSimpleSingle2bbin(a, b, c, d) [ e >= 1 ]
		(3*c + 1, 1)    evalSimpleSingle2bbin(a, b, c, d) -> evalSimpleSingle2bb1in(a, b, c, d) [ c >= b + 1 ]
		(4*d + 2, 1)    evalSimpleSingle2bbin(a, b, c, d) -> evalSimpleSingle2bb2in(a, b, c, d) [ b >= c ]
		(?, 1)          evalSimpleSingle2bb1in(a, b, c, d) -> evalSimpleSingle2bb4in(a + 1, b + 1, c, d)
		(4*d + 1, 1)    evalSimpleSingle2bb2in(a, b, c, d) -> evalSimpleSingle2bb3in(a, b, c, d) [ d >= a + 1 ]
		(4*d + 1, 1)    evalSimpleSingle2bb3in(a, b, c, d) -> evalSimpleSingle2bb4in(a + 1, b + 1, c, d)
	start location:	evalSimpleSingle2start
	leaf cost:	3

Repeatedly propagating knowledge in problem 7 produces the following problem:
8:	T:
		(1, 1)                evalSimpleSingle2start(a, b, c, d) -> evalSimpleSingle2entryin(a, b, c, d)
		(1, 1)                evalSimpleSingle2entryin(a, b, c, d) -> evalSimpleSingle2bb4in(0, 0, c, d)
		(4*d + 3*c + 3, 1)    evalSimpleSingle2bb4in(a, b, c, d) -> evalSimpleSingle2bbin(a, b, c, d) [ 0 >= e + 1 ]
		(4*d + 3*c + 3, 1)    evalSimpleSingle2bb4in(a, b, c, d) -> evalSimpleSingle2bbin(a, b, c, d) [ e >= 1 ]
		(3*c + 1, 1)          evalSimpleSingle2bbin(a, b, c, d) -> evalSimpleSingle2bb1in(a, b, c, d) [ c >= b + 1 ]
		(4*d + 2, 1)          evalSimpleSingle2bbin(a, b, c, d) -> evalSimpleSingle2bb2in(a, b, c, d) [ b >= c ]
		(3*c + 1, 1)          evalSimpleSingle2bb1in(a, b, c, d) -> evalSimpleSingle2bb4in(a + 1, b + 1, c, d)
		(4*d + 1, 1)          evalSimpleSingle2bb2in(a, b, c, d) -> evalSimpleSingle2bb3in(a, b, c, d) [ d >= a + 1 ]
		(4*d + 1, 1)          evalSimpleSingle2bb3in(a, b, c, d) -> evalSimpleSingle2bb4in(a + 1, b + 1, c, d)
	start location:	evalSimpleSingle2start
	leaf cost:	3

Complexity upper bound 20*d + 12*c + 17

Time: 0.280 sec (SMT: 0.264 sec)