YES(?, 6567)

Initial complexity problem:
1:	T:
		(1, 1)    f0(a, b, c) -> f10(1, b, c)
		(?, 1)    f10(a, b, c) -> f13(a, 1, c) [ 5 >= a ]
		(?, 1)    f13(a, b, c) -> f13(a, b + 1, c) [ 5 >= b ]
		(?, 1)    f21(a, b, c) -> f24(a, 1, c) [ 5 >= a ]
		(?, 1)    f24(a, b, c) -> f27(a, b, 1) [ 5 >= b ]
		(?, 1)    f27(a, b, c) -> f27(a, b, c + 1) [ 5 >= c ]
		(?, 1)    f27(a, b, c) -> f24(a, b + 1, c) [ c >= 6 ]
		(?, 1)    f24(a, b, c) -> f21(a + 1, b, c) [ b >= 6 ]
		(?, 1)    f21(a, b, c) -> f39(a, b, c) [ a >= 6 ]
		(?, 1)    f13(a, b, c) -> f10(a + 1, b, c) [ b >= 6 ]
		(?, 1)    f10(a, b, c) -> f21(1, b, c) [ a >= 6 ]
	start location:	f0
	leaf cost:	0

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

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

A polynomial rank function with
	Pol(f0) = 9
	Pol(f10) = 9
	Pol(f13) = 9
	Pol(f21) = -2*V_1 + 11
	Pol(f24) = -2*V_1 + 10
	Pol(f27) = -2*V_1 + 10
orients all transitions weakly and the transition
	f21(a, b, c) -> f24(a, 1, c) [ 5 >= a ]
strictly and produces the following problem:
4:	T:
		(1, 1)    f0(a, b, c) -> f10(1, b, c)
		(?, 1)    f10(a, b, c) -> f13(a, 1, c) [ 5 >= a ]
		(?, 1)    f13(a, b, c) -> f13(a, b + 1, c) [ 5 >= b ]
		(9, 1)    f21(a, b, c) -> f24(a, 1, c) [ 5 >= a ]
		(?, 1)    f24(a, b, c) -> f27(a, b, 1) [ 5 >= b ]
		(?, 1)    f27(a, b, c) -> f27(a, b, c + 1) [ 5 >= c ]
		(?, 1)    f27(a, b, c) -> f24(a, b + 1, c) [ c >= 6 ]
		(?, 1)    f24(a, b, c) -> f21(a + 1, b, c) [ b >= 6 ]
		(?, 1)    f13(a, b, c) -> f10(a + 1, b, c) [ b >= 6 ]
		(5, 1)    f10(a, b, c) -> f21(1, b, c) [ a >= 6 ]
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f27) = 5
	Pol(f24) = 5
	Pol(f21) = 4
	Pol(f13) = -6
	Pol(f10) = -6
