YES(?, 78*a + 330*a^2 + 216*a^3 + 8)

Initial complexity problem:
1:	T:
		(1, 1)    evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)
		(?, 1)    evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, 0, c, d, e) [ a = 0 ]
		(?, 1)    evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\ f >= 0 /\ a >= 2*f /\ 2*f + 1 >= a ]
		(?, 1)    evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ 0 >= a + 1 /\ 0 >= f /\ 2*f >= a /\ a + 1 >= 2*f ]
		(?, 1)    evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ b >= 1 ]
		(?, 1)    evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortreturnin(a, b, c, d, e) [ 0 >= b ]
		(?, 1)    evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ a >= c + 1 ]
		(?, 1)    evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= a ]
		(?, 1)    evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c)
		(?, 1)    evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ b >= e + 1 ]
		(?, 1)    evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ e >= b ]
		(?, 1)    evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ f >= d + 1 ]
		(?, 1)    evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ d >= f ]
		(?, 1)    evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b)
		(?, 1)    evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e)
		(?, 1)    evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, 0, c, d, e) [ b = 0 ]
		(?, 1)    evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ b >= 1 /\ f >= 0 /\ b >= 2*f /\ 2*f + 1 >= b ]
		(?, 1)    evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ 0 >= b + 1 /\ 0 >= f /\ 2*f >= b /\ b + 1 >= 2*f ]
		(?, 1)    evalrealshellsortreturnin(a, b, c, d, e) -> evalrealshellsortstop(a, b, c, d, e)
	start location:	evalrealshellsortstart
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(1, 1)    evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)
		(?, 1)    evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\ f >= 0 /\ a >= 2*f /\ 2*f + 1 >= a ]
		(?, 1)    evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ b >= 1 ]
		(?, 1)    evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ a >= c + 1 ]
		(?, 1)    evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= a ]
		(?, 1)    evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c)
		(?, 1)    evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ b >= e + 1 ]
		(?, 1)    evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ e >= b ]
		(?, 1)    evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ f >= d + 1 ]
		(?, 1)    evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ d >= f ]
		(?, 1)    evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b)
		(?, 1)    evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e)
		(?, 1)    evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ b >= 1 /\ f >= 0 /\ b >= 2*f /\ 2*f + 1 >= b ]
	start location:	evalrealshellsortstart
	leaf cost:	6

Repeatedly propagating knowledge in problem 2 produces the following problem:
3:	T:
		(1, 1)    evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)
		(1, 1)    evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\ f >= 0 /\ a >= 2*f /\ 2*f + 1 >= a ]
		(?, 1)    evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ b >= 1 ]
		(?, 1)    evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ a >= c + 1 ]
		(?, 1)    evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= a ]
		(?, 1)    evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c)
		(?, 1)    evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ b >= e + 1 ]
		(?, 1)    evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ e >= b ]
		(?, 1)    evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ f >= d + 1 ]
		(?, 1)    evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ d >= f ]
		(?, 1)    evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b)
		(?, 1)    evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e)
		(?, 1)    evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ b >= 1 /\ f >= 0 /\ b >= 2*f /\ 2*f + 1 >= b ]
	start location:	evalrealshellsortstart
	leaf cost:	6

A polynomial rank function with
	Pol(evalrealshellsortstart) = 3*V_1
	Pol(evalrealshellsortentryin) = 3*V_1
	Pol(evalrealshellsortbb8in) = 6*V_2
	Pol(evalrealshellsortbb6in) = 6*V_2 - 1
	Pol(evalrealshellsortbb1in) = 6*V_2 - 1
	Pol(evalrealshellsortbb7in) = 6*V_2 - 2
	Pol(evalrealshellsortbb3in) = 6*V_2 - 1
	Pol(evalrealshellsortbb5in) = 6*V_2 - 1
	Pol(evalrealshellsortbb4in) = 6*V_2 - 1
	Pol(evalrealshellsortbb2in) = 6*V_2 - 1
orients all transitions weakly and the transitions
	evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ b >= 1 ]
	evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ b >= 1 /\ f >= 0 /\ b >= 2*f /\ 2*f + 1 >= b ]
strictly and produces the following problem:
4:	T:
		(1, 1)      evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)
		(1, 1)      evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\ f >= 0 /\ a >= 2*f /\ 2*f + 1 >= a ]
		(3*a, 1)    evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ b >= 1 ]
		(?, 1)      evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ a >= c + 1 ]
		(?, 1)      evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= a ]
		(?, 1)      evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c)
		(?, 1)      evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ b >= e + 1 ]
		(?, 1)      evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ e >= b ]
		(?, 1)      evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ f >= d + 1 ]
		(?, 1)      evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ d >= f ]
		(?, 1)      evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b)
		(?, 1)      evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e)
		(3*a, 1)    evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ b >= 1 /\ f >= 0 /\ b >= 2*f /\ 2*f + 1 >= b ]
	start location:	evalrealshellsortstart
	leaf cost:	6

A polynomial rank function with
	Pol(evalrealshellsortbb6in) = 1
	Pol(evalrealshellsortbb7in) = 0
	Pol(evalrealshellsortbb1in) = 1
	Pol(evalrealshellsortbb5in) = 1
	Pol(evalrealshellsortbb4in) = 1
	Pol(evalrealshellsortbb2in) = 1
	Pol(evalrealshellsortbb3in) = 1
