YES(?, 6*c + 6*d + 8)

Initial complexity problem:
1:	T:
		(1, 1)    evalSimpleMultiplestart(a, b, c, d) -> evalSimpleMultipleentryin(a, b, c, d)
		(?, 1)    evalSimpleMultipleentryin(a, b, c, d) -> evalSimpleMultiplebb3in(0, 0, c, d)
		(?, 1)    evalSimpleMultiplebb3in(a, b, c, d) -> evalSimpleMultiplebbin(a, b, c, d) [ c >= b + 1 ]
		(?, 1)    evalSimpleMultiplebb3in(a, b, c, d) -> evalSimpleMultiplereturnin(a, b, c, d) [ b >= c ]
		(?, 1)    evalSimpleMultiplebbin(a, b, c, d) -> evalSimpleMultiplebb1in(a, b, c, d) [ d >= a + 1 ]
		(?, 1)    evalSimpleMultiplebbin(a, b, c, d) -> evalSimpleMultiplebb2in(a, b, c, d) [ a >= d ]
		(?, 1)    evalSimpleMultiplebb1in(a, b, c, d) -> evalSimpleMultiplebb3in(a + 1, b, c, d)
		(?, 1)    evalSimpleMultiplebb2in(a, b, c, d) -> evalSimpleMultiplebb3in(a, b + 1, c, d)
		(?, 1)    evalSimpleMultiplereturnin(a, b, c, d) -> evalSimpleMultiplestop(a, b, c, d)
	start location:	evalSimpleMultiplestart
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(1, 1)    evalSimpleMultiplestart(a, b, c, d) -> evalSimpleMultipleentryin(a, b, c, d)
		(?, 1)    evalSimpleMultipleentryin(a, b, c, d) -> evalSimpleMultiplebb3in(0, 0, c, d)
		(?, 1)    evalSimpleMultiplebb3in(a, b, c, d) -> evalSimpleMultiplebbin(a, b, c, d) [ c >= b + 1 ]
		(?, 1)    evalSimpleMultiplebbin(a, b, c, d) -> evalSimpleMultiplebb1in(a, b, c, d) [ d >= a + 1 ]
		(?, 1)    evalSimpleMultiplebbin(a, b, c, d) -> evalSimpleMultiplebb2in(a, b, c, d) [ a >= d ]
		(?, 1)    evalSimpleMultiplebb1in(a, b, c, d) -> evalSimpleMultiplebb3in(a + 1, b, c, d)
		(?, 1)    evalSimpleMultiplebb2in(a, b, c, d) -> evalSimpleMultiplebb3in(a, b + 1, c, d)
	start location:	evalSimpleMultiplestart
	leaf cost:	2

Repeatedly propagating knowledge in problem 2 produces the following problem:
3:	T:
		(1, 1)    evalSimpleMultiplestart(a, b, c, d) -> evalSimpleMultipleentryin(a, b, c, d)
		(1, 1)    evalSimpleMultipleentryin(a, b, c, d) -> evalSimpleMultiplebb3in(0, 0, c, d)
		(?, 1)    evalSimpleMultiplebb3in(a, b, c, d) -> evalSimpleMultiplebbin(a, b, c, d) [ c >= b + 1 ]
		(?, 1)    evalSimpleMultiplebbin(a, b, c, d) -> evalSimpleMultiplebb1in(a, b, c, d) [ d >= a + 1 ]
		(?, 1)    evalSimpleMultiplebbin(a, b, c, d) -> evalSimpleMultiplebb2in(a, b, c, d) [ a >= d ]
		(?, 1)    evalSimpleMultiplebb1in(a, b, c, d) -> evalSimpleMultiplebb3in(a + 1, b, c, d)
		(?, 1)    evalSimpleMultiplebb2in(a, b, c, d) -> evalSimpleMultiplebb3in(a, b + 1, c, d)
	start location:	evalSimpleMultiplestart
	leaf cost:	2

A polynomial rank function with
	Pol(evalSimpleMultiplestart) = 2*V_4
	Pol(evalSimpleMultipleentryin) = 2*V_4
	Pol(evalSimpleMultiplebb3in) = -2*V_1 + 2*V_4
	Pol(evalSimpleMultiplebbin) = -2*V_1 + 2*V_4
	Pol(evalSimpleMultiplebb1in) = -2*V_1 + 2*V_4 - 1
	Pol(evalSimpleMultiplebb2in) = -2*V_1 + 2*V_4
orients all transitions weakly and the transition
	evalSimpleMultiplebbin(a, b, c, d) -> evalSimpleMultiplebb1in(a, b, c, d) [ d >= a + 1 ]
strictly and produces the following problem:
4:	T:
		(1, 1)      evalSimpleMultiplestart(a, b, c, d) -> evalSimpleMultipleentryin(a, b, c, d)
		(1, 1)      evalSimpleMultipleentryin(a, b, c, d) -> evalSimpleMultiplebb3in(0, 0, c, d)
		(?, 1)      evalSimpleMultiplebb3in(a, b, c, d) -> evalSimpleMultiplebbin(a, b, c, d) [ c >= b + 1 ]
		(2*d, 1)    evalSimpleMultiplebbin(a, b, c, d) -> evalSimpleMultiplebb1in(a, b, c, d) [ d >= a + 1 ]
		(?, 1)      evalSimpleMultiplebbin(a, b, c, d) -> evalSimpleMultiplebb2in(a, b, c, d) [ a >= d ]
		(?, 1)      evalSimpleMultiplebb1in(a, b, c, d) -> evalSimpleMultiplebb3in(a + 1, b, c, d)
		(?, 1)      evalSimpleMultiplebb2in(a, b, c, d) -> evalSimpleMultiplebb3in(a, b + 1, c, d)
	start location:	evalSimpleMultiplestart
	leaf cost:	2

