YES(?, 12*c + 18*d + 18*c*d + 14)

Initial complexity problem:
1:	T:
		(1, 1)    evalSimpleMultipleDepstart(a, b, c, d) -> evalSimpleMultipleDepentryin(a, b, c, d)
		(?, 1)    evalSimpleMultipleDepentryin(a, b, c, d) -> evalSimpleMultipleDepbb3in(0, 0, c, d)
		(?, 1)    evalSimpleMultipleDepbb3in(a, b, c, d) -> evalSimpleMultipleDepbbin(a, b, c, d) [ c >= b + 1 ]
		(?, 1)    evalSimpleMultipleDepbb3in(a, b, c, d) -> evalSimpleMultipleDepreturnin(a, b, c, d) [ b >= c ]
		(?, 1)    evalSimpleMultipleDepbbin(a, b, c, d) -> evalSimpleMultipleDepbb1in(a, b, c, d) [ d >= a + 1 ]
		(?, 1)    evalSimpleMultipleDepbbin(a, b, c, d) -> evalSimpleMultipleDepbb2in(a, b, c, d) [ a >= d ]
		(?, 1)    evalSimpleMultipleDepbb1in(a, b, c, d) -> evalSimpleMultipleDepbb3in(a + 1, b, c, d)
		(?, 1)    evalSimpleMultipleDepbb2in(a, b, c, d) -> evalSimpleMultipleDepbb3in(0, b + 1, c, d)
		(?, 1)    evalSimpleMultipleDepreturnin(a, b, c, d) -> evalSimpleMultipleDepstop(a, b, c, d)
	start location:	evalSimpleMultipleDepstart
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(1, 1)    evalSimpleMultipleDepstart(a, b, c, d) -> evalSimpleMultipleDepentryin(a, b, c, d)
		(?, 1)    evalSimpleMultipleDepentryin(a, b, c, d) -> evalSimpleMultipleDepbb3in(0, 0, c, d)
		(?, 1)    evalSimpleMultipleDepbb3in(a, b, c, d) -> evalSimpleMultipleDepbbin(a, b, c, d) [ c >= b + 1 ]
		(?, 1)    evalSimpleMultipleDepbbin(a, b, c, d) -> evalSimpleMultipleDepbb1in(a, b, c, d) [ d >= a + 1 ]
		(?, 1)    evalSimpleMultipleDepbbin(a, b, c, d) -> evalSimpleMultipleDepbb2in(a, b, c, d) [ a >= d ]
		(?, 1)    evalSimpleMultipleDepbb1in(a, b, c, d) -> evalSimpleMultipleDepbb3in(a + 1, b, c, d)
		(?, 1)    evalSimpleMultipleDepbb2in(a, b, c, d) -> evalSimpleMultipleDepbb3in(0, b + 1, c, d)
	start location:	evalSimpleMultipleDepstart
	leaf cost:	2

Repeatedly propagating knowledge in problem 2 produces the following problem:
3:	T:
		(1, 1)    evalSimpleMultipleDepstart(a, b, c, d) -> evalSimpleMultipleDepentryin(a, b, c, d)
		(1, 1)    evalSimpleMultipleDepentryin(a, b, c, d) -> evalSimpleMultipleDepbb3in(0, 0, c, d)
		(?, 1)    evalSimpleMultipleDepbb3in(a, b, c, d) -> evalSimpleMultipleDepbbin(a, b, c, d) [ c >= b + 1 ]
		(?, 1)    evalSimpleMultipleDepbbin(a, b, c, d) -> evalSimpleMultipleDepbb1in(a, b, c, d) [ d >= a + 1 ]
		(?, 1)    evalSimpleMultipleDepbbin(a, b, c, d) -> evalSimpleMultipleDepbb2in(a, b, c, d) [ a >= d ]
		(?, 1)    evalSimpleMultipleDepbb1in(a, b, c, d) -> evalSimpleMultipleDepbb3in(a + 1, b, c, d)
		(?, 1)    evalSimpleMultipleDepbb2in(a, b, c, d) -> evalSimpleMultipleDepbb3in(0, b + 1, c, d)
	start location:	evalSimpleMultipleDepstart
	leaf cost:	2