and size complexities
	S("evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ b >= 1 /\\ f >= 0 /\\ b >= 2*f /\\ 2*f + 1 >= b ]", 0-0) = a
	S("evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ b >= 1 /\\ f >= 0 /\\ b >= 2*f /\\ 2*f + 1 >= b ]", 0-1) = ?
	S("evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ b >= 1 /\\ f >= 0 /\\ b >= 2*f /\\ 2*f + 1 >= b ]", 0-2) = ?
	S("evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ b >= 1 /\\ f >= 0 /\\ b >= 2*f /\\ 2*f + 1 >= b ]", 0-3) = ?
	S("evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ b >= 1 /\\ f >= 0 /\\ b >= 2*f /\\ 2*f + 1 >= b ]", 0-4) = ?
	S("evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e)", 0-0) = a
	S("evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e)", 0-1) = ?
	S("evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e)", 0-2) = ?
	S("evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e)", 0-3) = ?
	S("evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e)", 0-4) = ?
	S("evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b)", 0-0) = a
	S("evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b)", 0-1) = ?
	S("evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b)", 0-2) = ?
	S("evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b)", 0-3) = ?
	S("evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b)", 0-4) = ?
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ d >= f ]", 0-0) = a
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ d >= f ]", 0-1) = ?
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ d >= f ]", 0-2) = ?
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ d >= f ]", 0-3) = ?
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ d >= f ]", 0-4) = ?
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ f >= d + 1 ]", 0-0) = a
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ f >= d + 1 ]", 0-1) = ?
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ f >= d + 1 ]", 0-2) = ?
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ f >= d + 1 ]", 0-3) = ?
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ f >= d + 1 ]", 0-4) = ?
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ e >= b ]", 0-0) = a
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ e >= b ]", 0-1) = ?
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ e >= b ]", 0-2) = ?
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ e >= b ]", 0-3) = ?
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ e >= b ]", 0-4) = ?
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ b >= e + 1 ]", 0-0) = a
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ b >= e + 1 ]", 0-1) = ?
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ b >= e + 1 ]", 0-2) = ?
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ b >= e + 1 ]", 0-3) = ?
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ b >= e + 1 ]", 0-4) = ?
	S("evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c)", 0-0) = a
	S("evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c)", 0-1) = ?
	S("evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c)", 0-2) = ?
	S("evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c)", 0-3) = ?
	S("evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c)", 0-4) = ?
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= a ]", 0-0) = a
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= a ]", 0-1) = ?
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= a ]", 0-2) = ?
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= a ]", 0-3) = ?
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= a ]", 0-4) = ?
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ a >= c + 1 ]", 0-0) = a
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ a >= c + 1 ]", 0-1) = ?
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ a >= c + 1 ]", 0-2) = ?
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ a >= c + 1 ]", 0-3) = ?
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ a >= c + 1 ]", 0-4) = ?
	S("evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ b >= 1 ]", 0-0) = a
	S("evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ b >= 1 ]", 0-1) = ?
	S("evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ b >= 1 ]", 0-2) = 0
	S("evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ b >= 1 ]", 0-3) = ?
	S("evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ b >= 1 ]", 0-4) = ?
	S("evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\\ f >= 0 /\\ a >= 2*f /\\ 2*f + 1 >= a ]", 0-0) = a
	S("evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\\ f >= 0 /\\ a >= 2*f /\\ 2*f + 1 >= a ]", 0-1) = ?
	S("evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\\ f >= 0 /\\ a >= 2*f /\\ 2*f + 1 >= a ]", 0-2) = c
	S("evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\\ f >= 0 /\\ a >= 2*f /\\ 2*f + 1 >= a ]", 0-3) = d
	S("evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\\ f >= 0 /\\ a >= 2*f /\\ 2*f + 1 >= a ]", 0-4) = e
	S("evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)", 0-0) = a
	S("evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)", 0-1) = b
	S("evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)", 0-2) = c
	S("evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)", 0-3) = d
	S("evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)", 0-4) = e
orients the transitions
	evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= a ]
	evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ a >= c + 1 ]
	evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e)
	evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ d >= f ]
	evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ f >= d + 1 ]
	evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ b >= e + 1 ]
	evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ e >= b ]
	evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b)
	evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c)
weakly and the transition
	evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= a ]
strictly and produces the following problem:
5:	T:
		(1, 1)      evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)
		(1, 1)      evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\ f >= 0 /\ a >= 2*f /\ 2*f + 1 >= a ]
		(3*a, 1)    evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ b >= 1 ]
		(?, 1)      evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ a >= c + 1 ]
		(3*a, 1)    evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= a ]
		(?, 1)      evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c)
		(?, 1)      evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ b >= e + 1 ]
		(?, 1)      evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ e >= b ]
		(?, 1)      evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ f >= d + 1 ]
		(?, 1)      evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ d >= f ]
		(?, 1)      evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b)
		(?, 1)      evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e)
		(3*a, 1)    evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ b >= 1 /\ f >= 0 /\ b >= 2*f /\ 2*f + 1 >= b ]
	start location:	evalrealshellsortstart
	leaf cost:	6

A polynomial rank function with
	Pol(evalrealshellsortbb6in) = 4*V_1 - 4*V_3 + 1
	Pol(evalrealshellsortbb1in) = 4*V_1 - 4*V_3
	Pol(evalrealshellsortbb5in) = 4*V_1 - 4*V_3 - 2
	Pol(evalrealshellsortbb4in) = 4*V_1 - 4*V_3 - 1
	Pol(evalrealshellsortbb2in) = 4*V_1 - 4*V_3 - 1
	Pol(evalrealshellsortbb3in) = 4*V_1 - 4*V_3 - 1
