MAYBE

Initial complexity problem:
1:	T:
		(?, 1)    f12(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1) -> f12(a, b, c1, e1, b, g, g, a, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1) [ a >= 0 /\ c1 >= 2 /\ 0 >= d1 + 1 /\ 0 >= e1 + 1 /\ 0 >= b + 1 ]
		(?, 1)    f12(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1) -> f12(a, b, c1, e1, b, g, g, a, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1) [ a >= 0 /\ c1 >= 2 /\ 0 >= d1 + 1 /\ 0 >= e1 + 1 /\ b >= 1 ]
		(?, 1)    f12(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1) -> f12(a, b, c1, e1, b, g, g, a, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1) [ a >= 0 /\ c1 >= 2 /\ 0 >= d1 + 1 /\ e1 >= 1 /\ 0 >= b + 1 ]
		(?, 1)    f12(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1) -> f12(a, b, c1, e1, b, g, g, a, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1) [ a >= 0 /\ c1 >= 2 /\ 0 >= d1 + 1 /\ e1 >= 1 /\ b >= 1 ]
		(?, 1)    f12(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1) -> f12(a, b, c1, e1, b, g, g, a, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1) [ a >= 0 /\ c1 >= 2 /\ d1 >= 1 /\ 0 >= e1 + 1 /\ 0 >= b + 1 ]
		(?, 1)    f12(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1) -> f12(a, b, c1, e1, b, g, g, a, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1) [ a >= 0 /\ c1 >= 2 /\ d1 >= 1 /\ 0 >= e1 + 1 /\ b >= 1 ]
		(?, 1)    f12(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1) -> f12(a, b, c1, e1, b, g, g, a, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1) [ a >= 0 /\ c1 >= 2 /\ d1 >= 1 /\ e1 >= 1 /\ 0 >= b + 1 ]
		(?, 1)    f12(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1) -> f12(a, b, c1, e1, b, g, g, a, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1) [ a >= 0 /\ c1 >= 2 /\ d1 >= 1 /\ e1 >= 1 /\ b >= 1 ]
		(?, 1)    f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1) -> f1(a, b, c, d, e, f, g, h, i, j + 1, l, c1, l, e1, j, p, q, r, s, t, u, v, w, x, y, z, a1, b1) [ i >= j + 1 /\ j >= 0 ]
		(1, 1)    f8(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1) -> f1(a, b, c1, d, e, f, g, h, c1, 2, d1, f1, d1, n, o, e1, d1, g1, 2, t, u, v, w, x, y, z, a1, b1) [ c1 >= 2 ]
		(1, 1)    f8(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1) -> f9(a, 0, c1, 0, e, f, g, h, n1, l1, o1, r1, q1, n, o, m1, p1, r, s, e1, d1, f1, g1, k1, s1, t1, u1, b1) [ 0 >= h1 /\ 0 >= i1 /\ 0 >= c1 /\ 0 >= j1 ]
		(?, 1)    f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1) -> f12(a, k, c1, e1, e, f, g, h, g1, f1, k1, n1, m1, n, o, p, l1, r, s, t, u, v, w, x, o1, p1, a1, d1) [ j >= i /\ j >= 0 /\ q1 >= 2 /\ f1 >= q1 /\ f1 >= 0 /\ d1 >= c1 /\ c1 >= 2 /\ 0 >= k + 1 /\ 0 >= e1 + 1 ]
		(?, 1)    f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1) -> f12(a, k, c1, e1, e, f, g, h, g1, f1, k1, n1, m1, n, o, p, l1, r, s, t, u, v, w, x, o1, p1, a1, d1) [ j >= i /\ j >= 0 /\ q1 >= 2 /\ f1 >= q1 /\ f1 >= 0 /\ d1 >= c1 /\ c1 >= 2 /\ 0 >= k + 1 /\ e1 >= 1 ]
		(?, 1)    f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1) -> f12(a, k, c1, e1, e, f, g, h, g1, f1, k1, n1, m1, n, o, p, l1, r, s, t, u, v, w, x, o1, p1, a1, d1) [ j >= i /\ j >= 0 /\ q1 >= 2 /\ f1 >= q1 /\ f1 >= 0 /\ d1 >= c1 /\ c1 >= 2 /\ k >= 1 /\ 0 >= e1 + 1 ]
		(?, 1)    f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, a1, b1) -> f12(a, k, c1, e1, e, f, g, h, g1, f1, k1, n1, m1, n, o, p, l1, r, s, t, u, v, w, x, o1, p1, a1, d1) [ j >= i /\ j >= 0 /\ q1 >= 2 /\ f1 >= q1 /\ f1 >= 0 /\ d1 >= c1 /\ c1 >= 2 /\ k >= 1 /\ e1 >= 1 ]
	start location:	f8
	leaf cost:	0

Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, i, j, k, l].
We thus obtain the following problem:
2:	T:
		(?, 1)    f1(a, b, i, j, k, l) -> f12(a, k, g1, f1, k1, n1) [ j >= i /\ j >= 0 /\ q1 >= 2 /\ f1 >= q1 /\ f1 >= 0 /\ d1 >= c1 /\ c1 >= 2 /\ k >= 1 /\ e1 >= 1 ]
		(?, 1)    f1(a, b, i, j, k, l) -> f12(a, k, g1, f1, k1, n1) [ j >= i /\ j >= 0 /\ q1 >= 2 /\ f1 >= q1 /\ f1 >= 0 /\ d1 >= c1 /\ c1 >= 2 /\ k >= 1 /\ 0 >= e1 + 1 ]
		(?, 1)    f1(a, b, i, j, k, l) -> f12(a, k, g1, f1, k1, n1) [ j >= i /\ j >= 0 /\ q1 >= 2 /\ f1 >= q1 /\ f1 >= 0 /\ d1 >= c1 /\ c1 >= 2 /\ 0 >= k + 1 /\ e1 >= 1 ]
		(?, 1)    f1(a, b, i, j, k, l) -> f12(a, k, g1, f1, k1, n1) [ j >= i /\ j >= 0 /\ q1 >= 2 /\ f1 >= q1 /\ f1 >= 0 /\ d1 >= c1 /\ c1 >= 2 /\ 0 >= k + 1 /\ 0 >= e1 + 1 ]
		(1, 1)    f8(a, b, i, j, k, l) -> f9(a, 0, n1, l1, o1, r1) [ 0 >= h1 /\ 0 >= i1 /\ 0 >= c1 /\ 0 >= j1 ]
		(1, 1)    f8(a, b, i, j, k, l) -> f1(a, b, c1, 2, d1, f1) [ c1 >= 2 ]
		(?, 1)    f1(a, b, i, j, k, l) -> f1(a, b, i, j + 1, l, c1) [ i >= j + 1 /\ j >= 0 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ a >= 0 /\ c1 >= 2 /\ d1 >= 1 /\ e1 >= 1 /\ b >= 1 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ a >= 0 /\ c1 >= 2 /\ d1 >= 1 /\ e1 >= 1 /\ 0 >= b + 1 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ a >= 0 /\ c1 >= 2 /\ d1 >= 1 /\ 0 >= e1 + 1 /\ b >= 1 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ a >= 0 /\ c1 >= 2 /\ d1 >= 1 /\ 0 >= e1 + 1 /\ 0 >= b + 1 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ a >= 0 /\ c1 >= 2 /\ 0 >= d1 + 1 /\ e1 >= 1 /\ b >= 1 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ a >= 0 /\ c1 >= 2 /\ 0 >= d1 + 1 /\ e1 >= 1 /\ 0 >= b + 1 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ a >= 0 /\ c1 >= 2 /\ 0 >= d1 + 1 /\ 0 >= e1 + 1 /\ b >= 1 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ a >= 0 /\ c1 >= 2 /\ 0 >= d1 + 1 /\ 0 >= e1 + 1 /\ 0 >= b + 1 ]
	start location:	f8
	leaf cost:	0

