YES(?, 2 * pow(2, a) * 2 + pow(2, 2 * pow(2, a) * 2 + 2*a + 2) * 2 + 3*a + 7)

Initial complexity problem:
1:	T:
		(1, 1)    f(a, b, c) -> g(a, 1, 1)
		(?, 1)    g(a, b, c) -> g(a - 1, 2*b, c) [ a > 0 ]
		(?, 1)    g(a, b, c) -> h(a, b, c) [ a <= 0 ]
		(?, 1)    h(a, b, c) -> h(a, b - 1, 2*c) [ b > 0 ]
		(?, 1)    h(a, b, c) -> i(a, b, c) [ b <= 0 ]
		(?, 1)    i(a, b, c) -> i(a, b, c - 1) [ c > 0 ]
	start location:	f
	leaf cost:	0

A polynomial rank function with
	Pol(f) = 2
	Pol(g) = 2
	Pol(h) = 1
	Pol(i) = -1
orients all transitions weakly and the transitions
	h(a, b, c) -> i(a, b, c) [ b <= 0 ]
	g(a, b, c) -> h(a, b, c) [ a <= 0 ]
strictly and produces the following problem:
2:	T:
		(1, 1)    f(a, b, c) -> g(a, 1, 1)
		(?, 1)    g(a, b, c) -> g(a - 1, 2*b, c) [ a > 0 ]
		(2, 1)    g(a, b, c) -> h(a, b, c) [ a <= 0 ]
		(?, 1)    h(a, b, c) -> h(a, b - 1, 2*c) [ b > 0 ]
		(2, 1)    h(a, b, c) -> i(a, b, c) [ b <= 0 ]
		(?, 1)    i(a, b, c) -> i(a, b, c - 1) [ c > 0 ]
	start location:	f
	leaf cost:	0

A polynomial rank function with
	Pol(f) = V_1
	Pol(g) = V_1
	Pol(h) = V_1
	Pol(i) = V_1 + V_2
orients all transitions weakly and the transition
	g(a, b, c) -> g(a - 1, 2*b, c) [ a > 0 ]
strictly and produces the following problem:
3:	T:
		(1, 1)    f(a, b, c) -> g(a, 1, 1)
		(a, 1)    g(a, b, c) -> g(a - 1, 2*b, c) [ a > 0 ]
		(2, 1)    g(a, b, c) -> h(a, b, c) [ a <= 0 ]
		(?, 1)    h(a, b, c) -> h(a, b - 1, 2*c) [ b > 0 ]
		(2, 1)    h(a, b, c) -> i(a, b, c) [ b <= 0 ]
		(?, 1)    i(a, b, c) -> i(a, b, c - 1) [ c > 0 ]
	start location:	f
	leaf cost:	0

A polynomial rank function with
	Pol(i) = V_1 + V_2 + 1
	Pol(h) = V_2
and size complexities
	S("i(a, b, c) -> i(a, b, c - 1) [ c > 0 ]", 0-0) = a
	S("i(a, b, c) -> i(a, b, c - 1) [ c > 0 ]", 0-1) = pow(2, a)
	S("i(a, b, c) -> i(a, b, c - 1) [ c > 0 ]", 0-2) = ?
	S("h(a, b, c) -> i(a, b, c) [ b <= 0 ]", 0-0) = a
	S("h(a, b, c) -> i(a, b, c) [ b <= 0 ]", 0-1) = pow(2, a)
	S("h(a, b, c) -> i(a, b, c) [ b <= 0 ]", 0-2) = ?
	S("h(a, b, c) -> h(a, b - 1, 2*c) [ b > 0 ]", 0-0) = a
	S("h(a, b, c) -> h(a, b - 1, 2*c) [ b > 0 ]", 0-1) = pow(2, a)
	S("h(a, b, c) -> h(a, b - 1, 2*c) [ b > 0 ]", 0-2) = ?
	S("g(a, b, c) -> h(a, b, c) [ a <= 0 ]", 0-0) = a
	S("g(a, b, c) -> h(a, b, c) [ a <= 0 ]", 0-1) = pow(2, a)
	S("g(a, b, c) -> h(a, b, c) [ a <= 0 ]", 0-2) = 1
	S("g(a, b, c) -> g(a - 1, 2*b, c) [ a > 0 ]", 0-0) = a
	S("g(a, b, c) -> g(a - 1, 2*b, c) [ a > 0 ]", 0-1) = pow(2, a)
	S("g(a, b, c) -> g(a - 1, 2*b, c) [ a > 0 ]", 0-2) = 1
	S("f(a, b, c) -> g(a, 1, 1)", 0-0) = a
	S("f(a, b, c) -> g(a, 1, 1)", 0-1) = 1
	S("f(a, b, c) -> g(a, 1, 1)", 0-2) = 1
