YES(?, 422*c + 20*c^2 + 591)

Initial complexity problem:
1:	T:
		(1, 1)    f0(a, b, c, d, e, f, g) -> f10(h, 0, c, d, e, f, g)
		(?, 1)    f10(a, b, c, d, e, f, g) -> f10(a, b + 1, c, d, e, f, g) [ c >= b + 1 ]
		(?, 1)    f18(a, b, c, d, e, f, g) -> f21(a, b, c, d, e, 0, g) [ d >= e + 2 ]
		(?, 1)    f21(a, b, c, d, e, f, g) -> f21(a, b, c, d, e, f + 1, g) [ d >= e + f + 2 ]
		(?, 1)    f21(a, b, c, d, e, f, g) -> f21(a, b, c, d, e, f + 1, h) [ d >= e + f + 2 ]
		(?, 1)    f32(a, b, c, d, e, f, g) -> f32(a, b, c, d, e + 1, f, g) [ d >= e + 2 ]
		(?, 1)    f32(a, b, c, d, e, f, g) -> f41(a, b, c, d, e, f, g) [ e + 1 >= d ]
		(?, 1)    f21(a, b, c, d, e, f, g) -> f18(a, b, c, d, e + 1, f, g) [ f + e + 1 >= d ]
		(?, 1)    f18(a, b, c, d, e, f, g) -> f32(a, b, c, d, 0, f, g) [ e + 1 >= d ]
		(?, 1)    f10(a, b, c, d, e, f, g) -> f18(a, b, c, c, 0, f, g) [ b >= c ]
	start location:	f0
	leaf cost:	0

Slicing away variables that do not contribute to conditions from problem 1 leaves variables [b, c, d, e, f].
We thus obtain the following problem:
2:	T:
		(?, 1)    f10(b, c, d, e, f) -> f18(b, c, c, 0, f) [ b >= c ]
		(?, 1)    f18(b, c, d, e, f) -> f32(b, c, d, 0, f) [ e + 1 >= d ]
		(?, 1)    f21(b, c, d, e, f) -> f18(b, c, d, e + 1, f) [ f + e + 1 >= d ]
		(?, 1)    f32(b, c, d, e, f) -> f41(b, c, d, e, f) [ e + 1 >= d ]
		(?, 1)    f32(b, c, d, e, f) -> f32(b, c, d, e + 1, f) [ d >= e + 2 ]
		(?, 1)    f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]
		(?, 1)    f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]
		(?, 1)    f18(b, c, d, e, f) -> f21(b, c, d, e, 0) [ d >= e + 2 ]
		(?, 1)    f10(b, c, d, e, f) -> f10(b + 1, c, d, e, f) [ c >= b + 1 ]
		(1, 1)    f0(b, c, d, e, f) -> f10(0, c, d, e, f)
	start location:	f0
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem:
3:	T:
		(?, 1)    f10(b, c, d, e, f) -> f18(b, c, c, 0, f) [ b >= c ]
		(?, 1)    f18(b, c, d, e, f) -> f32(b, c, d, 0, f) [ e + 1 >= d ]
		(?, 1)    f21(b, c, d, e, f) -> f18(b, c, d, e + 1, f) [ f + e + 1 >= d ]
		(?, 1)    f32(b, c, d, e, f) -> f32(b, c, d, e + 1, f) [ d >= e + 2 ]
		(?, 1)    f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]
		(?, 1)    f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]
		(?, 1)    f18(b, c, d, e, f) -> f21(b, c, d, e, 0) [ d >= e + 2 ]
		(?, 1)    f10(b, c, d, e, f) -> f10(b + 1, c, d, e, f) [ c >= b + 1 ]
		(1, 1)    f0(b, c, d, e, f) -> f10(0, c, d, e, f)
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f10) = 1
	Pol(f18) = -2
	Pol(f32) = -3
	Pol(f21) = -2
	Pol(f0) = 1
orients all transitions weakly and the transition
	f10(b, c, d, e, f) -> f18(b, c, c, 0, f) [ b >= c ]