Applied AI with 'oct' on problem 3 to obtain the following invariants:
  For symbol evalSimpleMultipleDepbb1in: X_4 - 1 >= 0 /\ X_3 + X_4 - 2 >= 0 /\ X_2 + X_4 - 1 >= 0 /\ X_1 + X_4 - 1 >= 0 /\ -X_1 + X_4 - 1 >= 0 /\ X_3 - 1 >= 0 /\ X_2 + X_3 - 1 >= 0 /\ -X_2 + X_3 - 1 >= 0 /\ X_1 + X_3 - 1 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 >= 0 /\ X_1 >= 0
  For symbol evalSimpleMultipleDepbb2in: X_1 - X_4 >= 0 /\ X_3 - 1 >= 0 /\ X_2 + X_3 - 1 >= 0 /\ -X_2 + X_3 - 1 >= 0 /\ X_1 + X_3 - 1 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 >= 0 /\ X_1 >= 0
  For symbol evalSimpleMultipleDepbb3in: X_2 >= 0 /\ X_1 + X_2 >= 0 /\ X_1 >= 0
  For symbol evalSimpleMultipleDepbbin: X_3 - 1 >= 0 /\ X_2 + X_3 - 1 >= 0 /\ -X_2 + X_3 - 1 >= 0 /\ X_1 + X_3 - 1 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 >= 0 /\ X_1 >= 0


This yielded the following problem:
4:	T:
		(?, 1)    evalSimpleMultipleDepbb2in(a, b, c, d) -> evalSimpleMultipleDepbb3in(0, b + 1, c, d) [ a - d >= 0 /\ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 ]
		(?, 1)    evalSimpleMultipleDepbb1in(a, b, c, d) -> evalSimpleMultipleDepbb3in(a + 1, b, c, d) [ d - 1 >= 0 /\ c + d - 2 >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ -a + d - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 ]
		(?, 1)    evalSimpleMultipleDepbbin(a, b, c, d) -> evalSimpleMultipleDepbb2in(a, b, c, d) [ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= d ]
		(?, 1)    evalSimpleMultipleDepbbin(a, b, c, d) -> evalSimpleMultipleDepbb1in(a, b, c, d) [ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ d >= a + 1 ]
		(?, 1)    evalSimpleMultipleDepbb3in(a, b, c, d) -> evalSimpleMultipleDepbbin(a, b, c, d) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= b + 1 ]
		(1, 1)    evalSimpleMultipleDepentryin(a, b, c, d) -> evalSimpleMultipleDepbb3in(0, 0, c, d)
		(1, 1)    evalSimpleMultipleDepstart(a, b, c, d) -> evalSimpleMultipleDepentryin(a, b, c, d)
	start location:	evalSimpleMultipleDepstart
	leaf cost:	2

A polynomial rank function with
	Pol(evalSimpleMultipleDepbb2in) = -2*V_2 + 2*V_3 - 2
	Pol(evalSimpleMultipleDepbb3in) = -2*V_2 + 2*V_3 - 1
	Pol(evalSimpleMultipleDepbb1in) = -2*V_2 + 2*V_3 - 1
	Pol(evalSimpleMultipleDepbbin) = -2*V_2 + 2*V_3 - 1
	Pol(evalSimpleMultipleDepentryin) = 2*V_3 - 1
	Pol(evalSimpleMultipleDepstart) = 2*V_3 - 1
orients all transitions weakly and the transition
	evalSimpleMultipleDepbbin(a, b, c, d) -> evalSimpleMultipleDepbb2in(a, b, c, d) [ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= d ]
strictly and produces the following problem:
5:	T:
		(?, 1)          evalSimpleMultipleDepbb2in(a, b, c, d) -> evalSimpleMultipleDepbb3in(0, b + 1, c, d) [ a - d >= 0 /\ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 ]
		(?, 1)          evalSimpleMultipleDepbb1in(a, b, c, d) -> evalSimpleMultipleDepbb3in(a + 1, b, c, d) [ d - 1 >= 0 /\ c + d - 2 >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ -a + d - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 ]
		(2*c + 1, 1)    evalSimpleMultipleDepbbin(a, b, c, d) -> evalSimpleMultipleDepbb2in(a, b, c, d) [ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= d ]
		(?, 1)          evalSimpleMultipleDepbbin(a, b, c, d) -> evalSimpleMultipleDepbb1in(a, b, c, d) [ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ d >= a + 1 ]
		(?, 1)          evalSimpleMultipleDepbb3in(a, b, c, d) -> evalSimpleMultipleDepbbin(a, b, c, d) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= b + 1 ]
		(1, 1)          evalSimpleMultipleDepentryin(a, b, c, d) -> evalSimpleMultipleDepbb3in(0, 0, c, d)
		(1, 1)          evalSimpleMultipleDepstart(a, b, c, d) -> evalSimpleMultipleDepentryin(a, b, c, d)
	start location:	evalSimpleMultipleDepstart
	leaf cost:	2

