YES(?, 39*a + 12*a^2 + 36)

Initial complexity problem:
1:	T:
		(1, 1)    evalperfectstart(a, b, c, d) -> evalperfectentryin(a, b, c, d)
		(?, 1)    evalperfectentryin(a, b, c, d) -> evalperfectreturnin(a, b, c, d) [ 1 >= a ]
		(?, 1)    evalperfectentryin(a, b, c, d) -> evalperfectbb1in(a, b, c, d) [ a >= 2 ]
		(?, 1)    evalperfectbb1in(a, b, c, d) -> evalperfectbb8in(a, a, a - 1, d)
		(?, 1)    evalperfectbb8in(a, b, c, d) -> evalperfectbb4in(a, b, c, a) [ c >= 1 ]
		(?, 1)    evalperfectbb8in(a, b, c, d) -> evalperfectbb9in(b, b, c, d) [ 0 >= c ]
		(?, 1)    evalperfectbb4in(a, b, c, d) -> evalperfectbb3in(a, b, c, d) [ d >= c ]
		(?, 1)    evalperfectbb4in(a, b, c, d) -> evalperfectbb5in(a, b, c, d) [ c >= d + 1 ]
		(?, 1)    evalperfectbb3in(a, b, c, d) -> evalperfectbb4in(a, b, c, d - c)
		(?, 1)    evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b - c, c - 1, d) [ d = 0 ]
		(?, 1)    evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ 0 >= d + 1 ]
		(?, 1)    evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ d >= 1 ]
		(?, 1)    evalperfectbb9in(a, b, c, d) -> evalperfectreturnin(a, b, c, d) [ 0 >= a + 1 ]
		(?, 1)    evalperfectbb9in(a, b, c, d) -> evalperfectreturnin(a, b, c, d) [ a >= 1 ]
		(?, 1)    evalperfectbb9in(a, b, c, d) -> evalperfectreturnin(a, b, c, d) [ a = 0 ]
		(?, 1)    evalperfectreturnin(a, b, c, d) -> evalperfectstop(a, b, c, d)
	start location:	evalperfectstart
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(1, 1)    evalperfectstart(a, b, c, d) -> evalperfectentryin(a, b, c, d)
		(?, 1)    evalperfectentryin(a, b, c, d) -> evalperfectbb1in(a, b, c, d) [ a >= 2 ]
		(?, 1)    evalperfectbb1in(a, b, c, d) -> evalperfectbb8in(a, a, a - 1, d)
		(?, 1)    evalperfectbb8in(a, b, c, d) -> evalperfectbb4in(a, b, c, a) [ c >= 1 ]
		(?, 1)    evalperfectbb4in(a, b, c, d) -> evalperfectbb3in(a, b, c, d) [ d >= c ]
		(?, 1)    evalperfectbb4in(a, b, c, d) -> evalperfectbb5in(a, b, c, d) [ c >= d + 1 ]
		(?, 1)    evalperfectbb3in(a, b, c, d) -> evalperfectbb4in(a, b, c, d - c)
		(?, 1)    evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b - c, c - 1, d) [ d = 0 ]
		(?, 1)    evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ 0 >= d + 1 ]
		(?, 1)    evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ d >= 1 ]
	start location:	evalperfectstart
	leaf cost:	6

Repeatedly propagating knowledge in problem 2 produces the following problem:
3:	T:
		(1, 1)    evalperfectstart(a, b, c, d) -> evalperfectentryin(a, b, c, d)
		(1, 1)    evalperfectentryin(a, b, c, d) -> evalperfectbb1in(a, b, c, d) [ a >= 2 ]
		(1, 1)    evalperfectbb1in(a, b, c, d) -> evalperfectbb8in(a, a, a - 1, d)
		(?, 1)    evalperfectbb8in(a, b, c, d) -> evalperfectbb4in(a, b, c, a) [ c >= 1 ]
		(?, 1)    evalperfectbb4in(a, b, c, d) -> evalperfectbb3in(a, b, c, d) [ d >= c ]
		(?, 1)    evalperfectbb4in(a, b, c, d) -> evalperfectbb5in(a, b, c, d) [ c >= d + 1 ]
		(?, 1)    evalperfectbb3in(a, b, c, d) -> evalperfectbb4in(a, b, c, d - c)
		(?, 1)    evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b - c, c - 1, d) [ d = 0 ]
		(?, 1)    evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ 0 >= d + 1 ]
		(?, 1)    evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ d >= 1 ]
	start location:	evalperfectstart
	leaf cost:	6