and size complexities
	S("evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ b >= 1 /\\ f >= 0 /\\ b >= 2*f /\\ 2*f + 1 >= b ]", 0-0) = a
	S("evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ b >= 1 /\\ f >= 0 /\\ b >= 2*f /\\ 2*f + 1 >= b ]", 0-1) = ?
	S("evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ b >= 1 /\\ f >= 0 /\\ b >= 2*f /\\ 2*f + 1 >= b ]", 0-2) = ?
	S("evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ b >= 1 /\\ f >= 0 /\\ b >= 2*f /\\ 2*f + 1 >= b ]", 0-3) = ?
	S("evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ b >= 1 /\\ f >= 0 /\\ b >= 2*f /\\ 2*f + 1 >= b ]", 0-4) = ?
	S("evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e)", 0-0) = a
	S("evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e)", 0-1) = ?
	S("evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e)", 0-2) = ?
	S("evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e)", 0-3) = ?
	S("evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e)", 0-4) = ?
	S("evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b)", 0-0) = a
	S("evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b)", 0-1) = ?
	S("evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b)", 0-2) = ?
	S("evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b)", 0-3) = ?
	S("evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b)", 0-4) = ?
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ d >= f ]", 0-0) = a
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ d >= f ]", 0-1) = ?
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ d >= f ]", 0-2) = ?
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ d >= f ]", 0-3) = ?
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ d >= f ]", 0-4) = ?
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ f >= d + 1 ]", 0-0) = a
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ f >= d + 1 ]", 0-1) = ?
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ f >= d + 1 ]", 0-2) = ?
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ f >= d + 1 ]", 0-3) = ?
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ f >= d + 1 ]", 0-4) = ?
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ e >= b ]", 0-0) = a
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ e >= b ]", 0-1) = ?
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ e >= b ]", 0-2) = ?
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ e >= b ]", 0-3) = ?
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ e >= b ]", 0-4) = ?
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ b >= e + 1 ]", 0-0) = a
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ b >= e + 1 ]", 0-1) = ?
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ b >= e + 1 ]", 0-2) = ?
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ b >= e + 1 ]", 0-3) = ?
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ b >= e + 1 ]", 0-4) = ?
	S("evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c)", 0-0) = a
	S("evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c)", 0-1) = ?
	S("evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c)", 0-2) = ?
	S("evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c)", 0-3) = ?
	S("evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c)", 0-4) = ?
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= a ]", 0-0) = a
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= a ]", 0-1) = ?
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= a ]", 0-2) = ?
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= a ]", 0-3) = ?
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= a ]", 0-4) = ?
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ a >= c + 1 ]", 0-0) = a
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ a >= c + 1 ]", 0-1) = ?
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ a >= c + 1 ]", 0-2) = ?
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ a >= c + 1 ]", 0-3) = ?
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ a >= c + 1 ]", 0-4) = ?
	S("evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ b >= 1 ]", 0-0) = a
	S("evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ b >= 1 ]", 0-1) = ?
	S("evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ b >= 1 ]", 0-2) = 0
	S("evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ b >= 1 ]", 0-3) = ?
	S("evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ b >= 1 ]", 0-4) = ?
	S("evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\\ f >= 0 /\\ a >= 2*f /\\ 2*f + 1 >= a ]", 0-0) = a
	S("evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\\ f >= 0 /\\ a >= 2*f /\\ 2*f + 1 >= a ]", 0-1) = ?
	S("evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\\ f >= 0 /\\ a >= 2*f /\\ 2*f + 1 >= a ]", 0-2) = c
	S("evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\\ f >= 0 /\\ a >= 2*f /\\ 2*f + 1 >= a ]", 0-3) = d
	S("evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\\ f >= 0 /\\ a >= 2*f /\\ 2*f + 1 >= a ]", 0-4) = e
	S("evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)", 0-0) = a
	S("evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)", 0-1) = b
	S("evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)", 0-2) = c
	S("evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)", 0-3) = d
	S("evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)", 0-4) = e
orients the transitions
	evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ a >= c + 1 ]
	evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e)
	evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ d >= f ]
	evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ f >= d + 1 ]
	evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ b >= e + 1 ]
	evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ e >= b ]
	evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b)
	evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c)
weakly and the transition
	evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ a >= c + 1 ]
strictly and produces the following problem:
6:	T:
		(1, 1)               evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)
		(1, 1)               evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\ f >= 0 /\ a >= 2*f /\ 2*f + 1 >= a ]
		(3*a, 1)             evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ b >= 1 ]
		(12*a^2 + 3*a, 1)    evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ a >= c + 1 ]
		(3*a, 1)             evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= a ]
		(?, 1)               evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c)
		(?, 1)               evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ b >= e + 1 ]
		(?, 1)               evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ e >= b ]
		(?, 1)               evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ f >= d + 1 ]
		(?, 1)               evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ d >= f ]
		(?, 1)               evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b)
		(?, 1)               evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e)
		(3*a, 1)             evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ b >= 1 /\ f >= 0 /\ b >= 2*f /\ 2*f + 1 >= b ]
	start location:	evalrealshellsortstart
	leaf cost:	6

Repeatedly propagating knowledge in problem 6 produces the following problem:
7:	T:
		(1, 1)               evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)
		(1, 1)               evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\ f >= 0 /\ a >= 2*f /\ 2*f + 1 >= a ]
		(3*a, 1)             evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ b >= 1 ]
		(12*a^2 + 3*a, 1)    evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ a >= c + 1 ]
		(3*a, 1)             evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= a ]
		(12*a^2 + 3*a, 1)    evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c)
		(?, 1)               evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ b >= e + 1 ]
		(?, 1)               evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ e >= b ]
		(?, 1)               evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ f >= d + 1 ]
		(?, 1)               evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ d >= f ]
		(?, 1)               evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b)
		(?, 1)               evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e)
		(3*a, 1)             evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ b >= 1 /\ f >= 0 /\ b >= 2*f /\ 2*f + 1 >= b ]
	start location:	evalrealshellsortstart
	leaf cost:	6

A polynomial rank function with
	Pol(evalrealshellsortbb5in) = 1
	Pol(evalrealshellsortbb6in) = 0
	Pol(evalrealshellsortbb4in) = 2
	Pol(evalrealshellsortbb2in) = 2
	Pol(evalrealshellsortbb3in) = 2