Repeatedly propagating knowledge in problem 5 produces the following problem:
6:	T:
		(2*c + 1, 1)    evalSimpleMultipleDepbb2in(a, b, c, d) -> evalSimpleMultipleDepbb3in(0, b + 1, c, d) [ a - d >= 0 /\ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 ]
		(?, 1)          evalSimpleMultipleDepbb1in(a, b, c, d) -> evalSimpleMultipleDepbb3in(a + 1, b, c, d) [ d - 1 >= 0 /\ c + d - 2 >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ -a + d - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 ]
		(2*c + 1, 1)    evalSimpleMultipleDepbbin(a, b, c, d) -> evalSimpleMultipleDepbb2in(a, b, c, d) [ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= d ]
		(?, 1)          evalSimpleMultipleDepbbin(a, b, c, d) -> evalSimpleMultipleDepbb1in(a, b, c, d) [ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ d >= a + 1 ]
		(?, 1)          evalSimpleMultipleDepbb3in(a, b, c, d) -> evalSimpleMultipleDepbbin(a, b, c, d) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= b + 1 ]
		(1, 1)          evalSimpleMultipleDepentryin(a, b, c, d) -> evalSimpleMultipleDepbb3in(0, 0, c, d)
		(1, 1)          evalSimpleMultipleDepstart(a, b, c, d) -> evalSimpleMultipleDepentryin(a, b, c, d)
	start location:	evalSimpleMultipleDepstart
	leaf cost:	2

A polynomial rank function with
	Pol(evalSimpleMultipleDepbbin) = -3*V_1 + 3*V_4
	Pol(evalSimpleMultipleDepbb1in) = -3*V_1 + 3*V_4 - 1
	Pol(evalSimpleMultipleDepbb3in) = -3*V_1 + 3*V_4 + 1
