YES(?, 172748*b + 384*b^2 + 129349)

Initial complexity problem:
1:	T:
		(1, 1)    evalinsertsortstart(a, b, c, d) -> evalinsertsortentryin(a, b, c, d)
		(?, 1)    evalinsertsortentryin(a, b, c, d) -> evalinsertsortbb5in(1, b, c, d)
		(?, 1)    evalinsertsortbb5in(a, b, c, d) -> evalinsertsortbbin(a, b, c, d) [ b >= a + 1 ]
		(?, 1)    evalinsertsortbb5in(a, b, c, d) -> evalinsertsortreturnin(a, b, c, d) [ a >= b ]
		(?, 1)    evalinsertsortbbin(a, b, c, d) -> evalinsertsortbb2in(a, b, e, a - 1)
		(?, 1)    evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ 0 >= d + 1 ]
		(?, 1)    evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb3in(a, b, c, d) [ d >= 0 ]
		(?, 1)    evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb1in(a, b, c, d) [ e >= c + 1 ]
		(?, 1)    evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ c >= e ]
		(?, 1)    evalinsertsortbb1in(a, b, c, d) -> evalinsertsortbb2in(a, b, c, d - 1)
		(?, 1)    evalinsertsortbb4in(a, b, c, d) -> evalinsertsortbb5in(a + 1, b, c, d)
		(?, 1)    evalinsertsortreturnin(a, b, c, d) -> evalinsertsortstop(a, b, c, d)
	start location:	evalinsertsortstart
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(1, 1)    evalinsertsortstart(a, b, c, d) -> evalinsertsortentryin(a, b, c, d)
		(?, 1)    evalinsertsortentryin(a, b, c, d) -> evalinsertsortbb5in(1, b, c, d)
		(?, 1)    evalinsertsortbb5in(a, b, c, d) -> evalinsertsortbbin(a, b, c, d) [ b >= a + 1 ]
		(?, 1)    evalinsertsortbbin(a, b, c, d) -> evalinsertsortbb2in(a, b, e, a - 1)
		(?, 1)    evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ 0 >= d + 1 ]
		(?, 1)    evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb3in(a, b, c, d) [ d >= 0 ]
		(?, 1)    evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb1in(a, b, c, d) [ e >= c + 1 ]
		(?, 1)    evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ c >= e ]
		(?, 1)    evalinsertsortbb1in(a, b, c, d) -> evalinsertsortbb2in(a, b, c, d - 1)
		(?, 1)    evalinsertsortbb4in(a, b, c, d) -> evalinsertsortbb5in(a + 1, b, c, d)
	start location:	evalinsertsortstart
	leaf cost:	2

Repeatedly propagating knowledge in problem 2 produces the following problem:
3:	T:
		(1, 1)    evalinsertsortstart(a, b, c, d) -> evalinsertsortentryin(a, b, c, d)
		(1, 1)    evalinsertsortentryin(a, b, c, d) -> evalinsertsortbb5in(1, b, c, d)
		(?, 1)    evalinsertsortbb5in(a, b, c, d) -> evalinsertsortbbin(a, b, c, d) [ b >= a + 1 ]
		(?, 1)    evalinsertsortbbin(a, b, c, d) -> evalinsertsortbb2in(a, b, e, a - 1)
		(?, 1)    evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ 0 >= d + 1 ]
		(?, 1)    evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb3in(a, b, c, d) [ d >= 0 ]
		(?, 1)    evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb1in(a, b, c, d) [ e >= c + 1 ]
		(?, 1)    evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ c >= e ]
		(?, 1)    evalinsertsortbb1in(a, b, c, d) -> evalinsertsortbb2in(a, b, c, d - 1)
		(?, 1)    evalinsertsortbb4in(a, b, c, d) -> evalinsertsortbb5in(a + 1, b, c, d)
	start location:	evalinsertsortstart
	leaf cost:	2

A polynomial rank function with
	Pol(evalinsertsortstart) = 4*V_2 - 3
	Pol(evalinsertsortentryin) = 4*V_2 - 3
	Pol(evalinsertsortbb5in) = -4*V_1 + 4*V_2 + 1
	Pol(evalinsertsortbbin) = -4*V_1 + 4*V_2
	Pol(evalinsertsortbb2in) = -4*V_1 + 4*V_2 - 1
	Pol(evalinsertsortbb4in) = -4*V_1 + 4*V_2 - 2
	Pol(evalinsertsortbb3in) = -4*V_1 + 4*V_2 - 1
	Pol(evalinsertsortbb1in) = -4*V_1 + 4*V_2 - 1