strictly and produces the following problem:
4:	T:
		(1, 1)    f10(b, c, d, e, f) -> f18(b, c, c, 0, f) [ b >= c ]
		(?, 1)    f18(b, c, d, e, f) -> f32(b, c, d, 0, f) [ e + 1 >= d ]
		(?, 1)    f21(b, c, d, e, f) -> f18(b, c, d, e + 1, f) [ f + e + 1 >= d ]
		(?, 1)    f32(b, c, d, e, f) -> f32(b, c, d, e + 1, f) [ d >= e + 2 ]
		(?, 1)    f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]
		(?, 1)    f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]
		(?, 1)    f18(b, c, d, e, f) -> f21(b, c, d, e, 0) [ d >= e + 2 ]
		(?, 1)    f10(b, c, d, e, f) -> f10(b + 1, c, d, e, f) [ c >= b + 1 ]
		(1, 1)    f0(b, c, d, e, f) -> f10(0, c, d, e, f)
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f10) = 2
	Pol(f18) = 2
	Pol(f32) = -2
	Pol(f21) = 2
	Pol(f0) = 2
orients all transitions weakly and the transition
	f18(b, c, d, e, f) -> f32(b, c, d, 0, f) [ e + 1 >= d ]
strictly and produces the following problem:
5:	T:
		(1, 1)    f10(b, c, d, e, f) -> f18(b, c, c, 0, f) [ b >= c ]
		(2, 1)    f18(b, c, d, e, f) -> f32(b, c, d, 0, f) [ e + 1 >= d ]
		(?, 1)    f21(b, c, d, e, f) -> f18(b, c, d, e + 1, f) [ f + e + 1 >= d ]
		(?, 1)    f32(b, c, d, e, f) -> f32(b, c, d, e + 1, f) [ d >= e + 2 ]
		(?, 1)    f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]
		(?, 1)    f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]
		(?, 1)    f18(b, c, d, e, f) -> f21(b, c, d, e, 0) [ d >= e + 2 ]
		(?, 1)    f10(b, c, d, e, f) -> f10(b + 1, c, d, e, f) [ c >= b + 1 ]
		(1, 1)    f0(b, c, d, e, f) -> f10(0, c, d, e, f)
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f10) = -V_1 + V_2
	Pol(f18) = -4*V_1 + V_2 + 3*V_3 - 2
	Pol(f32) = -4*V_1 + V_2 + 3*V_3 - V_4 - 4
	Pol(f21) = -4*V_1 + V_2 + 3*V_3 - 2
	Pol(f0) = V_2
orients all transitions weakly and the transition
	f10(b, c, d, e, f) -> f10(b + 1, c, d, e, f) [ c >= b + 1 ]
strictly and produces the following problem:
6:	T:
		(1, 1)    f10(b, c, d, e, f) -> f18(b, c, c, 0, f) [ b >= c ]
		(2, 1)    f18(b, c, d, e, f) -> f32(b, c, d, 0, f) [ e + 1 >= d ]
		(?, 1)    f21(b, c, d, e, f) -> f18(b, c, d, e + 1, f) [ f + e + 1 >= d ]
		(?, 1)    f32(b, c, d, e, f) -> f32(b, c, d, e + 1, f) [ d >= e + 2 ]
		(?, 1)    f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]
		(?, 1)    f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]
		(?, 1)    f18(b, c, d, e, f) -> f21(b, c, d, e, 0) [ d >= e + 2 ]
		(c, 1)    f10(b, c, d, e, f) -> f10(b + 1, c, d, e, f) [ c >= b + 1 ]
		(1, 1)    f0(b, c, d, e, f) -> f10(0, c, d, e, f)
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f10) = V_2 - 1
	Pol(f18) = V_3 - 1
	Pol(f32) = V_3 - V_4 - 1
	Pol(f21) = V_3 - 1
	Pol(f0) = V_2 - 1