A polynomial rank function with
	Pol(evalperfectstart) = 3*V_1 - 3
	Pol(evalperfectentryin) = 3*V_1 - 3
	Pol(evalperfectbb1in) = 3*V_1 - 3
	Pol(evalperfectbb8in) = 3*V_3
	Pol(evalperfectbb4in) = 3*V_3 - 1
	Pol(evalperfectbb3in) = 3*V_3 - 1
	Pol(evalperfectbb5in) = 3*V_3 - 2
orients all transitions weakly and the transition
	evalperfectbb8in(a, b, c, d) -> evalperfectbb4in(a, b, c, a) [ c >= 1 ]
strictly and produces the following problem:
4:	T:
		(1, 1)          evalperfectstart(a, b, c, d) -> evalperfectentryin(a, b, c, d)
		(1, 1)          evalperfectentryin(a, b, c, d) -> evalperfectbb1in(a, b, c, d) [ a >= 2 ]
		(1, 1)          evalperfectbb1in(a, b, c, d) -> evalperfectbb8in(a, a, a - 1, d)
		(3*a + 3, 1)    evalperfectbb8in(a, b, c, d) -> evalperfectbb4in(a, b, c, a) [ c >= 1 ]
		(?, 1)          evalperfectbb4in(a, b, c, d) -> evalperfectbb3in(a, b, c, d) [ d >= c ]
		(?, 1)          evalperfectbb4in(a, b, c, d) -> evalperfectbb5in(a, b, c, d) [ c >= d + 1 ]
		(?, 1)          evalperfectbb3in(a, b, c, d) -> evalperfectbb4in(a, b, c, d - c)
		(?, 1)          evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b - c, c - 1, d) [ d = 0 ]
		(?, 1)          evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ 0 >= d + 1 ]
		(?, 1)          evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ d >= 1 ]
	start location:	evalperfectstart
	leaf cost:	6

A polynomial rank function with
	Pol(evalperfectbb5in) = 1
	Pol(evalperfectbb8in) = 0
	Pol(evalperfectbb4in) = 2
	Pol(evalperfectbb3in) = 2