orients all transitions weakly and the transition
	evalinsertsortbb5in(a, b, c, d) -> evalinsertsortbbin(a, b, c, d) [ b >= a + 1 ]
strictly and produces the following problem:
4:	T:
		(1, 1)          evalinsertsortstart(a, b, c, d) -> evalinsertsortentryin(a, b, c, d)
		(1, 1)          evalinsertsortentryin(a, b, c, d) -> evalinsertsortbb5in(1, b, c, d)
		(4*b + 3, 1)    evalinsertsortbb5in(a, b, c, d) -> evalinsertsortbbin(a, b, c, d) [ b >= a + 1 ]
		(?, 1)          evalinsertsortbbin(a, b, c, d) -> evalinsertsortbb2in(a, b, e, a - 1)
		(?, 1)          evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ 0 >= d + 1 ]
		(?, 1)          evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb3in(a, b, c, d) [ d >= 0 ]
		(?, 1)          evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb1in(a, b, c, d) [ e >= c + 1 ]
		(?, 1)          evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ c >= e ]
		(?, 1)          evalinsertsortbb1in(a, b, c, d) -> evalinsertsortbb2in(a, b, c, d - 1)
		(?, 1)          evalinsertsortbb4in(a, b, c, d) -> evalinsertsortbb5in(a + 1, b, c, d)
	start location:	evalinsertsortstart
	leaf cost:	2

Repeatedly propagating knowledge in problem 4 produces the following problem:
5:	T:
		(1, 1)          evalinsertsortstart(a, b, c, d) -> evalinsertsortentryin(a, b, c, d)
		(1, 1)          evalinsertsortentryin(a, b, c, d) -> evalinsertsortbb5in(1, b, c, d)
		(4*b + 3, 1)    evalinsertsortbb5in(a, b, c, d) -> evalinsertsortbbin(a, b, c, d) [ b >= a + 1 ]
		(4*b + 3, 1)    evalinsertsortbbin(a, b, c, d) -> evalinsertsortbb2in(a, b, e, a - 1)
		(?, 1)          evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ 0 >= d + 1 ]
		(?, 1)          evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb3in(a, b, c, d) [ d >= 0 ]
		(?, 1)          evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb1in(a, b, c, d) [ e >= c + 1 ]
		(?, 1)          evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ c >= e ]
		(?, 1)          evalinsertsortbb1in(a, b, c, d) -> evalinsertsortbb2in(a, b, c, d - 1)
		(?, 1)          evalinsertsortbb4in(a, b, c, d) -> evalinsertsortbb5in(a + 1, b, c, d)
	start location:	evalinsertsortstart
	leaf cost:	2

A polynomial rank function with
	Pol(evalinsertsortbb4in) = 1
	Pol(evalinsertsortbb5in) = 0
	Pol(evalinsertsortbb3in) = 2
	Pol(evalinsertsortbb1in) = 2
	Pol(evalinsertsortbb2in) = 2