and size complexities
	S("evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ b >= 1 /\\ f >= 0 /\\ b >= 2*f /\\ 2*f + 1 >= b ]", 0-0) = a
	S("evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ b >= 1 /\\ f >= 0 /\\ b >= 2*f /\\ 2*f + 1 >= b ]", 0-1) = ?
	S("evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ b >= 1 /\\ f >= 0 /\\ b >= 2*f /\\ 2*f + 1 >= b ]", 0-2) = ?
	S("evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ b >= 1 /\\ f >= 0 /\\ b >= 2*f /\\ 2*f + 1 >= b ]", 0-3) = ?
	S("evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ b >= 1 /\\ f >= 0 /\\ b >= 2*f /\\ 2*f + 1 >= b ]", 0-4) = ?
	S("evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e)", 0-0) = a
	S("evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e)", 0-1) = ?
	S("evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e)", 0-2) = ?
	S("evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e)", 0-3) = ?
	S("evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e)", 0-4) = ?
	S("evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b)", 0-0) = a
	S("evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b)", 0-1) = ?
	S("evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b)", 0-2) = ?
	S("evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b)", 0-3) = ?
	S("evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b)", 0-4) = ?
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ d >= f ]", 0-0) = a
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ d >= f ]", 0-1) = ?
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ d >= f ]", 0-2) = ?
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ d >= f ]", 0-3) = ?
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ d >= f ]", 0-4) = ?
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ f >= d + 1 ]", 0-0) = a
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ f >= d + 1 ]", 0-1) = ?
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ f >= d + 1 ]", 0-2) = ?
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ f >= d + 1 ]", 0-3) = ?
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ f >= d + 1 ]", 0-4) = ?
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ e >= b ]", 0-0) = a
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ e >= b ]", 0-1) = ?
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ e >= b ]", 0-2) = ?
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ e >= b ]", 0-3) = ?
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ e >= b ]", 0-4) = ?
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ b >= e + 1 ]", 0-0) = a
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ b >= e + 1 ]", 0-1) = ?
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ b >= e + 1 ]", 0-2) = ?
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ b >= e + 1 ]", 0-3) = ?
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ b >= e + 1 ]", 0-4) = ?
	S("evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c)", 0-0) = a
	S("evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c)", 0-1) = ?
	S("evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c)", 0-2) = ?
	S("evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c)", 0-3) = ?
	S("evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c)", 0-4) = ?
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= a ]", 0-0) = a
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= a ]", 0-1) = ?
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= a ]", 0-2) = ?
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= a ]", 0-3) = ?
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= a ]", 0-4) = ?
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ a >= c + 1 ]", 0-0) = a
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ a >= c + 1 ]", 0-1) = ?
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ a >= c + 1 ]", 0-2) = ?
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ a >= c + 1 ]", 0-3) = ?
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ a >= c + 1 ]", 0-4) = ?
	S("evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ b >= 1 ]", 0-0) = a
	S("evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ b >= 1 ]", 0-1) = ?
	S("evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ b >= 1 ]", 0-2) = 0
	S("evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ b >= 1 ]", 0-3) = ?
	S("evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ b >= 1 ]", 0-4) = ?
	S("evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\\ f >= 0 /\\ a >= 2*f /\\ 2*f + 1 >= a ]", 0-0) = a
	S("evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\\ f >= 0 /\\ a >= 2*f /\\ 2*f + 1 >= a ]", 0-1) = ?
	S("evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\\ f >= 0 /\\ a >= 2*f /\\ 2*f + 1 >= a ]", 0-2) = c
	S("evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\\ f >= 0 /\\ a >= 2*f /\\ 2*f + 1 >= a ]", 0-3) = d
	S("evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\\ f >= 0 /\\ a >= 2*f /\\ 2*f + 1 >= a ]", 0-4) = e
	S("evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)", 0-0) = a
	S("evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)", 0-1) = b
	S("evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)", 0-2) = c
	S("evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)", 0-3) = d
	S("evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)", 0-4) = e
orients the transitions
	evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e)
	evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ d >= f ]
	evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ f >= d + 1 ]
	evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ b >= e + 1 ]
	evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ e >= b ]
	evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b)
weakly and the transitions
	evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e)
	evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ d >= f ]
	evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ b >= e + 1 ]
strictly and produces the following problem:
8:	T:
		(1, 1)               evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)
		(1, 1)               evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\ f >= 0 /\ a >= 2*f /\ 2*f + 1 >= a ]
		(3*a, 1)             evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ b >= 1 ]
		(12*a^2 + 3*a, 1)    evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ a >= c + 1 ]
		(3*a, 1)             evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= a ]
		(12*a^2 + 3*a, 1)    evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c)
		(24*a^2 + 6*a, 1)    evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ b >= e + 1 ]
		(?, 1)               evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ e >= b ]
		(?, 1)               evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ f >= d + 1 ]
		(24*a^2 + 6*a, 1)    evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ d >= f ]
		(?, 1)               evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b)
		(24*a^2 + 6*a, 1)    evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e)
		(3*a, 1)             evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ b >= 1 /\ f >= 0 /\ b >= 2*f /\ 2*f + 1 >= b ]
	start location:	evalrealshellsortstart
	leaf cost:	6

