YES(?, 6*a + 6*b + 6*c + 6*d + 5)

Initial complexity problem:
1:	T:
		(1, 1)    evalDis1start(a, b, c, d) -> evalDis1entryin(a, b, c, d)
		(?, 1)    evalDis1entryin(a, b, c, d) -> evalDis1bb3in(b, a, d, c)
		(?, 1)    evalDis1bb3in(a, b, c, d) -> evalDis1bbin(a, b, c, d) [ a >= b + 1 ]
		(?, 1)    evalDis1bb3in(a, b, c, d) -> evalDis1returnin(a, b, c, d) [ b >= a ]
		(?, 1)    evalDis1bbin(a, b, c, d) -> evalDis1bb1in(a, b, c, d) [ c >= d + 1 ]
		(?, 1)    evalDis1bbin(a, b, c, d) -> evalDis1bb2in(a, b, c, d) [ d >= c ]
		(?, 1)    evalDis1bb1in(a, b, c, d) -> evalDis1bb3in(a, b, c, d + 1)
		(?, 1)    evalDis1bb2in(a, b, c, d) -> evalDis1bb3in(a, b + 1, c, d)
		(?, 1)    evalDis1returnin(a, b, c, d) -> evalDis1stop(a, b, c, d)
	start location:	evalDis1start
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(1, 1)    evalDis1start(a, b, c, d) -> evalDis1entryin(a, b, c, d)
		(?, 1)    evalDis1entryin(a, b, c, d) -> evalDis1bb3in(b, a, d, c)
		(?, 1)    evalDis1bb3in(a, b, c, d) -> evalDis1bbin(a, b, c, d) [ a >= b + 1 ]
		(?, 1)    evalDis1bbin(a, b, c, d) -> evalDis1bb1in(a, b, c, d) [ c >= d + 1 ]
		(?, 1)    evalDis1bbin(a, b, c, d) -> evalDis1bb2in(a, b, c, d) [ d >= c ]
		(?, 1)    evalDis1bb1in(a, b, c, d) -> evalDis1bb3in(a, b, c, d + 1)
		(?, 1)    evalDis1bb2in(a, b, c, d) -> evalDis1bb3in(a, b + 1, c, d)
	start location:	evalDis1start
	leaf cost:	2

Repeatedly propagating knowledge in problem 2 produces the following problem:
3:	T:
		(1, 1)    evalDis1start(a, b, c, d) -> evalDis1entryin(a, b, c, d)
		(1, 1)    evalDis1entryin(a, b, c, d) -> evalDis1bb3in(b, a, d, c)
		(?, 1)    evalDis1bb3in(a, b, c, d) -> evalDis1bbin(a, b, c, d) [ a >= b + 1 ]
		(?, 1)    evalDis1bbin(a, b, c, d) -> evalDis1bb1in(a, b, c, d) [ c >= d + 1 ]
		(?, 1)    evalDis1bbin(a, b, c, d) -> evalDis1bb2in(a, b, c, d) [ d >= c ]
		(?, 1)    evalDis1bb1in(a, b, c, d) -> evalDis1bb3in(a, b, c, d + 1)
		(?, 1)    evalDis1bb2in(a, b, c, d) -> evalDis1bb3in(a, b + 1, c, d)
	start location:	evalDis1start
	leaf cost:	2

A polynomial rank function with
	Pol(evalDis1start) = -2*V_3 + 2*V_4
	Pol(evalDis1entryin) = -2*V_3 + 2*V_4
	Pol(evalDis1bb3in) = 2*V_3 - 2*V_4
	Pol(evalDis1bbin) = 2*V_3 - 2*V_4
	Pol(evalDis1bb1in) = 2*V_3 - 2*V_4 - 1
	Pol(evalDis1bb2in) = 2*V_3 - 2*V_4
orients all transitions weakly and the transition
	evalDis1bbin(a, b, c, d) -> evalDis1bb1in(a, b, c, d) [ c >= d + 1 ]
strictly and produces the following problem:
4:	T:
		(1, 1)            evalDis1start(a, b, c, d) -> evalDis1entryin(a, b, c, d)
		(1, 1)            evalDis1entryin(a, b, c, d) -> evalDis1bb3in(b, a, d, c)
		(?, 1)            evalDis1bb3in(a, b, c, d) -> evalDis1bbin(a, b, c, d) [ a >= b + 1 ]
		(2*c + 2*d, 1)    evalDis1bbin(a, b, c, d) -> evalDis1bb1in(a, b, c, d) [ c >= d + 1 ]
		(?, 1)            evalDis1bbin(a, b, c, d) -> evalDis1bb2in(a, b, c, d) [ d >= c ]
		(?, 1)            evalDis1bb1in(a, b, c, d) -> evalDis1bb3in(a, b, c, d + 1)
		(?, 1)            evalDis1bb2in(a, b, c, d) -> evalDis1bb3in(a, b + 1, c, d)
	start location:	evalDis1start
	leaf cost:	2

Repeatedly propagating knowledge in problem 4 produces the following problem:
5:	T:
		(1, 1)            evalDis1start(a, b, c, d) -> evalDis1entryin(a, b, c, d)
		(1, 1)            evalDis1entryin(a, b, c, d) -> evalDis1bb3in(b, a, d, c)
		(?, 1)            evalDis1bb3in(a, b, c, d) -> evalDis1bbin(a, b, c, d) [ a >= b + 1 ]
		(2*c + 2*d, 1)    evalDis1bbin(a, b, c, d) -> evalDis1bb1in(a, b, c, d) [ c >= d + 1 ]
		(?, 1)            evalDis1bbin(a, b, c, d) -> evalDis1bb2in(a, b, c, d) [ d >= c ]
		(2*c + 2*d, 1)    evalDis1bb1in(a, b, c, d) -> evalDis1bb3in(a, b, c, d + 1)
		(?, 1)            evalDis1bb2in(a, b, c, d) -> evalDis1bb3in(a, b + 1, c, d)
	start location:	evalDis1start
	leaf cost:	2