orients all transitions weakly and the transition
	f32(b, c, d, e, f) -> f32(b, c, d, e + 1, f) [ d >= e + 2 ]
strictly and produces the following problem:
7:	T:
		(1, 1)        f10(b, c, d, e, f) -> f18(b, c, c, 0, f) [ b >= c ]
		(2, 1)        f18(b, c, d, e, f) -> f32(b, c, d, 0, f) [ e + 1 >= d ]
		(?, 1)        f21(b, c, d, e, f) -> f18(b, c, d, e + 1, f) [ f + e + 1 >= d ]
		(c + 1, 1)    f32(b, c, d, e, f) -> f32(b, c, d, e + 1, f) [ d >= e + 2 ]
		(?, 1)        f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]
		(?, 1)        f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]
		(?, 1)        f18(b, c, d, e, f) -> f21(b, c, d, e, 0) [ d >= e + 2 ]
		(c, 1)        f10(b, c, d, e, f) -> f10(b + 1, c, d, e, f) [ c >= b + 1 ]
		(1, 1)        f0(b, c, d, e, f) -> f10(0, c, d, e, f)
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f21) = 2*V_3 - 2*V_4 - 4
	Pol(f18) = 2*V_3 - 2*V_4 - 3
and size complexities
	S("f0(b, c, d, e, f) -> f10(0, c, d, e, f)", 0-0) = 0
	S("f0(b, c, d, e, f) -> f10(0, c, d, e, f)", 0-1) = c
	S("f0(b, c, d, e, f) -> f10(0, c, d, e, f)", 0-2) = d
	S("f0(b, c, d, e, f) -> f10(0, c, d, e, f)", 0-3) = e
	S("f0(b, c, d, e, f) -> f10(0, c, d, e, f)", 0-4) = f
	S("f10(b, c, d, e, f) -> f10(b + 1, c, d, e, f) [ c >= b + 1 ]", 0-0) = c
	S("f10(b, c, d, e, f) -> f10(b + 1, c, d, e, f) [ c >= b + 1 ]", 0-1) = c
	S("f10(b, c, d, e, f) -> f10(b + 1, c, d, e, f) [ c >= b + 1 ]", 0-2) = d
	S("f10(b, c, d, e, f) -> f10(b + 1, c, d, e, f) [ c >= b + 1 ]", 0-3) = e
	S("f10(b, c, d, e, f) -> f10(b + 1, c, d, e, f) [ c >= b + 1 ]", 0-4) = f
	S("f18(b, c, d, e, f) -> f21(b, c, d, e, 0) [ d >= e + 2 ]", 0-0) = c
	S("f18(b, c, d, e, f) -> f21(b, c, d, e, 0) [ d >= e + 2 ]", 0-1) = c
	S("f18(b, c, d, e, f) -> f21(b, c, d, e, 0) [ d >= e + 2 ]", 0-2) = c
	S("f18(b, c, d, e, f) -> f21(b, c, d, e, 0) [ d >= e + 2 ]", 0-3) = ?
	S("f18(b, c, d, e, f) -> f21(b, c, d, e, 0) [ d >= e + 2 ]", 0-4) = 0
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-0) = c
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-1) = c
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-2) = c
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-3) = ?
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-4) = ?
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-0) = c
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-1) = c
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-2) = c
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-3) = ?
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-4) = ?
	S("f32(b, c, d, e, f) -> f32(b, c, d, e + 1, f) [ d >= e + 2 ]", 0-0) = c
	S("f32(b, c, d, e, f) -> f32(b, c, d, e + 1, f) [ d >= e + 2 ]", 0-1) = c
	S("f32(b, c, d, e, f) -> f32(b, c, d, e + 1, f) [ d >= e + 2 ]", 0-2) = c
	S("f32(b, c, d, e, f) -> f32(b, c, d, e + 1, f) [ d >= e + 2 ]", 0-3) = c + 1
	S("f32(b, c, d, e, f) -> f32(b, c, d, e + 1, f) [ d >= e + 2 ]", 0-4) = ?
	S("f21(b, c, d, e, f) -> f18(b, c, d, e + 1, f) [ f + e + 1 >= d ]", 0-0) = c
	S("f21(b, c, d, e, f) -> f18(b, c, d, e + 1, f) [ f + e + 1 >= d ]", 0-1) = c
	S("f21(b, c, d, e, f) -> f18(b, c, d, e + 1, f) [ f + e + 1 >= d ]", 0-2) = c
	S("f21(b, c, d, e, f) -> f18(b, c, d, e + 1, f) [ f + e + 1 >= d ]", 0-3) = ?
	S("f21(b, c, d, e, f) -> f18(b, c, d, e + 1, f) [ f + e + 1 >= d ]", 0-4) = ?
	S("f18(b, c, d, e, f) -> f32(b, c, d, 0, f) [ e + 1 >= d ]", 0-0) = c
	S("f18(b, c, d, e, f) -> f32(b, c, d, 0, f) [ e + 1 >= d ]", 0-1) = c
	S("f18(b, c, d, e, f) -> f32(b, c, d, 0, f) [ e + 1 >= d ]", 0-2) = c
	S("f18(b, c, d, e, f) -> f32(b, c, d, 0, f) [ e + 1 >= d ]", 0-3) = 0
	S("f18(b, c, d, e, f) -> f32(b, c, d, 0, f) [ e + 1 >= d ]", 0-4) = ?
	S("f10(b, c, d, e, f) -> f18(b, c, c, 0, f) [ b >= c ]", 0-0) = c
	S("f10(b, c, d, e, f) -> f18(b, c, c, 0, f) [ b >= c ]", 0-1) = c
	S("f10(b, c, d, e, f) -> f18(b, c, c, 0, f) [ b >= c ]", 0-2) = c
	S("f10(b, c, d, e, f) -> f18(b, c, c, 0, f) [ b >= c ]", 0-3) = 0
	S("f10(b, c, d, e, f) -> f18(b, c, c, 0, f) [ b >= c ]", 0-4) = f
