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

Initial complexity problem:
1:	T:
		(1, 1)    evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d)
		(?, 1)    evalfentryin(a, b, c, d) -> evalfbb3in(0, 0, c, d)
		(?, 1)    evalfbb3in(a, b, c, d) -> evalfbbin(a, b, c, d) [ c >= b + 1 ]
		(?, 1)    evalfbb3in(a, b, c, d) -> evalfreturnin(a, b, c, d) [ b >= c ]
		(?, 1)    evalfbbin(a, b, c, d) -> evalfbb1in(a, b, c, d) [ d >= a + 1 ]
		(?, 1)    evalfbbin(a, b, c, d) -> evalfbb2in(a, b, c, d) [ a >= d ]
		(?, 1)    evalfbb1in(a, b, c, d) -> evalfbb3in(a + 1, b, c, d)
		(?, 1)    evalfbb2in(a, b, c, d) -> evalfbb3in(0, b + 1, c, d)
		(?, 1)    evalfreturnin(a, b, c, d) -> evalfstop(a, b, c, d)
	start location:	evalfstart
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(1, 1)    evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d)
		(?, 1)    evalfentryin(a, b, c, d) -> evalfbb3in(0, 0, c, d)
		(?, 1)    evalfbb3in(a, b, c, d) -> evalfbbin(a, b, c, d) [ c >= b + 1 ]
		(?, 1)    evalfbbin(a, b, c, d) -> evalfbb1in(a, b, c, d) [ d >= a + 1 ]
		(?, 1)    evalfbbin(a, b, c, d) -> evalfbb2in(a, b, c, d) [ a >= d ]
		(?, 1)    evalfbb1in(a, b, c, d) -> evalfbb3in(a + 1, b, c, d)
		(?, 1)    evalfbb2in(a, b, c, d) -> evalfbb3in(0, b + 1, c, d)
	start location:	evalfstart
	leaf cost:	2

Repeatedly propagating knowledge in problem 2 produces the following problem:
3:	T:
		(1, 1)    evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d)
		(1, 1)    evalfentryin(a, b, c, d) -> evalfbb3in(0, 0, c, d)
		(?, 1)    evalfbb3in(a, b, c, d) -> evalfbbin(a, b, c, d) [ c >= b + 1 ]
		(?, 1)    evalfbbin(a, b, c, d) -> evalfbb1in(a, b, c, d) [ d >= a + 1 ]
		(?, 1)    evalfbbin(a, b, c, d) -> evalfbb2in(a, b, c, d) [ a >= d ]
		(?, 1)    evalfbb1in(a, b, c, d) -> evalfbb3in(a + 1, b, c, d)
		(?, 1)    evalfbb2in(a, b, c, d) -> evalfbb3in(0, b + 1, c, d)
	start location:	evalfstart
	leaf cost:	2

Applied AI with 'oct' on problem 3 to obtain the following invariants:
  For symbol evalfbb1in: 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 evalfbb2in: 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 evalfbb3in: X_2 >= 0 /\ X_1 + X_2 >= 0 /\ X_1 >= 0
  For symbol evalfbbin: 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)    evalfbb2in(a, b, c, d) -> evalfbb3in(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)    evalfbb1in(a, b, c, d) -> evalfbb3in(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)    evalfbbin(a, b, c, d) -> evalfbb2in(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)    evalfbbin(a, b, c, d) -> evalfbb1in(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)    evalfbb3in(a, b, c, d) -> evalfbbin(a, b, c, d) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= b + 1 ]
		(1, 1)    evalfentryin(a, b, c, d) -> evalfbb3in(0, 0, c, d)
		(1, 1)    evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d)
	start location:	evalfstart
	leaf cost:	2

A polynomial rank function with
	Pol(evalfbb2in) = -2*V_2 + 2*V_3 - 2
	Pol(evalfbb3in) = -2*V_2 + 2*V_3 - 1
	Pol(evalfbb1in) = -2*V_2 + 2*V_3 - 1
	Pol(evalfbbin) = -2*V_2 + 2*V_3 - 1
	Pol(evalfentryin) = 2*V_3 - 1
	Pol(evalfstart) = 2*V_3 - 1
orients all transitions weakly and the transition
	evalfbbin(a, b, c, d) -> evalfbb2in(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)          evalfbb2in(a, b, c, d) -> evalfbb3in(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)          evalfbb1in(a, b, c, d) -> evalfbb3in(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)    evalfbbin(a, b, c, d) -> evalfbb2in(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)          evalfbbin(a, b, c, d) -> evalfbb1in(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)          evalfbb3in(a, b, c, d) -> evalfbbin(a, b, c, d) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= b + 1 ]
		(1, 1)          evalfentryin(a, b, c, d) -> evalfbb3in(0, 0, c, d)
		(1, 1)          evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d)
	start location:	evalfstart
	leaf cost:	2