and size complexities
	S("evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ d >= 1 ]", 0-0) = a
	S("evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ d >= 1 ]", 0-1) = ?
	S("evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ d >= 1 ]", 0-2) = ?
	S("evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ d >= 1 ]", 0-3) = ?
	S("evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ 0 >= d + 1 ]", 0-0) = a
	S("evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ 0 >= d + 1 ]", 0-1) = ?
	S("evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ 0 >= d + 1 ]", 0-2) = ?
	S("evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ 0 >= d + 1 ]", 0-3) = ?
	S("evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b - c, c - 1, d) [ d = 0 ]", 0-0) = a
	S("evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b - c, c - 1, d) [ d = 0 ]", 0-1) = ?
	S("evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b - c, c - 1, d) [ d = 0 ]", 0-2) = ?
	S("evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b - c, c - 1, d) [ d = 0 ]", 0-3) = 0
	S("evalperfectbb3in(a, b, c, d) -> evalperfectbb4in(a, b, c, d - c)", 0-0) = a
	S("evalperfectbb3in(a, b, c, d) -> evalperfectbb4in(a, b, c, d - c)", 0-1) = ?
	S("evalperfectbb3in(a, b, c, d) -> evalperfectbb4in(a, b, c, d - c)", 0-2) = ?
	S("evalperfectbb3in(a, b, c, d) -> evalperfectbb4in(a, b, c, d - c)", 0-3) = ?
	S("evalperfectbb4in(a, b, c, d) -> evalperfectbb5in(a, b, c, d) [ c >= d + 1 ]", 0-0) = a
	S("evalperfectbb4in(a, b, c, d) -> evalperfectbb5in(a, b, c, d) [ c >= d + 1 ]", 0-1) = ?
	S("evalperfectbb4in(a, b, c, d) -> evalperfectbb5in(a, b, c, d) [ c >= d + 1 ]", 0-2) = ?
	S("evalperfectbb4in(a, b, c, d) -> evalperfectbb5in(a, b, c, d) [ c >= d + 1 ]", 0-3) = ?
	S("evalperfectbb4in(a, b, c, d) -> evalperfectbb3in(a, b, c, d) [ d >= c ]", 0-0) = a
	S("evalperfectbb4in(a, b, c, d) -> evalperfectbb3in(a, b, c, d) [ d >= c ]", 0-1) = ?
	S("evalperfectbb4in(a, b, c, d) -> evalperfectbb3in(a, b, c, d) [ d >= c ]", 0-2) = ?
	S("evalperfectbb4in(a, b, c, d) -> evalperfectbb3in(a, b, c, d) [ d >= c ]", 0-3) = ?
	S("evalperfectbb8in(a, b, c, d) -> evalperfectbb4in(a, b, c, a) [ c >= 1 ]", 0-0) = a
	S("evalperfectbb8in(a, b, c, d) -> evalperfectbb4in(a, b, c, a) [ c >= 1 ]", 0-1) = ?
	S("evalperfectbb8in(a, b, c, d) -> evalperfectbb4in(a, b, c, a) [ c >= 1 ]", 0-2) = ?
	S("evalperfectbb8in(a, b, c, d) -> evalperfectbb4in(a, b, c, a) [ c >= 1 ]", 0-3) = a
	S("evalperfectbb1in(a, b, c, d) -> evalperfectbb8in(a, a, a - 1, d)", 0-0) = a
	S("evalperfectbb1in(a, b, c, d) -> evalperfectbb8in(a, a, a - 1, d)", 0-1) = a
	S("evalperfectbb1in(a, b, c, d) -> evalperfectbb8in(a, a, a - 1, d)", 0-2) = a + 1
	S("evalperfectbb1in(a, b, c, d) -> evalperfectbb8in(a, a, a - 1, d)", 0-3) = d
	S("evalperfectentryin(a, b, c, d) -> evalperfectbb1in(a, b, c, d) [ a >= 2 ]", 0-0) = a
	S("evalperfectentryin(a, b, c, d) -> evalperfectbb1in(a, b, c, d) [ a >= 2 ]", 0-1) = b
	S("evalperfectentryin(a, b, c, d) -> evalperfectbb1in(a, b, c, d) [ a >= 2 ]", 0-2) = c
	S("evalperfectentryin(a, b, c, d) -> evalperfectbb1in(a, b, c, d) [ a >= 2 ]", 0-3) = d
	S("evalperfectstart(a, b, c, d) -> evalperfectentryin(a, b, c, d)", 0-0) = a
	S("evalperfectstart(a, b, c, d) -> evalperfectentryin(a, b, c, d)", 0-1) = b
	S("evalperfectstart(a, b, c, d) -> evalperfectentryin(a, b, c, d)", 0-2) = c
	S("evalperfectstart(a, b, c, d) -> evalperfectentryin(a, b, c, d)", 0-3) = d
orients the transitions
	evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b - c, c - 1, d) [ d = 0 ]
	evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ d >= 1 ]
	evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ 0 >= d + 1 ]
	evalperfectbb4in(a, b, c, d) -> evalperfectbb5in(a, b, c, d) [ c >= d + 1 ]
	evalperfectbb4in(a, b, c, d) -> evalperfectbb3in(a, b, c, d) [ d >= c ]
	evalperfectbb3in(a, b, c, d) -> evalperfectbb4in(a, b, c, d - c)
weakly and the transitions
	evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b - c, c - 1, d) [ d = 0 ]
	evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ 0 >= d + 1 ]
	evalperfectbb4in(a, b, c, d) -> evalperfectbb5in(a, b, c, d) [ c >= d + 1 ]
