YES(?, 4*b + 4*f + 5)

Initial complexity problem:
1:	T:
		(1, 1)    start(a, b, c, d, e, f) -> m1(a, b, c, d, e, f) [ a >= 0 /\ b + a + 2 >= 2*c /\ b >= a + 1 /\ 2*c >= b + a /\ d >= 0 /\ e + 1 = c /\ f = a ]
		(?, 1)    m1(a, b, c, d, e, f) -> m1(a, b, h, d, e, g) [ b >= 1 /\ d >= 0 /\ a >= e + 1 /\ b + 1 >= g /\ c + 1 >= h /\ h >= c + 1 /\ f + 1 >= g /\ g >= f + 1 ]
		(?, 1)    m1(a, b, c, d, e, f) -> m1(h, b, c, d, e, g) [ b >= 1 /\ d >= 0 /\ b >= f /\ e + 1 >= h /\ c >= b + 1 /\ f + 1 >= g /\ g >= f + 1 /\ a + 1 >= h /\ h >= a + 1 ]
		(?, 1)    m1(a, b, c, d, e, f) -> m1(a, b, h, d, e, g) [ b >= 1 /\ d >= 0 /\ b >= f /\ b + 1 >= h /\ e >= a /\ f + 1 >= g /\ g >= f + 1 /\ c + 1 >= h /\ h >= c + 1 ]
		(?, 1)    m1(a, b, c, d, e, f) -> m1(h, b, c, d, e, g) [ b >= 1 /\ d >= 0 /\ b >= f /\ b >= c /\ e + 1 >= h /\ a + 1 >= h /\ h >= a + 1 /\ f + 1 >= g /\ g >= f + 1 ]
	start location:	start
	leaf cost:	0

A polynomial rank function with
	Pol(start) = V_2 - V_6 + 1
	Pol(m1) = V_2 - V_6 + 1
orients all transitions weakly and the transitions
	m1(a, b, c, d, e, f) -> m1(h, b, c, d, e, g) [ b >= 1 /\ d >= 0 /\ b >= f /\ e + 1 >= h /\ c >= b + 1 /\ f + 1 >= g /\ g >= f + 1 /\ a + 1 >= h /\ h >= a + 1 ]
	m1(a, b, c, d, e, f) -> m1(h, b, c, d, e, g) [ b >= 1 /\ d >= 0 /\ b >= f /\ b >= c /\ e + 1 >= h /\ a + 1 >= h /\ h >= a + 1 /\ f + 1 >= g /\ g >= f + 1 ]
	m1(a, b, c, d, e, f) -> m1(a, b, h, d, e, g) [ b >= 1 /\ d >= 0 /\ b >= f /\ b + 1 >= h /\ e >= a /\ f + 1 >= g /\ g >= f + 1 /\ c + 1 >= h /\ h >= c + 1 ]
	m1(a, b, c, d, e, f) -> m1(a, b, h, d, e, g) [ b >= 1 /\ d >= 0 /\ a >= e + 1 /\ b + 1 >= g /\ c + 1 >= h /\ h >= c + 1 /\ f + 1 >= g /\ g >= f + 1 ]
strictly and produces the following problem:
2:	T:
		(1, 1)            start(a, b, c, d, e, f) -> m1(a, b, c, d, e, f) [ a >= 0 /\ b + a + 2 >= 2*c /\ b >= a + 1 /\ 2*c >= b + a /\ d >= 0 /\ e + 1 = c /\ f = a ]
		(b + f + 1, 1)    m1(a, b, c, d, e, f) -> m1(a, b, h, d, e, g) [ b >= 1 /\ d >= 0 /\ a >= e + 1 /\ b + 1 >= g /\ c + 1 >= h /\ h >= c + 1 /\ f + 1 >= g /\ g >= f + 1 ]
		(b + f + 1, 1)    m1(a, b, c, d, e, f) -> m1(h, b, c, d, e, g) [ b >= 1 /\ d >= 0 /\ b >= f /\ e + 1 >= h /\ c >= b + 1 /\ f + 1 >= g /\ g >= f + 1 /\ a + 1 >= h /\ h >= a + 1 ]
		(b + f + 1, 1)    m1(a, b, c, d, e, f) -> m1(a, b, h, d, e, g) [ b >= 1 /\ d >= 0 /\ b >= f /\ b + 1 >= h /\ e >= a /\ f + 1 >= g /\ g >= f + 1 /\ c + 1 >= h /\ h >= c + 1 ]
		(b + f + 1, 1)    m1(a, b, c, d, e, f) -> m1(h, b, c, d, e, g) [ b >= 1 /\ d >= 0 /\ b >= f /\ b >= c /\ e + 1 >= h /\ a + 1 >= h /\ h >= a + 1 /\ f + 1 >= g /\ g >= f + 1 ]
	start location:	start
	leaf cost:	0

Complexity upper bound 4*b + 4*f + 5

Time: 0.192 sec (SMT: 0.178 sec)