YES(?, 924*a + 240*a^2 + 888)

Initial complexity problem:
1:	T:
		(1, 1)    evalrealheapsortstep2start(a, b, c, d) -> evalrealheapsortstep2entryin(a, b, c, d)
		(?, 1)    evalrealheapsortstep2entryin(a, b, c, d) -> evalrealheapsortstep2bbin(a, b, c, d) [ a >= 3 ]
		(?, 1)    evalrealheapsortstep2entryin(a, b, c, d) -> evalrealheapsortstep2returnin(a, b, c, d) [ 2 >= a ]
		(?, 1)    evalrealheapsortstep2bbin(a, b, c, d) -> evalrealheapsortstep2bb11in(a, 0, c, d)
		(?, 1)    evalrealheapsortstep2bb11in(a, b, c, d) -> evalrealheapsortstep2bb1in(a, b, c, d) [ a >= b + 2 ]
		(?, 1)    evalrealheapsortstep2bb11in(a, b, c, d) -> evalrealheapsortstep2returnin(a, b, c, d) [ b + 1 >= a ]
		(?, 1)    evalrealheapsortstep2bb1in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, 0, d)
		(?, 1)    evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb2in(a, b, c, d) [ a >= b + 2*c + 3 ]
		(?, 1)    evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb10in(a, b, c, d) [ 2*c + b + 2 >= a ]
		(?, 1)    evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d) [ a = 2*c + b + 3 ]
		(?, 1)    evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb3in(a, b, c, d) [ a >= b + 2*c + 4 ]
		(?, 1)    evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb3in(a, b, c, d) [ 2*c + b + 2 >= a ]
		(?, 1)    evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d)
		(?, 1)    evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb5in(a, b, c, d)
		(?, 1)    evalrealheapsortstep2bb4in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 1)
		(?, 1)    evalrealheapsortstep2bb5in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 2)
		(?, 1)    evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb7in(a, b, c, d)
		(?, 1)    evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, a, d)
		(?, 1)    evalrealheapsortstep2bb7in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, d, d)
		(?, 1)    evalrealheapsortstep2bb10in(a, b, c, d) -> evalrealheapsortstep2bb11in(a, b + 1, c, d)
		(?, 1)    evalrealheapsortstep2returnin(a, b, c, d) -> evalrealheapsortstep2stop(a, b, c, d)
	start location:	evalrealheapsortstep2start
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(1, 1)    evalrealheapsortstep2start(a, b, c, d) -> evalrealheapsortstep2entryin(a, b, c, d)
		(?, 1)    evalrealheapsortstep2entryin(a, b, c, d) -> evalrealheapsortstep2bbin(a, b, c, d) [ a >= 3 ]
		(?, 1)    evalrealheapsortstep2bbin(a, b, c, d) -> evalrealheapsortstep2bb11in(a, 0, c, d)
		(?, 1)    evalrealheapsortstep2bb11in(a, b, c, d) -> evalrealheapsortstep2bb1in(a, b, c, d) [ a >= b + 2 ]
		(?, 1)    evalrealheapsortstep2bb1in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, 0, d)
		(?, 1)    evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb2in(a, b, c, d) [ a >= b + 2*c + 3 ]
		(?, 1)    evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb10in(a, b, c, d) [ 2*c + b + 2 >= a ]
		(?, 1)    evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d) [ a = 2*c + b + 3 ]
		(?, 1)    evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb3in(a, b, c, d) [ a >= b + 2*c + 4 ]
		(?, 1)    evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb3in(a, b, c, d) [ 2*c + b + 2 >= a ]
		(?, 1)    evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d)
		(?, 1)    evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb5in(a, b, c, d)
		(?, 1)    evalrealheapsortstep2bb4in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 1)
		(?, 1)    evalrealheapsortstep2bb5in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 2)
		(?, 1)    evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb7in(a, b, c, d)
		(?, 1)    evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, a, d)
		(?, 1)    evalrealheapsortstep2bb7in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, d, d)
		(?, 1)    evalrealheapsortstep2bb10in(a, b, c, d) -> evalrealheapsortstep2bb11in(a, b + 1, c, d)
	start location:	evalrealheapsortstep2start
	leaf cost:	3

Testing for reachability in the complexity graph removes the following transition from problem 2:
	evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb3in(a, b, c, d) [ 2*c + b + 2 >= a ]
We thus obtain the following problem:
3:	T:
		(?, 1)    evalrealheapsortstep2bb7in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, d, d)
		(?, 1)    evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, a, d)
		(?, 1)    evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb7in(a, b, c, d)
		(?, 1)    evalrealheapsortstep2bb5in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 2)
		(?, 1)    evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb5in(a, b, c, d)
		(?, 1)    evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d)
		(?, 1)    evalrealheapsortstep2bb4in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 1)
		(?, 1)    evalrealheapsortstep2bb10in(a, b, c, d) -> evalrealheapsortstep2bb11in(a, b + 1, c, d)
		(?, 1)    evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb3in(a, b, c, d) [ a >= b + 2*c + 4 ]
		(?, 1)    evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d) [ a = 2*c + b + 3 ]
		(?, 1)    evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb10in(a, b, c, d) [ 2*c + b + 2 >= a ]
		(?, 1)    evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb2in(a, b, c, d) [ a >= b + 2*c + 3 ]
		(?, 1)    evalrealheapsortstep2bb1in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, 0, d)
		(?, 1)    evalrealheapsortstep2bb11in(a, b, c, d) -> evalrealheapsortstep2bb1in(a, b, c, d) [ a >= b + 2 ]
		(?, 1)    evalrealheapsortstep2bbin(a, b, c, d) -> evalrealheapsortstep2bb11in(a, 0, c, d)
		(?, 1)    evalrealheapsortstep2entryin(a, b, c, d) -> evalrealheapsortstep2bbin(a, b, c, d) [ a >= 3 ]
		(1, 1)    evalrealheapsortstep2start(a, b, c, d) -> evalrealheapsortstep2entryin(a, b, c, d)
	start location:	evalrealheapsortstep2start
	leaf cost:	3