and size complexities
	S("f10(a, b, c) -> f21(1, b, c) [ a >= 6 ]", 0-0) = 1
	S("f10(a, b, c) -> f21(1, b, c) [ a >= 6 ]", 0-1) = 6
	S("f10(a, b, c) -> f21(1, b, c) [ a >= 6 ]", 0-2) = c
	S("f13(a, b, c) -> f10(a + 1, b, c) [ b >= 6 ]", 0-0) = ?
	S("f13(a, b, c) -> f10(a + 1, b, c) [ b >= 6 ]", 0-1) = 6
	S("f13(a, b, c) -> f10(a + 1, b, c) [ b >= 6 ]", 0-2) = c
	S("f24(a, b, c) -> f21(a + 1, b, c) [ b >= 6 ]", 0-0) = ?
	S("f24(a, b, c) -> f21(a + 1, b, c) [ b >= 6 ]", 0-1) = ?
	S("f24(a, b, c) -> f21(a + 1, b, c) [ b >= 6 ]", 0-2) = 6
	S("f27(a, b, c) -> f24(a, b + 1, c) [ c >= 6 ]", 0-0) = ?
	S("f27(a, b, c) -> f24(a, b + 1, c) [ c >= 6 ]", 0-1) = ?
	S("f27(a, b, c) -> f24(a, b + 1, c) [ c >= 6 ]", 0-2) = 6
	S("f27(a, b, c) -> f27(a, b, c + 1) [ 5 >= c ]", 0-0) = ?
	S("f27(a, b, c) -> f27(a, b, c + 1) [ 5 >= c ]", 0-1) = ?
	S("f27(a, b, c) -> f27(a, b, c + 1) [ 5 >= c ]", 0-2) = 6
	S("f24(a, b, c) -> f27(a, b, 1) [ 5 >= b ]", 0-0) = ?
	S("f24(a, b, c) -> f27(a, b, 1) [ 5 >= b ]", 0-1) = ?
	S("f24(a, b, c) -> f27(a, b, 1) [ 5 >= b ]", 0-2) = 1
	S("f21(a, b, c) -> f24(a, 1, c) [ 5 >= a ]", 0-0) = ?
	S("f21(a, b, c) -> f24(a, 1, c) [ 5 >= a ]", 0-1) = 1
	S("f21(a, b, c) -> f24(a, 1, c) [ 5 >= a ]", 0-2) = c + 6
	S("f13(a, b, c) -> f13(a, b + 1, c) [ 5 >= b ]", 0-0) = ?
	S("f13(a, b, c) -> f13(a, b + 1, c) [ 5 >= b ]", 0-1) = 6
	S("f13(a, b, c) -> f13(a, b + 1, c) [ 5 >= b ]", 0-2) = c
	S("f10(a, b, c) -> f13(a, 1, c) [ 5 >= a ]", 0-0) = ?
	S("f10(a, b, c) -> f13(a, 1, c) [ 5 >= a ]", 0-1) = 1
	S("f10(a, b, c) -> f13(a, 1, c) [ 5 >= a ]", 0-2) = c
	S("f0(a, b, c) -> f10(1, b, c)", 0-0) = 1
	S("f0(a, b, c) -> f10(1, b, c)", 0-1) = b
	S("f0(a, b, c) -> f10(1, b, c)", 0-2) = c
orients the transitions
	f27(a, b, c) -> f27(a, b, c + 1) [ 5 >= c ]
	f27(a, b, c) -> f24(a, b + 1, c) [ c >= 6 ]
	f24(a, b, c) -> f27(a, b, 1) [ 5 >= b ]
	f24(a, b, c) -> f21(a + 1, b, c) [ b >= 6 ]
	f13(a, b, c) -> f13(a, b + 1, c) [ 5 >= b ]
	f13(a, b, c) -> f10(a + 1, b, c) [ b >= 6 ]
	f10(a, b, c) -> f13(a, 1, c) [ 5 >= a ]
weakly and the transition
	f24(a, b, c) -> f21(a + 1, b, c) [ b >= 6 ]
strictly and produces the following problem:
5:	T:
		(1, 1)     f0(a, b, c) -> f10(1, b, c)
		(?, 1)     f10(a, b, c) -> f13(a, 1, c) [ 5 >= a ]
		(?, 1)     f13(a, b, c) -> f13(a, b + 1, c) [ 5 >= b ]
		(9, 1)     f21(a, b, c) -> f24(a, 1, c) [ 5 >= a ]
		(?, 1)     f24(a, b, c) -> f27(a, b, 1) [ 5 >= b ]
		(?, 1)     f27(a, b, c) -> f27(a, b, c + 1) [ 5 >= c ]
		(?, 1)     f27(a, b, c) -> f24(a, b + 1, c) [ c >= 6 ]
		(51, 1)    f24(a, b, c) -> f21(a + 1, b, c) [ b >= 6 ]
		(?, 1)     f13(a, b, c) -> f10(a + 1, b, c) [ b >= 6 ]
		(5, 1)     f10(a, b, c) -> f21(1, b, c) [ a >= 6 ]
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f27) = -2*V_2 + 10
	Pol(f24) = -2*V_2 + 11
	Pol(f13) = -2*V_1 + 10
	Pol(f10) = -2*V_1 + 11