Applied AI with 'oct' on problem 5 to obtain the following invariants:
  For symbol evalDis1bb1in: X_3 - X_4 - 1 >= 0 /\ X_1 - X_2 - 1 >= 0
  For symbol evalDis1bb2in: -X_3 + X_4 >= 0 /\ X_1 - X_2 - 1 >= 0
  For symbol evalDis1bbin: X_1 - X_2 - 1 >= 0


This yielded the following problem:
6:	T:
		(?, 1)            evalDis1bb2in(a, b, c, d) -> evalDis1bb3in(a, b + 1, c, d) [ -c + d >= 0 /\ a - b - 1 >= 0 ]
		(2*c + 2*d, 1)    evalDis1bb1in(a, b, c, d) -> evalDis1bb3in(a, b, c, d + 1) [ c - d - 1 >= 0 /\ a - b - 1 >= 0 ]
		(?, 1)            evalDis1bbin(a, b, c, d) -> evalDis1bb2in(a, b, c, d) [ a - b - 1 >= 0 /\ d >= c ]
		(2*c + 2*d, 1)    evalDis1bbin(a, b, c, d) -> evalDis1bb1in(a, b, c, d) [ a - b - 1 >= 0 /\ c >= d + 1 ]
		(?, 1)            evalDis1bb3in(a, b, c, d) -> evalDis1bbin(a, b, c, d) [ a >= b + 1 ]
		(1, 1)            evalDis1entryin(a, b, c, d) -> evalDis1bb3in(b, a, d, c)
		(1, 1)            evalDis1start(a, b, c, d) -> evalDis1entryin(a, b, c, d)
	start location:	evalDis1start
	leaf cost:	2

A polynomial rank function with
	Pol(evalDis1bb2in) = 2*V_1 - 2*V_2 - 1
	Pol(evalDis1bb3in) = 2*V_1 - 2*V_2
	Pol(evalDis1bb1in) = 2*V_1 - 2*V_2
	Pol(evalDis1bbin) = 2*V_1 - 2*V_2
	Pol(evalDis1entryin) = -2*V_1 + 2*V_2
	Pol(evalDis1start) = -2*V_1 + 2*V_2
orients all transitions weakly and the transitions
	evalDis1bbin(a, b, c, d) -> evalDis1bb2in(a, b, c, d) [ a - b - 1 >= 0 /\ d >= c ]
	evalDis1bb2in(a, b, c, d) -> evalDis1bb3in(a, b + 1, c, d) [ -c + d >= 0 /\ a - b - 1 >= 0 ]
strictly and produces the following problem:
7:	T:
		(2*a + 2*b, 1)    evalDis1bb2in(a, b, c, d) -> evalDis1bb3in(a, b + 1, c, d) [ -c + d >= 0 /\ a - b - 1 >= 0 ]
		(2*c + 2*d, 1)    evalDis1bb1in(a, b, c, d) -> evalDis1bb3in(a, b, c, d + 1) [ c - d - 1 >= 0 /\ a - b - 1 >= 0 ]
		(2*a + 2*b, 1)    evalDis1bbin(a, b, c, d) -> evalDis1bb2in(a, b, c, d) [ a - b - 1 >= 0 /\ d >= c ]
		(2*c + 2*d, 1)    evalDis1bbin(a, b, c, d) -> evalDis1bb1in(a, b, c, d) [ a - b - 1 >= 0 /\ c >= d + 1 ]
		(?, 1)            evalDis1bb3in(a, b, c, d) -> evalDis1bbin(a, b, c, d) [ a >= b + 1 ]
		(1, 1)            evalDis1entryin(a, b, c, d) -> evalDis1bb3in(b, a, d, c)
		(1, 1)            evalDis1start(a, b, c, d) -> evalDis1entryin(a, b, c, d)
	start location:	evalDis1start
	leaf cost:	2

Repeatedly propagating knowledge in problem 7 produces the following problem:
8:	T:
		(2*a + 2*b, 1)                    evalDis1bb2in(a, b, c, d) -> evalDis1bb3in(a, b + 1, c, d) [ -c + d >= 0 /\ a - b - 1 >= 0 ]
		(2*c + 2*d, 1)                    evalDis1bb1in(a, b, c, d) -> evalDis1bb3in(a, b, c, d + 1) [ c - d - 1 >= 0 /\ a - b - 1 >= 0 ]
		(2*a + 2*b, 1)                    evalDis1bbin(a, b, c, d) -> evalDis1bb2in(a, b, c, d) [ a - b - 1 >= 0 /\ d >= c ]
		(2*c + 2*d, 1)                    evalDis1bbin(a, b, c, d) -> evalDis1bb1in(a, b, c, d) [ a - b - 1 >= 0 /\ c >= d + 1 ]
		(2*c + 2*d + 2*a + 2*b + 1, 1)    evalDis1bb3in(a, b, c, d) -> evalDis1bbin(a, b, c, d) [ a >= b + 1 ]
		(1, 1)                            evalDis1entryin(a, b, c, d) -> evalDis1bb3in(b, a, d, c)
		(1, 1)                            evalDis1start(a, b, c, d) -> evalDis1entryin(a, b, c, d)
	start location:	evalDis1start
	leaf cost:	2

Complexity upper bound 6*a + 6*b + 6*c + 6*d + 5

Time: 0.414 sec (SMT: 0.390 sec)