Repeatedly propagating knowledge in problem 5 produces the following problem:
6:	T:
		(2*c + 1, 1)    evalfbb2in(a, b, c, d) -> evalfbb3in(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)          evalfbb1in(a, b, c, d) -> evalfbb3in(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)    evalfbbin(a, b, c, d) -> evalfbb2in(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)          evalfbbin(a, b, c, d) -> evalfbb1in(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)          evalfbb3in(a, b, c, d) -> evalfbbin(a, b, c, d) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= b + 1 ]
		(1, 1)          evalfentryin(a, b, c, d) -> evalfbb3in(0, 0, c, d)
		(1, 1)          evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d)
	start location:	evalfstart
	leaf cost:	2

A polynomial rank function with
	Pol(evalfbbin) = -3*V_1 + 3*V_4
	Pol(evalfbb1in) = -3*V_1 + 3*V_4 - 1
	Pol(evalfbb3in) = -3*V_1 + 3*V_4 + 1
and size complexities
	S("evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d)", 0-0) = a
	S("evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d)", 0-1) = b
	S("evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d)", 0-2) = c
	S("evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d)", 0-3) = d
	S("evalfentryin(a, b, c, d) -> evalfbb3in(0, 0, c, d)", 0-0) = 0
	S("evalfentryin(a, b, c, d) -> evalfbb3in(0, 0, c, d)", 0-1) = 0
	S("evalfentryin(a, b, c, d) -> evalfbb3in(0, 0, c, d)", 0-2) = c
	S("evalfentryin(a, b, c, d) -> evalfbb3in(0, 0, c, d)", 0-3) = d
	S("evalfbb3in(a, b, c, d) -> evalfbbin(a, b, c, d) [ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ c >= b + 1 ]", 0-0) = d
	S("evalfbb3in(a, b, c, d) -> evalfbbin(a, b, c, d) [ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ c >= b + 1 ]", 0-1) = c
	S("evalfbb3in(a, b, c, d) -> evalfbbin(a, b, c, d) [ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ c >= b + 1 ]", 0-2) = c
	S("evalfbb3in(a, b, c, d) -> evalfbbin(a, b, c, d) [ b >= 0 /\\ a + b >= 0 /\\ a >= 0 /\\ c >= b + 1 ]", 0-3) = d
	S("evalfbbin(a, b, c, d) -> evalfbb1in(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("evalfbbin(a, b, c, d) -> evalfbb1in(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("evalfbbin(a, b, c, d) -> evalfbb1in(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("evalfbbin(a, b, c, d) -> evalfbb1in(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("evalfbbin(a, b, c, d) -> evalfbb2in(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("evalfbbin(a, b, c, d) -> evalfbb2in(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("evalfbbin(a, b, c, d) -> evalfbb2in(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("evalfbbin(a, b, c, d) -> evalfbb2in(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("evalfbb1in(a, b, c, d) -> evalfbb3in(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("evalfbb1in(a, b, c, d) -> evalfbb3in(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("evalfbb1in(a, b, c, d) -> evalfbb3in(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("evalfbb1in(a, b, c, d) -> evalfbb3in(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("evalfbb2in(a, b, c, d) -> evalfbb3in(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("evalfbb2in(a, b, c, d) -> evalfbb3in(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("evalfbb2in(a, b, c, d) -> evalfbb3in(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("evalfbb2in(a, b, c, d) -> evalfbb3in(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
	evalfbbin(a, b, c, d) -> evalfbb1in(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 ]
	evalfbb3in(a, b, c, d) -> evalfbbin(a, b, c, d) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= b + 1 ]
	evalfbb1in(a, b, c, d) -> evalfbb3in(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
	evalfbbin(a, b, c, d) -> evalfbb1in(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 ]
	evalfbb1in(a, b, c, d) -> evalfbb3in(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)                  evalfbb2in(a, b, c, d) -> evalfbb3in(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)    evalfbb1in(a, b, c, d) -> evalfbb3in(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)                  evalfbbin(a, b, c, d) -> evalfbb2in(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)    evalfbbin(a, b, c, d) -> evalfbb1in(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)                        evalfbb3in(a, b, c, d) -> evalfbbin(a, b, c, d) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= b + 1 ]
		(1, 1)                        evalfentryin(a, b, c, d) -> evalfbb3in(0, 0, c, d)
		(1, 1)                        evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d)
	start location:	evalfstart
	leaf cost:	2

Repeatedly propagating knowledge in problem 7 produces the following problem:
8:	T:
		(2*c + 1, 1)                  evalfbb2in(a, b, c, d) -> evalfbb3in(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)    evalfbb1in(a, b, c, d) -> evalfbb3in(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)                  evalfbbin(a, b, c, d) -> evalfbb2in(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)    evalfbbin(a, b, c, d) -> evalfbb1in(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)    evalfbb3in(a, b, c, d) -> evalfbbin(a, b, c, d) [ b >= 0 /\ a + b >= 0 /\ a >= 0 /\ c >= b + 1 ]
		(1, 1)                        evalfentryin(a, b, c, d) -> evalfbb3in(0, 0, c, d)
		(1, 1)                        evalfstart(a, b, c, d) -> evalfentryin(a, b, c, d)
	start location:	evalfstart
	leaf cost:	2

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

Time: 0.460 sec (SMT: 0.430 sec)