and size complexities
	S("f10(a, b, c) -> f21(1, b, c) [ a >= 6 ]", 0-0) = 1
	S("f10(a, b, c) -> f21(1, b, c) [ a >= 6 ]", 0-1) = 6
	S("f10(a, b, c) -> f21(1, b, c) [ a >= 6 ]", 0-2) = c
	S("f13(a, b, c) -> f10(a + 1, b, c) [ b >= 6 ]", 0-0) = ?
	S("f13(a, b, c) -> f10(a + 1, b, c) [ b >= 6 ]", 0-1) = 6
	S("f13(a, b, c) -> f10(a + 1, b, c) [ b >= 6 ]", 0-2) = c
	S("f24(a, b, c) -> f21(a + 1, b, c) [ b >= 6 ]", 0-0) = 52
	S("f24(a, b, c) -> f21(a + 1, b, c) [ b >= 6 ]", 0-1) = ?
	S("f24(a, b, c) -> f21(a + 1, b, c) [ b >= 6 ]", 0-2) = 6
	S("f27(a, b, c) -> f24(a, b + 1, c) [ c >= 6 ]", 0-0) = 52
	S("f27(a, b, c) -> f24(a, b + 1, c) [ c >= 6 ]", 0-1) = ?
	S("f27(a, b, c) -> f24(a, b + 1, c) [ c >= 6 ]", 0-2) = 6
	S("f27(a, b, c) -> f27(a, b, c + 1) [ 5 >= c ]", 0-0) = 52
	S("f27(a, b, c) -> f27(a, b, c + 1) [ 5 >= c ]", 0-1) = ?
	S("f27(a, b, c) -> f27(a, b, c + 1) [ 5 >= c ]", 0-2) = 6
	S("f24(a, b, c) -> f27(a, b, 1) [ 5 >= b ]", 0-0) = 52
	S("f24(a, b, c) -> f27(a, b, 1) [ 5 >= b ]", 0-1) = ?
	S("f24(a, b, c) -> f27(a, b, 1) [ 5 >= b ]", 0-2) = 1
	S("f21(a, b, c) -> f24(a, 1, c) [ 5 >= a ]", 0-0) = 52
	S("f21(a, b, c) -> f24(a, 1, c) [ 5 >= a ]", 0-1) = 1
	S("f21(a, b, c) -> f24(a, 1, c) [ 5 >= a ]", 0-2) = c + 6
	S("f13(a, b, c) -> f13(a, b + 1, c) [ 5 >= b ]", 0-0) = ?
	S("f13(a, b, c) -> f13(a, b + 1, c) [ 5 >= b ]", 0-1) = 6
	S("f13(a, b, c) -> f13(a, b + 1, c) [ 5 >= b ]", 0-2) = c
	S("f10(a, b, c) -> f13(a, 1, c) [ 5 >= a ]", 0-0) = ?
	S("f10(a, b, c) -> f13(a, 1, c) [ 5 >= a ]", 0-1) = 1
	S("f10(a, b, c) -> f13(a, 1, c) [ 5 >= a ]", 0-2) = c
	S("f0(a, b, c) -> f10(1, b, c)", 0-0) = 1
	S("f0(a, b, c) -> f10(1, b, c)", 0-1) = b
	S("f0(a, b, c) -> f10(1, b, c)", 0-2) = c