Repeatedly propagating knowledge in problem 3 produces the following problem:
4:	T:
		(?, 1)    evalrealheapsortstep2bb7in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, d, d)
		(?, 1)    evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, a, d)
		(?, 1)    evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb7in(a, b, c, d)
		(?, 1)    evalrealheapsortstep2bb5in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 2)
		(?, 1)    evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb5in(a, b, c, d)
		(?, 1)    evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d)
		(?, 1)    evalrealheapsortstep2bb4in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 1)
		(?, 1)    evalrealheapsortstep2bb10in(a, b, c, d) -> evalrealheapsortstep2bb11in(a, b + 1, c, d)
		(?, 1)    evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb3in(a, b, c, d) [ a >= b + 2*c + 4 ]
		(?, 1)    evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d) [ a = 2*c + b + 3 ]
		(?, 1)    evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb10in(a, b, c, d) [ 2*c + b + 2 >= a ]
		(?, 1)    evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb2in(a, b, c, d) [ a >= b + 2*c + 3 ]
		(?, 1)    evalrealheapsortstep2bb1in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, 0, d)
		(?, 1)    evalrealheapsortstep2bb11in(a, b, c, d) -> evalrealheapsortstep2bb1in(a, b, c, d) [ a >= b + 2 ]
		(1, 1)    evalrealheapsortstep2bbin(a, b, c, d) -> evalrealheapsortstep2bb11in(a, 0, c, d)
		(1, 1)    evalrealheapsortstep2entryin(a, b, c, d) -> evalrealheapsortstep2bbin(a, b, c, d) [ a >= 3 ]
		(1, 1)    evalrealheapsortstep2start(a, b, c, d) -> evalrealheapsortstep2entryin(a, b, c, d)
	start location:	evalrealheapsortstep2start
	leaf cost:	3

A polynomial rank function with
	Pol(evalrealheapsortstep2bb7in) = 4*V_1 - 4*V_2 - 9
	Pol(evalrealheapsortstep2bb9in) = 4*V_1 - 4*V_2 - 9
	Pol(evalrealheapsortstep2bb6in) = 4*V_1 - 4*V_2 - 9
	Pol(evalrealheapsortstep2bb5in) = 4*V_1 - 4*V_2 - 9
	Pol(evalrealheapsortstep2bb3in) = 4*V_1 - 4*V_2 - 9
	Pol(evalrealheapsortstep2bb4in) = 4*V_1 - 4*V_2 - 9
	Pol(evalrealheapsortstep2bb10in) = 4*V_1 - 4*V_2 - 10
	Pol(evalrealheapsortstep2bb11in) = 4*V_1 - 4*V_2 - 7
	Pol(evalrealheapsortstep2bb2in) = 4*V_1 - 4*V_2 - 9
	Pol(evalrealheapsortstep2bb1in) = 4*V_1 - 4*V_2 - 8
	Pol(evalrealheapsortstep2bbin) = 4*V_1 - 7
	Pol(evalrealheapsortstep2entryin) = 4*V_1 - 7
	Pol(evalrealheapsortstep2start) = 4*V_1 - 7
orients all transitions weakly and the transition
	evalrealheapsortstep2bb11in(a, b, c, d) -> evalrealheapsortstep2bb1in(a, b, c, d) [ a >= b + 2 ]
strictly and produces the following problem:
5:	T:
		(?, 1)          evalrealheapsortstep2bb7in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, d, d)
		(?, 1)          evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, a, d)
		(?, 1)          evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb7in(a, b, c, d)
		(?, 1)          evalrealheapsortstep2bb5in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 2)
		(?, 1)          evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb5in(a, b, c, d)
		(?, 1)          evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d)
		(?, 1)          evalrealheapsortstep2bb4in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 1)
		(?, 1)          evalrealheapsortstep2bb10in(a, b, c, d) -> evalrealheapsortstep2bb11in(a, b + 1, c, d)
		(?, 1)          evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb3in(a, b, c, d) [ a >= b + 2*c + 4 ]
		(?, 1)          evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d) [ a = 2*c + b + 3 ]
		(?, 1)          evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb10in(a, b, c, d) [ 2*c + b + 2 >= a ]
		(?, 1)          evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb2in(a, b, c, d) [ a >= b + 2*c + 3 ]
		(?, 1)          evalrealheapsortstep2bb1in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, 0, d)
		(4*a + 7, 1)    evalrealheapsortstep2bb11in(a, b, c, d) -> evalrealheapsortstep2bb1in(a, b, c, d) [ a >= b + 2 ]
		(1, 1)          evalrealheapsortstep2bbin(a, b, c, d) -> evalrealheapsortstep2bb11in(a, 0, c, d)
		(1, 1)          evalrealheapsortstep2entryin(a, b, c, d) -> evalrealheapsortstep2bbin(a, b, c, d) [ a >= 3 ]
		(1, 1)          evalrealheapsortstep2start(a, b, c, d) -> evalrealheapsortstep2entryin(a, b, c, d)
	start location:	evalrealheapsortstep2start
	leaf cost:	3

Repeatedly propagating knowledge in problem 5 produces the following problem:
6:	T:
		(?, 1)          evalrealheapsortstep2bb7in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, d, d)
		(?, 1)          evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, a, d)
		(?, 1)          evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb7in(a, b, c, d)
		(?, 1)          evalrealheapsortstep2bb5in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 2)
		(?, 1)          evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb5in(a, b, c, d)
		(?, 1)          evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d)
		(?, 1)          evalrealheapsortstep2bb4in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 1)
		(?, 1)          evalrealheapsortstep2bb10in(a, b, c, d) -> evalrealheapsortstep2bb11in(a, b + 1, c, d)
		(?, 1)          evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb3in(a, b, c, d) [ a >= b + 2*c + 4 ]
		(?, 1)          evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d) [ a = 2*c + b + 3 ]
		(?, 1)          evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb10in(a, b, c, d) [ 2*c + b + 2 >= a ]
		(?, 1)          evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb2in(a, b, c, d) [ a >= b + 2*c + 3 ]
		(4*a + 7, 1)    evalrealheapsortstep2bb1in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, 0, d)
		(4*a + 7, 1)    evalrealheapsortstep2bb11in(a, b, c, d) -> evalrealheapsortstep2bb1in(a, b, c, d) [ a >= b + 2 ]
		(1, 1)          evalrealheapsortstep2bbin(a, b, c, d) -> evalrealheapsortstep2bb11in(a, 0, c, d)
		(1, 1)          evalrealheapsortstep2entryin(a, b, c, d) -> evalrealheapsortstep2bbin(a, b, c, d) [ a >= 3 ]
		(1, 1)          evalrealheapsortstep2start(a, b, c, d) -> evalrealheapsortstep2entryin(a, b, c, d)
	start location:	evalrealheapsortstep2start
	leaf cost:	3