and size complexities
	S("evalSimpleMultipleDepstart(a, b, c, d) -> evalSimpleMultipleDepentryin(a, b, c, d)", 0-0) = a
	S("evalSimpleMultipleDepstart(a, b, c, d) -> evalSimpleMultipleDepentryin(a, b, c, d)", 0-1) = b
	S("evalSimpleMultipleDepstart(a, b, c, d) -> evalSimpleMultipleDepentryin(a, b, c, d)", 0-2) = c
	S("evalSimpleMultipleDepstart(a, b, c, d) -> evalSimpleMultipleDepentryin(a, b, c, d)", 0-3) = d
	S("evalSimpleMultipleDepentryin(a, b, c, d) -> evalSimpleMultipleDepbb3in(0, 0, c, d)", 0-0) = 0
	S("evalSimpleMultipleDepentryin(a, b, c, d) -> evalSimpleMultipleDepbb3in(0, 0, c, d)", 0-1) = 0
	S("evalSimpleMultipleDepentryin(a, b, c, d) -> evalSimpleMultipleDepbb3in(0, 0, c, d)", 0-2) = c
	S("evalSimpleMultipleDepentryin(a, b, c, d) -> evalSimpleMultipleDepbb3in(0, 0, c, d)", 0-3) = d
	S("evalSimpleMultipleDepbb3in(a, b, c, d) -> evalSimpleMultipleDepbbin(a, b, c, d) [ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ c >= b + 1 ]", 0-0) = d
	S("evalSimpleMultipleDepbb3in(a, b, c, d) -> evalSimpleMultipleDepbbin(a, b, c, d) [ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ c >= b + 1 ]", 0-1) = c
	S("evalSimpleMultipleDepbb3in(a, b, c, d) -> evalSimpleMultipleDepbbin(a, b, c, d) [ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ c >= b + 1 ]", 0-2) = c
	S("evalSimpleMultipleDepbb3in(a, b, c, d) -> evalSimpleMultipleDepbbin(a, b, c, d) [ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ c >= b + 1 ]", 0-3) = d
	S("evalSimpleMultipleDepbbin(a, b, c, d) -> evalSimpleMultipleDepbb1in(a, b, c, d) [ c - 1 >= 0 /\\ b + c - 1 >= 0 /\\ -b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ d >= a + 1 ]", 0-0) = d
	S("evalSimpleMultipleDepbbin(a, b, c, d) -> evalSimpleMultipleDepbb1in(a, b, c, d) [ c - 1 >= 0 /\\ b + c - 1 >= 0 /\\ -b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ d >= a + 1 ]", 0-1) = c
	S("evalSimpleMultipleDepbbin(a, b, c, d) -> evalSimpleMultipleDepbb1in(a, b, c, d) [ c - 1 >= 0 /\\ b + c - 1 >= 0 /\\ -b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ d >= a + 1 ]", 0-2) = c
	S("evalSimpleMultipleDepbbin(a, b, c, d) -> evalSimpleMultipleDepbb1in(a, b, c, d) [ c - 1 >= 0 /\\ b + c - 1 >= 0 /\\ -b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ d >= a + 1 ]", 0-3) = d
	S("evalSimpleMultipleDepbbin(a, b, c, d) -> evalSimpleMultipleDepbb2in(a, b, c, d) [ c - 1 >= 0 /\\ b + c - 1 >= 0 /\\ -b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ a >= d ]", 0-0) = d
	S("evalSimpleMultipleDepbbin(a, b, c, d) -> evalSimpleMultipleDepbb2in(a, b, c, d) [ c - 1 >= 0 /\\ b + c - 1 >= 0 /\\ -b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ a >= d ]", 0-1) = c
	S("evalSimpleMultipleDepbbin(a, b, c, d) -> evalSimpleMultipleDepbb2in(a, b, c, d) [ c - 1 >= 0 /\\ b + c - 1 >= 0 /\\ -b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ a >= d ]", 0-2) = c
	S("evalSimpleMultipleDepbbin(a, b, c, d) -> evalSimpleMultipleDepbb2in(a, b, c, d) [ c - 1 >= 0 /\\ b + c - 1 >= 0 /\\ -b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ a >= d ]", 0-3) = d
	S("evalSimpleMultipleDepbb1in(a, b, c, d) -> evalSimpleMultipleDepbb3in(a + 1, b, c, d) [ d - 1 >= 0 /\\ c + d - 2 >= 0 /\\ b + d - 1 >= 0 /\\ a + d - 1 >= 0 /\\ -a + d - 1 >= 0 /\\ c - 1 >= 0 /\\ b + c - 1 >= 0 /\\ -b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 ]", 0-0) = d
	S("evalSimpleMultipleDepbb1in(a, b, c, d) -> evalSimpleMultipleDepbb3in(a + 1, b, c, d) [ d - 1 >= 0 /\\ c + d - 2 >= 0 /\\ b + d - 1 >= 0 /\\ a + d - 1 >= 0 /\\ -a + d - 1 >= 0 /\\ c - 1 >= 0 /\\ b + c - 1 >= 0 /\\ -b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 ]", 0-1) = c
	S("evalSimpleMultipleDepbb1in(a, b, c, d) -> evalSimpleMultipleDepbb3in(a + 1, b, c, d) [ d - 1 >= 0 /\\ c + d - 2 >= 0 /\\ b + d - 1 >= 0 /\\ a + d - 1 >= 0 /\\ -a + d - 1 >= 0 /\\ c - 1 >= 0 /\\ b + c - 1 >= 0 /\\ -b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 ]", 0-2) = c
	S("evalSimpleMultipleDepbb1in(a, b, c, d) -> evalSimpleMultipleDepbb3in(a + 1, b, c, d) [ d - 1 >= 0 /\\ c + d - 2 >= 0 /\\ b + d - 1 >= 0 /\\ a + d - 1 >= 0 /\\ -a + d - 1 >= 0 /\\ c - 1 >= 0 /\\ b + c - 1 >= 0 /\\ -b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 ]", 0-3) = d
	S("evalSimpleMultipleDepbb2in(a, b, c, d) -> evalSimpleMultipleDepbb3in(0, b + 1, c, d) [ a - d >= 0 /\\ c - 1 >= 0 /\\ b + c - 1 >= 0 /\\ -b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 ]", 0-0) = 0
	S("evalSimpleMultipleDepbb2in(a, b, c, d) -> evalSimpleMultipleDepbb3in(0, b + 1, c, d) [ a - d >= 0 /\\ c - 1 >= 0 /\\ b + c - 1 >= 0 /\\ -b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 ]", 0-1) = c
	S("evalSimpleMultipleDepbb2in(a, b, c, d) -> evalSimpleMultipleDepbb3in(0, b + 1, c, d) [ a - d >= 0 /\\ c - 1 >= 0 /\\ b + c - 1 >= 0 /\\ -b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 ]", 0-2) = c
	S("evalSimpleMultipleDepbb2in(a, b, c, d) -> evalSimpleMultipleDepbb3in(0, b + 1, c, d) [ a - d >= 0 /\\ c - 1 >= 0 /\\ b + c - 1 >= 0 /\\ -b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ b >= 0 /\\ a + b >= 0 /\\ a >= 0 ]", 0-3) = d