Applied AI with 'oct' on problem 8 to obtain the following invariants:
  For symbol evalrealshellsortbb1in: X_1 - X_3 - 1 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 - 1 >= 0 /\ X_1 + X_3 - 1 >= 0 /\ X_1 - X_2 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 2 >= 0 /\ X_1 - 1 >= 0
  For symbol evalrealshellsortbb2in: X_3 - X_5 >= 0 /\ X_1 - X_5 - 1 >= 0 /\ X_5 - 1 >= 0 /\ X_3 + X_5 - 2 >= 0 /\ X_2 + X_5 - 2 >= 0 /\ -X_2 + X_5 >= 0 /\ X_1 + X_5 - 3 >= 0 /\ X_1 - X_3 - 1 >= 0 /\ X_3 - 1 >= 0 /\ X_2 + X_3 - 2 >= 0 /\ -X_2 + X_3 >= 0 /\ X_1 + X_3 - 3 >= 0 /\ X_1 - X_2 - 1 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 3 >= 0 /\ X_1 - 2 >= 0
  For symbol evalrealshellsortbb3in: X_3 - X_5 >= 0 /\ X_1 - X_5 - 1 >= 0 /\ X_3 + X_5 >= 0 /\ X_2 + X_5 - 1 >= 0 /\ X_1 + X_5 - 1 >= 0 /\ X_1 - X_3 - 1 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 - 1 >= 0 /\ X_1 + X_3 - 1 >= 0 /\ X_1 - X_2 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 2 >= 0 /\ X_1 - 1 >= 0
  For symbol evalrealshellsortbb4in: X_3 - X_5 >= 0 /\ X_1 - X_5 - 1 >= 0 /\ X_5 - 1 >= 0 /\ X_3 + X_5 - 2 >= 0 /\ X_2 + X_5 - 2 >= 0 /\ -X_2 + X_5 >= 0 /\ X_1 + X_5 - 3 >= 0 /\ X_1 - X_3 - 1 >= 0 /\ X_3 - 1 >= 0 /\ X_2 + X_3 - 2 >= 0 /\ -X_2 + X_3 >= 0 /\ X_1 + X_3 - 3 >= 0 /\ X_1 - X_2 - 1 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 3 >= 0 /\ X_1 - 2 >= 0
  For symbol evalrealshellsortbb5in: X_3 - X_5 >= 0 /\ X_1 - X_5 - 1 >= 0 /\ X_3 + X_5 >= 0 /\ X_2 + X_5 - 1 >= 0 /\ X_1 + X_5 - 1 >= 0 /\ X_1 - X_3 - 1 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 - 1 >= 0 /\ X_1 + X_3 - 1 >= 0 /\ X_1 - X_2 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 2 >= 0 /\ X_1 - 1 >= 0
  For symbol evalrealshellsortbb6in: X_3 >= 0 /\ X_2 + X_3 - 1 >= 0 /\ X_1 + X_3 - 1 >= 0 /\ X_1 - X_2 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 2 >= 0 /\ X_1 - 1 >= 0
  For symbol evalrealshellsortbb7in: X_3 - 1 >= 0 /\ X_2 + X_3 - 2 >= 0 /\ -X_2 + X_3 >= 0 /\ X_1 + X_3 - 2 >= 0 /\ -X_1 + X_3 >= 0 /\ X_1 - X_2 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 2 >= 0 /\ X_1 - 1 >= 0
  For symbol evalrealshellsortbb8in: X_1 - X_2 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 - 1 >= 0 /\ X_1 - 1 >= 0


This yielded the following problem:
9:	T:
		(3*a, 1)             evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 2 >= 0 /\ -a + c >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= 1 /\ f >= 0 /\ b >= 2*f /\ 2*f + 1 >= b ]
		(24*a^2 + 6*a, 1)    evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e) [ c - e >= 0 /\ a - e - 1 >= 0 /\ c + e >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ a - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 ]
		(?, 1)               evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b) [ c - e >= 0 /\ a - e - 1 >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ b + e - 2 >= 0 /\ -b + e >= 0 /\ a + e - 3 >= 0 /\ a - c - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 ]
		(24*a^2 + 6*a, 1)    evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ c - e >= 0 /\ a - e - 1 >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ b + e - 2 >= 0 /\ -b + e >= 0 /\ a + e - 3 >= 0 /\ a - c - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ d >= f ]
		(?, 1)               evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ c - e >= 0 /\ a - e - 1 >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ b + e - 2 >= 0 /\ -b + e >= 0 /\ a + e - 3 >= 0 /\ a - c - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ f >= d + 1 ]
		(?, 1)               evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ c - e >= 0 /\ a - e - 1 >= 0 /\ c + e >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ a - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ e >= b ]
		(24*a^2 + 6*a, 1)    evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ c - e >= 0 /\ a - e - 1 >= 0 /\ c + e >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ a - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= e + 1 ]
		(12*a^2 + 3*a, 1)    evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c) [ a - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 ]
		(3*a, 1)             evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ c >= a ]
		(12*a^2 + 3*a, 1)    evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a >= c + 1 ]
		(3*a, 1)             evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ a - b >= 0 /\ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ b >= 1 ]
		(1, 1)               evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\ f >= 0 /\ a >= 2*f /\ 2*f + 1 >= a ]
		(1, 1)               evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)
	start location:	evalrealshellsortstart
	leaf cost:	6

A polynomial rank function with
	Pol(evalrealshellsortbb4in) = 3*V_1 + 3*V_5 - 6
	Pol(evalrealshellsortbb2in) = 3*V_1 + 3*V_5 - 7
	Pol(evalrealshellsortbb3in) = 3*V_1 + 3*V_5 - 5