Repeatedly propagating knowledge in problem 4 produces the following problem:
5:	T:
		(1, 1)      evalSimpleMultiplestart(a, b, c, d) -> evalSimpleMultipleentryin(a, b, c, d)
		(1, 1)      evalSimpleMultipleentryin(a, b, c, d) -> evalSimpleMultiplebb3in(0, 0, c, d)
		(?, 1)      evalSimpleMultiplebb3in(a, b, c, d) -> evalSimpleMultiplebbin(a, b, c, d) [ c >= b + 1 ]
		(2*d, 1)    evalSimpleMultiplebbin(a, b, c, d) -> evalSimpleMultiplebb1in(a, b, c, d) [ d >= a + 1 ]
		(?, 1)      evalSimpleMultiplebbin(a, b, c, d) -> evalSimpleMultiplebb2in(a, b, c, d) [ a >= d ]
		(2*d, 1)    evalSimpleMultiplebb1in(a, b, c, d) -> evalSimpleMultiplebb3in(a + 1, b, c, d)
		(?, 1)      evalSimpleMultiplebb2in(a, b, c, d) -> evalSimpleMultiplebb3in(a, b + 1, c, d)
	start location:	evalSimpleMultiplestart
	leaf cost:	2

Applied AI with 'oct' on problem 5 to obtain the following invariants:
  For symbol evalSimpleMultiplebb1in: 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 evalSimpleMultiplebb2in: 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 evalSimpleMultiplebb3in: X_2 >= 0 /\ X_1 + X_2 >= 0 /\ X_1 >= 0
  For symbol evalSimpleMultiplebbin: 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:
6:	T:
		(?, 1)      evalSimpleMultiplebb2in(a, b, c, d) -> evalSimpleMultiplebb3in(a, 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 ]
		(2*d, 1)    evalSimpleMultiplebb1in(a, b, c, d) -> evalSimpleMultiplebb3in(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)      evalSimpleMultiplebbin(a, b, c, d) -> evalSimpleMultiplebb2in(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 ]
		(2*d, 1)    evalSimpleMultiplebbin(a, b, c, d) -> evalSimpleMultiplebb1in(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)      evalSimpleMultiplebb3in(a, b, c, d) -> evalSimpleMultiplebbin(a, b, c, d) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= b + 1 ]
		(1, 1)      evalSimpleMultipleentryin(a, b, c, d) -> evalSimpleMultiplebb3in(0, 0, c, d)
		(1, 1)      evalSimpleMultiplestart(a, b, c, d) -> evalSimpleMultipleentryin(a, b, c, d)
	start location:	evalSimpleMultiplestart
	leaf cost:	2

A polynomial rank function with
	Pol(evalSimpleMultiplebb2in) = -2*V_2 + 2*V_3 - 2
	Pol(evalSimpleMultiplebb3in) = -2*V_2 + 2*V_3 - 1
	Pol(evalSimpleMultiplebb1in) = -2*V_2 + 2*V_3 - 1
	Pol(evalSimpleMultiplebbin) = -2*V_2 + 2*V_3 - 1
	Pol(evalSimpleMultipleentryin) = 2*V_3 - 1
	Pol(evalSimpleMultiplestart) = 2*V_3 - 1
orients all transitions weakly and the transition
	evalSimpleMultiplebbin(a, b, c, d) -> evalSimpleMultiplebb2in(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:
7:	T:
		(?, 1)          evalSimpleMultiplebb2in(a, b, c, d) -> evalSimpleMultiplebb3in(a, 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 ]
		(2*d, 1)        evalSimpleMultiplebb1in(a, b, c, d) -> evalSimpleMultiplebb3in(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)    evalSimpleMultiplebbin(a, b, c, d) -> evalSimpleMultiplebb2in(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 ]
		(2*d, 1)        evalSimpleMultiplebbin(a, b, c, d) -> evalSimpleMultiplebb1in(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)          evalSimpleMultiplebb3in(a, b, c, d) -> evalSimpleMultiplebbin(a, b, c, d) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= b + 1 ]
		(1, 1)          evalSimpleMultipleentryin(a, b, c, d) -> evalSimpleMultiplebb3in(0, 0, c, d)
		(1, 1)          evalSimpleMultiplestart(a, b, c, d) -> evalSimpleMultipleentryin(a, b, c, d)
	start location:	evalSimpleMultiplestart
	leaf cost:	2

Repeatedly propagating knowledge in problem 7 produces the following problem:
8:	T:
		(2*c + 1, 1)          evalSimpleMultiplebb2in(a, b, c, d) -> evalSimpleMultiplebb3in(a, 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 ]
		(2*d, 1)              evalSimpleMultiplebb1in(a, b, c, d) -> evalSimpleMultiplebb3in(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)          evalSimpleMultiplebbin(a, b, c, d) -> evalSimpleMultiplebb2in(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 ]
		(2*d, 1)              evalSimpleMultiplebbin(a, b, c, d) -> evalSimpleMultiplebb1in(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 ]
		(2*d + 2*c + 2, 1)    evalSimpleMultiplebb3in(a, b, c, d) -> evalSimpleMultiplebbin(a, b, c, d) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= b + 1 ]
		(1, 1)                evalSimpleMultipleentryin(a, b, c, d) -> evalSimpleMultiplebb3in(0, 0, c, d)
		(1, 1)                evalSimpleMultiplestart(a, b, c, d) -> evalSimpleMultipleentryin(a, b, c, d)
	start location:	evalSimpleMultiplestart
	leaf cost:	2

Complexity upper bound 6*c + 6*d + 8

Time: 0.446 sec (SMT: 0.419 sec)