YES(?, 24)

Initial complexity problem:
1:	T:
		(1, 1)    f0(a, b, c) -> f1(a, b, 2) [ a >= 0 /\ 3 >= a /\ 3 >= b /\ b >= 0 ]
		(?, 1)    f1(a, b, c) -> f1(a, b + 1, c) [ c + a >= 2*b + 1 ]
		(?, 1)    f1(a, b, c) -> f1(a, b - 1, c) [ 2*b >= c + a + 2 ]
	start location:	f0
	leaf cost:	0

A polynomial rank function with
	Pol(f1) = V_1 - 2*V_2 + V_3
and size complexities
	S("f1(a, b, c) -> f1(a, b - 1, c) [ 2*b >= c + a + 2 ]", 0-0) = 3
	S("f1(a, b, c) -> f1(a, b - 1, c) [ 2*b >= c + a + 2 ]", 0-1) = ?
	S("f1(a, b, c) -> f1(a, b - 1, c) [ 2*b >= c + a + 2 ]", 0-2) = 2
	S("f1(a, b, c) -> f1(a, b + 1, c) [ c + a >= 2*b + 1 ]", 0-0) = 3
	S("f1(a, b, c) -> f1(a, b + 1, c) [ c + a >= 2*b + 1 ]", 0-1) = ?
	S("f1(a, b, c) -> f1(a, b + 1, c) [ c + a >= 2*b + 1 ]", 0-2) = 2
	S("f0(a, b, c) -> f1(a, b, 2) [ a >= 0 /\\ 3 >= a /\\ 3 >= b /\\ b >= 0 ]", 0-0) = 3
	S("f0(a, b, c) -> f1(a, b, 2) [ a >= 0 /\\ 3 >= a /\\ 3 >= b /\\ b >= 0 ]", 0-1) = 3
	S("f0(a, b, c) -> f1(a, b, 2) [ a >= 0 /\\ 3 >= a /\\ 3 >= b /\\ b >= 0 ]", 0-2) = 2
orients the transition
	f1(a, b, c) -> f1(a, b + 1, c) [ c + a >= 2*b + 1 ]
weakly and the transition
	f1(a, b, c) -> f1(a, b + 1, c) [ c + a >= 2*b + 1 ]
strictly and produces the following problem:
2:	T:
		(1, 1)     f0(a, b, c) -> f1(a, b, 2) [ a >= 0 /\ 3 >= a /\ 3 >= b /\ b >= 0 ]
		(11, 1)    f1(a, b, c) -> f1(a, b + 1, c) [ c + a >= 2*b + 1 ]
		(?, 1)     f1(a, b, c) -> f1(a, b - 1, c) [ 2*b >= c + a + 2 ]
	start location:	f0
	leaf cost:	0

A polynomial rank function with
	Pol(f1) = -V_1 + 2*V_2 - V_3 - 1
and size complexities
	S("f1(a, b, c) -> f1(a, b - 1, c) [ 2*b >= c + a + 2 ]", 0-0) = 3
	S("f1(a, b, c) -> f1(a, b - 1, c) [ 2*b >= c + a + 2 ]", 0-1) = ?
	S("f1(a, b, c) -> f1(a, b - 1, c) [ 2*b >= c + a + 2 ]", 0-2) = 2
	S("f1(a, b, c) -> f1(a, b + 1, c) [ c + a >= 2*b + 1 ]", 0-0) = 3
	S("f1(a, b, c) -> f1(a, b + 1, c) [ c + a >= 2*b + 1 ]", 0-1) = 14
	S("f1(a, b, c) -> f1(a, b + 1, c) [ c + a >= 2*b + 1 ]", 0-2) = 2
	S("f0(a, b, c) -> f1(a, b, 2) [ a >= 0 /\\ 3 >= a /\\ 3 >= b /\\ b >= 0 ]", 0-0) = 3
	S("f0(a, b, c) -> f1(a, b, 2) [ a >= 0 /\\ 3 >= a /\\ 3 >= b /\\ b >= 0 ]", 0-1) = 3
	S("f0(a, b, c) -> f1(a, b, 2) [ a >= 0 /\\ 3 >= a /\\ 3 >= b /\\ b >= 0 ]", 0-2) = 2
orients the transition
	f1(a, b, c) -> f1(a, b - 1, c) [ 2*b >= c + a + 2 ]
weakly and the transition
	f1(a, b, c) -> f1(a, b - 1, c) [ 2*b >= c + a + 2 ]
strictly and produces the following problem:
3:	T:
		(1, 1)     f0(a, b, c) -> f1(a, b, 2) [ a >= 0 /\ 3 >= a /\ 3 >= b /\ b >= 0 ]
		(11, 1)    f1(a, b, c) -> f1(a, b + 1, c) [ c + a >= 2*b + 1 ]
		(12, 1)    f1(a, b, c) -> f1(a, b - 1, c) [ 2*b >= c + a + 2 ]
	start location:	f0
	leaf cost:	0

Complexity upper bound 24

Time: 0.189 sec (SMT: 0.177 sec)