MAYBE

Initial complexity problem:
1:	T:
		(1, 1)    f0(a, b, c, d, e, f, g, h, i, j, k) -> f5(a, b, c, d, e, f, g, h, i, j, k)
		(1, 1)    f0(a, b, c, d, e, f, g, h, i, j, k) -> f12(m, b, c, d, e, f, g, h, i, j, k) [ 15 >= l ]
		(?, 1)    f12(a, b, c, d, e, f, g, h, i, j, k) -> f20(a, m, m, d, e, f, g, h, i, j, k) [ 0 >= a + 1 ]
		(?, 1)    f12(a, b, c, d, e, f, g, h, i, j, k) -> f20(a, m, m, d, e, f, g, h, i, j, k) [ a >= 1 ]
		(1, 1)    f0(a, b, c, d, e, f, g, h, i, j, k) -> f5(a, b, c, 1, 1, f, g, h, i, j, k) [ 15 >= m ]
		(?, 1)    f20(a, b, c, d, e, f, g, h, i, j, k) -> f12(a - 1, b, c, d, e, 0, 0, h, i, j, k)
		(?, 1)    f12(a, b, c, d, e, f, g, h, i, j, k) -> f5(0, b, c, 0, 0, f, g, m, m, 0, 0) [ a = 0 ]
	start location:	f0
	leaf cost:	0

Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a].
We thus obtain the following problem:
2:	T:
		(?, 1)    f12(a) -> f5(0) [ a = 0 ]
		(?, 1)    f20(a) -> f12(a - 1)
		(1, 1)    f0(a) -> f5(a) [ 15 >= m ]
		(?, 1)    f12(a) -> f20(a) [ a >= 1 ]
		(?, 1)    f12(a) -> f20(a) [ 0 >= a + 1 ]
		(1, 1)    f0(a) -> f12(m) [ 15 >= l ]
		(1, 1)    f0(a) -> f5(a)
	start location:	f0
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem:
3:	T:
		(?, 1)    f20(a) -> f12(a - 1)
		(?, 1)    f12(a) -> f20(a) [ a >= 1 ]
		(?, 1)    f12(a) -> f20(a) [ 0 >= a + 1 ]
		(1, 1)    f0(a) -> f12(m) [ 15 >= l ]
	start location:	f0
	leaf cost:	3

By chaining the transition f12(a) -> f20(a) [ a >= 1 ] with all transitions in problem 3, the following new transition is obtained:
	f12(a) -> f12(a - 1) [ a >= 1 ]
We thus obtain the following problem:
4:	T:
		(?, 2)    f12(a) -> f12(a - 1) [ a >= 1 ]
		(?, 1)    f20(a) -> f12(a - 1)
		(?, 1)    f12(a) -> f20(a) [ 0 >= a + 1 ]
		(1, 1)    f0(a) -> f12(m) [ 15 >= l ]
	start location:	f0
	leaf cost:	3

By chaining the transition f12(a) -> f20(a) [ 0 >= a + 1 ] with all transitions in problem 4, the following new transition is obtained:
	f12(a) -> f12(a - 1) [ 0 >= a + 1 ]
We thus obtain the following problem:
5:	T:
		(?, 2)    f12(a) -> f12(a - 1) [ 0 >= a + 1 ]
		(?, 2)    f12(a) -> f12(a - 1) [ a >= 1 ]
		(?, 1)    f20(a) -> f12(a - 1)
		(1, 1)    f0(a) -> f12(m) [ 15 >= l ]
	start location:	f0
	leaf cost:	3

Testing for reachability in the complexity graph removes the following transition from problem 5:
	f20(a) -> f12(a - 1)
We thus obtain the following problem:
6:	T:
		(?, 2)    f12(a) -> f12(a - 1) [ 0 >= a + 1 ]
		(?, 2)    f12(a) -> f12(a - 1) [ a >= 1 ]
		(1, 1)    f0(a) -> f12(m) [ 15 >= l ]
	start location:	f0
	leaf cost:	3

By chaining the transition f0(a) -> f12(m) [ 15 >= l ] with all transitions in problem 6, the following new transitions are obtained:
	f0(a) -> f12(m - 1) [ 15 >= l /\ 0 >= m + 1 ]
	f0(a) -> f12(m - 1) [ 15 >= l /\ m >= 1 ]