and size complexities
	S("evalinsertsortbb4in(a, b, c, d) -> evalinsertsortbb5in(a + 1, b, c, d)", 0-0) = ?
	S("evalinsertsortbb4in(a, b, c, d) -> evalinsertsortbb5in(a + 1, b, c, d)", 0-1) = b
	S("evalinsertsortbb4in(a, b, c, d) -> evalinsertsortbb5in(a + 1, b, c, d)", 0-2) = ?
	S("evalinsertsortbb4in(a, b, c, d) -> evalinsertsortbb5in(a + 1, b, c, d)", 0-3) = ?
	S("evalinsertsortbb1in(a, b, c, d) -> evalinsertsortbb2in(a, b, c, d - 1)", 0-0) = ?
	S("evalinsertsortbb1in(a, b, c, d) -> evalinsertsortbb2in(a, b, c, d - 1)", 0-1) = b
	S("evalinsertsortbb1in(a, b, c, d) -> evalinsertsortbb2in(a, b, c, d - 1)", 0-2) = ?
	S("evalinsertsortbb1in(a, b, c, d) -> evalinsertsortbb2in(a, b, c, d - 1)", 0-3) = ?
	S("evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ c >= e ]", 0-0) = ?
	S("evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ c >= e ]", 0-1) = b
	S("evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ c >= e ]", 0-2) = ?
	S("evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ c >= e ]", 0-3) = ?
	S("evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb1in(a, b, c, d) [ e >= c + 1 ]", 0-0) = ?
	S("evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb1in(a, b, c, d) [ e >= c + 1 ]", 0-1) = b
	S("evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb1in(a, b, c, d) [ e >= c + 1 ]", 0-2) = ?
	S("evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb1in(a, b, c, d) [ e >= c + 1 ]", 0-3) = ?
	S("evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb3in(a, b, c, d) [ d >= 0 ]", 0-0) = ?
	S("evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb3in(a, b, c, d) [ d >= 0 ]", 0-1) = b
	S("evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb3in(a, b, c, d) [ d >= 0 ]", 0-2) = ?
	S("evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb3in(a, b, c, d) [ d >= 0 ]", 0-3) = ?
	S("evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ 0 >= d + 1 ]", 0-0) = ?
	S("evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ 0 >= d + 1 ]", 0-1) = b
	S("evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ 0 >= d + 1 ]", 0-2) = ?
	S("evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ 0 >= d + 1 ]", 0-3) = ?
	S("evalinsertsortbbin(a, b, c, d) -> evalinsertsortbb2in(a, b, e, a - 1)", 0-0) = ?
	S("evalinsertsortbbin(a, b, c, d) -> evalinsertsortbb2in(a, b, e, a - 1)", 0-1) = b
	S("evalinsertsortbbin(a, b, c, d) -> evalinsertsortbb2in(a, b, e, a - 1)", 0-2) = ?
	S("evalinsertsortbbin(a, b, c, d) -> evalinsertsortbb2in(a, b, e, a - 1)", 0-3) = ?
	S("evalinsertsortbb5in(a, b, c, d) -> evalinsertsortbbin(a, b, c, d) [ b >= a + 1 ]", 0-0) = ?
	S("evalinsertsortbb5in(a, b, c, d) -> evalinsertsortbbin(a, b, c, d) [ b >= a + 1 ]", 0-1) = b
	S("evalinsertsortbb5in(a, b, c, d) -> evalinsertsortbbin(a, b, c, d) [ b >= a + 1 ]", 0-2) = ?
	S("evalinsertsortbb5in(a, b, c, d) -> evalinsertsortbbin(a, b, c, d) [ b >= a + 1 ]", 0-3) = ?
	S("evalinsertsortentryin(a, b, c, d) -> evalinsertsortbb5in(1, b, c, d)", 0-0) = 1
	S("evalinsertsortentryin(a, b, c, d) -> evalinsertsortbb5in(1, b, c, d)", 0-1) = b
	S("evalinsertsortentryin(a, b, c, d) -> evalinsertsortbb5in(1, b, c, d)", 0-2) = c
	S("evalinsertsortentryin(a, b, c, d) -> evalinsertsortbb5in(1, b, c, d)", 0-3) = d
	S("evalinsertsortstart(a, b, c, d) -> evalinsertsortentryin(a, b, c, d)", 0-0) = a
	S("evalinsertsortstart(a, b, c, d) -> evalinsertsortentryin(a, b, c, d)", 0-1) = b
	S("evalinsertsortstart(a, b, c, d) -> evalinsertsortentryin(a, b, c, d)", 0-2) = c
	S("evalinsertsortstart(a, b, c, d) -> evalinsertsortentryin(a, b, c, d)", 0-3) = d
orients the transitions
	evalinsertsortbb4in(a, b, c, d) -> evalinsertsortbb5in(a + 1, b, c, d)
	evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ c >= e ]
	evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb1in(a, b, c, d) [ e >= c + 1 ]
	evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ 0 >= d + 1 ]
	evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb3in(a, b, c, d) [ d >= 0 ]
	evalinsertsortbb1in(a, b, c, d) -> evalinsertsortbb2in(a, b, c, d - 1)
weakly and the transitions
	evalinsertsortbb4in(a, b, c, d) -> evalinsertsortbb5in(a + 1, b, c, d)
	evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ c >= e ]
	evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ 0 >= d + 1 ]
strictly and produces the following problem:
6:	T:
		(1, 1)          evalinsertsortstart(a, b, c, d) -> evalinsertsortentryin(a, b, c, d)
		(1, 1)          evalinsertsortentryin(a, b, c, d) -> evalinsertsortbb5in(1, b, c, d)
		(4*b + 3, 1)    evalinsertsortbb5in(a, b, c, d) -> evalinsertsortbbin(a, b, c, d) [ b >= a + 1 ]
		(4*b + 3, 1)    evalinsertsortbbin(a, b, c, d) -> evalinsertsortbb2in(a, b, e, a - 1)
		(8*b + 6, 1)    evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ 0 >= d + 1 ]
		(?, 1)          evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb3in(a, b, c, d) [ d >= 0 ]
		(?, 1)          evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb1in(a, b, c, d) [ e >= c + 1 ]
		(8*b + 6, 1)    evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ c >= e ]
		(?, 1)          evalinsertsortbb1in(a, b, c, d) -> evalinsertsortbb2in(a, b, c, d - 1)
		(8*b + 6, 1)    evalinsertsortbb4in(a, b, c, d) -> evalinsertsortbb5in(a + 1, b, c, d)
	start location:	evalinsertsortstart
	leaf cost:	2