A polynomial rank function with
	Pol(evalrealheapsortstep2bb9in) = 2
	Pol(evalrealheapsortstep2bb2in) = 2
	Pol(evalrealheapsortstep2bb10in) = 1
	Pol(evalrealheapsortstep2bb7in) = 2
	Pol(evalrealheapsortstep2bb6in) = 2
	Pol(evalrealheapsortstep2bb5in) = 2
	Pol(evalrealheapsortstep2bb4in) = 2
	Pol(evalrealheapsortstep2bb3in) = 2
	Pol(evalrealheapsortstep2bb11in) = 0
and size complexities
	S("evalrealheapsortstep2start(a, b, c, d) -> evalrealheapsortstep2entryin(a, b, c, d)", 0-0) = a
	S("evalrealheapsortstep2start(a, b, c, d) -> evalrealheapsortstep2entryin(a, b, c, d)", 0-1) = b
	S("evalrealheapsortstep2start(a, b, c, d) -> evalrealheapsortstep2entryin(a, b, c, d)", 0-2) = c
	S("evalrealheapsortstep2start(a, b, c, d) -> evalrealheapsortstep2entryin(a, b, c, d)", 0-3) = d
	S("evalrealheapsortstep2entryin(a, b, c, d) -> evalrealheapsortstep2bbin(a, b, c, d) [ a >= 3 ]", 0-0) = a
	S("evalrealheapsortstep2entryin(a, b, c, d) -> evalrealheapsortstep2bbin(a, b, c, d) [ a >= 3 ]", 0-1) = b
	S("evalrealheapsortstep2entryin(a, b, c, d) -> evalrealheapsortstep2bbin(a, b, c, d) [ a >= 3 ]", 0-2) = c
	S("evalrealheapsortstep2entryin(a, b, c, d) -> evalrealheapsortstep2bbin(a, b, c, d) [ a >= 3 ]", 0-3) = d
	S("evalrealheapsortstep2bbin(a, b, c, d) -> evalrealheapsortstep2bb11in(a, 0, c, d)", 0-0) = a
	S("evalrealheapsortstep2bbin(a, b, c, d) -> evalrealheapsortstep2bb11in(a, 0, c, d)", 0-1) = 0
	S("evalrealheapsortstep2bbin(a, b, c, d) -> evalrealheapsortstep2bb11in(a, 0, c, d)", 0-2) = c
	S("evalrealheapsortstep2bbin(a, b, c, d) -> evalrealheapsortstep2bb11in(a, 0, c, d)", 0-3) = d
	S("evalrealheapsortstep2bb11in(a, b, c, d) -> evalrealheapsortstep2bb1in(a, b, c, d) [ a >= b + 2 ]", 0-0) = a
	S("evalrealheapsortstep2bb11in(a, b, c, d) -> evalrealheapsortstep2bb1in(a, b, c, d) [ a >= b + 2 ]", 0-1) = ?
	S("evalrealheapsortstep2bb11in(a, b, c, d) -> evalrealheapsortstep2bb1in(a, b, c, d) [ a >= b + 2 ]", 0-2) = ?
	S("evalrealheapsortstep2bb11in(a, b, c, d) -> evalrealheapsortstep2bb1in(a, b, c, d) [ a >= b + 2 ]", 0-3) = ?
	S("evalrealheapsortstep2bb1in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, 0, d)", 0-0) = a
	S("evalrealheapsortstep2bb1in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, 0, d)", 0-1) = ?
	S("evalrealheapsortstep2bb1in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, 0, d)", 0-2) = 0
	S("evalrealheapsortstep2bb1in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, 0, d)", 0-3) = ?
	S("evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb2in(a, b, c, d) [ a >= b + 2*c + 3 ]", 0-0) = a
	S("evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb2in(a, b, c, d) [ a >= b + 2*c + 3 ]", 0-1) = ?
	S("evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb2in(a, b, c, d) [ a >= b + 2*c + 3 ]", 0-2) = ?
	S("evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb2in(a, b, c, d) [ a >= b + 2*c + 3 ]", 0-3) = ?
	S("evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb10in(a, b, c, d) [ 2*c + b + 2 >= a ]", 0-0) = a
	S("evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb10in(a, b, c, d) [ 2*c + b + 2 >= a ]", 0-1) = ?
	S("evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb10in(a, b, c, d) [ 2*c + b + 2 >= a ]", 0-2) = ?
	S("evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb10in(a, b, c, d) [ 2*c + b + 2 >= a ]", 0-3) = ?
	S("evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d) [ a = 2*c + b + 3 ]", 0-0) = a
	S("evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d) [ a = 2*c + b + 3 ]", 0-1) = ?
	S("evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d) [ a = 2*c + b + 3 ]", 0-2) = ?
	S("evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d) [ a = 2*c + b + 3 ]", 0-3) = ?
	S("evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb3in(a, b, c, d) [ a >= b + 2*c + 4 ]", 0-0) = a
	S("evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb3in(a, b, c, d) [ a >= b + 2*c + 4 ]", 0-1) = ?
	S("evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb3in(a, b, c, d) [ a >= b + 2*c + 4 ]", 0-2) = ?
	S("evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb3in(a, b, c, d) [ a >= b + 2*c + 4 ]", 0-3) = ?
	S("evalrealheapsortstep2bb10in(a, b, c, d) -> evalrealheapsortstep2bb11in(a, b + 1, c, d)", 0-0) = a
	S("evalrealheapsortstep2bb10in(a, b, c, d) -> evalrealheapsortstep2bb11in(a, b + 1, c, d)", 0-1) = ?
	S("evalrealheapsortstep2bb10in(a, b, c, d) -> evalrealheapsortstep2bb11in(a, b + 1, c, d)", 0-2) = ?
	S("evalrealheapsortstep2bb10in(a, b, c, d) -> evalrealheapsortstep2bb11in(a, b + 1, c, d)", 0-3) = ?
	S("evalrealheapsortstep2bb4in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 1)", 0-0) = a
	S("evalrealheapsortstep2bb4in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 1)", 0-1) = ?
	S("evalrealheapsortstep2bb4in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 1)", 0-2) = ?
	S("evalrealheapsortstep2bb4in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 1)", 0-3) = ?
	S("evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d)", 0-0) = a
	S("evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d)", 0-1) = ?
	S("evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d)", 0-2) = ?
	S("evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d)", 0-3) = ?
	S("evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb5in(a, b, c, d)", 0-0) = a
	S("evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb5in(a, b, c, d)", 0-1) = ?
	S("evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb5in(a, b, c, d)", 0-2) = ?
	S("evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb5in(a, b, c, d)", 0-3) = ?
	S("evalrealheapsortstep2bb5in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 2)", 0-0) = a
	S("evalrealheapsortstep2bb5in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 2)", 0-1) = ?
	S("evalrealheapsortstep2bb5in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 2)", 0-2) = ?
	S("evalrealheapsortstep2bb5in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 2)", 0-3) = ?
	S("evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb7in(a, b, c, d)", 0-0) = a
	S("evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb7in(a, b, c, d)", 0-1) = ?
	S("evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb7in(a, b, c, d)", 0-2) = ?
	S("evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb7in(a, b, c, d)", 0-3) = ?
	S("evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, a, d)", 0-0) = a
	S("evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, a, d)", 0-1) = ?
	S("evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, a, d)", 0-2) = a
	S("evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, a, d)", 0-3) = ?
	S("evalrealheapsortstep2bb7in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, d, d)", 0-0) = a
	S("evalrealheapsortstep2bb7in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, d, d)", 0-1) = ?
	S("evalrealheapsortstep2bb7in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, d, d)", 0-2) = ?
	S("evalrealheapsortstep2bb7in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, d, d)", 0-3) = ?