orients the transitions
	f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]
	f21(b, c, d, e, f) -> f18(b, c, d, e + 1, f) [ f + e + 1 >= d ]
	f18(b, c, d, e, f) -> f21(b, c, d, e, 0) [ d >= e + 2 ]
weakly and the transition
	f18(b, c, d, e, f) -> f21(b, c, d, e, 0) [ d >= e + 2 ]
strictly and produces the following problem:
8:	T:
		(1, 1)          f10(b, c, d, e, f) -> f18(b, c, c, 0, f) [ b >= c ]
		(2, 1)          f18(b, c, d, e, f) -> f32(b, c, d, 0, f) [ e + 1 >= d ]
		(?, 1)          f21(b, c, d, e, f) -> f18(b, c, d, e + 1, f) [ f + e + 1 >= d ]
		(c + 1, 1)      f32(b, c, d, e, f) -> f32(b, c, d, e + 1, f) [ d >= e + 2 ]
		(?, 1)          f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]
		(?, 1)          f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]
		(2*c + 3, 1)    f18(b, c, d, e, f) -> f21(b, c, d, e, 0) [ d >= e + 2 ]
		(c, 1)          f10(b, c, d, e, f) -> f10(b + 1, c, d, e, f) [ c >= b + 1 ]
		(1, 1)          f0(b, c, d, e, f) -> f10(0, c, d, e, f)
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f21) = 2
	Pol(f18) = 1