We thus obtain the following problem:
7:	T:
		(1, 3)    f0(a) -> f12(m - 1) [ 15 >= l /\ 0 >= m + 1 ]
		(1, 3)    f0(a) -> f12(m - 1) [ 15 >= l /\ m >= 1 ]
		(?, 2)    f12(a) -> f12(a - 1) [ 0 >= a + 1 ]
		(?, 2)    f12(a) -> f12(a - 1) [ a >= 1 ]
	start location:	f0
	leaf cost:	3

By chaining the transition f0(a) -> f12(m - 1) [ 15 >= l /\ 0 >= m + 1 ] with all transitions in problem 7, the following new transition is obtained:
	f0(a) -> f12(m - 2) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m ]
We thus obtain the following problem:
8:	T:
		(1, 5)    f0(a) -> f12(m - 2) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m ]
		(1, 3)    f0(a) -> f12(m - 1) [ 15 >= l /\ m >= 1 ]
		(?, 2)    f12(a) -> f12(a - 1) [ 0 >= a + 1 ]
		(?, 2)    f12(a) -> f12(a - 1) [ a >= 1 ]
	start location:	f0
	leaf cost:	3

By chaining the transition f0(a) -> f12(m - 2) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m ] with all transitions in problem 8, the following new transition is obtained:
	f0(a) -> f12(m - 3) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 ]
We thus obtain the following problem:
9:	T:
		(1, 7)    f0(a) -> f12(m - 3) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 ]
		(1, 3)    f0(a) -> f12(m - 1) [ 15 >= l /\ m >= 1 ]
		(?, 2)    f12(a) -> f12(a - 1) [ 0 >= a + 1 ]
		(?, 2)    f12(a) -> f12(a - 1) [ a >= 1 ]
	start location:	f0
	leaf cost:	3

By chaining the transition f0(a) -> f12(m - 3) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 ] with all transitions in problem 9, the following new transition is obtained:
	f0(a) -> f12(m - 4) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 /\ 0 >= m - 2 ]
We thus obtain the following problem:
10:	T:
		(1, 9)    f0(a) -> f12(m - 4) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 /\ 0 >= m - 2 ]
		(1, 3)    f0(a) -> f12(m - 1) [ 15 >= l /\ m >= 1 ]
		(?, 2)    f12(a) -> f12(a - 1) [ 0 >= a + 1 ]
		(?, 2)    f12(a) -> f12(a - 1) [ a >= 1 ]
	start location:	f0
	leaf cost:	3

By chaining the transition f0(a) -> f12(m - 4) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 /\ 0 >= m - 2 ] with all transitions in problem 10, the following new transition is obtained:
	f0(a) -> f12(m - 5) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 /\ 0 >= m - 2 /\ 0 >= m - 3 ]
We thus obtain the following problem:
11:	T:
		(1, 11)    f0(a) -> f12(m - 5) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 /\ 0 >= m - 2 /\ 0 >= m - 3 ]
		(1, 3)     f0(a) -> f12(m - 1) [ 15 >= l /\ m >= 1 ]
		(?, 2)     f12(a) -> f12(a - 1) [ 0 >= a + 1 ]
		(?, 2)     f12(a) -> f12(a - 1) [ a >= 1 ]
	start location:	f0
	leaf cost:	3

By chaining the transition f0(a) -> f12(m - 5) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 /\ 0 >= m - 2 /\ 0 >= m - 3 ] with all transitions in problem 11, the following new transition is obtained:
	f0(a) -> f12(m - 6) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 /\ 0 >= m - 2 /\ 0 >= m - 3 /\ 0 >= m - 4 ]
We thus obtain the following problem:
12:	T:
		(1, 13)    f0(a) -> f12(m - 6) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 /\ 0 >= m - 2 /\ 0 >= m - 3 /\ 0 >= m - 4 ]
		(1, 3)     f0(a) -> f12(m - 1) [ 15 >= l /\ m >= 1 ]
		(?, 2)     f12(a) -> f12(a - 1) [ 0 >= a + 1 ]
		(?, 2)     f12(a) -> f12(a - 1) [ a >= 1 ]
	start location:	f0
	leaf cost:	3

By chaining the transition f0(a) -> f12(m - 6) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 /\ 0 >= m - 2 /\ 0 >= m - 3 /\ 0 >= m - 4 ] with all transitions in problem 12, the following new transition is obtained:
	f0(a) -> f12(m - 7) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 /\ 0 >= m - 2 /\ 0 >= m - 3 /\ 0 >= m - 4 /\ 0 >= m - 5 ]