orients the transitions
	evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb2in(a, b, c, d) [ a >= b + 2*c + 3 ]
	evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb10in(a, b, c, d) [ 2*c + b + 2 >= a ]
	evalrealheapsortstep2bb7in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, d, d)
	evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, a, d)
	evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb7in(a, b, c, d)
	evalrealheapsortstep2bb5in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 2)
	evalrealheapsortstep2bb4in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 1)
	evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb5in(a, b, c, d)
	evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d)
	evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d) [ a = 2*c + b + 3 ]
	evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb3in(a, b, c, d) [ a >= b + 2*c + 4 ]
	evalrealheapsortstep2bb10in(a, b, c, d) -> evalrealheapsortstep2bb11in(a, b + 1, c, d)
weakly and the transitions
	evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb10in(a, b, c, d) [ 2*c + b + 2 >= a ]
	evalrealheapsortstep2bb10in(a, b, c, d) -> evalrealheapsortstep2bb11in(a, b + 1, c, d)
strictly and produces the following problem:
7:	T:
		(?, 1)           evalrealheapsortstep2bb7in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, d, d)
		(?, 1)           evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, a, d)
		(?, 1)           evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb7in(a, b, c, d)
		(?, 1)           evalrealheapsortstep2bb5in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 2)
		(?, 1)           evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb5in(a, b, c, d)
		(?, 1)           evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d)
		(?, 1)           evalrealheapsortstep2bb4in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 1)
		(8*a + 14, 1)    evalrealheapsortstep2bb10in(a, b, c, d) -> evalrealheapsortstep2bb11in(a, b + 1, c, d)
		(?, 1)           evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb3in(a, b, c, d) [ a >= b + 2*c + 4 ]
		(?, 1)           evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d) [ a = 2*c + b + 3 ]
		(8*a + 14, 1)    evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb10in(a, b, c, d) [ 2*c + b + 2 >= a ]
		(?, 1)           evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb2in(a, b, c, d) [ a >= b + 2*c + 3 ]
		(4*a + 7, 1)     evalrealheapsortstep2bb1in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, 0, d)
		(4*a + 7, 1)     evalrealheapsortstep2bb11in(a, b, c, d) -> evalrealheapsortstep2bb1in(a, b, c, d) [ a >= b + 2 ]
		(1, 1)           evalrealheapsortstep2bbin(a, b, c, d) -> evalrealheapsortstep2bb11in(a, 0, c, d)
		(1, 1)           evalrealheapsortstep2entryin(a, b, c, d) -> evalrealheapsortstep2bbin(a, b, c, d) [ a >= 3 ]
		(1, 1)           evalrealheapsortstep2start(a, b, c, d) -> evalrealheapsortstep2entryin(a, b, c, d)
	start location:	evalrealheapsortstep2start
	leaf cost:	3

Applied AI with 'oct' on problem 7 to obtain the following invariants:
  For symbol evalrealheapsortstep2bb10in: X_3 >= 0 /\ X_2 + X_3 >= 0 /\ X_1 + X_3 - 3 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 - 3 >= 0 /\ X_1 - 3 >= 0
  For symbol evalrealheapsortstep2bb11in: X_2 >= 0 /\ X_1 + X_2 - 3 >= 0 /\ X_1 - 3 >= 0
  For symbol evalrealheapsortstep2bb1in: X_1 - X_2 - 2 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 - 3 >= 0 /\ X_1 - 3 >= 0
  For symbol evalrealheapsortstep2bb2in: X_1 - X_3 - 3 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 >= 0 /\ X_1 + X_3 - 3 >= 0 /\ X_1 - X_2 - 3 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 - 3 >= 0 /\ X_1 - 3 >= 0
  For symbol evalrealheapsortstep2bb3in: X_1 - X_3 - 4 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 >= 0 /\ X_1 + X_3 - 4 >= 0 /\ X_1 - X_2 - 4 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 - 4 >= 0 /\ X_1 - 4 >= 0
  For symbol evalrealheapsortstep2bb4in: X_1 - X_3 - 3 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 >= 0 /\ X_1 + X_3 - 3 >= 0 /\ X_1 - X_2 - 3 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 - 3 >= 0 /\ X_1 - 3 >= 0
  For symbol evalrealheapsortstep2bb5in: X_1 - X_3 - 4 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 >= 0 /\ X_1 + X_3 - 4 >= 0 /\ X_1 - X_2 - 4 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 - 4 >= 0 /\ X_1 - 4 >= 0
  For symbol evalrealheapsortstep2bb6in: X_4 - 1 >= 0 /\ X_3 + X_4 - 1 >= 0 /\ -X_3 + X_4 - 1 >= 0 /\ X_2 + X_4 - 1 >= 0 /\ X_1 + X_4 - 4 >= 0 /\ X_1 - X_3 - 3 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 >= 0 /\ X_1 + X_3 - 3 >= 0 /\ X_1 - X_2 - 3 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 - 3 >= 0 /\ X_1 - 3 >= 0
  For symbol evalrealheapsortstep2bb7in: X_4 - 1 >= 0 /\ X_3 + X_4 - 1 >= 0 /\ -X_3 + X_4 - 1 >= 0 /\ X_2 + X_4 - 1 >= 0 /\ X_1 + X_4 - 4 >= 0 /\ X_1 - X_3 - 3 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 >= 0 /\ X_1 + X_3 - 3 >= 0 /\ X_1 - X_2 - 3 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 - 3 >= 0 /\ X_1 - 3 >= 0
  For symbol evalrealheapsortstep2bb9in: X_3 >= 0 /\ X_2 + X_3 >= 0 /\ X_1 + X_3 - 3 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 - 3 >= 0 /\ X_1 - 3 >= 0
  For symbol evalrealheapsortstep2bbin: X_1 - 3 >= 0