A polynomial rank function with
	Pol(f1) = 1
	Pol(f12) = -5
	Pol(f8) = 1
	Pol(f9) = 1
orients all transitions weakly and the transitions
	f1(a, b, i, j, k, l) -> f12(a, k, g1, f1, k1, n1) [ j >= i /\ j >= 0 /\ q1 >= 2 /\ f1 >= q1 /\ f1 >= 0 /\ d1 >= c1 /\ c1 >= 2 /\ k >= 1 /\ 0 >= e1 + 1 ]
	f1(a, b, i, j, k, l) -> f12(a, k, g1, f1, k1, n1) [ j >= i /\ j >= 0 /\ q1 >= 2 /\ f1 >= q1 /\ f1 >= 0 /\ d1 >= c1 /\ c1 >= 2 /\ 0 >= k + 1 /\ e1 >= 1 ]
	f1(a, b, i, j, k, l) -> f12(a, k, g1, f1, k1, n1) [ j >= i /\ j >= 0 /\ q1 >= 2 /\ f1 >= q1 /\ f1 >= 0 /\ d1 >= c1 /\ c1 >= 2 /\ 0 >= k + 1 /\ 0 >= e1 + 1 ]
strictly and produces the following problem:
3:	T:
		(?, 1)    f1(a, b, i, j, k, l) -> f12(a, k, g1, f1, k1, n1) [ j >= i /\ j >= 0 /\ q1 >= 2 /\ f1 >= q1 /\ f1 >= 0 /\ d1 >= c1 /\ c1 >= 2 /\ k >= 1 /\ e1 >= 1 ]
		(1, 1)    f1(a, b, i, j, k, l) -> f12(a, k, g1, f1, k1, n1) [ j >= i /\ j >= 0 /\ q1 >= 2 /\ f1 >= q1 /\ f1 >= 0 /\ d1 >= c1 /\ c1 >= 2 /\ k >= 1 /\ 0 >= e1 + 1 ]
		(1, 1)    f1(a, b, i, j, k, l) -> f12(a, k, g1, f1, k1, n1) [ j >= i /\ j >= 0 /\ q1 >= 2 /\ f1 >= q1 /\ f1 >= 0 /\ d1 >= c1 /\ c1 >= 2 /\ 0 >= k + 1 /\ e1 >= 1 ]
		(1, 1)    f1(a, b, i, j, k, l) -> f12(a, k, g1, f1, k1, n1) [ j >= i /\ j >= 0 /\ q1 >= 2 /\ f1 >= q1 /\ f1 >= 0 /\ d1 >= c1 /\ c1 >= 2 /\ 0 >= k + 1 /\ 0 >= e1 + 1 ]
		(1, 1)    f8(a, b, i, j, k, l) -> f9(a, 0, n1, l1, o1, r1) [ 0 >= h1 /\ 0 >= i1 /\ 0 >= c1 /\ 0 >= j1 ]
		(1, 1)    f8(a, b, i, j, k, l) -> f1(a, b, c1, 2, d1, f1) [ c1 >= 2 ]
		(?, 1)    f1(a, b, i, j, k, l) -> f1(a, b, i, j + 1, l, c1) [ i >= j + 1 /\ j >= 0 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ a >= 0 /\ c1 >= 2 /\ d1 >= 1 /\ e1 >= 1 /\ b >= 1 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ a >= 0 /\ c1 >= 2 /\ d1 >= 1 /\ e1 >= 1 /\ 0 >= b + 1 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ a >= 0 /\ c1 >= 2 /\ d1 >= 1 /\ 0 >= e1 + 1 /\ b >= 1 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ a >= 0 /\ c1 >= 2 /\ d1 >= 1 /\ 0 >= e1 + 1 /\ 0 >= b + 1 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ a >= 0 /\ c1 >= 2 /\ 0 >= d1 + 1 /\ e1 >= 1 /\ b >= 1 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ a >= 0 /\ c1 >= 2 /\ 0 >= d1 + 1 /\ e1 >= 1 /\ 0 >= b + 1 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ a >= 0 /\ c1 >= 2 /\ 0 >= d1 + 1 /\ 0 >= e1 + 1 /\ b >= 1 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ a >= 0 /\ c1 >= 2 /\ 0 >= d1 + 1 /\ 0 >= e1 + 1 /\ 0 >= b + 1 ]
	start location:	f8
	leaf cost:	0