We thus obtain the following problem:
13:	T:
		(1, 15)    f0(a) -> f12(m - 7) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 /\ 0 >= m - 2 /\ 0 >= m - 3 /\ 0 >= m - 4 /\ 0 >= m - 5 ]
		(1, 3)     f0(a) -> f12(m - 1) [ 15 >= l /\ m >= 1 ]
		(?, 2)     f12(a) -> f12(a - 1) [ 0 >= a + 1 ]
		(?, 2)     f12(a) -> f12(a - 1) [ a >= 1 ]
	start location:	f0
	leaf cost:	3

By chaining the transition f0(a) -> f12(m - 7) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 /\ 0 >= m - 2 /\ 0 >= m - 3 /\ 0 >= m - 4 /\ 0 >= m - 5 ] with all transitions in problem 13, the following new transition is obtained:
	f0(a) -> f12(m - 8) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 /\ 0 >= m - 2 /\ 0 >= m - 3 /\ 0 >= m - 4 /\ 0 >= m - 5 /\ 0 >= m - 6 ]
We thus obtain the following problem:
14:	T:
		(1, 17)    f0(a) -> f12(m - 8) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 /\ 0 >= m - 2 /\ 0 >= m - 3 /\ 0 >= m - 4 /\ 0 >= m - 5 /\ 0 >= m - 6 ]
		(1, 3)     f0(a) -> f12(m - 1) [ 15 >= l /\ m >= 1 ]
		(?, 2)     f12(a) -> f12(a - 1) [ 0 >= a + 1 ]
		(?, 2)     f12(a) -> f12(a - 1) [ a >= 1 ]
	start location:	f0
	leaf cost:	3

By chaining the transition f0(a) -> f12(m - 8) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 /\ 0 >= m - 2 /\ 0 >= m - 3 /\ 0 >= m - 4 /\ 0 >= m - 5 /\ 0 >= m - 6 ] with all transitions in problem 14, the following new transition is obtained:
	f0(a) -> f12(m - 9) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 /\ 0 >= m - 2 /\ 0 >= m - 3 /\ 0 >= m - 4 /\ 0 >= m - 5 /\ 0 >= m - 6 /\ 0 >= m - 7 ]
We thus obtain the following problem:
15:	T:
		(1, 19)    f0(a) -> f12(m - 9) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 /\ 0 >= m - 2 /\ 0 >= m - 3 /\ 0 >= m - 4 /\ 0 >= m - 5 /\ 0 >= m - 6 /\ 0 >= m - 7 ]
		(1, 3)     f0(a) -> f12(m - 1) [ 15 >= l /\ m >= 1 ]
		(?, 2)     f12(a) -> f12(a - 1) [ 0 >= a + 1 ]
		(?, 2)     f12(a) -> f12(a - 1) [ a >= 1 ]
	start location:	f0
	leaf cost:	3

By chaining the transition f0(a) -> f12(m - 9) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 /\ 0 >= m - 2 /\ 0 >= m - 3 /\ 0 >= m - 4 /\ 0 >= m - 5 /\ 0 >= m - 6 /\ 0 >= m - 7 ] with all transitions in problem 15, the following new transition is obtained:
	f0(a) -> f12(m - 10) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 /\ 0 >= m - 2 /\ 0 >= m - 3 /\ 0 >= m - 4 /\ 0 >= m - 5 /\ 0 >= m - 6 /\ 0 >= m - 7 /\ 0 >= m - 8 ]
We thus obtain the following problem:
16:	T:
		(1, 21)    f0(a) -> f12(m - 10) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 /\ 0 >= m - 2 /\ 0 >= m - 3 /\ 0 >= m - 4 /\ 0 >= m - 5 /\ 0 >= m - 6 /\ 0 >= m - 7 /\ 0 >= m - 8 ]
		(1, 3)     f0(a) -> f12(m - 1) [ 15 >= l /\ m >= 1 ]
		(?, 2)     f12(a) -> f12(a - 1) [ 0 >= a + 1 ]
		(?, 2)     f12(a) -> f12(a - 1) [ a >= 1 ]
	start location:	f0
	leaf cost:	3