orients the transitions
	f27(a, b, c) -> f27(a, b, c + 1) [ 5 >= c ]
	f27(a, b, c) -> f24(a, b + 1, c) [ c >= 6 ]
	f24(a, b, c) -> f27(a, b, 1) [ 5 >= b ]
	f13(a, b, c) -> f13(a, b + 1, c) [ 5 >= b ]
	f13(a, b, c) -> f10(a + 1, b, c) [ b >= 6 ]
	f10(a, b, c) -> f13(a, 1, c) [ 5 >= a ]
weakly and the transitions
	f24(a, b, c) -> f27(a, b, 1) [ 5 >= b ]
	f10(a, b, c) -> f13(a, 1, c) [ 5 >= a ]
strictly and produces the following problem:
6:	T:
		(1, 1)      f0(a, b, c) -> f10(1, b, c)
		(130, 1)    f10(a, b, c) -> f13(a, 1, c) [ 5 >= a ]
		(?, 1)      f13(a, b, c) -> f13(a, b + 1, c) [ 5 >= b ]
		(9, 1)      f21(a, b, c) -> f24(a, 1, c) [ 5 >= a ]
		(130, 1)    f24(a, b, c) -> f27(a, b, 1) [ 5 >= b ]
		(?, 1)      f27(a, b, c) -> f27(a, b, c + 1) [ 5 >= c ]
		(?, 1)      f27(a, b, c) -> f24(a, b + 1, c) [ c >= 6 ]
		(51, 1)     f24(a, b, c) -> f21(a + 1, b, c) [ b >= 6 ]
		(?, 1)      f13(a, b, c) -> f10(a + 1, b, c) [ b >= 6 ]
		(5, 1)      f10(a, b, c) -> f21(1, b, c) [ a >= 6 ]
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f27) = 5
	Pol(f24) = 4
	Pol(f13) = 5
	Pol(f10) = 4
and size complexities
	S("f10(a, b, c) -> f21(1, b, c) [ a >= 6 ]", 0-0) = 1
	S("f10(a, b, c) -> f21(1, b, c) [ a >= 6 ]", 0-1) = 6
	S("f10(a, b, c) -> f21(1, b, c) [ a >= 6 ]", 0-2) = c
	S("f13(a, b, c) -> f10(a + 1, b, c) [ b >= 6 ]", 0-0) = ?
	S("f13(a, b, c) -> f10(a + 1, b, c) [ b >= 6 ]", 0-1) = 6
	S("f13(a, b, c) -> f10(a + 1, b, c) [ b >= 6 ]", 0-2) = c
	S("f24(a, b, c) -> f21(a + 1, b, c) [ b >= 6 ]", 0-0) = 52
	S("f24(a, b, c) -> f21(a + 1, b, c) [ b >= 6 ]", 0-1) = ?
	S("f24(a, b, c) -> f21(a + 1, b, c) [ b >= 6 ]", 0-2) = 6
	S("f27(a, b, c) -> f24(a, b + 1, c) [ c >= 6 ]", 0-0) = 52
	S("f27(a, b, c) -> f24(a, b + 1, c) [ c >= 6 ]", 0-1) = ?
	S("f27(a, b, c) -> f24(a, b + 1, c) [ c >= 6 ]", 0-2) = 6
	S("f27(a, b, c) -> f27(a, b, c + 1) [ 5 >= c ]", 0-0) = 52
	S("f27(a, b, c) -> f27(a, b, c + 1) [ 5 >= c ]", 0-1) = ?
	S("f27(a, b, c) -> f27(a, b, c + 1) [ 5 >= c ]", 0-2) = 6
	S("f24(a, b, c) -> f27(a, b, 1) [ 5 >= b ]", 0-0) = 52
	S("f24(a, b, c) -> f27(a, b, 1) [ 5 >= b ]", 0-1) = ?
	S("f24(a, b, c) -> f27(a, b, 1) [ 5 >= b ]", 0-2) = 1
	S("f21(a, b, c) -> f24(a, 1, c) [ 5 >= a ]", 0-0) = 52
	S("f21(a, b, c) -> f24(a, 1, c) [ 5 >= a ]", 0-1) = 1
	S("f21(a, b, c) -> f24(a, 1, c) [ 5 >= a ]", 0-2) = c + 6
	S("f13(a, b, c) -> f13(a, b + 1, c) [ 5 >= b ]", 0-0) = ?
	S("f13(a, b, c) -> f13(a, b + 1, c) [ 5 >= b ]", 0-1) = 6
	S("f13(a, b, c) -> f13(a, b + 1, c) [ 5 >= b ]", 0-2) = c
	S("f10(a, b, c) -> f13(a, 1, c) [ 5 >= a ]", 0-0) = ?
	S("f10(a, b, c) -> f13(a, 1, c) [ 5 >= a ]", 0-1) = 1
	S("f10(a, b, c) -> f13(a, 1, c) [ 5 >= a ]", 0-2) = c
	S("f0(a, b, c) -> f10(1, b, c)", 0-0) = 1
	S("f0(a, b, c) -> f10(1, b, c)", 0-1) = b
	S("f0(a, b, c) -> f10(1, b, c)", 0-2) = c