This yielded the following problem:
8:	T:
		(1, 1)           evalrealheapsortstep2start(a, b, c, d) -> evalrealheapsortstep2entryin(a, b, c, d)
		(1, 1)           evalrealheapsortstep2entryin(a, b, c, d) -> evalrealheapsortstep2bbin(a, b, c, d) [ a >= 3 ]
		(1, 1)           evalrealheapsortstep2bbin(a, b, c, d) -> evalrealheapsortstep2bb11in(a, 0, c, d) [ a - 3 >= 0 ]
		(4*a + 7, 1)     evalrealheapsortstep2bb11in(a, b, c, d) -> evalrealheapsortstep2bb1in(a, b, c, d) [ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 /\ a >= b + 2 ]
		(4*a + 7, 1)     evalrealheapsortstep2bb1in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, 0, d) [ a - b - 2 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 ]
		(?, 1)           evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb2in(a, b, c, d) [ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 /\ a >= b + 2*c + 3 ]
		(8*a + 14, 1)    evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb10in(a, b, c, d) [ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 /\ 2*c + b + 2 >= a ]
		(?, 1)           evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d) [ a - c - 3 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 /\ a = 2*c + b + 3 ]
		(?, 1)           evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb3in(a, b, c, d) [ a - c - 3 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 /\ a >= b + 2*c + 4 ]
		(8*a + 14, 1)    evalrealheapsortstep2bb10in(a, b, c, d) -> evalrealheapsortstep2bb11in(a, b + 1, c, d) [ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 ]
		(?, 1)           evalrealheapsortstep2bb4in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 1) [ a - c - 3 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 ]
		(?, 1)           evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d) [ a - c - 4 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 4 >= 0 /\ a - b - 4 >= 0 /\ b >= 0 /\ a + b - 4 >= 0 /\ a - 4 >= 0 ]
		(?, 1)           evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb5in(a, b, c, d) [ a - c - 4 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 4 >= 0 /\ a - b - 4 >= 0 /\ b >= 0 /\ a + b - 4 >= 0 /\ a - 4 >= 0 ]
		(?, 1)           evalrealheapsortstep2bb5in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 2) [ a - c - 4 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 4 >= 0 /\ a - b - 4 >= 0 /\ b >= 0 /\ a + b - 4 >= 0 /\ a - 4 >= 0 ]
		(?, 1)           evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb7in(a, b, c, d) [ d - 1 >= 0 /\ c + d - 1 >= 0 /\ -c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d - 4 >= 0 /\ a - c - 3 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 ]
		(?, 1)           evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, a, d) [ d - 1 >= 0 /\ c + d - 1 >= 0 /\ -c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d - 4 >= 0 /\ a - c - 3 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 ]
		(?, 1)           evalrealheapsortstep2bb7in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, d, d) [ d - 1 >= 0 /\ c + d - 1 >= 0 /\ -c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d - 4 >= 0 /\ a - c - 3 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 ]
	start location:	evalrealheapsortstep2start
	leaf cost:	3

A polynomial rank function with
	Pol(evalrealheapsortstep2bb9in) = 6*V_1 - 6*V_3 - 12
	Pol(evalrealheapsortstep2bb2in) = 6*V_1 - 6*V_3 - 13
	Pol(evalrealheapsortstep2bb7in) = 6*V_1 - 6*V_3 - 17
	Pol(evalrealheapsortstep2bb6in) = 6*V_1 - 6*V_3 - 16
	Pol(evalrealheapsortstep2bb5in) = 6*V_1 - 6*V_3 - 15
	Pol(evalrealheapsortstep2bb4in) = 6*V_1 - 6*V_3 - 15
	Pol(evalrealheapsortstep2bb3in) = 6*V_1 - 6*V_3 - 14