By chaining the transition f0(a) -> f12(m - 10) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 /\ 0 >= m - 2 /\ 0 >= m - 3 /\ 0 >= m - 4 /\ 0 >= m - 5 /\ 0 >= m - 6 /\ 0 >= m - 7 /\ 0 >= m - 8 ] with all transitions in problem 16, the following new transition is obtained:
	f0(a) -> f12(m - 11) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 /\ 0 >= m - 2 /\ 0 >= m - 3 /\ 0 >= m - 4 /\ 0 >= m - 5 /\ 0 >= m - 6 /\ 0 >= m - 7 /\ 0 >= m - 8 /\ 0 >= m - 9 ]
We thus obtain the following problem:
17:	T:
		(1, 23)    f0(a) -> f12(m - 11) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 /\ 0 >= m - 2 /\ 0 >= m - 3 /\ 0 >= m - 4 /\ 0 >= m - 5 /\ 0 >= m - 6 /\ 0 >= m - 7 /\ 0 >= m - 8 /\ 0 >= m - 9 ]
		(1, 3)     f0(a) -> f12(m - 1) [ 15 >= l /\ m >= 1 ]
		(?, 2)     f12(a) -> f12(a - 1) [ 0 >= a + 1 ]
		(?, 2)     f12(a) -> f12(a - 1) [ a >= 1 ]
	start location:	f0
	leaf cost:	3

By chaining the transition f0(a) -> f12(m - 11) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 /\ 0 >= m - 2 /\ 0 >= m - 3 /\ 0 >= m - 4 /\ 0 >= m - 5 /\ 0 >= m - 6 /\ 0 >= m - 7 /\ 0 >= m - 8 /\ 0 >= m - 9 ] with all transitions in problem 17, the following new transition is obtained:
	f0(a) -> f12(m - 12) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 /\ 0 >= m - 2 /\ 0 >= m - 3 /\ 0 >= m - 4 /\ 0 >= m - 5 /\ 0 >= m - 6 /\ 0 >= m - 7 /\ 0 >= m - 8 /\ 0 >= m - 9 /\ 0 >= m - 10 ]
We thus obtain the following problem:
18:	T:
		(1, 25)    f0(a) -> f12(m - 12) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 /\ 0 >= m - 2 /\ 0 >= m - 3 /\ 0 >= m - 4 /\ 0 >= m - 5 /\ 0 >= m - 6 /\ 0 >= m - 7 /\ 0 >= m - 8 /\ 0 >= m - 9 /\ 0 >= m - 10 ]
		(1, 3)     f0(a) -> f12(m - 1) [ 15 >= l /\ m >= 1 ]
		(?, 2)     f12(a) -> f12(a - 1) [ 0 >= a + 1 ]
		(?, 2)     f12(a) -> f12(a - 1) [ a >= 1 ]
	start location:	f0
	leaf cost:	3

By chaining the transition f0(a) -> f12(m - 12) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 /\ 0 >= m - 2 /\ 0 >= m - 3 /\ 0 >= m - 4 /\ 0 >= m - 5 /\ 0 >= m - 6 /\ 0 >= m - 7 /\ 0 >= m - 8 /\ 0 >= m - 9 /\ 0 >= m - 10 ] with all transitions in problem 18, the following new transition is obtained:
	f0(a) -> f12(m - 13) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 /\ 0 >= m - 2 /\ 0 >= m - 3 /\ 0 >= m - 4 /\ 0 >= m - 5 /\ 0 >= m - 6 /\ 0 >= m - 7 /\ 0 >= m - 8 /\ 0 >= m - 9 /\ 0 >= m - 10 /\ 0 >= m - 11 ]
We thus obtain the following problem:
19:	T:
		(1, 27)    f0(a) -> f12(m - 13) [ 15 >= l /\ 0 >= m + 1 /\ 0 >= m /\ 0 >= m - 1 /\ 0 >= m - 2 /\ 0 >= m - 3 /\ 0 >= m - 4 /\ 0 >= m - 5 /\ 0 >= m - 6 /\ 0 >= m - 7 /\ 0 >= m - 8 /\ 0 >= m - 9 /\ 0 >= m - 10 /\ 0 >= m - 11 ]
		(1, 3)     f0(a) -> f12(m - 1) [ 15 >= l /\ m >= 1 ]
		(?, 2)     f12(a) -> f12(a - 1) [ 0 >= a + 1 ]
		(?, 2)     f12(a) -> f12(a - 1) [ a >= 1 ]
	start location:	f0
	leaf cost:	3

Complexity upper bound ?

Time: 0.805 sec (SMT: 0.746 sec)