A polynomial rank function with
	Pol(evalinsertsortbb3in) = 4*V_4 - 1
	Pol(evalinsertsortbb1in) = 4*V_4 - 2
	Pol(evalinsertsortbb2in) = 4*V_4 + 1
and size complexities
	S("evalinsertsortbb4in(a, b, c, d) -> evalinsertsortbb5in(a + 1, b, c, d)", 0-0) = 8*b + 448
	S("evalinsertsortbb4in(a, b, c, d) -> evalinsertsortbb5in(a + 1, b, c, d)", 0-1) = b
	S("evalinsertsortbb4in(a, b, c, d) -> evalinsertsortbb5in(a + 1, b, c, d)", 0-2) = ?
	S("evalinsertsortbb4in(a, b, c, d) -> evalinsertsortbb5in(a + 1, b, c, d)", 0-3) = ?
	S("evalinsertsortbb1in(a, b, c, d) -> evalinsertsortbb2in(a, b, c, d - 1)", 0-0) = 8*b + 448
	S("evalinsertsortbb1in(a, b, c, d) -> evalinsertsortbb2in(a, b, c, d - 1)", 0-1) = b
	S("evalinsertsortbb1in(a, b, c, d) -> evalinsertsortbb2in(a, b, c, d - 1)", 0-2) = ?
	S("evalinsertsortbb1in(a, b, c, d) -> evalinsertsortbb2in(a, b, c, d - 1)", 0-3) = ?
	S("evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ c >= e ]", 0-0) = 8*b + 448
	S("evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ c >= e ]", 0-1) = b
	S("evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ c >= e ]", 0-2) = ?
	S("evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ c >= e ]", 0-3) = ?
	S("evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb1in(a, b, c, d) [ e >= c + 1 ]", 0-0) = 8*b + 448
	S("evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb1in(a, b, c, d) [ e >= c + 1 ]", 0-1) = b
	S("evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb1in(a, b, c, d) [ e >= c + 1 ]", 0-2) = ?
	S("evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb1in(a, b, c, d) [ e >= c + 1 ]", 0-3) = ?
	S("evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb3in(a, b, c, d) [ d >= 0 ]", 0-0) = 8*b + 448
	S("evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb3in(a, b, c, d) [ d >= 0 ]", 0-1) = b
	S("evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb3in(a, b, c, d) [ d >= 0 ]", 0-2) = ?
	S("evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb3in(a, b, c, d) [ d >= 0 ]", 0-3) = ?
	S("evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ 0 >= d + 1 ]", 0-0) = 8*b + 448
	S("evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ 0 >= d + 1 ]", 0-1) = b
	S("evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ 0 >= d + 1 ]", 0-2) = ?
	S("evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ 0 >= d + 1 ]", 0-3) = ?
	S("evalinsertsortbbin(a, b, c, d) -> evalinsertsortbb2in(a, b, e, a - 1)", 0-0) = 8*b + 448
	S("evalinsertsortbbin(a, b, c, d) -> evalinsertsortbb2in(a, b, e, a - 1)", 0-1) = b
	S("evalinsertsortbbin(a, b, c, d) -> evalinsertsortbb2in(a, b, e, a - 1)", 0-2) = ?
	S("evalinsertsortbbin(a, b, c, d) -> evalinsertsortbb2in(a, b, e, a - 1)", 0-3) = 8*b + 3592
	S("evalinsertsortbb5in(a, b, c, d) -> evalinsertsortbbin(a, b, c, d) [ b >= a + 1 ]", 0-0) = 8*b + 448
	S("evalinsertsortbb5in(a, b, c, d) -> evalinsertsortbbin(a, b, c, d) [ b >= a + 1 ]", 0-1) = b
	S("evalinsertsortbb5in(a, b, c, d) -> evalinsertsortbbin(a, b, c, d) [ b >= a + 1 ]", 0-2) = ?
	S("evalinsertsortbb5in(a, b, c, d) -> evalinsertsortbbin(a, b, c, d) [ b >= a + 1 ]", 0-3) = ?
	S("evalinsertsortentryin(a, b, c, d) -> evalinsertsortbb5in(1, b, c, d)", 0-0) = 1
	S("evalinsertsortentryin(a, b, c, d) -> evalinsertsortbb5in(1, b, c, d)", 0-1) = b
	S("evalinsertsortentryin(a, b, c, d) -> evalinsertsortbb5in(1, b, c, d)", 0-2) = c
	S("evalinsertsortentryin(a, b, c, d) -> evalinsertsortbb5in(1, b, c, d)", 0-3) = d
	S("evalinsertsortstart(a, b, c, d) -> evalinsertsortentryin(a, b, c, d)", 0-0) = a
	S("evalinsertsortstart(a, b, c, d) -> evalinsertsortentryin(a, b, c, d)", 0-1) = b
	S("evalinsertsortstart(a, b, c, d) -> evalinsertsortentryin(a, b, c, d)", 0-2) = c
	S("evalinsertsortstart(a, b, c, d) -> evalinsertsortentryin(a, b, c, d)", 0-3) = d