and size complexities
	S("evalrealheapsortstep2bb7in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, d, d) [ d - 1 >= 0 /\\ c + d - 1 >= 0 /\\ -c + d - 1 >= 0 /\\ b + d - 1 >= 0 /\\ a + d - 4 >= 0 /\\ a - c - 3 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 ]", 0-0) = a
	S("evalrealheapsortstep2bb7in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, d, d) [ d - 1 >= 0 /\\ c + d - 1 >= 0 /\\ -c + d - 1 >= 0 /\\ b + d - 1 >= 0 /\\ a + d - 4 >= 0 /\\ a - c - 3 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 ]", 0-1) = 8*a + 896
	S("evalrealheapsortstep2bb7in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, d, d) [ d - 1 >= 0 /\\ c + d - 1 >= 0 /\\ -c + d - 1 >= 0 /\\ b + d - 1 >= 0 /\\ a + d - 4 >= 0 /\\ a - c - 3 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 ]", 0-2) = ?
	S("evalrealheapsortstep2bb7in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, d, d) [ d - 1 >= 0 /\\ c + d - 1 >= 0 /\\ -c + d - 1 >= 0 /\\ b + d - 1 >= 0 /\\ a + d - 4 >= 0 /\\ a - c - 3 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 ]", 0-3) = ?
	S("evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, a, d) [ d - 1 >= 0 /\\ c + d - 1 >= 0 /\\ -c + d - 1 >= 0 /\\ b + d - 1 >= 0 /\\ a + d - 4 >= 0 /\\ a - c - 3 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 ]", 0-0) = a
	S("evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, a, d) [ d - 1 >= 0 /\\ c + d - 1 >= 0 /\\ -c + d - 1 >= 0 /\\ b + d - 1 >= 0 /\\ a + d - 4 >= 0 /\\ a - c - 3 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 ]", 0-1) = 8*a + 896
	S("evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, a, d) [ d - 1 >= 0 /\\ c + d - 1 >= 0 /\\ -c + d - 1 >= 0 /\\ b + d - 1 >= 0 /\\ a + d - 4 >= 0 /\\ a - c - 3 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 ]", 0-2) = a
	S("evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, a, d) [ d - 1 >= 0 /\\ c + d - 1 >= 0 /\\ -c + d - 1 >= 0 /\\ b + d - 1 >= 0 /\\ a + d - 4 >= 0 /\\ a - c - 3 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 ]", 0-3) = ?
	S("evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb7in(a, b, c, d) [ d - 1 >= 0 /\\ c + d - 1 >= 0 /\\ -c + d - 1 >= 0 /\\ b + d - 1 >= 0 /\\ a + d - 4 >= 0 /\\ a - c - 3 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 ]", 0-0) = a
	S("evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb7in(a, b, c, d) [ d - 1 >= 0 /\\ c + d - 1 >= 0 /\\ -c + d - 1 >= 0 /\\ b + d - 1 >= 0 /\\ a + d - 4 >= 0 /\\ a - c - 3 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 ]", 0-1) = 8*a + 896
	S("evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb7in(a, b, c, d) [ d - 1 >= 0 /\\ c + d - 1 >= 0 /\\ -c + d - 1 >= 0 /\\ b + d - 1 >= 0 /\\ a + d - 4 >= 0 /\\ a - c - 3 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 ]", 0-2) = ?
	S("evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb7in(a, b, c, d) [ d - 1 >= 0 /\\ c + d - 1 >= 0 /\\ -c + d - 1 >= 0 /\\ b + d - 1 >= 0 /\\ a + d - 4 >= 0 /\\ a - c - 3 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 ]", 0-3) = ?
	S("evalrealheapsortstep2bb5in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 2) [ a - c - 4 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 4 >= 0 /\\ a - b - 4 >= 0 /\\ b >= 0 /\\ a + b - 4 >= 0 /\\ a - 4 >= 0 ]", 0-0) = a
	S("evalrealheapsortstep2bb5in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 2) [ a - c - 4 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 4 >= 0 /\\ a - b - 4 >= 0 /\\ b >= 0 /\\ a + b - 4 >= 0 /\\ a - 4 >= 0 ]", 0-1) = 8*a + 896
	S("evalrealheapsortstep2bb5in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 2) [ a - c - 4 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 4 >= 0 /\\ a - b - 4 >= 0 /\\ b >= 0 /\\ a + b - 4 >= 0 /\\ a - 4 >= 0 ]", 0-2) = ?
	S("evalrealheapsortstep2bb5in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 2) [ a - c - 4 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 4 >= 0 /\\ a - b - 4 >= 0 /\\ b >= 0 /\\ a + b - 4 >= 0 /\\ a - 4 >= 0 ]", 0-3) = ?
	S("evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb5in(a, b, c, d) [ a - c - 4 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 4 >= 0 /\\ a - b - 4 >= 0 /\\ b >= 0 /\\ a + b - 4 >= 0 /\\ a - 4 >= 0 ]", 0-0) = a
	S("evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb5in(a, b, c, d) [ a - c - 4 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 4 >= 0 /\\ a - b - 4 >= 0 /\\ b >= 0 /\\ a + b - 4 >= 0 /\\ a - 4 >= 0 ]", 0-1) = 8*a + 896
	S("evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb5in(a, b, c, d) [ a - c - 4 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 4 >= 0 /\\ a - b - 4 >= 0 /\\ b >= 0 /\\ a + b - 4 >= 0 /\\ a - 4 >= 0 ]", 0-2) = ?
	S("evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb5in(a, b, c, d) [ a - c - 4 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 4 >= 0 /\\ a - b - 4 >= 0 /\\ b >= 0 /\\ a + b - 4 >= 0 /\\ a - 4 >= 0 ]", 0-3) = ?
	S("evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d) [ a - c - 4 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 4 >= 0 /\\ a - b - 4 >= 0 /\\ b >= 0 /\\ a + b - 4 >= 0 /\\ a - 4 >= 0 ]", 0-0) = a
	S("evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d) [ a - c - 4 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 4 >= 0 /\\ a - b - 4 >= 0 /\\ b >= 0 /\\ a + b - 4 >= 0 /\\ a - 4 >= 0 ]", 0-1) = 8*a + 896
	S("evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d) [ a - c - 4 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 4 >= 0 /\\ a - b - 4 >= 0 /\\ b >= 0 /\\ a + b - 4 >= 0 /\\ a - 4 >= 0 ]", 0-2) = ?
	S("evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d) [ a - c - 4 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 4 >= 0 /\\ a - b - 4 >= 0 /\\ b >= 0 /\\ a + b - 4 >= 0 /\\ a - 4 >= 0 ]", 0-3) = ?
	S("evalrealheapsortstep2bb4in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 1) [ a - c - 3 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 ]", 0-0) = a
	S("evalrealheapsortstep2bb4in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 1) [ a - c - 3 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 ]", 0-1) = 8*a + 896
	S("evalrealheapsortstep2bb4in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 1) [ a - c - 3 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 ]", 0-2) = ?
	S("evalrealheapsortstep2bb4in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 1) [ a - c - 3 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 ]", 0-3) = ?
	S("evalrealheapsortstep2bb10in(a, b, c, d) -> evalrealheapsortstep2bb11in(a, b + 1, c, d) [ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 ]", 0-0) = a
	S("evalrealheapsortstep2bb10in(a, b, c, d) -> evalrealheapsortstep2bb11in(a, b + 1, c, d) [ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 ]", 0-1) = 8*a + 896
	S("evalrealheapsortstep2bb10in(a, b, c, d) -> evalrealheapsortstep2bb11in(a, b + 1, c, d) [ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 ]", 0-2) = ?
	S("evalrealheapsortstep2bb10in(a, b, c, d) -> evalrealheapsortstep2bb11in(a, b + 1, c, d) [ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 ]", 0-3) = ?
	S("evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb3in(a, b, c, d) [ a - c - 3 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 /\\ a >= b + 2*c + 4 ]", 0-0) = a
	S("evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb3in(a, b, c, d) [ a - c - 3 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 /\\ a >= b + 2*c + 4 ]", 0-1) = 8*a + 896
	S("evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb3in(a, b, c, d) [ a - c - 3 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 /\\ a >= b + 2*c + 4 ]", 0-2) = ?
	S("evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb3in(a, b, c, d) [ a - c - 3 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 /\\ a >= b + 2*c + 4 ]", 0-3) = ?
	S("evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d) [ a - c - 3 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 /\\ a = 2*c + b + 3 ]", 0-0) = a
	S("evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d) [ a - c - 3 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 /\\ a = 2*c + b + 3 ]", 0-1) = 8*a + 896
	S("evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d) [ a - c - 3 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 /\\ a = 2*c + b + 3 ]", 0-2) = ?
	S("evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d) [ a - c - 3 >= 0 /\\ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ a - b - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 /\\ a = 2*c + b + 3 ]", 0-3) = ?
	S("evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb10in(a, b, c, d) [ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 /\\ 2*c + b + 2 >= a ]", 0-0) = a
	S("evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb10in(a, b, c, d) [ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 /\\ 2*c + b + 2 >= a ]", 0-1) = 8*a + 896
	S("evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb10in(a, b, c, d) [ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 /\\ 2*c + b + 2 >= a ]", 0-2) = ?
	S("evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb10in(a, b, c, d) [ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 /\\ 2*c + b + 2 >= a ]", 0-3) = ?
	S("evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb2in(a, b, c, d) [ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 /\\ a >= b + 2*c + 3 ]", 0-0) = a
	S("evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb2in(a, b, c, d) [ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 /\\ a >= b + 2*c + 3 ]", 0-1) = 8*a + 896
	S("evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb2in(a, b, c, d) [ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 /\\ a >= b + 2*c + 3 ]", 0-2) = ?
	S("evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb2in(a, b, c, d) [ c >= 0 /\\ b + c >= 0 /\\ a + c - 3 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 /\\ a >= b + 2*c + 3 ]", 0-3) = ?
	S("evalrealheapsortstep2bb1in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, 0, d) [ a - b - 2 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 ]", 0-0) = a
	S("evalrealheapsortstep2bb1in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, 0, d) [ a - b - 2 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 ]", 0-1) = 8*a + 896
	S("evalrealheapsortstep2bb1in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, 0, d) [ a - b - 2 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 ]", 0-2) = 0
	S("evalrealheapsortstep2bb1in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, 0, d) [ a - b - 2 >= 0 /\\ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 ]", 0-3) = ?
	S("evalrealheapsortstep2bb11in(a, b, c, d) -> evalrealheapsortstep2bb1in(a, b, c, d) [ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 /\\ a >= b + 2 ]", 0-0) = a
	S("evalrealheapsortstep2bb11in(a, b, c, d) -> evalrealheapsortstep2bb1in(a, b, c, d) [ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 /\\ a >= b + 2 ]", 0-1) = 8*a + 896
	S("evalrealheapsortstep2bb11in(a, b, c, d) -> evalrealheapsortstep2bb1in(a, b, c, d) [ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 /\\ a >= b + 2 ]", 0-2) = ?
	S("evalrealheapsortstep2bb11in(a, b, c, d) -> evalrealheapsortstep2bb1in(a, b, c, d) [ b >= 0 /\\ a + b - 3 >= 0 /\\ a - 3 >= 0 /\\ a >= b + 2 ]", 0-3) = ?
	S("evalrealheapsortstep2bbin(a, b, c, d) -> evalrealheapsortstep2bb11in(a, 0, c, d) [ a - 3 >= 0 ]", 0-0) = a
	S("evalrealheapsortstep2bbin(a, b, c, d) -> evalrealheapsortstep2bb11in(a, 0, c, d) [ a - 3 >= 0 ]", 0-1) = 0
	S("evalrealheapsortstep2bbin(a, b, c, d) -> evalrealheapsortstep2bb11in(a, 0, c, d) [ a - 3 >= 0 ]", 0-2) = c
	S("evalrealheapsortstep2bbin(a, b, c, d) -> evalrealheapsortstep2bb11in(a, 0, c, d) [ a - 3 >= 0 ]", 0-3) = d
	S("evalrealheapsortstep2entryin(a, b, c, d) -> evalrealheapsortstep2bbin(a, b, c, d) [ a >= 3 ]", 0-0) = a
	S("evalrealheapsortstep2entryin(a, b, c, d) -> evalrealheapsortstep2bbin(a, b, c, d) [ a >= 3 ]", 0-1) = b
	S("evalrealheapsortstep2entryin(a, b, c, d) -> evalrealheapsortstep2bbin(a, b, c, d) [ a >= 3 ]", 0-2) = c
	S("evalrealheapsortstep2entryin(a, b, c, d) -> evalrealheapsortstep2bbin(a, b, c, d) [ a >= 3 ]", 0-3) = d
	S("evalrealheapsortstep2start(a, b, c, d) -> evalrealheapsortstep2entryin(a, b, c, d)", 0-0) = a
	S("evalrealheapsortstep2start(a, b, c, d) -> evalrealheapsortstep2entryin(a, b, c, d)", 0-1) = b
	S("evalrealheapsortstep2start(a, b, c, d) -> evalrealheapsortstep2entryin(a, b, c, d)", 0-2) = c
	S("evalrealheapsortstep2start(a, b, c, d) -> evalrealheapsortstep2entryin(a, b, c, d)", 0-3) = d