orients the transitions
	f27(a, b, c) -> f27(a, b, c + 1) [ 5 >= c ]
	f27(a, b, c) -> f24(a, b + 1, c) [ c >= 6 ]
	f13(a, b, c) -> f13(a, b + 1, c) [ 5 >= b ]
	f13(a, b, c) -> f10(a + 1, b, c) [ b >= 6 ]
weakly and the transitions
	f27(a, b, c) -> f24(a, b + 1, c) [ c >= 6 ]
	f13(a, b, c) -> f10(a + 1, b, c) [ b >= 6 ]
strictly and produces the following problem:
7:	T:
		(1, 1)       f0(a, b, c) -> f10(1, b, c)
		(130, 1)     f10(a, b, c) -> f13(a, 1, c) [ 5 >= a ]
		(?, 1)       f13(a, b, c) -> f13(a, b + 1, c) [ 5 >= b ]
		(9, 1)       f21(a, b, c) -> f24(a, 1, c) [ 5 >= a ]
		(130, 1)     f24(a, b, c) -> f27(a, b, 1) [ 5 >= b ]
		(?, 1)       f27(a, b, c) -> f27(a, b, c + 1) [ 5 >= c ]
		(1300, 1)    f27(a, b, c) -> f24(a, b + 1, c) [ c >= 6 ]
		(51, 1)      f24(a, b, c) -> f21(a + 1, b, c) [ b >= 6 ]
		(1300, 1)    f13(a, b, c) -> f10(a + 1, b, c) [ b >= 6 ]
		(5, 1)       f10(a, b, c) -> f21(1, b, c) [ a >= 6 ]
	start location:	f0
	leaf cost:	1

A polynomial rank function with
	Pol(f27) = -V_3 + 6
	Pol(f13) = -V_2 + 6
