YES(?, a + 64*b + 1314)

Initial complexity problem:
1:	T:
		(?, 1)    f2(a, b, c) -> f2(a - 1, b, c) [ a >= 31 ]
		(?, 1)    f2(a, b, c) -> f300(a, b - 1, c) [ 30 >= a ]
		(?, 1)    f300(a, b, c) -> f2(a, b, c) [ b >= 21 ]
		(?, 1)    f300(a, b, c) -> f1(a, b, d) [ 20 >= b ]
		(1, 1)    f3(a, b, c) -> f300(a, b, c)
	start location:	f3
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(?, 1)    f2(a, b, c) -> f2(a - 1, b, c) [ a >= 31 ]
		(?, 1)    f2(a, b, c) -> f300(a, b - 1, c) [ 30 >= a ]
		(?, 1)    f300(a, b, c) -> f2(a, b, c) [ b >= 21 ]
		(1, 1)    f3(a, b, c) -> f300(a, b, c)
	start location:	f3
	leaf cost:	1

A polynomial rank function with
	Pol(f2) = 2*V_2 - 42
	Pol(f300) = 2*V_2 - 41
	Pol(f3) = 2*V_2 - 41
orients all transitions weakly and the transition
	f300(a, b, c) -> f2(a, b, c) [ b >= 21 ]
strictly and produces the following problem:
3:	T:
		(?, 1)           f2(a, b, c) -> f2(a - 1, b, c) [ a >= 31 ]
		(?, 1)           f2(a, b, c) -> f300(a, b - 1, c) [ 30 >= a ]
		(2*b + 41, 1)    f300(a, b, c) -> f2(a, b, c) [ b >= 21 ]
		(1, 1)           f3(a, b, c) -> f300(a, b, c)
	start location:	f3
	leaf cost:	1

A polynomial rank function with
	Pol(f2) = 31
	Pol(f300) = 30
and size complexities
	S("f3(a, b, c) -> f300(a, b, c)", 0-0) = a
	S("f3(a, b, c) -> f300(a, b, c)", 0-1) = b
	S("f3(a, b, c) -> f300(a, b, c)", 0-2) = c
	S("f300(a, b, c) -> f2(a, b, c) [ b >= 21 ]", 0-0) = a
	S("f300(a, b, c) -> f2(a, b, c) [ b >= 21 ]", 0-1) = ?
	S("f300(a, b, c) -> f2(a, b, c) [ b >= 21 ]", 0-2) = c
	S("f2(a, b, c) -> f300(a, b - 1, c) [ 30 >= a ]", 0-0) = a
	S("f2(a, b, c) -> f300(a, b - 1, c) [ 30 >= a ]", 0-1) = ?
	S("f2(a, b, c) -> f300(a, b - 1, c) [ 30 >= a ]", 0-2) = c
	S("f2(a, b, c) -> f2(a - 1, b, c) [ a >= 31 ]", 0-0) = a
	S("f2(a, b, c) -> f2(a - 1, b, c) [ a >= 31 ]", 0-1) = ?
	S("f2(a, b, c) -> f2(a - 1, b, c) [ a >= 31 ]", 0-2) = c
orients the transitions
	f2(a, b, c) -> f300(a, b - 1, c) [ 30 >= a ]
	f2(a, b, c) -> f2(a - 1, b, c) [ a >= 31 ]
weakly and the transition
	f2(a, b, c) -> f300(a, b - 1, c) [ 30 >= a ]
strictly and produces the following problem:
4:	T:
		(?, 1)              f2(a, b, c) -> f2(a - 1, b, c) [ a >= 31 ]
		(62*b + 1271, 1)    f2(a, b, c) -> f300(a, b - 1, c) [ 30 >= a ]
		(2*b + 41, 1)       f300(a, b, c) -> f2(a, b, c) [ b >= 21 ]
		(1, 1)              f3(a, b, c) -> f300(a, b, c)
	start location:	f3
	leaf cost:	1

A polynomial rank function with
	Pol(f2) = V_1
	Pol(f300) = V_1
	Pol(f3) = V_1
orients all transitions weakly and the transition
	f2(a, b, c) -> f2(a - 1, b, c) [ a >= 31 ]
strictly and produces the following problem:
5:	T:
		(a, 1)              f2(a, b, c) -> f2(a - 1, b, c) [ a >= 31 ]
		(62*b + 1271, 1)    f2(a, b, c) -> f300(a, b - 1, c) [ 30 >= a ]
		(2*b + 41, 1)       f300(a, b, c) -> f2(a, b, c) [ b >= 21 ]
		(1, 1)              f3(a, b, c) -> f300(a, b, c)
	start location:	f3
	leaf cost:	1

Complexity upper bound a + 64*b + 1314

Time: 0.157 sec (SMT: 0.147 sec)