orients the transitions
	evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb2in(a, b, c, d) [ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 /\ a >= b + 2*c + 3 ]
	evalrealheapsortstep2bb7in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, d, d) [ d - 1 >= 0 /\ c + d - 1 >= 0 /\ -c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d - 4 >= 0 /\ a - c - 3 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 ]
	evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, a, d) [ d - 1 >= 0 /\ c + d - 1 >= 0 /\ -c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d - 4 >= 0 /\ a - c - 3 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 ]
	evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb7in(a, b, c, d) [ d - 1 >= 0 /\ c + d - 1 >= 0 /\ -c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d - 4 >= 0 /\ a - c - 3 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 ]
	evalrealheapsortstep2bb5in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 2) [ a - c - 4 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 4 >= 0 /\ a - b - 4 >= 0 /\ b >= 0 /\ a + b - 4 >= 0 /\ a - 4 >= 0 ]
	evalrealheapsortstep2bb4in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 1) [ a - c - 3 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 ]
	evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb5in(a, b, c, d) [ a - c - 4 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 4 >= 0 /\ a - b - 4 >= 0 /\ b >= 0 /\ a + b - 4 >= 0 /\ a - 4 >= 0 ]
	evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d) [ a - c - 4 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 4 >= 0 /\ a - b - 4 >= 0 /\ b >= 0 /\ a + b - 4 >= 0 /\ a - 4 >= 0 ]
	evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d) [ a - c - 3 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 /\ a = 2*c + b + 3 ]
	evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb3in(a, b, c, d) [ a - c - 3 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 /\ a >= b + 2*c + 4 ]