and size complexities
	S("f0(b, c, d, e, f) -> f10(0, c, d, e, f)", 0-0) = 0
	S("f0(b, c, d, e, f) -> f10(0, c, d, e, f)", 0-1) = c
	S("f0(b, c, d, e, f) -> f10(0, c, d, e, f)", 0-2) = d
	S("f0(b, c, d, e, f) -> f10(0, c, d, e, f)", 0-3) = e
	S("f0(b, c, d, e, f) -> f10(0, c, d, e, f)", 0-4) = f
	S("f10(b, c, d, e, f) -> f10(b + 1, c, d, e, f) [ c >= b + 1 ]", 0-0) = c
	S("f10(b, c, d, e, f) -> f10(b + 1, c, d, e, f) [ c >= b + 1 ]", 0-1) = c
	S("f10(b, c, d, e, f) -> f10(b + 1, c, d, e, f) [ c >= b + 1 ]", 0-2) = d
	S("f10(b, c, d, e, f) -> f10(b + 1, c, d, e, f) [ c >= b + 1 ]", 0-3) = e
	S("f10(b, c, d, e, f) -> f10(b + 1, c, d, e, f) [ c >= b + 1 ]", 0-4) = f
	S("f18(b, c, d, e, f) -> f21(b, c, d, e, 0) [ d >= e + 2 ]", 0-0) = c
	S("f18(b, c, d, e, f) -> f21(b, c, d, e, 0) [ d >= e + 2 ]", 0-1) = c
	S("f18(b, c, d, e, f) -> f21(b, c, d, e, 0) [ d >= e + 2 ]", 0-2) = c
	S("f18(b, c, d, e, f) -> f21(b, c, d, e, 0) [ d >= e + 2 ]", 0-3) = ?
	S("f18(b, c, d, e, f) -> f21(b, c, d, e, 0) [ d >= e + 2 ]", 0-4) = 0
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-0) = c
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-1) = c
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-2) = c
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-3) = ?
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-4) = ?
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-0) = c
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-1) = c
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-2) = c
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-3) = ?
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-4) = ?
	S("f32(b, c, d, e, f) -> f32(b, c, d, e + 1, f) [ d >= e + 2 ]", 0-0) = c
	S("f32(b, c, d, e, f) -> f32(b, c, d, e + 1, f) [ d >= e + 2 ]", 0-1) = c
	S("f32(b, c, d, e, f) -> f32(b, c, d, e + 1, f) [ d >= e + 2 ]", 0-2) = c
	S("f32(b, c, d, e, f) -> f32(b, c, d, e + 1, f) [ d >= e + 2 ]", 0-3) = c + 1
	S("f32(b, c, d, e, f) -> f32(b, c, d, e + 1, f) [ d >= e + 2 ]", 0-4) = ?
	S("f21(b, c, d, e, f) -> f18(b, c, d, e + 1, f) [ f + e + 1 >= d ]", 0-0) = c
	S("f21(b, c, d, e, f) -> f18(b, c, d, e + 1, f) [ f + e + 1 >= d ]", 0-1) = c
	S("f21(b, c, d, e, f) -> f18(b, c, d, e + 1, f) [ f + e + 1 >= d ]", 0-2) = c
	S("f21(b, c, d, e, f) -> f18(b, c, d, e + 1, f) [ f + e + 1 >= d ]", 0-3) = ?
	S("f21(b, c, d, e, f) -> f18(b, c, d, e + 1, f) [ f + e + 1 >= d ]", 0-4) = ?
	S("f18(b, c, d, e, f) -> f32(b, c, d, 0, f) [ e + 1 >= d ]", 0-0) = c
	S("f18(b, c, d, e, f) -> f32(b, c, d, 0, f) [ e + 1 >= d ]", 0-1) = c
	S("f18(b, c, d, e, f) -> f32(b, c, d, 0, f) [ e + 1 >= d ]", 0-2) = c
	S("f18(b, c, d, e, f) -> f32(b, c, d, 0, f) [ e + 1 >= d ]", 0-3) = 0
	S("f18(b, c, d, e, f) -> f32(b, c, d, 0, f) [ e + 1 >= d ]", 0-4) = ?
	S("f10(b, c, d, e, f) -> f18(b, c, c, 0, f) [ b >= c ]", 0-0) = c
	S("f10(b, c, d, e, f) -> f18(b, c, c, 0, f) [ b >= c ]", 0-1) = c
	S("f10(b, c, d, e, f) -> f18(b, c, c, 0, f) [ b >= c ]", 0-2) = c
	S("f10(b, c, d, e, f) -> f18(b, c, c, 0, f) [ b >= c ]", 0-3) = 0
	S("f10(b, c, d, e, f) -> f18(b, c, c, 0, f) [ b >= c ]", 0-4) = f
