YES(?, 2*a + 2*b + 5)

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

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

Complexity upper bound 2*a + 2*b + 5

Time: 0.126 sec (SMT: 0.121 sec)