and size complexities
	S("evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)", 0-0) = a
	S("evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)", 0-1) = b
	S("evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)", 0-2) = c
	S("evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)", 0-3) = d
	S("evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)", 0-4) = e
	S("evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\\ f >= 0 /\\ a >= 2*f /\\ 2*f + 1 >= a ]", 0-0) = a
	S("evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\\ f >= 0 /\\ a >= 2*f /\\ 2*f + 1 >= a ]", 0-1) = ?
	S("evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\\ f >= 0 /\\ a >= 2*f /\\ 2*f + 1 >= a ]", 0-2) = c
	S("evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\\ f >= 0 /\\ a >= 2*f /\\ 2*f + 1 >= a ]", 0-3) = d
	S("evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\\ f >= 0 /\\ a >= 2*f /\\ 2*f + 1 >= a ]", 0-4) = e
	S("evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ a - b >= 0 /\\ b >= 0 /\\ a + b - 1 >= 0 /\\ a - 1 >= 0 /\\ b >= 1 ]", 0-0) = a
	S("evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ a - b >= 0 /\\ b >= 0 /\\ a + b - 1 >= 0 /\\ a - 1 >= 0 /\\ b >= 1 ]", 0-1) = ?
	S("evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ a - b >= 0 /\\ b >= 0 /\\ a + b - 1 >= 0 /\\ a - 1 >= 0 /\\ b >= 1 ]", 0-2) = 0
	S("evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ a - b >= 0 /\\ b >= 0 /\\ a + b - 1 >= 0 /\\ a - 1 >= 0 /\\ b >= 1 ]", 0-3) = ?
	S("evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ a - b >= 0 /\\ b >= 0 /\\ a + b - 1 >= 0 /\\ a - 1 >= 0 /\\ b >= 1 ]", 0-4) = a + e
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 /\\ a >= c + 1 ]", 0-0) = a
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 /\\ a >= c + 1 ]", 0-1) = ?
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 /\\ a >= c + 1 ]", 0-2) = a
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 /\\ a >= c + 1 ]", 0-3) = ?
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 /\\ a >= c + 1 ]", 0-4) = a + e
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 /\\ c >= a ]", 0-0) = a
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 /\\ c >= a ]", 0-1) = ?
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 /\\ c >= a ]", 0-2) = a
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 /\\ c >= a ]", 0-3) = ?
	S("evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 /\\ c >= a ]", 0-4) = a
	S("evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c) [ a - c - 1 >= 0 /\\ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 ]", 0-0) = a
	S("evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c) [ a - c - 1 >= 0 /\\ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 ]", 0-1) = ?
	S("evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c) [ a - c - 1 >= 0 /\\ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 ]", 0-2) = a
	S("evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c) [ a - c - 1 >= 0 /\\ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 ]", 0-3) = ?
	S("evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c) [ a - c - 1 >= 0 /\\ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 ]", 0-4) = a
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ c + e >= 0 /\\ b + e - 1 >= 0 /\\ a + e - 1 >= 0 /\\ a - c - 1 >= 0 /\\ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 /\\ b >= e + 1 ]", 0-0) = a
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ c + e >= 0 /\\ b + e - 1 >= 0 /\\ a + e - 1 >= 0 /\\ a - c - 1 >= 0 /\\ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 /\\ b >= e + 1 ]", 0-1) = ?
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ c + e >= 0 /\\ b + e - 1 >= 0 /\\ a + e - 1 >= 0 /\\ a - c - 1 >= 0 /\\ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 /\\ b >= e + 1 ]", 0-2) = a
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ c + e >= 0 /\\ b + e - 1 >= 0 /\\ a + e - 1 >= 0 /\\ a - c - 1 >= 0 /\\ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 /\\ b >= e + 1 ]", 0-3) = ?
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ c + e >= 0 /\\ b + e - 1 >= 0 /\\ a + e - 1 >= 0 /\\ a - c - 1 >= 0 /\\ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 /\\ b >= e + 1 ]", 0-4) = a
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ c + e >= 0 /\\ b + e - 1 >= 0 /\\ a + e - 1 >= 0 /\\ a - c - 1 >= 0 /\\ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 /\\ e >= b ]", 0-0) = a
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ c + e >= 0 /\\ b + e - 1 >= 0 /\\ a + e - 1 >= 0 /\\ a - c - 1 >= 0 /\\ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 /\\ e >= b ]", 0-1) = ?
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ c + e >= 0 /\\ b + e - 1 >= 0 /\\ a + e - 1 >= 0 /\\ a - c - 1 >= 0 /\\ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 /\\ e >= b ]", 0-2) = a
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ c + e >= 0 /\\ b + e - 1 >= 0 /\\ a + e - 1 >= 0 /\\ a - c - 1 >= 0 /\\ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 /\\ e >= b ]", 0-3) = ?
	S("evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ c + e >= 0 /\\ b + e - 1 >= 0 /\\ a + e - 1 >= 0 /\\ a - c - 1 >= 0 /\\ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 /\\ e >= b ]", 0-4) = a
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ e - 1 >= 0 /\\ c + e - 2 >= 0 /\\ b + e - 2 >= 0 /\\ -b + e >= 0 /\\ a + e - 3 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ b + c - 2 >= 0 /\\ -b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 1 >= 0 /\\ b - 1 >= 0 /\\ a + b - 3 >= 0 /\\ a - 2 >= 0 /\\ f >= d + 1 ]", 0-0) = a
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ e - 1 >= 0 /\\ c + e - 2 >= 0 /\\ b + e - 2 >= 0 /\\ -b + e >= 0 /\\ a + e - 3 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ b + c - 2 >= 0 /\\ -b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 1 >= 0 /\\ b - 1 >= 0 /\\ a + b - 3 >= 0 /\\ a - 2 >= 0 /\\ f >= d + 1 ]", 0-1) = ?
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ e - 1 >= 0 /\\ c + e - 2 >= 0 /\\ b + e - 2 >= 0 /\\ -b + e >= 0 /\\ a + e - 3 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ b + c - 2 >= 0 /\\ -b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 1 >= 0 /\\ b - 1 >= 0 /\\ a + b - 3 >= 0 /\\ a - 2 >= 0 /\\ f >= d + 1 ]", 0-2) = a
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ e - 1 >= 0 /\\ c + e - 2 >= 0 /\\ b + e - 2 >= 0 /\\ -b + e >= 0 /\\ a + e - 3 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ b + c - 2 >= 0 /\\ -b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 1 >= 0 /\\ b - 1 >= 0 /\\ a + b - 3 >= 0 /\\ a - 2 >= 0 /\\ f >= d + 1 ]", 0-3) = ?
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ e - 1 >= 0 /\\ c + e - 2 >= 0 /\\ b + e - 2 >= 0 /\\ -b + e >= 0 /\\ a + e - 3 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ b + c - 2 >= 0 /\\ -b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 1 >= 0 /\\ b - 1 >= 0 /\\ a + b - 3 >= 0 /\\ a - 2 >= 0 /\\ f >= d + 1 ]", 0-4) = a
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ e - 1 >= 0 /\\ c + e - 2 >= 0 /\\ b + e - 2 >= 0 /\\ -b + e >= 0 /\\ a + e - 3 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ b + c - 2 >= 0 /\\ -b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 1 >= 0 /\\ b - 1 >= 0 /\\ a + b - 3 >= 0 /\\ a - 2 >= 0 /\\ d >= f ]", 0-0) = a
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ e - 1 >= 0 /\\ c + e - 2 >= 0 /\\ b + e - 2 >= 0 /\\ -b + e >= 0 /\\ a + e - 3 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ b + c - 2 >= 0 /\\ -b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 1 >= 0 /\\ b - 1 >= 0 /\\ a + b - 3 >= 0 /\\ a - 2 >= 0 /\\ d >= f ]", 0-1) = ?
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ e - 1 >= 0 /\\ c + e - 2 >= 0 /\\ b + e - 2 >= 0 /\\ -b + e >= 0 /\\ a + e - 3 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ b + c - 2 >= 0 /\\ -b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 1 >= 0 /\\ b - 1 >= 0 /\\ a + b - 3 >= 0 /\\ a - 2 >= 0 /\\ d >= f ]", 0-2) = a
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ e - 1 >= 0 /\\ c + e - 2 >= 0 /\\ b + e - 2 >= 0 /\\ -b + e >= 0 /\\ a + e - 3 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ b + c - 2 >= 0 /\\ -b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 1 >= 0 /\\ b - 1 >= 0 /\\ a + b - 3 >= 0 /\\ a - 2 >= 0 /\\ d >= f ]", 0-3) = ?
	S("evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ e - 1 >= 0 /\\ c + e - 2 >= 0 /\\ b + e - 2 >= 0 /\\ -b + e >= 0 /\\ a + e - 3 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ b + c - 2 >= 0 /\\ -b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 1 >= 0 /\\ b - 1 >= 0 /\\ a + b - 3 >= 0 /\\ a - 2 >= 0 /\\ d >= f ]", 0-4) = a
	S("evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ e - 1 >= 0 /\\ c + e - 2 >= 0 /\\ b + e - 2 >= 0 /\\ -b + e >= 0 /\\ a + e - 3 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ b + c - 2 >= 0 /\\ -b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 1 >= 0 /\\ b - 1 >= 0 /\\ a + b - 3 >= 0 /\\ a - 2 >= 0 ]", 0-0) = a
	S("evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ e - 1 >= 0 /\\ c + e - 2 >= 0 /\\ b + e - 2 >= 0 /\\ -b + e >= 0 /\\ a + e - 3 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ b + c - 2 >= 0 /\\ -b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 1 >= 0 /\\ b - 1 >= 0 /\\ a + b - 3 >= 0 /\\ a - 2 >= 0 ]", 0-1) = ?
	S("evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ e - 1 >= 0 /\\ c + e - 2 >= 0 /\\ b + e - 2 >= 0 /\\ -b + e >= 0 /\\ a + e - 3 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ b + c - 2 >= 0 /\\ -b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 1 >= 0 /\\ b - 1 >= 0 /\\ a + b - 3 >= 0 /\\ a - 2 >= 0 ]", 0-2) = a
	S("evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ e - 1 >= 0 /\\ c + e - 2 >= 0 /\\ b + e - 2 >= 0 /\\ -b + e >= 0 /\\ a + e - 3 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ b + c - 2 >= 0 /\\ -b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 1 >= 0 /\\ b - 1 >= 0 /\\ a + b - 3 >= 0 /\\ a - 2 >= 0 ]", 0-3) = ?
	S("evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ e - 1 >= 0 /\\ c + e - 2 >= 0 /\\ b + e - 2 >= 0 /\\ -b + e >= 0 /\\ a + e - 3 >= 0 /\\ a - c - 1 >= 0 /\\ c - 1 >= 0 /\\ b + c - 2 >= 0 /\\ -b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 1 >= 0 /\\ b - 1 >= 0 /\\ a + b - 3 >= 0 /\\ a - 2 >= 0 ]", 0-4) = a
	S("evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ c + e >= 0 /\\ b + e - 1 >= 0 /\\ a + e - 1 >= 0 /\\ a - c - 1 >= 0 /\\ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 ]", 0-0) = a
	S("evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ c + e >= 0 /\\ b + e - 1 >= 0 /\\ a + e - 1 >= 0 /\\ a - c - 1 >= 0 /\\ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 ]", 0-1) = ?
	S("evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ c + e >= 0 /\\ b + e - 1 >= 0 /\\ a + e - 1 >= 0 /\\ a - c - 1 >= 0 /\\ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 ]", 0-2) = a
	S("evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ c + e >= 0 /\\ b + e - 1 >= 0 /\\ a + e - 1 >= 0 /\\ a - c - 1 >= 0 /\\ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 ]", 0-3) = ?
	S("evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e) [ c - e >= 0 /\\ a - e - 1 >= 0 /\\ c + e >= 0 /\\ b + e - 1 >= 0 /\\ a + e - 1 >= 0 /\\ a - c - 1 >= 0 /\\ c >= 0 /\\ b + c - 1 >= 0 /\\ a + c - 1 >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 ]", 0-4) = a
	S("evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ c - 1 >= 0 /\\ b + c - 2 >= 0 /\\ -b + c >= 0 /\\ a + c - 2 >= 0 /\\ -a + c >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 /\\ b >= 1 /\\ f >= 0 /\\ b >= 2*f /\\ 2*f + 1 >= b ]", 0-0) = a
	S("evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ c - 1 >= 0 /\\ b + c - 2 >= 0 /\\ -b + c >= 0 /\\ a + c - 2 >= 0 /\\ -a + c >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 /\\ b >= 1 /\\ f >= 0 /\\ b >= 2*f /\\ 2*f + 1 >= b ]", 0-1) = ?
	S("evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ c - 1 >= 0 /\\ b + c - 2 >= 0 /\\ -b + c >= 0 /\\ a + c - 2 >= 0 /\\ -a + c >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 /\\ b >= 1 /\\ f >= 0 /\\ b >= 2*f /\\ 2*f + 1 >= b ]", 0-2) = a
	S("evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ c - 1 >= 0 /\\ b + c - 2 >= 0 /\\ -b + c >= 0 /\\ a + c - 2 >= 0 /\\ -a + c >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 /\\ b >= 1 /\\ f >= 0 /\\ b >= 2*f /\\ 2*f + 1 >= b ]", 0-3) = ?
	S("evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ c - 1 >= 0 /\\ b + c - 2 >= 0 /\\ -b + c >= 0 /\\ a + c - 2 >= 0 /\\ -a + c >= 0 /\\ a - b >= 0 /\\ b - 1 >= 0 /\\ a + b - 2 >= 0 /\\ a - 1 >= 0 /\\ b >= 1 /\\ f >= 0 /\\ b >= 2*f /\\ 2*f + 1 >= b ]", 0-4) = a