weakly and the transitions
	evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb2in(a, b, c, d) [ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 /\ a >= b + 2*c + 3 ]
	evalrealheapsortstep2bb7in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, d, d) [ d - 1 >= 0 /\ c + d - 1 >= 0 /\ -c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d - 4 >= 0 /\ a - c - 3 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 ]
	evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, a, d) [ d - 1 >= 0 /\ c + d - 1 >= 0 /\ -c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d - 4 >= 0 /\ a - c - 3 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 ]
	evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb7in(a, b, c, d) [ d - 1 >= 0 /\ c + d - 1 >= 0 /\ -c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d - 4 >= 0 /\ a - c - 3 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 ]
	evalrealheapsortstep2bb5in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 2) [ a - c - 4 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 4 >= 0 /\ a - b - 4 >= 0 /\ b >= 0 /\ a + b - 4 >= 0 /\ a - 4 >= 0 ]
	evalrealheapsortstep2bb4in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 1) [ a - c - 3 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 ]
	evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb5in(a, b, c, d) [ a - c - 4 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 4 >= 0 /\ a - b - 4 >= 0 /\ b >= 0 /\ a + b - 4 >= 0 /\ a - 4 >= 0 ]
	evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d) [ a - c - 4 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 4 >= 0 /\ a - b - 4 >= 0 /\ b >= 0 /\ a + b - 4 >= 0 /\ a - 4 >= 0 ]
	evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d) [ a - c - 3 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 /\ a = 2*c + b + 3 ]
	evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb3in(a, b, c, d) [ a - c - 3 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 /\ a >= b + 2*c + 4 ]
strictly and produces the following problem:
9:	T:
		(1, 1)                     evalrealheapsortstep2start(a, b, c, d) -> evalrealheapsortstep2entryin(a, b, c, d)
		(1, 1)                     evalrealheapsortstep2entryin(a, b, c, d) -> evalrealheapsortstep2bbin(a, b, c, d) [ a >= 3 ]
		(1, 1)                     evalrealheapsortstep2bbin(a, b, c, d) -> evalrealheapsortstep2bb11in(a, 0, c, d) [ a - 3 >= 0 ]
		(4*a + 7, 1)               evalrealheapsortstep2bb11in(a, b, c, d) -> evalrealheapsortstep2bb1in(a, b, c, d) [ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 /\ a >= b + 2 ]
		(4*a + 7, 1)               evalrealheapsortstep2bb1in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, 0, d) [ a - b - 2 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 ]
		(24*a^2 + 90*a + 84, 1)    evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb2in(a, b, c, d) [ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 /\ a >= b + 2*c + 3 ]
		(8*a + 14, 1)              evalrealheapsortstep2bb9in(a, b, c, d) -> evalrealheapsortstep2bb10in(a, b, c, d) [ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 /\ 2*c + b + 2 >= a ]
		(24*a^2 + 90*a + 84, 1)    evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d) [ a - c - 3 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 /\ a = 2*c + b + 3 ]
		(24*a^2 + 90*a + 84, 1)    evalrealheapsortstep2bb2in(a, b, c, d) -> evalrealheapsortstep2bb3in(a, b, c, d) [ a - c - 3 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 /\ a >= b + 2*c + 4 ]
		(8*a + 14, 1)              evalrealheapsortstep2bb10in(a, b, c, d) -> evalrealheapsortstep2bb11in(a, b + 1, c, d) [ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 ]
		(24*a^2 + 90*a + 84, 1)    evalrealheapsortstep2bb4in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 1) [ a - c - 3 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 ]
		(24*a^2 + 90*a + 84, 1)    evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb4in(a, b, c, d) [ a - c - 4 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 4 >= 0 /\ a - b - 4 >= 0 /\ b >= 0 /\ a + b - 4 >= 0 /\ a - 4 >= 0 ]
		(24*a^2 + 90*a + 84, 1)    evalrealheapsortstep2bb3in(a, b, c, d) -> evalrealheapsortstep2bb5in(a, b, c, d) [ a - c - 4 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 4 >= 0 /\ a - b - 4 >= 0 /\ b >= 0 /\ a + b - 4 >= 0 /\ a - 4 >= 0 ]
		(24*a^2 + 90*a + 84, 1)    evalrealheapsortstep2bb5in(a, b, c, d) -> evalrealheapsortstep2bb6in(a, b, c, 2*c + 2) [ a - c - 4 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 4 >= 0 /\ a - b - 4 >= 0 /\ b >= 0 /\ a + b - 4 >= 0 /\ a - 4 >= 0 ]
		(24*a^2 + 90*a + 84, 1)    evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb7in(a, b, c, d) [ d - 1 >= 0 /\ c + d - 1 >= 0 /\ -c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d - 4 >= 0 /\ a - c - 3 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 ]
		(24*a^2 + 90*a + 84, 1)    evalrealheapsortstep2bb6in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, a, d) [ d - 1 >= 0 /\ c + d - 1 >= 0 /\ -c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d - 4 >= 0 /\ a - c - 3 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 ]
		(24*a^2 + 90*a + 84, 1)    evalrealheapsortstep2bb7in(a, b, c, d) -> evalrealheapsortstep2bb9in(a, b, d, d) [ d - 1 >= 0 /\ c + d - 1 >= 0 /\ -c + d - 1 >= 0 /\ b + d - 1 >= 0 /\ a + d - 4 >= 0 /\ a - c - 3 >= 0 /\ c >= 0 /\ b + c >= 0 /\ a + c - 3 >= 0 /\ a - b - 3 >= 0 /\ b >= 0 /\ a + b - 3 >= 0 /\ a - 3 >= 0 ]
	start location:	evalrealheapsortstep2start
	leaf cost:	3

Complexity upper bound 924*a + 240*a^2 + 888

Time: 1.183 sec (SMT: 1.096 sec)