orients the transitions
	evalSimpleMultipleDepbbin(a, b, c, d) -> evalSimpleMultipleDepbb1in(a, b, c, d) [ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ d >= a + 1 ]
	evalSimpleMultipleDepbb3in(a, b, c, d) -> evalSimpleMultipleDepbbin(a, b, c, d) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= b + 1 ]
	evalSimpleMultipleDepbb1in(a, b, c, d) -> evalSimpleMultipleDepbb3in(a + 1, b, c, d) [ d - 1 >= 0 /\ c + d - 2 >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ -a + d - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 ]
weakly and the transitions
	evalSimpleMultipleDepbbin(a, b, c, d) -> evalSimpleMultipleDepbb1in(a, b, c, d) [ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ d >= a + 1 ]
	evalSimpleMultipleDepbb1in(a, b, c, d) -> evalSimpleMultipleDepbb3in(a + 1, b, c, d) [ d - 1 >= 0 /\ c + d - 2 >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ -a + d - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 ]
strictly and produces the following problem:
7:	T:
		(2*c + 1, 1)                  evalSimpleMultipleDepbb2in(a, b, c, d) -> evalSimpleMultipleDepbb3in(0, b + 1, c, d) [ a - d >= 0 /\ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 ]
		(6*d + 6*c*d + 2*c + 2, 1)    evalSimpleMultipleDepbb1in(a, b, c, d) -> evalSimpleMultipleDepbb3in(a + 1, b, c, d) [ d - 1 >= 0 /\ c + d - 2 >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ -a + d - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 ]
		(2*c + 1, 1)                  evalSimpleMultipleDepbbin(a, b, c, d) -> evalSimpleMultipleDepbb2in(a, b, c, d) [ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= d ]
		(6*d + 6*c*d + 2*c + 2, 1)    evalSimpleMultipleDepbbin(a, b, c, d) -> evalSimpleMultipleDepbb1in(a, b, c, d) [ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ d >= a + 1 ]
		(?, 1)                        evalSimpleMultipleDepbb3in(a, b, c, d) -> evalSimpleMultipleDepbbin(a, b, c, d) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= b + 1 ]
		(1, 1)                        evalSimpleMultipleDepentryin(a, b, c, d) -> evalSimpleMultipleDepbb3in(0, 0, c, d)
		(1, 1)                        evalSimpleMultipleDepstart(a, b, c, d) -> evalSimpleMultipleDepentryin(a, b, c, d)
	start location:	evalSimpleMultipleDepstart
	leaf cost:	2

Repeatedly propagating knowledge in problem 7 produces the following problem:
8:	T:
		(2*c + 1, 1)                  evalSimpleMultipleDepbb2in(a, b, c, d) -> evalSimpleMultipleDepbb3in(0, b + 1, c, d) [ a - d >= 0 /\ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 ]
		(6*d + 6*c*d + 2*c + 2, 1)    evalSimpleMultipleDepbb1in(a, b, c, d) -> evalSimpleMultipleDepbb3in(a + 1, b, c, d) [ d - 1 >= 0 /\ c + d - 2 >= 0 /\ b + d - 1 >= 0 /\ a + d - 1 >= 0 /\ -a + d - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 ]
		(2*c + 1, 1)                  evalSimpleMultipleDepbbin(a, b, c, d) -> evalSimpleMultipleDepbb2in(a, b, c, d) [ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ a >= d ]
		(6*d + 6*c*d + 2*c + 2, 1)    evalSimpleMultipleDepbbin(a, b, c, d) -> evalSimpleMultipleDepbb1in(a, b, c, d) [ c - 1 >= 0 /\ b + c - 1 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ d >= a + 1 ]
		(6*d + 6*c*d + 4*c + 4, 1)    evalSimpleMultipleDepbb3in(a, b, c, d) -> evalSimpleMultipleDepbbin(a, b, c, d) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= b + 1 ]
		(1, 1)                        evalSimpleMultipleDepentryin(a, b, c, d) -> evalSimpleMultipleDepbb3in(0, 0, c, d)
		(1, 1)                        evalSimpleMultipleDepstart(a, b, c, d) -> evalSimpleMultipleDepentryin(a, b, c, d)
	start location:	evalSimpleMultipleDepstart
	leaf cost:	2

Complexity upper bound 12*c + 18*d + 18*c*d + 14

Time: 0.481 sec (SMT: 0.448 sec)