A polynomial rank function with
	Pol(f1) = 1
	Pol(f12) = -5
	Pol(f8) = 1
	Pol(f9) = 0
orients all transitions weakly and the transition
	f1(a, b, i, j, k, l) -> f12(a, k, g1, f1, k1, n1) [ j >= i /\ j >= 0 /\ q1 >= 2 /\ f1 >= q1 /\ f1 >= 0 /\ d1 >= c1 /\ c1 >= 2 /\ k >= 1 /\ e1 >= 1 ]
strictly and produces the following problem:
4:	T:
		(1, 1)    f1(a, b, i, j, k, l) -> f12(a, k, g1, f1, k1, n1) [ j >= i /\ j >= 0 /\ q1 >= 2 /\ f1 >= q1 /\ f1 >= 0 /\ d1 >= c1 /\ c1 >= 2 /\ k >= 1 /\ e1 >= 1 ]
		(1, 1)    f1(a, b, i, j, k, l) -> f12(a, k, g1, f1, k1, n1) [ j >= i /\ j >= 0 /\ q1 >= 2 /\ f1 >= q1 /\ f1 >= 0 /\ d1 >= c1 /\ c1 >= 2 /\ k >= 1 /\ 0 >= e1 + 1 ]
		(1, 1)    f1(a, b, i, j, k, l) -> f12(a, k, g1, f1, k1, n1) [ j >= i /\ j >= 0 /\ q1 >= 2 /\ f1 >= q1 /\ f1 >= 0 /\ d1 >= c1 /\ c1 >= 2 /\ 0 >= k + 1 /\ e1 >= 1 ]
		(1, 1)    f1(a, b, i, j, k, l) -> f12(a, k, g1, f1, k1, n1) [ j >= i /\ j >= 0 /\ q1 >= 2 /\ f1 >= q1 /\ f1 >= 0 /\ d1 >= c1 /\ c1 >= 2 /\ 0 >= k + 1 /\ 0 >= e1 + 1 ]
		(1, 1)    f8(a, b, i, j, k, l) -> f9(a, 0, n1, l1, o1, r1) [ 0 >= h1 /\ 0 >= i1 /\ 0 >= c1 /\ 0 >= j1 ]
		(1, 1)    f8(a, b, i, j, k, l) -> f1(a, b, c1, 2, d1, f1) [ c1 >= 2 ]
		(?, 1)    f1(a, b, i, j, k, l) -> f1(a, b, i, j + 1, l, c1) [ i >= j + 1 /\ j >= 0 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ a >= 0 /\ c1 >= 2 /\ d1 >= 1 /\ e1 >= 1 /\ b >= 1 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ a >= 0 /\ c1 >= 2 /\ d1 >= 1 /\ e1 >= 1 /\ 0 >= b + 1 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ a >= 0 /\ c1 >= 2 /\ d1 >= 1 /\ 0 >= e1 + 1 /\ b >= 1 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ a >= 0 /\ c1 >= 2 /\ d1 >= 1 /\ 0 >= e1 + 1 /\ 0 >= b + 1 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ a >= 0 /\ c1 >= 2 /\ 0 >= d1 + 1 /\ e1 >= 1 /\ b >= 1 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ a >= 0 /\ c1 >= 2 /\ 0 >= d1 + 1 /\ e1 >= 1 /\ 0 >= b + 1 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ a >= 0 /\ c1 >= 2 /\ 0 >= d1 + 1 /\ 0 >= e1 + 1 /\ b >= 1 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ a >= 0 /\ c1 >= 2 /\ 0 >= d1 + 1 /\ 0 >= e1 + 1 /\ 0 >= b + 1 ]
	start location:	f8
	leaf cost:	0