strictly and produces the following problem:
5:	T:
		(1, 1)          evalperfectstart(a, b, c, d) -> evalperfectentryin(a, b, c, d)
		(1, 1)          evalperfectentryin(a, b, c, d) -> evalperfectbb1in(a, b, c, d) [ a >= 2 ]
		(1, 1)          evalperfectbb1in(a, b, c, d) -> evalperfectbb8in(a, a, a - 1, d)
		(3*a + 3, 1)    evalperfectbb8in(a, b, c, d) -> evalperfectbb4in(a, b, c, a) [ c >= 1 ]
		(?, 1)          evalperfectbb4in(a, b, c, d) -> evalperfectbb3in(a, b, c, d) [ d >= c ]
		(6*a + 6, 1)    evalperfectbb4in(a, b, c, d) -> evalperfectbb5in(a, b, c, d) [ c >= d + 1 ]
		(?, 1)          evalperfectbb3in(a, b, c, d) -> evalperfectbb4in(a, b, c, d - c)
		(6*a + 6, 1)    evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b - c, c - 1, d) [ d = 0 ]
		(6*a + 6, 1)    evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ 0 >= d + 1 ]
		(?, 1)          evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ d >= 1 ]
	start location:	evalperfectstart
	leaf cost:	6

Repeatedly propagating knowledge in problem 5 produces the following problem:
6:	T:
		(1, 1)          evalperfectstart(a, b, c, d) -> evalperfectentryin(a, b, c, d)
		(1, 1)          evalperfectentryin(a, b, c, d) -> evalperfectbb1in(a, b, c, d) [ a >= 2 ]
		(1, 1)          evalperfectbb1in(a, b, c, d) -> evalperfectbb8in(a, a, a - 1, d)
		(3*a + 3, 1)    evalperfectbb8in(a, b, c, d) -> evalperfectbb4in(a, b, c, a) [ c >= 1 ]
		(?, 1)          evalperfectbb4in(a, b, c, d) -> evalperfectbb3in(a, b, c, d) [ d >= c ]
		(6*a + 6, 1)    evalperfectbb4in(a, b, c, d) -> evalperfectbb5in(a, b, c, d) [ c >= d + 1 ]
		(?, 1)          evalperfectbb3in(a, b, c, d) -> evalperfectbb4in(a, b, c, d - c)
		(6*a + 6, 1)    evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b - c, c - 1, d) [ d = 0 ]
		(6*a + 6, 1)    evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ 0 >= d + 1 ]
		(6*a + 6, 1)    evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ d >= 1 ]
	start location:	evalperfectstart
	leaf cost:	6

Applied AI with 'oct' on problem 6 to obtain the following invariants:
  For symbol evalperfectbb1in: X_1 - 2 >= 0
  For symbol evalperfectbb3in: X_1 - X_4 >= 0 /\ X_4 - 1 >= 0 /\ X_3 + X_4 - 2 >= 0 /\ -X_3 + X_4 >= 0 /\ X_1 + X_4 - 3 >= 0 /\ X_1 - X_3 - 1 >= 0 /\ X_3 - 1 >= 0 /\ X_1 + X_3 - 3 >= 0 /\ X_1 - X_2 >= 0 /\ X_1 - 2 >= 0
  For symbol evalperfectbb4in: X_1 - X_4 >= 0 /\ X_1 - X_3 - 1 >= 0 /\ X_3 - 1 >= 0 /\ X_1 + X_3 - 3 >= 0 /\ X_1 - X_2 >= 0 /\ X_1 - 2 >= 0
  For symbol evalperfectbb5in: X_3 - X_4 - 1 >= 0 /\ X_1 - X_4 - 2 >= 0 /\ X_1 - X_3 - 1 >= 0 /\ X_3 - 1 >= 0 /\ X_1 + X_3 - 3 >= 0 /\ X_1 - X_2 >= 0 /\ X_1 - 2 >= 0
  For symbol evalperfectbb8in: X_1 - X_3 - 1 >= 0 /\ X_3 >= 0 /\ X_1 + X_3 - 2 >= 0 /\ X_1 - X_2 >= 0 /\ X_1 - 2 >= 0