orients the transitions
	evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ c - e >= 0 /\ a - e - 1 >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ b + e - 2 >= 0 /\ -b + e >= 0 /\ a + e - 3 >= 0 /\ a - c - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ f >= d + 1 ]
	evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ c - e >= 0 /\ a - e - 1 >= 0 /\ c + e >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ a - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ e >= b ]
	evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b) [ c - e >= 0 /\ a - e - 1 >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ b + e - 2 >= 0 /\ -b + e >= 0 /\ a + e - 3 >= 0 /\ a - c - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 ]
weakly and the transitions
	evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ c - e >= 0 /\ a - e - 1 >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ b + e - 2 >= 0 /\ -b + e >= 0 /\ a + e - 3 >= 0 /\ a - c - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ f >= d + 1 ]
	evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ c - e >= 0 /\ a - e - 1 >= 0 /\ c + e >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ a - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ e >= b ]
	evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b) [ c - e >= 0 /\ a - e - 1 >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ b + e - 2 >= 0 /\ -b + e >= 0 /\ a + e - 3 >= 0 /\ a - c - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 ]
strictly and produces the following problem:
10:	T:
		(3*a, 1)                       evalrealshellsortbb7in(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 2 >= 0 /\ -a + c >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= 1 /\ f >= 0 /\ b >= 2*f /\ 2*f + 1 >= b ]
		(24*a^2 + 6*a, 1)              evalrealshellsortbb5in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, c + 1, d, e) [ c - e >= 0 /\ a - e - 1 >= 0 /\ c + e >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ a - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 ]
		(72*a^3 + 78*a^2 + 15*a, 1)    evalrealshellsortbb2in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, d, e - b) [ c - e >= 0 /\ a - e - 1 >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ b + e - 2 >= 0 /\ -b + e >= 0 /\ a + e - 3 >= 0 /\ a - c - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 ]
		(24*a^2 + 6*a, 1)              evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ c - e >= 0 /\ a - e - 1 >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ b + e - 2 >= 0 /\ -b + e >= 0 /\ a + e - 3 >= 0 /\ a - c - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ d >= f ]
		(72*a^3 + 78*a^2 + 15*a, 1)    evalrealshellsortbb4in(a, b, c, d, e) -> evalrealshellsortbb2in(a, b, c, d, e) [ c - e >= 0 /\ a - e - 1 >= 0 /\ e - 1 >= 0 /\ c + e - 2 >= 0 /\ b + e - 2 >= 0 /\ -b + e >= 0 /\ a + e - 3 >= 0 /\ a - c - 1 >= 0 /\ c - 1 >= 0 /\ b + c - 2 >= 0 /\ -b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ f >= d + 1 ]
		(72*a^3 + 78*a^2 + 15*a, 1)    evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb4in(a, b, c, d, e) [ c - e >= 0 /\ a - e - 1 >= 0 /\ c + e >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ a - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ e >= b ]
		(24*a^2 + 6*a, 1)              evalrealshellsortbb3in(a, b, c, d, e) -> evalrealshellsortbb5in(a, b, c, d, e) [ c - e >= 0 /\ a - e - 1 >= 0 /\ c + e >= 0 /\ b + e - 1 >= 0 /\ a + e - 1 >= 0 /\ a - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ b >= e + 1 ]
		(12*a^2 + 3*a, 1)              evalrealshellsortbb1in(a, b, c, d, e) -> evalrealshellsortbb3in(a, b, c, f, c) [ a - c - 1 >= 0 /\ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 ]
		(3*a, 1)                       evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb7in(a, b, c, d, e) [ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ c >= a ]
		(12*a^2 + 3*a, 1)              evalrealshellsortbb6in(a, b, c, d, e) -> evalrealshellsortbb1in(a, b, c, d, e) [ c >= 0 /\ b + c - 1 >= 0 /\ a + c - 1 >= 0 /\ a - b >= 0 /\ b - 1 >= 0 /\ a + b - 2 >= 0 /\ a - 1 >= 0 /\ a >= c + 1 ]
		(3*a, 1)                       evalrealshellsortbb8in(a, b, c, d, e) -> evalrealshellsortbb6in(a, b, 0, d, e) [ a - b >= 0 /\ b >= 0 /\ a + b - 1 >= 0 /\ a - 1 >= 0 /\ b >= 1 ]
		(1, 1)                         evalrealshellsortentryin(a, b, c, d, e) -> evalrealshellsortbb8in(a, f, c, d, e) [ a >= 1 /\ f >= 0 /\ a >= 2*f /\ 2*f + 1 >= a ]
		(1, 1)                         evalrealshellsortstart(a, b, c, d, e) -> evalrealshellsortentryin(a, b, c, d, e)
	start location:	evalrealshellsortstart
	leaf cost:	6

Complexity upper bound 78*a + 330*a^2 + 216*a^3 + 8

Time: 1.043 sec (SMT: 0.957 sec)