YES(?, 107*a + 108*b + 3*c + 12*a^2 + 24*a*b + 12*b^2 + 3*a*c + 3*b*c + 67)

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

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

A polynomial rank function with
	Pol(f1) = V_2 - V_3
and size complexities
	S("f1(a, b, c) -> f1(a, b, c + 1) [ b >= c + 2 /\\ b >= a ]", 0-0) = a
	S("f1(a, b, c) -> f1(a, b, c + 1) [ b >= c + 2 /\\ b >= a ]", 0-1) = 4*a + 4*b + 128
	S("f1(a, b, c) -> f1(a, b, c + 1) [ b >= c + 2 /\\ b >= a ]", 0-2) = ?
	S("f3(a, b, c) -> f1(a, b, c) [ b >= c + 1 ]", 0-0) = a
	S("f3(a, b, c) -> f1(a, b, c) [ b >= c + 1 ]", 0-1) = b
	S("f3(a, b, c) -> f1(a, b, c) [ b >= c + 1 ]", 0-2) = c
	S("f1(a, b, c) -> f1(a, b + 1, c) [ a >= b + 1 ]", 0-0) = a
	S("f1(a, b, c) -> f1(a, b + 1, c) [ a >= b + 1 ]", 0-1) = 4*a + 4*b + 32
	S("f1(a, b, c) -> f1(a, b + 1, c) [ a >= b + 1 ]", 0-2) = c
orients the transition
	f1(a, b, c) -> f1(a, b, c + 1) [ b >= c + 2 /\ b >= a ]
weakly and the transition
	f1(a, b, c) -> f1(a, b, c + 1) [ b >= c + 2 /\ b >= a ]
strictly and produces the following problem:
3:	T:
		(3*a + 3*b + 2, 1)                                                          f1(a, b, c) -> f1(a, b + 1, c) [ a >= b + 1 ]
		(1, 1)                                                                      f3(a, b, c) -> f1(a, b, c) [ b >= c + 1 ]
		(105*b + 3*c + 12*a^2 + 24*a*b + 12*b^2 + 3*a*c + 3*b*c + 104*a + 64, 1)    f1(a, b, c) -> f1(a, b, c + 1) [ b >= c + 2 /\ b >= a ]
	start location:	f3
	leaf cost:	0

Complexity upper bound 107*a + 108*b + 3*c + 12*a^2 + 24*a*b + 12*b^2 + 3*a*c + 3*b*c + 67

Time: 0.120 sec (SMT: 0.112 sec)