This yielded the following problem:
7:	T:
		(6*a + 6, 1)    evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ c - d - 1 >= 0 /\ a - d - 2 >= 0 /\ a - c - 1 >= 0 /\ c - 1 >= 0 /\ a + c - 3 >= 0 /\ a - b >= 0 /\ a - 2 >= 0 /\ d >= 1 ]
		(6*a + 6, 1)    evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ c - d - 1 >= 0 /\ a - d - 2 >= 0 /\ a - c - 1 >= 0 /\ c - 1 >= 0 /\ a + c - 3 >= 0 /\ a - b >= 0 /\ a - 2 >= 0 /\ 0 >= d + 1 ]
		(6*a + 6, 1)    evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b - c, c - 1, d) [ c - d - 1 >= 0 /\ a - d - 2 >= 0 /\ a - c - 1 >= 0 /\ c - 1 >= 0 /\ a + c - 3 >= 0 /\ a - b >= 0 /\ a - 2 >= 0 /\ d = 0 ]
		(?, 1)          evalperfectbb3in(a, b, c, d) -> evalperfectbb4in(a, b, c, d - c) [ a - d >= 0 /\ d - 1 >= 0 /\ c + d - 2 >= 0 /\ -c + d >= 0 /\ a + d - 3 >= 0 /\ a - c - 1 >= 0 /\ c - 1 >= 0 /\ a + c - 3 >= 0 /\ a - b >= 0 /\ a - 2 >= 0 ]
		(6*a + 6, 1)    evalperfectbb4in(a, b, c, d) -> evalperfectbb5in(a, b, c, d) [ a - d >= 0 /\ a - c - 1 >= 0 /\ c - 1 >= 0 /\ a + c - 3 >= 0 /\ a - b >= 0 /\ a - 2 >= 0 /\ c >= d + 1 ]
		(?, 1)          evalperfectbb4in(a, b, c, d) -> evalperfectbb3in(a, b, c, d) [ a - d >= 0 /\ a - c - 1 >= 0 /\ c - 1 >= 0 /\ a + c - 3 >= 0 /\ a - b >= 0 /\ a - 2 >= 0 /\ d >= c ]
		(3*a + 3, 1)    evalperfectbb8in(a, b, c, d) -> evalperfectbb4in(a, b, c, a) [ a - c - 1 >= 0 /\ c >= 0 /\ a + c - 2 >= 0 /\ a - b >= 0 /\ a - 2 >= 0 /\ c >= 1 ]
		(1, 1)          evalperfectbb1in(a, b, c, d) -> evalperfectbb8in(a, a, a - 1, d) [ a - 2 >= 0 ]
		(1, 1)          evalperfectentryin(a, b, c, d) -> evalperfectbb1in(a, b, c, d) [ a >= 2 ]
		(1, 1)          evalperfectstart(a, b, c, d) -> evalperfectentryin(a, b, c, d)
	start location:	evalperfectstart
	leaf cost:	6

A polynomial rank function with
	Pol(evalperfectbb4in) = 2*V_4
	Pol(evalperfectbb3in) = 2*V_4 - 1
