MAYBE

Initial complexity problem:
1:	T:
		(?, 1)    f7(a, b) -> f7(c, b) [ 0 >= a + 1 ]
		(?, 1)    f7(a, b) -> f7(c, b) [ a >= 1 ]
		(?, 1)    f13(a, b) -> f13(a, b)
		(?, 1)    f15(a, b) -> f17(a, b)
		(?, 1)    f7(a, b) -> f13(0, 1) [ a = 0 ]
		(1, 1)    f0(a, b) -> f7(c, 1)
	start location:	f0
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(?, 1)    f7(a, b) -> f7(c, b) [ 0 >= a + 1 ]
		(?, 1)    f7(a, b) -> f7(c, b) [ a >= 1 ]
		(?, 1)    f13(a, b) -> f13(a, b)
		(?, 1)    f7(a, b) -> f13(0, 1) [ a = 0 ]
		(1, 1)    f0(a, b) -> f7(c, 1)
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f7) = 1
	Pol(f13) = 0
	Pol(f0) = 1
orients all transitions weakly and the transition
	f7(a, b) -> f13(0, 1) [ a = 0 ]
strictly and produces the following problem:
3:	T:
		(?, 1)    f7(a, b) -> f7(c, b) [ 0 >= a + 1 ]
		(?, 1)    f7(a, b) -> f7(c, b) [ a >= 1 ]
		(?, 1)    f13(a, b) -> f13(a, b)
		(1, 1)    f7(a, b) -> f13(0, 1) [ a = 0 ]
		(1, 1)    f0(a, b) -> f7(c, 1)
	start location:	f0
	leaf cost:	1

Applied AI with 'oct' on problem 3 to obtain the following invariants:
  For symbol f13: -X_2 + 1 >= 0 /\ X_1 - X_2 + 1 >= 0 /\ -X_1 - X_2 + 1 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 1 >= 0 /\ -X_1 + X_2 - 1 >= 0 /\ -X_1 >= 0 /\ X_1 >= 0
  For symbol f7: -X_2 + 1 >= 0 /\ X_2 - 1 >= 0


This yielded the following problem:
4:	T:
		(1, 1)    f0(a, b) -> f7(c, 1)
		(1, 1)    f7(a, b) -> f13(0, 1) [ -b + 1 >= 0 /\ b - 1 >= 0 /\ a = 0 ]
		(?, 1)    f13(a, b) -> f13(a, b) [ -b + 1 >= 0 /\ a - b + 1 >= 0 /\ -a - b + 1 >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ a >= 0 ]
		(?, 1)    f7(a, b) -> f7(c, b) [ -b + 1 >= 0 /\ b - 1 >= 0 /\ a >= 1 ]
		(?, 1)    f7(a, b) -> f7(c, b) [ -b + 1 >= 0 /\ b - 1 >= 0 /\ 0 >= a + 1 ]
	start location:	f0
	leaf cost:	1

By chaining the transition f7(a, b) -> f13(0, 1) [ -b + 1 >= 0 /\ b - 1 >= 0 /\ a = 0 ] with all transitions in problem 4, the following new transition is obtained:
	f7(a, b) -> f13(0, 1) [ -b + 1 >= 0 /\ b - 1 >= 0 /\ a = 0 /\ 0 >= 0 ]
We thus obtain the following problem:
5:	T:
		(1, 2)    f7(a, b) -> f13(0, 1) [ -b + 1 >= 0 /\ b - 1 >= 0 /\ a = 0 /\ 0 >= 0 ]
		(1, 1)    f0(a, b) -> f7(c, 1)
		(?, 1)    f13(a, b) -> f13(a, b) [ -b + 1 >= 0 /\ a - b + 1 >= 0 /\ -a - b + 1 >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ -a >= 0 /\ a >= 0 ]
		(?, 1)    f7(a, b) -> f7(c, b) [ -b + 1 >= 0 /\ b - 1 >= 0 /\ a >= 1 ]
		(?, 1)    f7(a, b) -> f7(c, b) [ -b + 1 >= 0 /\ b - 1 >= 0 /\ 0 >= a + 1 ]
	start location:	f0
	leaf cost:	1

Complexity upper bound ?

Time: 0.398 sec (SMT: 0.374 sec)