Applied AI with 'oct' on problem 4 to obtain the following invariants:
  For symbol f1: X_3 - X_4 >= 0 /\ X_4 - 2 >= 0 /\ X_3 + X_4 - 4 >= 0 /\ X_3 - 2 >= 0
  For symbol f12: X_4 - 2 >= 0


This yielded the following problem:
5:	T:
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ j - 2 >= 0 /\ a >= 0 /\ c1 >= 2 /\ 0 >= d1 + 1 /\ 0 >= e1 + 1 /\ 0 >= b + 1 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ j - 2 >= 0 /\ a >= 0 /\ c1 >= 2 /\ 0 >= d1 + 1 /\ 0 >= e1 + 1 /\ b >= 1 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ j - 2 >= 0 /\ a >= 0 /\ c1 >= 2 /\ 0 >= d1 + 1 /\ e1 >= 1 /\ 0 >= b + 1 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ j - 2 >= 0 /\ a >= 0 /\ c1 >= 2 /\ 0 >= d1 + 1 /\ e1 >= 1 /\ b >= 1 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ j - 2 >= 0 /\ a >= 0 /\ c1 >= 2 /\ d1 >= 1 /\ 0 >= e1 + 1 /\ 0 >= b + 1 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ j - 2 >= 0 /\ a >= 0 /\ c1 >= 2 /\ d1 >= 1 /\ 0 >= e1 + 1 /\ b >= 1 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ j - 2 >= 0 /\ a >= 0 /\ c1 >= 2 /\ d1 >= 1 /\ e1 >= 1 /\ 0 >= b + 1 ]
		(?, 1)    f12(a, b, i, j, k, l) -> f12(a, b, i, j, k, l) [ j - 2 >= 0 /\ a >= 0 /\ c1 >= 2 /\ d1 >= 1 /\ e1 >= 1 /\ b >= 1 ]
		(?, 1)    f1(a, b, i, j, k, l) -> f1(a, b, i, j + 1, l, c1) [ i - j >= 0 /\ j - 2 >= 0 /\ i + j - 4 >= 0 /\ i - 2 >= 0 /\ i >= j + 1 /\ j >= 0 ]
		(1, 1)    f8(a, b, i, j, k, l) -> f1(a, b, c1, 2, d1, f1) [ c1 >= 2 ]
		(1, 1)    f8(a, b, i, j, k, l) -> f9(a, 0, n1, l1, o1, r1) [ 0 >= h1 /\ 0 >= i1 /\ 0 >= c1 /\ 0 >= j1 ]
		(1, 1)    f1(a, b, i, j, k, l) -> f12(a, k, g1, f1, k1, n1) [ i - j >= 0 /\ j - 2 >= 0 /\ i + j - 4 >= 0 /\ i - 2 >= 0 /\ j >= i /\ j >= 0 /\ q1 >= 2 /\ f1 >= q1 /\ f1 >= 0 /\ d1 >= c1 /\ c1 >= 2 /\ 0 >= k + 1 /\ 0 >= e1 + 1 ]
		(1, 1)    f1(a, b, i, j, k, l) -> f12(a, k, g1, f1, k1, n1) [ i - j >= 0 /\ j - 2 >= 0 /\ i + j - 4 >= 0 /\ i - 2 >= 0 /\ j >= i /\ j >= 0 /\ q1 >= 2 /\ f1 >= q1 /\ f1 >= 0 /\ d1 >= c1 /\ c1 >= 2 /\ 0 >= k + 1 /\ e1 >= 1 ]
		(1, 1)    f1(a, b, i, j, k, l) -> f12(a, k, g1, f1, k1, n1) [ i - j >= 0 /\ j - 2 >= 0 /\ i + j - 4 >= 0 /\ i - 2 >= 0 /\ j >= i /\ j >= 0 /\ q1 >= 2 /\ f1 >= q1 /\ f1 >= 0 /\ d1 >= c1 /\ c1 >= 2 /\ k >= 1 /\ 0 >= e1 + 1 ]
		(1, 1)    f1(a, b, i, j, k, l) -> f12(a, k, g1, f1, k1, n1) [ i - j >= 0 /\ j - 2 >= 0 /\ i + j - 4 >= 0 /\ i - 2 >= 0 /\ j >= i /\ j >= 0 /\ q1 >= 2 /\ f1 >= q1 /\ f1 >= 0 /\ d1 >= c1 /\ c1 >= 2 /\ k >= 1 /\ e1 >= 1 ]
	start location:	f8
	leaf cost:	0

Complexity upper bound ?

Time: 1.631 sec (SMT: 1.391 sec)