and size complexities
	S("evalperfectstart(a, b, c, d) -> evalperfectentryin(a, b, c, d)", 0-0) = a
	S("evalperfectstart(a, b, c, d) -> evalperfectentryin(a, b, c, d)", 0-1) = b
	S("evalperfectstart(a, b, c, d) -> evalperfectentryin(a, b, c, d)", 0-2) = c
	S("evalperfectstart(a, b, c, d) -> evalperfectentryin(a, b, c, d)", 0-3) = d
	S("evalperfectentryin(a, b, c, d) -> evalperfectbb1in(a, b, c, d) [ a >= 2 ]", 0-0) = a
	S("evalperfectentryin(a, b, c, d) -> evalperfectbb1in(a, b, c, d) [ a >= 2 ]", 0-1) = b
	S("evalperfectentryin(a, b, c, d) -> evalperfectbb1in(a, b, c, d) [ a >= 2 ]", 0-2) = c
	S("evalperfectentryin(a, b, c, d) -> evalperfectbb1in(a, b, c, d) [ a >= 2 ]", 0-3) = d
	S("evalperfectbb1in(a, b, c, d) -> evalperfectbb8in(a, a, a - 1, d) [ a - 2 >= 0 ]", 0-0) = a
	S("evalperfectbb1in(a, b, c, d) -> evalperfectbb8in(a, a, a - 1, d) [ a - 2 >= 0 ]", 0-1) = a
	S("evalperfectbb1in(a, b, c, d) -> evalperfectbb8in(a, a, a - 1, d) [ a - 2 >= 0 ]", 0-2) = a
	S("evalperfectbb1in(a, b, c, d) -> evalperfectbb8in(a, a, a - 1, d) [ a - 2 >= 0 ]", 0-3) = d
	S("evalperfectbb8in(a, b, c, d) -> evalperfectbb4in(a, b, c, a) [ a - c - 1 >= 0 /\\ c >= 0 /\\ a + c - 2 >= 0 /\\ a - b >= 0 /\\ a - 2 >= 0 /\\ c >= 1 ]", 0-0) = a
	S("evalperfectbb8in(a, b, c, d) -> evalperfectbb4in(a, b, c, a) [ a - c - 1 >= 0 /\\ c >= 0 /\\ a + c - 2 >= 0 /\\ a - b >= 0 /\\ a - 2 >= 0 /\\ c >= 1 ]", 0-1) = 7*a + 6*a^2
	S("evalperfectbb8in(a, b, c, d) -> evalperfectbb4in(a, b, c, a) [ a - c - 1 >= 0 /\\ c >= 0 /\\ a + c - 2 >= 0 /\\ a - b >= 0 /\\ a - 2 >= 0 /\\ c >= 1 ]", 0-2) = a
	S("evalperfectbb8in(a, b, c, d) -> evalperfectbb4in(a, b, c, a) [ a - c - 1 >= 0 /\\ c >= 0 /\\ a + c - 2 >= 0 /\\ a - b >= 0 /\\ a - 2 >= 0 /\\ c >= 1 ]", 0-3) = a
	S("evalperfectbb4in(a, b, c, d) -> evalperfectbb3in(a, b, c, d) [ a - d >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ a + c - 3 >= 0 /\\ a - b >= 0 /\\ a - 2 >= 0 /\\ d >= c ]", 0-0) = a
	S("evalperfectbb4in(a, b, c, d) -> evalperfectbb3in(a, b, c, d) [ a - d >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ a + c - 3 >= 0 /\\ a - b >= 0 /\\ a - 2 >= 0 /\\ d >= c ]", 0-1) = 7*a + 6*a^2
	S("evalperfectbb4in(a, b, c, d) -> evalperfectbb3in(a, b, c, d) [ a - d >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ a + c - 3 >= 0 /\\ a - b >= 0 /\\ a - 2 >= 0 /\\ d >= c ]", 0-2) = a
	S("evalperfectbb4in(a, b, c, d) -> evalperfectbb3in(a, b, c, d) [ a - d >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ a + c - 3 >= 0 /\\ a - b >= 0 /\\ a - 2 >= 0 /\\ d >= c ]", 0-3) = a
	S("evalperfectbb4in(a, b, c, d) -> evalperfectbb5in(a, b, c, d) [ a - d >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ a + c - 3 >= 0 /\\ a - b >= 0 /\\ a - 2 >= 0 /\\ c >= d + 1 ]", 0-0) = a
	S("evalperfectbb4in(a, b, c, d) -> evalperfectbb5in(a, b, c, d) [ a - d >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ a + c - 3 >= 0 /\\ a - b >= 0 /\\ a - 2 >= 0 /\\ c >= d + 1 ]", 0-1) = 7*a + 6*a^2
	S("evalperfectbb4in(a, b, c, d) -> evalperfectbb5in(a, b, c, d) [ a - d >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ a + c - 3 >= 0 /\\ a - b >= 0 /\\ a - 2 >= 0 /\\ c >= d + 1 ]", 0-2) = a
	S("evalperfectbb4in(a, b, c, d) -> evalperfectbb5in(a, b, c, d) [ a - d >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ a + c - 3 >= 0 /\\ a - b >= 0 /\\ a - 2 >= 0 /\\ c >= d + 1 ]", 0-3) = a
	S("evalperfectbb3in(a, b, c, d) -> evalperfectbb4in(a, b, c, d - c) [ a - d >= 0 /\\ d - 1 >= 0 /\\ c + d - 2 >= 0 /\\ -c + d >= 0 /\\ a + d - 3 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ a + c - 3 >= 0 /\\ a - b >= 0 /\\ a - 2 >= 0 ]", 0-0) = a
	S("evalperfectbb3in(a, b, c, d) -> evalperfectbb4in(a, b, c, d - c) [ a - d >= 0 /\\ d - 1 >= 0 /\\ c + d - 2 >= 0 /\\ -c + d >= 0 /\\ a + d - 3 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ a + c - 3 >= 0 /\\ a - b >= 0 /\\ a - 2 >= 0 ]", 0-1) = 7*a + 6*a^2
	S("evalperfectbb3in(a, b, c, d) -> evalperfectbb4in(a, b, c, d - c) [ a - d >= 0 /\\ d - 1 >= 0 /\\ c + d - 2 >= 0 /\\ -c + d >= 0 /\\ a + d - 3 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ a + c - 3 >= 0 /\\ a - b >= 0 /\\ a - 2 >= 0 ]", 0-2) = a
	S("evalperfectbb3in(a, b, c, d) -> evalperfectbb4in(a, b, c, d - c) [ a - d >= 0 /\\ d - 1 >= 0 /\\ c + d - 2 >= 0 /\\ -c + d >= 0 /\\ a + d - 3 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ a + c - 3 >= 0 /\\ a - b >= 0 /\\ a - 2 >= 0 ]", 0-3) = a
	S("evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b - c, c - 1, d) [ c - d - 1 >= 0 /\\ a - d - 2 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ a + c - 3 >= 0 /\\ a - b >= 0 /\\ a - 2 >= 0 /\\ d = 0 ]", 0-0) = a
	S("evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b - c, c - 1, d) [ c - d - 1 >= 0 /\\ a - d - 2 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ a + c - 3 >= 0 /\\ a - b >= 0 /\\ a - 2 >= 0 /\\ d = 0 ]", 0-1) = 7*a + 6*a^2
	S("evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b - c, c - 1, d) [ c - d - 1 >= 0 /\\ a - d - 2 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ a + c - 3 >= 0 /\\ a - b >= 0 /\\ a - 2 >= 0 /\\ d = 0 ]", 0-2) = a
	S("evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b - c, c - 1, d) [ c - d - 1 >= 0 /\\ a - d - 2 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ a + c - 3 >= 0 /\\ a - b >= 0 /\\ a - 2 >= 0 /\\ d = 0 ]", 0-3) = 0
	S("evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ c - d - 1 >= 0 /\\ a - d - 2 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ a + c - 3 >= 0 /\\ a - b >= 0 /\\ a - 2 >= 0 /\\ 0 >= d + 1 ]", 0-0) = a
	S("evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ c - d - 1 >= 0 /\\ a - d - 2 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ a + c - 3 >= 0 /\\ a - b >= 0 /\\ a - 2 >= 0 /\\ 0 >= d + 1 ]", 0-1) = 7*a + 6*a^2
	S("evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ c - d - 1 >= 0 /\\ a - d - 2 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ a + c - 3 >= 0 /\\ a - b >= 0 /\\ a - 2 >= 0 /\\ 0 >= d + 1 ]", 0-2) = a
	S("evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ c - d - 1 >= 0 /\\ a - d - 2 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ a + c - 3 >= 0 /\\ a - b >= 0 /\\ a - 2 >= 0 /\\ 0 >= d + 1 ]", 0-3) = a
	S("evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ c - d - 1 >= 0 /\\ a - d - 2 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ a + c - 3 >= 0 /\\ a - b >= 0 /\\ a - 2 >= 0 /\\ d >= 1 ]", 0-0) = a
	S("evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ c - d - 1 >= 0 /\\ a - d - 2 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ a + c - 3 >= 0 /\\ a - b >= 0 /\\ a - 2 >= 0 /\\ d >= 1 ]", 0-1) = 7*a + 6*a^2
	S("evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ c - d - 1 >= 0 /\\ a - d - 2 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ a + c - 3 >= 0 /\\ a - b >= 0 /\\ a - 2 >= 0 /\\ d >= 1 ]", 0-2) = a
	S("evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ c - d - 1 >= 0 /\\ a - d - 2 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ a + c - 3 >= 0 /\\ a - b >= 0 /\\ a - 2 >= 0 /\\ d >= 1 ]", 0-3) = a