and size complexities
	S("f10(a, b, c) -> f21(1, b, c) [ a >= 6 ]", 0-0) = 1
	S("f10(a, b, c) -> f21(1, b, c) [ a >= 6 ]", 0-1) = 6
	S("f10(a, b, c) -> f21(1, b, c) [ a >= 6 ]", 0-2) = c
	S("f13(a, b, c) -> f10(a + 1, b, c) [ b >= 6 ]", 0-0) = 1301
	S("f13(a, b, c) -> f10(a + 1, b, c) [ b >= 6 ]", 0-1) = 6
	S("f13(a, b, c) -> f10(a + 1, b, c) [ b >= 6 ]", 0-2) = c
	S("f24(a, b, c) -> f21(a + 1, b, c) [ b >= 6 ]", 0-0) = 52
	S("f24(a, b, c) -> f21(a + 1, b, c) [ b >= 6 ]", 0-1) = 1301
	S("f24(a, b, c) -> f21(a + 1, b, c) [ b >= 6 ]", 0-2) = 6
	S("f27(a, b, c) -> f24(a, b + 1, c) [ c >= 6 ]", 0-0) = 52
	S("f27(a, b, c) -> f24(a, b + 1, c) [ c >= 6 ]", 0-1) = 1301
	S("f27(a, b, c) -> f24(a, b + 1, c) [ c >= 6 ]", 0-2) = 6
	S("f27(a, b, c) -> f27(a, b, c + 1) [ 5 >= c ]", 0-0) = 52
	S("f27(a, b, c) -> f27(a, b, c + 1) [ 5 >= c ]", 0-1) = 1301
	S("f27(a, b, c) -> f27(a, b, c + 1) [ 5 >= c ]", 0-2) = 6
	S("f24(a, b, c) -> f27(a, b, 1) [ 5 >= b ]", 0-0) = 52
	S("f24(a, b, c) -> f27(a, b, 1) [ 5 >= b ]", 0-1) = 1301
	S("f24(a, b, c) -> f27(a, b, 1) [ 5 >= b ]", 0-2) = 1
	S("f21(a, b, c) -> f24(a, 1, c) [ 5 >= a ]", 0-0) = 52
	S("f21(a, b, c) -> f24(a, 1, c) [ 5 >= a ]", 0-1) = 1
	S("f21(a, b, c) -> f24(a, 1, c) [ 5 >= a ]", 0-2) = c + 6
	S("f13(a, b, c) -> f13(a, b + 1, c) [ 5 >= b ]", 0-0) = 1301
	S("f13(a, b, c) -> f13(a, b + 1, c) [ 5 >= b ]", 0-1) = 6
	S("f13(a, b, c) -> f13(a, b + 1, c) [ 5 >= b ]", 0-2) = c
	S("f10(a, b, c) -> f13(a, 1, c) [ 5 >= a ]", 0-0) = 1301
	S("f10(a, b, c) -> f13(a, 1, c) [ 5 >= a ]", 0-1) = 1
	S("f10(a, b, c) -> f13(a, 1, c) [ 5 >= a ]", 0-2) = c
	S("f0(a, b, c) -> f10(1, b, c)", 0-0) = 1
	S("f0(a, b, c) -> f10(1, b, c)", 0-1) = b
	S("f0(a, b, c) -> f10(1, b, c)", 0-2) = c
orients the transitions
	f27(a, b, c) -> f27(a, b, c + 1) [ 5 >= c ]
	f13(a, b, c) -> f13(a, b + 1, c) [ 5 >= b ]
weakly and the transitions
	f27(a, b, c) -> f27(a, b, c + 1) [ 5 >= c ]
	f13(a, b, c) -> f13(a, b + 1, c) [ 5 >= b ]
strictly and produces the following problem:
8:	T:
		(1, 1)       f0(a, b, c) -> f10(1, b, c)
		(130, 1)     f10(a, b, c) -> f13(a, 1, c) [ 5 >= a ]
		(1820, 1)    f13(a, b, c) -> f13(a, b + 1, c) [ 5 >= b ]
		(9, 1)       f21(a, b, c) -> f24(a, 1, c) [ 5 >= a ]
		(130, 1)     f24(a, b, c) -> f27(a, b, 1) [ 5 >= b ]
		(1820, 1)    f27(a, b, c) -> f27(a, b, c + 1) [ 5 >= c ]
		(1300, 1)    f27(a, b, c) -> f24(a, b + 1, c) [ c >= 6 ]
		(51, 1)      f24(a, b, c) -> f21(a + 1, b, c) [ b >= 6 ]
		(1300, 1)    f13(a, b, c) -> f10(a + 1, b, c) [ b >= 6 ]
		(5, 1)       f10(a, b, c) -> f21(1, b, c) [ a >= 6 ]
	start location:	f0
	leaf cost:	1

Complexity upper bound 6567

Time: 0.373 sec (SMT: 0.349 sec)