orients the transitions
	f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]
	f21(b, c, d, e, f) -> f18(b, c, d, e + 1, f) [ f + e + 1 >= d ]
weakly and the transition
	f21(b, c, d, e, f) -> f18(b, c, d, e + 1, f) [ f + e + 1 >= d ]
strictly and produces the following problem:
9:	T:
		(1, 1)          f10(b, c, d, e, f) -> f18(b, c, c, 0, f) [ b >= c ]
		(2, 1)          f18(b, c, d, e, f) -> f32(b, c, d, 0, f) [ e + 1 >= d ]
		(4*c + 6, 1)    f21(b, c, d, e, f) -> f18(b, c, d, e + 1, f) [ f + e + 1 >= d ]
		(c + 1, 1)      f32(b, c, d, e, f) -> f32(b, c, d, e + 1, f) [ d >= e + 2 ]
		(?, 1)          f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]
		(?, 1)          f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]
		(2*c + 3, 1)    f18(b, c, d, e, f) -> f21(b, c, d, e, 0) [ d >= e + 2 ]
		(c, 1)          f10(b, c, d, e, f) -> f10(b + 1, c, d, e, f) [ c >= b + 1 ]
		(1, 1)          f0(b, c, d, e, f) -> f10(0, c, d, e, f)
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f21) = V_3 - V_4 - V_5
and size complexities
	S("f0(b, c, d, e, f) -> f10(0, c, d, e, f)", 0-0) = 0
	S("f0(b, c, d, e, f) -> f10(0, c, d, e, f)", 0-1) = c
	S("f0(b, c, d, e, f) -> f10(0, c, d, e, f)", 0-2) = d
	S("f0(b, c, d, e, f) -> f10(0, c, d, e, f)", 0-3) = e
	S("f0(b, c, d, e, f) -> f10(0, c, d, e, f)", 0-4) = f
	S("f10(b, c, d, e, f) -> f10(b + 1, c, d, e, f) [ c >= b + 1 ]", 0-0) = c
	S("f10(b, c, d, e, f) -> f10(b + 1, c, d, e, f) [ c >= b + 1 ]", 0-1) = c
	S("f10(b, c, d, e, f) -> f10(b + 1, c, d, e, f) [ c >= b + 1 ]", 0-2) = d
	S("f10(b, c, d, e, f) -> f10(b + 1, c, d, e, f) [ c >= b + 1 ]", 0-3) = e
	S("f10(b, c, d, e, f) -> f10(b + 1, c, d, e, f) [ c >= b + 1 ]", 0-4) = f
	S("f18(b, c, d, e, f) -> f21(b, c, d, e, 0) [ d >= e + 2 ]", 0-0) = c
	S("f18(b, c, d, e, f) -> f21(b, c, d, e, 0) [ d >= e + 2 ]", 0-1) = c
	S("f18(b, c, d, e, f) -> f21(b, c, d, e, 0) [ d >= e + 2 ]", 0-2) = c
	S("f18(b, c, d, e, f) -> f21(b, c, d, e, 0) [ d >= e + 2 ]", 0-3) = 4*c + 96
	S("f18(b, c, d, e, f) -> f21(b, c, d, e, 0) [ d >= e + 2 ]", 0-4) = 0
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-0) = c
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-1) = c
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-2) = c
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-3) = 4*c + 96
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-4) = ?
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-0) = c
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-1) = c
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-2) = c
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-3) = 4*c + 96
	S("f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]", 0-4) = ?
	S("f32(b, c, d, e, f) -> f32(b, c, d, e + 1, f) [ d >= e + 2 ]", 0-0) = c
	S("f32(b, c, d, e, f) -> f32(b, c, d, e + 1, f) [ d >= e + 2 ]", 0-1) = c
	S("f32(b, c, d, e, f) -> f32(b, c, d, e + 1, f) [ d >= e + 2 ]", 0-2) = c
	S("f32(b, c, d, e, f) -> f32(b, c, d, e + 1, f) [ d >= e + 2 ]", 0-3) = c + 1
	S("f32(b, c, d, e, f) -> f32(b, c, d, e + 1, f) [ d >= e + 2 ]", 0-4) = ?
	S("f21(b, c, d, e, f) -> f18(b, c, d, e + 1, f) [ f + e + 1 >= d ]", 0-0) = c
	S("f21(b, c, d, e, f) -> f18(b, c, d, e + 1, f) [ f + e + 1 >= d ]", 0-1) = c
	S("f21(b, c, d, e, f) -> f18(b, c, d, e + 1, f) [ f + e + 1 >= d ]", 0-2) = c
	S("f21(b, c, d, e, f) -> f18(b, c, d, e + 1, f) [ f + e + 1 >= d ]", 0-3) = 4*c + 96
	S("f21(b, c, d, e, f) -> f18(b, c, d, e + 1, f) [ f + e + 1 >= d ]", 0-4) = ?
	S("f18(b, c, d, e, f) -> f32(b, c, d, 0, f) [ e + 1 >= d ]", 0-0) = c
	S("f18(b, c, d, e, f) -> f32(b, c, d, 0, f) [ e + 1 >= d ]", 0-1) = c
	S("f18(b, c, d, e, f) -> f32(b, c, d, 0, f) [ e + 1 >= d ]", 0-2) = c
	S("f18(b, c, d, e, f) -> f32(b, c, d, 0, f) [ e + 1 >= d ]", 0-3) = 0
	S("f18(b, c, d, e, f) -> f32(b, c, d, 0, f) [ e + 1 >= d ]", 0-4) = ?
	S("f10(b, c, d, e, f) -> f18(b, c, c, 0, f) [ b >= c ]", 0-0) = c
	S("f10(b, c, d, e, f) -> f18(b, c, c, 0, f) [ b >= c ]", 0-1) = c
	S("f10(b, c, d, e, f) -> f18(b, c, c, 0, f) [ b >= c ]", 0-2) = c
	S("f10(b, c, d, e, f) -> f18(b, c, c, 0, f) [ b >= c ]", 0-3) = 0
	S("f10(b, c, d, e, f) -> f18(b, c, c, 0, f) [ b >= c ]", 0-4) = f