orients the transitions
	evalperfectbb4in(a, b, c, d) -> evalperfectbb3in(a, b, c, d) [ a - d >= 0 /\ a - c - 1 >= 0 /\ c - 1 >= 0 /\ a + c - 3 >= 0 /\ a - b >= 0 /\ a - 2 >= 0 /\ d >= c ]
	evalperfectbb3in(a, b, c, d) -> evalperfectbb4in(a, b, c, d - c) [ a - d >= 0 /\ d - 1 >= 0 /\ c + d - 2 >= 0 /\ -c + d >= 0 /\ a + d - 3 >= 0 /\ a - c - 1 >= 0 /\ c - 1 >= 0 /\ a + c - 3 >= 0 /\ a - b >= 0 /\ a - 2 >= 0 ]
weakly and the transitions
	evalperfectbb4in(a, b, c, d) -> evalperfectbb3in(a, b, c, d) [ a - d >= 0 /\ a - c - 1 >= 0 /\ c - 1 >= 0 /\ a + c - 3 >= 0 /\ a - b >= 0 /\ a - 2 >= 0 /\ d >= c ]
	evalperfectbb3in(a, b, c, d) -> evalperfectbb4in(a, b, c, d - c) [ a - d >= 0 /\ d - 1 >= 0 /\ c + d - 2 >= 0 /\ -c + d >= 0 /\ a + d - 3 >= 0 /\ a - c - 1 >= 0 /\ c - 1 >= 0 /\ a + c - 3 >= 0 /\ a - b >= 0 /\ a - 2 >= 0 ]