orients the transitions
	evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb1in(a, b, c, d) [ e >= c + 1 ]
	evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb3in(a, b, c, d) [ d >= 0 ]
	evalinsertsortbb1in(a, b, c, d) -> evalinsertsortbb2in(a, b, c, d - 1)
weakly and the transition
	evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb3in(a, b, c, d) [ d >= 0 ]
strictly and produces the following problem:
7:	T:
		(1, 1)                            evalinsertsortstart(a, b, c, d) -> evalinsertsortentryin(a, b, c, d)
		(1, 1)                            evalinsertsortentryin(a, b, c, d) -> evalinsertsortbb5in(1, b, c, d)
		(4*b + 3, 1)                      evalinsertsortbb5in(a, b, c, d) -> evalinsertsortbbin(a, b, c, d) [ b >= a + 1 ]
		(4*b + 3, 1)                      evalinsertsortbbin(a, b, c, d) -> evalinsertsortbb2in(a, b, e, a - 1)
		(8*b + 6, 1)                      evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ 0 >= d + 1 ]
		(128*b^2 + 57572*b + 43107, 1)    evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb3in(a, b, c, d) [ d >= 0 ]
		(?, 1)                            evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb1in(a, b, c, d) [ e >= c + 1 ]
		(8*b + 6, 1)                      evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ c >= e ]
		(?, 1)                            evalinsertsortbb1in(a, b, c, d) -> evalinsertsortbb2in(a, b, c, d - 1)
		(8*b + 6, 1)                      evalinsertsortbb4in(a, b, c, d) -> evalinsertsortbb5in(a + 1, b, c, d)
	start location:	evalinsertsortstart
	leaf cost:	2

Repeatedly propagating knowledge in problem 7 produces the following problem:
8:	T:
		(1, 1)                            evalinsertsortstart(a, b, c, d) -> evalinsertsortentryin(a, b, c, d)
		(1, 1)                            evalinsertsortentryin(a, b, c, d) -> evalinsertsortbb5in(1, b, c, d)
		(4*b + 3, 1)                      evalinsertsortbb5in(a, b, c, d) -> evalinsertsortbbin(a, b, c, d) [ b >= a + 1 ]
		(4*b + 3, 1)                      evalinsertsortbbin(a, b, c, d) -> evalinsertsortbb2in(a, b, e, a - 1)
		(8*b + 6, 1)                      evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ 0 >= d + 1 ]
		(128*b^2 + 57572*b + 43107, 1)    evalinsertsortbb2in(a, b, c, d) -> evalinsertsortbb3in(a, b, c, d) [ d >= 0 ]
		(128*b^2 + 57572*b + 43107, 1)    evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb1in(a, b, c, d) [ e >= c + 1 ]
		(8*b + 6, 1)                      evalinsertsortbb3in(a, b, c, d) -> evalinsertsortbb4in(a, b, c, d) [ c >= e ]
		(128*b^2 + 57572*b + 43107, 1)    evalinsertsortbb1in(a, b, c, d) -> evalinsertsortbb2in(a, b, c, d - 1)
		(8*b + 6, 1)                      evalinsertsortbb4in(a, b, c, d) -> evalinsertsortbb5in(a + 1, b, c, d)
	start location:	evalinsertsortstart
	leaf cost:	2

Complexity upper bound 172748*b + 384*b^2 + 129349

Time: 0.279 sec (SMT: 0.260 sec)