orients the transition
	f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]
weakly and the transition
	f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]
strictly and produces the following problem:
10:	T:
		(1, 1)                       f10(b, c, d, e, f) -> f18(b, c, c, 0, f) [ b >= c ]
		(2, 1)                       f18(b, c, d, e, f) -> f32(b, c, d, 0, f) [ e + 1 >= d ]
		(4*c + 6, 1)                 f21(b, c, d, e, f) -> f18(b, c, d, e + 1, f) [ f + e + 1 >= d ]
		(c + 1, 1)                   f32(b, c, d, e, f) -> f32(b, c, d, e + 1, f) [ d >= e + 2 ]
		(10*c^2 + 207*c + 288, 1)    f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]
		(10*c^2 + 207*c + 288, 1)    f21(b, c, d, e, f) -> f21(b, c, d, e, f + 1) [ d >= e + f + 2 ]
		(2*c + 3, 1)                 f18(b, c, d, e, f) -> f21(b, c, d, e, 0) [ d >= e + 2 ]
		(c, 1)                       f10(b, c, d, e, f) -> f10(b + 1, c, d, e, f) [ c >= b + 1 ]
		(1, 1)                       f0(b, c, d, e, f) -> f10(0, c, d, e, f)
	start location:	f0
	leaf cost:	1

Complexity upper bound 422*c + 20*c^2 + 591

Time: 0.382 sec (SMT: 0.351 sec)