orients the transitions
	i(a, b, c) -> i(a, b, c - 1) [ c > 0 ]
	h(a, b, c) -> h(a, b - 1, 2*c) [ b > 0 ]
weakly and the transition
	h(a, b, c) -> h(a, b - 1, 2*c) [ b > 0 ]
strictly and produces the following problem:
4:	T:
		(1, 1)                              f(a, b, c) -> g(a, 1, 1)
		(a, 1)                              g(a, b, c) -> g(a - 1, 2*b, c) [ a > 0 ]
		(2, 1)                              g(a, b, c) -> h(a, b, c) [ a <= 0 ]
		(2 * pow(2, a) * 2 + 2*a + 2, 1)    h(a, b, c) -> h(a, b - 1, 2*c) [ b > 0 ]
		(2, 1)                              h(a, b, c) -> i(a, b, c) [ b <= 0 ]
		(?, 1)                              i(a, b, c) -> i(a, b, c - 1) [ c > 0 ]
	start location:	f
	leaf cost:	0

A polynomial rank function with
	Pol(i) = V_3
and size complexities
	S("i(a, b, c) -> i(a, b, c - 1) [ c > 0 ]", 0-0) = a
	S("i(a, b, c) -> i(a, b, c - 1) [ c > 0 ]", 0-1) = pow(2, a)
	S("i(a, b, c) -> i(a, b, c - 1) [ c > 0 ]", 0-2) = pow(2, 2 * pow(2, a) * 2 + 2*a + 2)
	S("h(a, b, c) -> i(a, b, c) [ b <= 0 ]", 0-0) = a
	S("h(a, b, c) -> i(a, b, c) [ b <= 0 ]", 0-1) = pow(2, a)
	S("h(a, b, c) -> i(a, b, c) [ b <= 0 ]", 0-2) = pow(2, 2 * pow(2, a) * 2 + 2*a + 2)
	S("h(a, b, c) -> h(a, b - 1, 2*c) [ b > 0 ]", 0-0) = a
	S("h(a, b, c) -> h(a, b - 1, 2*c) [ b > 0 ]", 0-1) = pow(2, a)
	S("h(a, b, c) -> h(a, b - 1, 2*c) [ b > 0 ]", 0-2) = pow(2, 2 * pow(2, a) * 2 + 2*a + 2)
	S("g(a, b, c) -> h(a, b, c) [ a <= 0 ]", 0-0) = a
	S("g(a, b, c) -> h(a, b, c) [ a <= 0 ]", 0-1) = pow(2, a)
	S("g(a, b, c) -> h(a, b, c) [ a <= 0 ]", 0-2) = 1
	S("g(a, b, c) -> g(a - 1, 2*b, c) [ a > 0 ]", 0-0) = a
	S("g(a, b, c) -> g(a - 1, 2*b, c) [ a > 0 ]", 0-1) = pow(2, a)
	S("g(a, b, c) -> g(a - 1, 2*b, c) [ a > 0 ]", 0-2) = 1
	S("f(a, b, c) -> g(a, 1, 1)", 0-0) = a
	S("f(a, b, c) -> g(a, 1, 1)", 0-1) = 1
	S("f(a, b, c) -> g(a, 1, 1)", 0-2) = 1
orients the transition
	i(a, b, c) -> i(a, b, c - 1) [ c > 0 ]
weakly and the transition
	i(a, b, c) -> i(a, b, c - 1) [ c > 0 ]
strictly and produces the following problem:
5:	T:
		(1, 1)                                          f(a, b, c) -> g(a, 1, 1)
		(a, 1)                                          g(a, b, c) -> g(a - 1, 2*b, c) [ a > 0 ]
		(2, 1)                                          g(a, b, c) -> h(a, b, c) [ a <= 0 ]
		(2 * pow(2, a) * 2 + 2*a + 2, 1)                h(a, b, c) -> h(a, b - 1, 2*c) [ b > 0 ]
		(2, 1)                                          h(a, b, c) -> i(a, b, c) [ b <= 0 ]
		(pow(2, 2 * pow(2, a) * 2 + 2*a + 2) * 2, 1)    i(a, b, c) -> i(a, b, c - 1) [ c > 0 ]
	start location:	f
	leaf cost:	0

Complexity upper bound 2 * pow(2, a) * 2 + pow(2, 2 * pow(2, a) * 2 + 2*a + 2) * 2 + 3*a + 7

Time: 0.438 sec (SMT: 0.418 sec)