strictly and produces the following problem:
8:	T:
		(6*a + 6, 1)        evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ c - d - 1 >= 0 /\ a - d - 2 >= 0 /\ a - c - 1 >= 0 /\ c - 1 >= 0 /\ a + c - 3 >= 0 /\ a - b >= 0 /\ a - 2 >= 0 /\ d >= 1 ]
		(6*a + 6, 1)        evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b, c - 1, d) [ c - d - 1 >= 0 /\ a - d - 2 >= 0 /\ a - c - 1 >= 0 /\ c - 1 >= 0 /\ a + c - 3 >= 0 /\ a - b >= 0 /\ a - 2 >= 0 /\ 0 >= d + 1 ]
		(6*a + 6, 1)        evalperfectbb5in(a, b, c, d) -> evalperfectbb8in(a, b - c, c - 1, d) [ c - d - 1 >= 0 /\ a - d - 2 >= 0 /\ a - c - 1 >= 0 /\ c - 1 >= 0 /\ a + c - 3 >= 0 /\ a - b >= 0 /\ a - 2 >= 0 /\ d = 0 ]
		(6*a^2 + 6*a, 1)    evalperfectbb3in(a, b, c, d) -> evalperfectbb4in(a, b, c, d - c) [ a - d >= 0 /\ d - 1 >= 0 /\ c + d - 2 >= 0 /\ -c + d >= 0 /\ a + d - 3 >= 0 /\ a - c - 1 >= 0 /\ c - 1 >= 0 /\ a + c - 3 >= 0 /\ a - b >= 0 /\ a - 2 >= 0 ]
		(6*a + 6, 1)        evalperfectbb4in(a, b, c, d) -> evalperfectbb5in(a, b, c, d) [ a - d >= 0 /\ a - c - 1 >= 0 /\ c - 1 >= 0 /\ a + c - 3 >= 0 /\ a - b >= 0 /\ a - 2 >= 0 /\ c >= d + 1 ]
		(6*a^2 + 6*a, 1)    evalperfectbb4in(a, b, c, d) -> evalperfectbb3in(a, b, c, d) [ a - d >= 0 /\ a - c - 1 >= 0 /\ c - 1 >= 0 /\ a + c - 3 >= 0 /\ a - b >= 0 /\ a - 2 >= 0 /\ d >= c ]
		(3*a + 3, 1)        evalperfectbb8in(a, b, c, d) -> evalperfectbb4in(a, b, c, a) [ a - c - 1 >= 0 /\ c >= 0 /\ a + c - 2 >= 0 /\ a - b >= 0 /\ a - 2 >= 0 /\ c >= 1 ]
		(1, 1)              evalperfectbb1in(a, b, c, d) -> evalperfectbb8in(a, a, a - 1, d) [ a - 2 >= 0 ]
		(1, 1)              evalperfectentryin(a, b, c, d) -> evalperfectbb1in(a, b, c, d) [ a >= 2 ]
		(1, 1)              evalperfectstart(a, b, c, d) -> evalperfectentryin(a, b, c, d)
	start location:	evalperfectstart
	leaf cost:	6

Complexity upper bound 39*a + 12*a^2 + 36

Time: 1.035 sec (SMT: 0.976 sec)