Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f47 -> f51 : [ A>=1 ], cost: 1
     20: f47 -> f51 : [ B>=1 && 0>=A ], cost: 1
     19: f47 -> f45 : P'=2, [ 0>=B && 0>=A ], cost: 1
      1: f51 -> f45 : [ 0>=B ], cost: 1
     21: f51 -> f45 : P'=3, [ B>=1 ], cost: 1
     24: f45 -> f58 : O'=0, Q_1'=free_7, [ free_7>=0 && O>=1 && 1>=free_7 ], cost: 1
     25: f45 -> f58 : O'=1, Q_1'=free_8, [ free_8>=0 && 0>=O && 1>=free_8 ], cost: 1
      2: f0 -> f10 : C'=free, D'=free_1, E'=0, F'=1, G'=0, [ free>=1 && free_1>=0 ], cost: 1
      3: f10 -> f14 : H'=1, [ C>=1+G && 0>=G ], cost: 1
      4: f10 -> f14 : H'=0, [ C>=1+G && G>=1 ], cost: 1
     35: f10 -> f81 : [ G>=C ], cost: 1
      5: f14 -> f22 : Q'=1, J'=K, L'=free_2, [ 1+G>=C && 1>=free_2 && free_2>=0 ], cost: 1
      6: f14 -> f22 : Q'=0, J'=K, L'=free_3, [ C>=2+G && 1>=free_3 && free_3>=0 ], cost: 1
      7: f22 -> f26 : E'=1+E, [ L>=1 && 0>=D && 0>=E ], cost: 1
      8: f22 -> f26 : E'=1+E, [ L>=1 && 0>=D && E==1 ], cost: 1
      9: f22 -> f26 : D'=free_4, E'=0, F'=1+F, [ E>=2 && 0>=D && free_4>=0 ], cost: 1
     10: f22 -> f26 : D'=-1+D, [ D>=1 ], cost: 1
     32: f26 -> f22 : L'=free_12, [ 0>=L && C>=F && 1>=free_12 && free_12>=0 ], cost: 1
     11: f26 -> f41 : A'=H, B'=Q, M'=1, N'=J, [ M>=1 && L>=1 ], cost: 1
     12: f26 -> f41 : A'=H, B'=Q, M'=1, N'=J, O'=J, [ 0>=M && L>=1 ], cost: 1
     15: f41 -> f47 : A'=0, O'=N, [ A==0 && N==O ], cost: 1
     13: f41 -> f43 : O'=N, [ 0>=1+A && N==O ], cost: 1
     14: f41 -> f43 : O'=N, [ A>=1 && N==O ], cost: 1
     22: f41 -> f58 : Q_1'=free_5, [ free_5>=0 && N>=1+O && 1>=free_5 ], cost: 1
     23: f41 -> f58 : Q_1'=free_6, [ free_6>=0 && O>=1+N && 1>=free_6 ], cost: 1
     17: f43 -> f47 : [ 0>=1+B ], cost: 1
     18: f43 -> f47 : [ B>=1 ], cost: 1
     16: f43 -> f45 : B'=0, P'=1, [ B==0 ], cost: 1
     26: f58 -> f62 : E'=1+E, [ 0>=E && 0>=D && Q_1>=1 ], cost: 1
     27: f58 -> f62 : E'=1+E, [ 0>=D && Q_1>=1 && E==1 ], cost: 1
     28: f58 -> f62 : D'=free_9, E'=0, F'=1+F, [ E>=2 && 0>=D && free_9>=0 ], cost: 1
     29: f58 -> f62 : D'=-1+D, [ D>=1 ], cost: 1
     33: f62 -> f10 : G'=1+G, K'=0, Q_1'=1, [ K>=1 && C>=F && Q_1==1 ], cost: 1
     34: f62 -> f10 : G'=1+G, K'=1, Q_1'=1, [ 0>=K && C>=F && Q_1==1 ], cost: 1
     30: f62 -> f22 : L'=free_10, [ C>=F && free_10>=0 && 0>=Q_1 && 1>=free_10 ], cost: 1
     31: f62 -> f22 : L'=free_11, [ C>=F && free_11>=0 && Q_1>=2 && 1>=free_11 ], cost: 1


Simplified the transitions:
  Start location: f0
      0: f47 -> f51 : [ A>=1 ], cost: 1
     20: f47 -> f51 : [ B>=1 && 0>=A ], cost: 1
     19: f47 -> f45 : P'=2, [ 0>=B && 0>=A ], cost: 1
      1: f51 -> f45 : [ 0>=B ], cost: 1
     21: f51 -> f45 : P'=3, [ B>=1 ], cost: 1
     24: f45 -> f58 : O'=0, Q_1'=free_7, [ free_7>=0 && O>=1 && 1>=free_7 ], cost: 1
     25: f45 -> f58 : O'=1, Q_1'=free_8, [ free_8>=0 && 0>=O && 1>=free_8 ], cost: 1
      2: f0 -> f10 : C'=free, D'=free_1, E'=0, F'=1, G'=0, [ free>=1 && free_1>=0 ], cost: 1
      3: f10 -> f14 : H'=1, [ C>=1+G && 0>=G ], cost: 1
      4: f10 -> f14 : H'=0, [ C>=1+G && G>=1 ], cost: 1
      5: f14 -> f22 : Q'=1, J'=K, L'=free_2, [ 1+G>=C && 1>=free_2 && free_2>=0 ], cost: 1
      6: f14 -> f22 : Q'=0, J'=K, L'=free_3, [ C>=2+G && 1>=free_3 && free_3>=0 ], cost: 1
      7: f22 -> f26 : E'=1+E, [ L>=1 && 0>=D && 0>=E ], cost: 1
      8: f22 -> f26 : E'=1+E, [ L>=1 && 0>=D && E==1 ], cost: 1
      9: f22 -> f26 : D'=free_4, E'=0, F'=1+F, [ E>=2 && 0>=D && free_4>=0 ], cost: 1
     10: f22 -> f26 : D'=-1+D, [ D>=1 ], cost: 1
     32: f26 -> f22 : L'=free_12, [ 0>=L && C>=F && 1>=free_12 && free_12>=0 ], cost: 1
     11: f26 -> f41 : A'=H, B'=Q, M'=1, N'=J, [ M>=1 && L>=1 ], cost: 1
     12: f26 -> f41 : A'=H, B'=Q, M'=1, N'=J, O'=J, [ 0>=M && L>=1 ], cost: 1
     15: f41 -> f47 : A'=0, O'=N, [ A==0 && N==O ], cost: 1
     13: f41 -> f43 : O'=N, [ 0>=1+A && N==O ], cost: 1
     14: f41 -> f43 : O'=N, [ A>=1 && N==O ], cost: 1
     22: f41 -> f58 : Q_1'=free_5, [ free_5>=0 && N>=1+O && 1>=free_5 ], cost: 1
     23: f41 -> f58 : Q_1'=free_6, [ free_6>=0 && O>=1+N && 1>=free_6 ], cost: 1
     17: f43 -> f47 : [ 0>=1+B ], cost: 1
     18: f43 -> f47 : [ B>=1 ], cost: 1
     16: f43 -> f45 : B'=0, P'=1, [ B==0 ], cost: 1
     26: f58 -> f62 : E'=1+E, [ 0>=E && 0>=D && Q_1>=1 ], cost: 1
     27: f58 -> f62 : E'=1+E, [ 0>=D && Q_1>=1 && E==1 ], cost: 1
     28: f58 -> f62 : D'=free_9, E'=0, F'=1+F, [ E>=2 && 0>=D && free_9>=0 ], cost: 1
     29: f58 -> f62 : D'=-1+D, [ D>=1 ], cost: 1
     33: f62 -> f10 : G'=1+G, K'=0, Q_1'=1, [ K>=1 && C>=F && Q_1==1 ], cost: 1
     34: f62 -> f10 : G'=1+G, K'=1, Q_1'=1, [ 0>=K && C>=F && Q_1==1 ], cost: 1
     30: f62 -> f22 : L'=free_10, [ C>=F && free_10>=0 && 0>=Q_1 && 1>=free_10 ], cost: 1
     31: f62 -> f22 : L'=free_11, [ C>=F && free_11>=0 && Q_1>=2 && 1>=free_11 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
     19: f47 -> f45 : P'=2, [ 0>=B && 0>=A ], cost: 1
     56: f47 -> f45 : [ A>=1 && 0>=B ], cost: 2
     57: f47 -> f45 : P'=3, [ A>=1 && B>=1 ], cost: 2
     58: f47 -> f45 : P'=3, [ B>=1 && 0>=A && B>=1 ], cost: 2
     24: f45 -> f58 : O'=0, Q_1'=free_7, [ free_7>=0 && O>=1 && 1>=free_7 ], cost: 1
     25: f45 -> f58 : O'=1, Q_1'=free_8, [ free_8>=0 && 0>=O && 1>=free_8 ], cost: 1
      2: f0 -> f10 : C'=free, D'=free_1, E'=0, F'=1, G'=0, [ free>=1 && free_1>=0 ], cost: 1
     36: f10 -> f22 : H'=1, Q'=1, J'=K, L'=free_2, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_2 && free_2>=0 ], cost: 2
     37: f10 -> f22 : H'=1, Q'=0, J'=K, L'=free_3, [ C>=1+G && 0>=G && C>=2+G && 1>=free_3 && free_3>=0 ], cost: 2
     38: f10 -> f22 : H'=0, Q'=1, J'=K, L'=free_2, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_2 && free_2>=0 ], cost: 2
     39: f10 -> f22 : H'=0, Q'=0, J'=K, L'=free_3, [ C>=1+G && G>=1 && C>=2+G && 1>=free_3 && free_3>=0 ], cost: 2
     44: f22 -> f22 : D'=free_4, E'=0, F'=1+F, L'=free_12, [ E>=2 && 0>=D && free_4>=0 && 0>=L && C>=1+F && 1>=free_12 && free_12>=0 ], cost: 2
     47: f22 -> f22 : D'=-1+D, L'=free_12, [ D>=1 && 0>=L && C>=F && 1>=free_12 && free_12>=0 ], cost: 2
     40: f22 -> f41 : A'=H, B'=Q, E'=1+E, M'=1, N'=J, [ L>=1 && 0>=D && 0>=E && M>=1 && L>=1 ], cost: 2
     41: f22 -> f41 : A'=H, B'=Q, E'=1+E, M'=1, N'=J, O'=J, [ L>=1 && 0>=D && 0>=E && 0>=M && L>=1 ], cost: 2
     43: f22 -> f41 : A'=H, B'=Q, E'=1+E, M'=1, N'=J, O'=J, [ L>=1 && 0>=D && E==1 && 0>=M && L>=1 ], cost: 2
     45: f22 -> f41 : A'=H, B'=Q, D'=free_4, E'=0, F'=1+F, M'=1, N'=J, [ E>=2 && 0>=D && free_4>=0 && M>=1 && L>=1 ], cost: 2
     46: f22 -> f41 : A'=H, B'=Q, D'=free_4, E'=0, F'=1+F, M'=1, N'=J, O'=J, [ E>=2 && 0>=D && free_4>=0 && 0>=M && L>=1 ], cost: 2
     15: f41 -> f47 : A'=0, O'=N, [ A==0 && N==O ], cost: 1
     50: f41 -> f47 : O'=N, [ 0>=1+A && N==O && 0>=1+B ], cost: 2
     51: f41 -> f47 : O'=N, [ 0>=1+A && N==O && B>=1 ], cost: 2
     53: f41 -> f47 : O'=N, [ A>=1 && N==O && 0>=1+B ], cost: 2
     54: f41 -> f47 : O'=N, [ A>=1 && N==O && B>=1 ], cost: 2
     52: f41 -> f45 : B'=0, O'=N, P'=1, [ 0>=1+A && N==O && B==0 ], cost: 2
     55: f41 -> f45 : B'=0, O'=N, P'=1, [ A>=1 && N==O && B==0 ], cost: 2
     22: f41 -> f58 : Q_1'=free_5, [ free_5>=0 && N>=1+O && 1>=free_5 ], cost: 1
     23: f41 -> f58 : Q_1'=free_6, [ free_6>=0 && O>=1+N && 1>=free_6 ], cost: 1
     59: f58 -> f10 : E'=1+E, G'=1+G, K'=0, Q_1'=1, [ 0>=E && 0>=D && Q_1>=1 && K>=1 && C>=F && Q_1==1 ], cost: 2
     60: f58 -> f10 : E'=1+E, G'=1+G, K'=1, Q_1'=1, [ 0>=E && 0>=D && Q_1>=1 && 0>=K && C>=F && Q_1==1 ], cost: 2
     63: f58 -> f10 : E'=1+E, G'=1+G, K'=1, Q_1'=1, [ 0>=D && Q_1>=1 && E==1 && 0>=K && C>=F && Q_1==1 ], cost: 2
     65: f58 -> f10 : D'=free_9, E'=0, F'=1+F, G'=1+G, K'=0, Q_1'=1, [ E>=2 && 0>=D && free_9>=0 && K>=1 && C>=1+F && Q_1==1 ], cost: 2
     66: f58 -> f10 : D'=free_9, E'=0, F'=1+F, G'=1+G, K'=1, Q_1'=1, [ E>=2 && 0>=D && free_9>=0 && 0>=K && C>=1+F && Q_1==1 ], cost: 2
     61: f58 -> f22 : E'=1+E, L'=free_11, [ 0>=E && 0>=D && Q_1>=1 && C>=F && free_11>=0 && Q_1>=2 && 1>=free_11 ], cost: 2
     64: f58 -> f22 : E'=1+E, L'=free_11, [ 0>=D && Q_1>=1 && E==1 && C>=F && free_11>=0 && Q_1>=2 && 1>=free_11 ], cost: 2
     67: f58 -> f22 : D'=free_9, E'=0, F'=1+F, L'=free_10, [ E>=2 && 0>=D && free_9>=0 && C>=1+F && free_10>=0 && 0>=Q_1 && 1>=free_10 ], cost: 2
     68: f58 -> f22 : D'=free_9, E'=0, F'=1+F, L'=free_11, [ E>=2 && 0>=D && free_9>=0 && C>=1+F && free_11>=0 && Q_1>=2 && 1>=free_11 ], cost: 2
     72: f58 -> f22 : D'=-1+D, L'=free_11, [ D>=1 && C>=F && free_11>=0 && Q_1>=2 && 1>=free_11 ], cost: 2

Eliminating 2 self-loops for location f22
  Self-Loop 47 has the metering function: D, resulting in the new transition 74.
  Removing the self-loops: 44 47.
Adding an epsilon transition (to model nonexecution of the loops): 75.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
     19: f47 -> f45 : P'=2, [ 0>=B && 0>=A ], cost: 1
     56: f47 -> f45 : [ A>=1 && 0>=B ], cost: 2
     57: f47 -> f45 : P'=3, [ A>=1 && B>=1 ], cost: 2
     58: f47 -> f45 : P'=3, [ B>=1 && 0>=A && B>=1 ], cost: 2
     24: f45 -> f58 : O'=0, Q_1'=free_7, [ free_7>=0 && O>=1 && 1>=free_7 ], cost: 1
     25: f45 -> f58 : O'=1, Q_1'=free_8, [ free_8>=0 && 0>=O && 1>=free_8 ], cost: 1
      2: f0 -> f10 : C'=free, D'=free_1, E'=0, F'=1, G'=0, [ free>=1 && free_1>=0 ], cost: 1
     36: f10 -> f22 : H'=1, Q'=1, J'=K, L'=free_2, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_2 && free_2>=0 ], cost: 2
     37: f10 -> f22 : H'=1, Q'=0, J'=K, L'=free_3, [ C>=1+G && 0>=G && C>=2+G && 1>=free_3 && free_3>=0 ], cost: 2
     38: f10 -> f22 : H'=0, Q'=1, J'=K, L'=free_2, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_2 && free_2>=0 ], cost: 2
     39: f10 -> f22 : H'=0, Q'=0, J'=K, L'=free_3, [ C>=1+G && G>=1 && C>=2+G && 1>=free_3 && free_3>=0 ], cost: 2
     73: f22 -> [13] : D'=free_4, E'=0, F'=1+F, L'=free_12, [ E>=2 && 0>=D && free_4>=0 && 0>=L && C>=1+F && 1>=free_12 && free_12>=0 ], cost: 2
     74: f22 -> [13] : D'=0, L'=0, [ D>=1 && 0>=L && C>=F && 1>=0 && 0>=0 ], cost: 2*D
     75: f22 -> [13] : [], cost: 0
     15: f41 -> f47 : A'=0, O'=N, [ A==0 && N==O ], cost: 1
     50: f41 -> f47 : O'=N, [ 0>=1+A && N==O && 0>=1+B ], cost: 2
     51: f41 -> f47 : O'=N, [ 0>=1+A && N==O && B>=1 ], cost: 2
     53: f41 -> f47 : O'=N, [ A>=1 && N==O && 0>=1+B ], cost: 2
     54: f41 -> f47 : O'=N, [ A>=1 && N==O && B>=1 ], cost: 2
     52: f41 -> f45 : B'=0, O'=N, P'=1, [ 0>=1+A && N==O && B==0 ], cost: 2
     55: f41 -> f45 : B'=0, O'=N, P'=1, [ A>=1 && N==O && B==0 ], cost: 2
     22: f41 -> f58 : Q_1'=free_5, [ free_5>=0 && N>=1+O && 1>=free_5 ], cost: 1
     23: f41 -> f58 : Q_1'=free_6, [ free_6>=0 && O>=1+N && 1>=free_6 ], cost: 1
     59: f58 -> f10 : E'=1+E, G'=1+G, K'=0, Q_1'=1, [ 0>=E && 0>=D && Q_1>=1 && K>=1 && C>=F && Q_1==1 ], cost: 2
     60: f58 -> f10 : E'=1+E, G'=1+G, K'=1, Q_1'=1, [ 0>=E && 0>=D && Q_1>=1 && 0>=K && C>=F && Q_1==1 ], cost: 2
     63: f58 -> f10 : E'=1+E, G'=1+G, K'=1, Q_1'=1, [ 0>=D && Q_1>=1 && E==1 && 0>=K && C>=F && Q_1==1 ], cost: 2
     65: f58 -> f10 : D'=free_9, E'=0, F'=1+F, G'=1+G, K'=0, Q_1'=1, [ E>=2 && 0>=D && free_9>=0 && K>=1 && C>=1+F && Q_1==1 ], cost: 2
     66: f58 -> f10 : D'=free_9, E'=0, F'=1+F, G'=1+G, K'=1, Q_1'=1, [ E>=2 && 0>=D && free_9>=0 && 0>=K && C>=1+F && Q_1==1 ], cost: 2
     61: f58 -> f22 : E'=1+E, L'=free_11, [ 0>=E && 0>=D && Q_1>=1 && C>=F && free_11>=0 && Q_1>=2 && 1>=free_11 ], cost: 2
     64: f58 -> f22 : E'=1+E, L'=free_11, [ 0>=D && Q_1>=1 && E==1 && C>=F && free_11>=0 && Q_1>=2 && 1>=free_11 ], cost: 2
     67: f58 -> f22 : D'=free_9, E'=0, F'=1+F, L'=free_10, [ E>=2 && 0>=D && free_9>=0 && C>=1+F && free_10>=0 && 0>=Q_1 && 1>=free_10 ], cost: 2
     68: f58 -> f22 : D'=free_9, E'=0, F'=1+F, L'=free_11, [ E>=2 && 0>=D && free_9>=0 && C>=1+F && free_11>=0 && Q_1>=2 && 1>=free_11 ], cost: 2
     72: f58 -> f22 : D'=-1+D, L'=free_11, [ D>=1 && C>=F && free_11>=0 && Q_1>=2 && 1>=free_11 ], cost: 2
     40: [13] -> f41 : A'=H, B'=Q, E'=1+E, M'=1, N'=J, [ L>=1 && 0>=D && 0>=E && M>=1 && L>=1 ], cost: 2
     41: [13] -> f41 : A'=H, B'=Q, E'=1+E, M'=1, N'=J, O'=J, [ L>=1 && 0>=D && 0>=E && 0>=M && L>=1 ], cost: 2
     43: [13] -> f41 : A'=H, B'=Q, E'=1+E, M'=1, N'=J, O'=J, [ L>=1 && 0>=D && E==1 && 0>=M && L>=1 ], cost: 2
     45: [13] -> f41 : A'=H, B'=Q, D'=free_4, E'=0, F'=1+F, M'=1, N'=J, [ E>=2 && 0>=D && free_4>=0 && M>=1 && L>=1 ], cost: 2
     46: [13] -> f41 : A'=H, B'=Q, D'=free_4, E'=0, F'=1+F, M'=1, N'=J, O'=J, [ E>=2 && 0>=D && free_4>=0 && 0>=M && L>=1 ], cost: 2


Applied chaining over branches and pruning:
  Start location: f0
     24: f45 -> f58 : O'=0, Q_1'=free_7, [ free_7>=0 && O>=1 && 1>=free_7 ], cost: 1
     25: f45 -> f58 : O'=1, Q_1'=free_8, [ free_8>=0 && 0>=O && 1>=free_8 ], cost: 1
      2: f0 -> f10 : C'=free, D'=free_1, E'=0, F'=1, G'=0, [ free>=1 && free_1>=0 ], cost: 1
     36: f10 -> f22 : H'=1, Q'=1, J'=K, L'=free_2, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_2 && free_2>=0 ], cost: 2
     37: f10 -> f22 : H'=1, Q'=0, J'=K, L'=free_3, [ C>=1+G && 0>=G && C>=2+G && 1>=free_3 && free_3>=0 ], cost: 2
     38: f10 -> f22 : H'=0, Q'=1, J'=K, L'=free_2, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_2 && free_2>=0 ], cost: 2
     39: f10 -> f22 : H'=0, Q'=0, J'=K, L'=free_3, [ C>=1+G && G>=1 && C>=2+G && 1>=free_3 && free_3>=0 ], cost: 2
     76: f22 -> f41 : A'=H, B'=Q, D'=free_4, E'=1, F'=1+F, L'=free_12, M'=1, N'=J, [ E>=2 && 0>=D && free_4>=0 && 0>=L && C>=1+F && 1>=free_12 && free_12>=0 && free_12>=1 && 0>=free_4 && 0>=0 && M>=1 && free_12>=1 ], cost: 4
     77: f22 -> f41 : A'=H, B'=Q, D'=free_4, E'=1, F'=1+F, L'=free_12, M'=1, N'=J, O'=J, [ E>=2 && 0>=D && free_4>=0 && 0>=L && C>=1+F && 1>=free_12 && free_12>=0 && free_12>=1 && 0>=free_4 && 0>=0 && 0>=M && free_12>=1 ], cost: 4
     83: f22 -> f41 : A'=H, B'=Q, E'=1+E, M'=1, N'=J, [ L>=1 && 0>=D && 0>=E && M>=1 && L>=1 ], cost: 2
     84: f22 -> f41 : A'=H, B'=Q, E'=1+E, M'=1, N'=J, O'=J, [ L>=1 && 0>=D && 0>=E && 0>=M && L>=1 ], cost: 2
     85: f22 -> f41 : A'=H, B'=Q, E'=1+E, M'=1, N'=J, O'=J, [ L>=1 && 0>=D && E==1 && 0>=M && L>=1 ], cost: 2
     78: f22 -> [14] : D'=0, L'=0, [ D>=1 && 0>=L && C>=F && 1>=0 && 0>=0 ], cost: 2*D
     79: f22 -> [15] : D'=0, L'=0, [ D>=1 && 0>=L && C>=F && 1>=0 && 0>=0 ], cost: 2*D
     80: f22 -> [16] : D'=0, L'=0, [ D>=1 && 0>=L && C>=F && 1>=0 && 0>=0 ], cost: 2*D
     81: f22 -> [17] : D'=0, L'=0, [ D>=1 && 0>=L && C>=F && 1>=0 && 0>=0 ], cost: 2*D
     82: f22 -> [18] : D'=0, L'=0, [ D>=1 && 0>=L && C>=F && 1>=0 && 0>=0 ], cost: 2*D
     52: f41 -> f45 : B'=0, O'=N, P'=1, [ 0>=1+A && N==O && B==0 ], cost: 2
     55: f41 -> f45 : B'=0, O'=N, P'=1, [ A>=1 && N==O && B==0 ], cost: 2
     89: f41 -> f45 : A'=0, O'=N, P'=3, [ A==0 && N==O && B>=1 && 0>=0 && B>=1 ], cost: 3
     90: f41 -> f45 : O'=N, P'=2, [ 0>=1+A && N==O && 0>=1+B && 0>=B && 0>=A ], cost: 3
     91: f41 -> f45 : O'=N, P'=3, [ 0>=1+A && N==O && B>=1 && B>=1 && 0>=A && B>=1 ], cost: 4
     22: f41 -> f58 : Q_1'=free_5, [ free_5>=0 && N>=1+O && 1>=free_5 ], cost: 1
     23: f41 -> f58 : Q_1'=free_6, [ free_6>=0 && O>=1+N && 1>=free_6 ], cost: 1
     59: f58 -> f10 : E'=1+E, G'=1+G, K'=0, Q_1'=1, [ 0>=E && 0>=D && Q_1>=1 && K>=1 && C>=F && Q_1==1 ], cost: 2
     60: f58 -> f10 : E'=1+E, G'=1+G, K'=1, Q_1'=1, [ 0>=E && 0>=D && Q_1>=1 && 0>=K && C>=F && Q_1==1 ], cost: 2
     63: f58 -> f10 : E'=1+E, G'=1+G, K'=1, Q_1'=1, [ 0>=D && Q_1>=1 && E==1 && 0>=K && C>=F && Q_1==1 ], cost: 2
     65: f58 -> f10 : D'=free_9, E'=0, F'=1+F, G'=1+G, K'=0, Q_1'=1, [ E>=2 && 0>=D && free_9>=0 && K>=1 && C>=1+F && Q_1==1 ], cost: 2
     66: f58 -> f10 : D'=free_9, E'=0, F'=1+F, G'=1+G, K'=1, Q_1'=1, [ E>=2 && 0>=D && free_9>=0 && 0>=K && C>=1+F && Q_1==1 ], cost: 2
     61: f58 -> f22 : E'=1+E, L'=free_11, [ 0>=E && 0>=D && Q_1>=1 && C>=F && free_11>=0 && Q_1>=2 && 1>=free_11 ], cost: 2
     64: f58 -> f22 : E'=1+E, L'=free_11, [ 0>=D && Q_1>=1 && E==1 && C>=F && free_11>=0 && Q_1>=2 && 1>=free_11 ], cost: 2
     67: f58 -> f22 : D'=free_9, E'=0, F'=1+F, L'=free_10, [ E>=2 && 0>=D && free_9>=0 && C>=1+F && free_10>=0 && 0>=Q_1 && 1>=free_10 ], cost: 2
     68: f58 -> f22 : D'=free_9, E'=0, F'=1+F, L'=free_11, [ E>=2 && 0>=D && free_9>=0 && C>=1+F && free_11>=0 && Q_1>=2 && 1>=free_11 ], cost: 2
     72: f58 -> f22 : D'=-1+D, L'=free_11, [ D>=1 && C>=F && free_11>=0 && Q_1>=2 && 1>=free_11 ], cost: 2


Applied chaining over branches and pruning:
  Start location: f0
     24: f45 -> f58 : O'=0, Q_1'=free_7, [ free_7>=0 && O>=1 && 1>=free_7 ], cost: 1
     25: f45 -> f58 : O'=1, Q_1'=free_8, [ free_8>=0 && 0>=O && 1>=free_8 ], cost: 1
      2: f0 -> f10 : C'=free, D'=free_1, E'=0, F'=1, G'=0, [ free>=1 && free_1>=0 ], cost: 1
     36: f10 -> f22 : H'=1, Q'=1, J'=K, L'=free_2, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_2 && free_2>=0 ], cost: 2
     37: f10 -> f22 : H'=1, Q'=0, J'=K, L'=free_3, [ C>=1+G && 0>=G && C>=2+G && 1>=free_3 && free_3>=0 ], cost: 2
     38: f10 -> f22 : H'=0, Q'=1, J'=K, L'=free_2, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_2 && free_2>=0 ], cost: 2
     39: f10 -> f22 : H'=0, Q'=0, J'=K, L'=free_3, [ C>=1+G && G>=1 && C>=2+G && 1>=free_3 && free_3>=0 ], cost: 2
     94: f22 -> f45 : A'=H, B'=0, D'=free_4, E'=1, F'=1+F, L'=free_12, M'=1, N'=J, O'=J, P'=1, [ E>=2 && 0>=D && free_4>=0 && 0>=L && C>=1+F && 1>=free_12 && free_12>=0 && free_12>=1 && 0>=free_4 && 0>=0 && M>=1 && free_12>=1 && 0>=1+H && J==O && Q==0 ], cost: 6
     95: f22 -> f45 : A'=H, B'=0, D'=free_4, E'=1, F'=1+F, L'=free_12, M'=1, N'=J, O'=J, P'=1, [ E>=2 && 0>=D && free_4>=0 && 0>=L && C>=1+F && 1>=free_12 && free_12>=0 && free_12>=1 && 0>=free_4 && 0>=0 && M>=1 && free_12>=1 && H>=1 && J==O && Q==0 ], cost: 6
     97: f22 -> f45 : A'=H, B'=Q, D'=free_4, E'=1, F'=1+F, L'=free_12, M'=1, N'=J, O'=J, P'=2, [ E>=2 && 0>=D && free_4>=0 && 0>=L && C>=1+F && 1>=free_12 && free_12>=0 && free_12>=1 && 0>=free_4 && 0>=0 && M>=1 && free_12>=1 && 0>=1+H && J==O && 0>=1+Q && 0>=Q && 0>=H ], cost: 7
    103: f22 -> f45 : A'=0, B'=Q, D'=free_4, E'=1, F'=1+F, L'=free_12, M'=1, N'=J, O'=J, P'=3, [ E>=2 && 0>=D && free_4>=0 && 0>=L && C>=1+F && 1>=free_12 && free_12>=0 && free_12>=1 && 0>=free_4 && 0>=0 && 0>=M && free_12>=1 && H==0 && J==J && Q>=1 && 0>=0 && Q>=1 ], cost: 7
    108: f22 -> f45 : A'=0, B'=Q, E'=1+E, M'=1, N'=J, O'=J, P'=3, [ L>=1 && 0>=D && 0>=E && M>=1 && L>=1 && H==0 && J==O && Q>=1 && 0>=0 && Q>=1 ], cost: 5
     99: f22 -> f58 : A'=H, B'=Q, D'=free_4, E'=1, F'=1+F, L'=free_12, M'=1, N'=J, Q_1'=free_5, [ E>=2 && 0>=D && free_4>=0 && 0>=L && C>=1+F && 1>=free_12 && free_12>=0 && free_12>=1 && 0>=free_4 && 0>=0 && M>=1 && free_12>=1 && free_5>=0 && J>=1+O && 1>=free_5 ], cost: 5
    100: f22 -> f58 : A'=H, B'=Q, D'=free_4, E'=1, F'=1+F, L'=free_12, M'=1, N'=J, Q_1'=free_6, [ E>=2 && 0>=D && free_4>=0 && 0>=L && C>=1+F && 1>=free_12 && free_12>=0 && free_12>=1 && 0>=free_4 && 0>=0 && M>=1 && free_12>=1 && free_6>=0 && O>=1+J && 1>=free_6 ], cost: 5
    111: f22 -> f58 : A'=H, B'=Q, E'=1+E, M'=1, N'=J, Q_1'=free_5, [ L>=1 && 0>=D && 0>=E && M>=1 && L>=1 && free_5>=0 && J>=1+O && 1>=free_5 ], cost: 3
    112: f22 -> f58 : A'=H, B'=Q, E'=1+E, M'=1, N'=J, Q_1'=free_6, [ L>=1 && 0>=D && 0>=E && M>=1 && L>=1 && free_6>=0 && O>=1+J && 1>=free_6 ], cost: 3
     78: f22 -> [14] : D'=0, L'=0, [ D>=1 && 0>=L && C>=F && 1>=0 && 0>=0 ], cost: 2*D
     79: f22 -> [15] : D'=0, L'=0, [ D>=1 && 0>=L && C>=F && 1>=0 && 0>=0 ], cost: 2*D
     80: f22 -> [16] : D'=0, L'=0, [ D>=1 && 0>=L && C>=F && 1>=0 && 0>=0 ], cost: 2*D
     81: f22 -> [17] : D'=0, L'=0, [ D>=1 && 0>=L && C>=F && 1>=0 && 0>=0 ], cost: 2*D
     82: f22 -> [18] : D'=0, L'=0, [ D>=1 && 0>=L && C>=F && 1>=0 && 0>=0 ], cost: 2*D
     59: f58 -> f10 : E'=1+E, G'=1+G, K'=0, Q_1'=1, [ 0>=E && 0>=D && Q_1>=1 && K>=1 && C>=F && Q_1==1 ], cost: 2
     60: f58 -> f10 : E'=1+E, G'=1+G, K'=1, Q_1'=1, [ 0>=E && 0>=D && Q_1>=1 && 0>=K && C>=F && Q_1==1 ], cost: 2
     63: f58 -> f10 : E'=1+E, G'=1+G, K'=1, Q_1'=1, [ 0>=D && Q_1>=1 && E==1 && 0>=K && C>=F && Q_1==1 ], cost: 2
     65: f58 -> f10 : D'=free_9, E'=0, F'=1+F, G'=1+G, K'=0, Q_1'=1, [ E>=2 && 0>=D && free_9>=0 && K>=1 && C>=1+F && Q_1==1 ], cost: 2
     66: f58 -> f10 : D'=free_9, E'=0, F'=1+F, G'=1+G, K'=1, Q_1'=1, [ E>=2 && 0>=D && free_9>=0 && 0>=K && C>=1+F && Q_1==1 ], cost: 2
     61: f58 -> f22 : E'=1+E, L'=free_11, [ 0>=E && 0>=D && Q_1>=1 && C>=F && free_11>=0 && Q_1>=2 && 1>=free_11 ], cost: 2
     64: f58 -> f22 : E'=1+E, L'=free_11, [ 0>=D && Q_1>=1 && E==1 && C>=F && free_11>=0 && Q_1>=2 && 1>=free_11 ], cost: 2
     67: f58 -> f22 : D'=free_9, E'=0, F'=1+F, L'=free_10, [ E>=2 && 0>=D && free_9>=0 && C>=1+F && free_10>=0 && 0>=Q_1 && 1>=free_10 ], cost: 2
     68: f58 -> f22 : D'=free_9, E'=0, F'=1+F, L'=free_11, [ E>=2 && 0>=D && free_9>=0 && C>=1+F && free_11>=0 && Q_1>=2 && 1>=free_11 ], cost: 2
     72: f58 -> f22 : D'=-1+D, L'=free_11, [ D>=1 && C>=F && free_11>=0 && Q_1>=2 && 1>=free_11 ], cost: 2


Applied chaining over branches and pruning:
  Start location: f0
      2: f0 -> f10 : C'=free, D'=free_1, E'=0, F'=1, G'=0, [ free>=1 && free_1>=0 ], cost: 1
     36: f10 -> f22 : H'=1, Q'=1, J'=K, L'=free_2, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_2 && free_2>=0 ], cost: 2
     37: f10 -> f22 : H'=1, Q'=0, J'=K, L'=free_3, [ C>=1+G && 0>=G && C>=2+G && 1>=free_3 && free_3>=0 ], cost: 2
     38: f10 -> f22 : H'=0, Q'=1, J'=K, L'=free_2, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_2 && free_2>=0 ], cost: 2
     39: f10 -> f22 : H'=0, Q'=0, J'=K, L'=free_3, [ C>=1+G && G>=1 && C>=2+G && 1>=free_3 && free_3>=0 ], cost: 2
     99: f22 -> f58 : A'=H, B'=Q, D'=free_4, E'=1, F'=1+F, L'=free_12, M'=1, N'=J, Q_1'=free_5, [ E>=2 && 0>=D && free_4>=0 && 0>=L && C>=1+F && 1>=free_12 && free_12>=0 && free_12>=1 && 0>=free_4 && 0>=0 && M>=1 && free_12>=1 && free_5>=0 && J>=1+O && 1>=free_5 ], cost: 5
    100: f22 -> f58 : A'=H, B'=Q, D'=free_4, E'=1, F'=1+F, L'=free_12, M'=1, N'=J, Q_1'=free_6, [ E>=2 && 0>=D && free_4>=0 && 0>=L && C>=1+F && 1>=free_12 && free_12>=0 && free_12>=1 && 0>=free_4 && 0>=0 && M>=1 && free_12>=1 && free_6>=0 && O>=1+J && 1>=free_6 ], cost: 5
    112: f22 -> f58 : A'=H, B'=Q, E'=1+E, M'=1, N'=J, Q_1'=free_6, [ L>=1 && 0>=D && 0>=E && M>=1 && L>=1 && free_6>=0 && O>=1+J && 1>=free_6 ], cost: 3
    125: f22 -> f58 : A'=H, B'=0, D'=free_4, E'=1, F'=1+F, L'=free_12, M'=1, N'=J, O'=0, P'=1, Q_1'=free_7, [ E>=2 && 0>=D && free_4>=0 && 0>=L && C>=1+F && 1>=free_12 && free_12>=0 && free_12>=1 && 0>=free_4 && 0>=0 && M>=1 && free_12>=1 && H>=1 && J==O && Q==0 && free_7>=0 && J>=1 && 1>=free_7 ], cost: 7
    126: f22 -> f58 : A'=H, B'=0, D'=free_4, E'=1, F'=1+F, L'=free_12, M'=1, N'=J, O'=1, P'=1, Q_1'=free_8, [ E>=2 && 0>=D && free_4>=0 && 0>=L && C>=1+F && 1>=free_12 && free_12>=0 && free_12>=1 && 0>=free_4 && 0>=0 && M>=1 && free_12>=1 && H>=1 && J==O && Q==0 && free_8>=0 && 0>=J && 1>=free_8 ], cost: 7
     78: f22 -> [14] : D'=0, L'=0, [ D>=1 && 0>=L && C>=F && 1>=0 && 0>=0 ], cost: 2*D
     79: f22 -> [15] : D'=0, L'=0, [ D>=1 && 0>=L && C>=F && 1>=0 && 0>=0 ], cost: 2*D
     80: f22 -> [16] : D'=0, L'=0, [ D>=1 && 0>=L && C>=F && 1>=0 && 0>=0 ], cost: 2*D
     81: f22 -> [17] : D'=0, L'=0, [ D>=1 && 0>=L && C>=F && 1>=0 && 0>=0 ], cost: 2*D
     82: f22 -> [18] : D'=0, L'=0, [ D>=1 && 0>=L && C>=F && 1>=0 && 0>=0 ], cost: 2*D
     59: f58 -> f10 : E'=1+E, G'=1+G, K'=0, Q_1'=1, [ 0>=E && 0>=D && Q_1>=1 && K>=1 && C>=F && Q_1==1 ], cost: 2
     60: f58 -> f10 : E'=1+E, G'=1+G, K'=1, Q_1'=1, [ 0>=E && 0>=D && Q_1>=1 && 0>=K && C>=F && Q_1==1 ], cost: 2
     63: f58 -> f10 : E'=1+E, G'=1+G, K'=1, Q_1'=1, [ 0>=D && Q_1>=1 && E==1 && 0>=K && C>=F && Q_1==1 ], cost: 2
     65: f58 -> f10 : D'=free_9, E'=0, F'=1+F, G'=1+G, K'=0, Q_1'=1, [ E>=2 && 0>=D && free_9>=0 && K>=1 && C>=1+F && Q_1==1 ], cost: 2
     66: f58 -> f10 : D'=free_9, E'=0, F'=1+F, G'=1+G, K'=1, Q_1'=1, [ E>=2 && 0>=D && free_9>=0 && 0>=K && C>=1+F && Q_1==1 ], cost: 2
     61: f58 -> f22 : E'=1+E, L'=free_11, [ 0>=E && 0>=D && Q_1>=1 && C>=F && free_11>=0 && Q_1>=2 && 1>=free_11 ], cost: 2
     64: f58 -> f22 : E'=1+E, L'=free_11, [ 0>=D && Q_1>=1 && E==1 && C>=F && free_11>=0 && Q_1>=2 && 1>=free_11 ], cost: 2
     67: f58 -> f22 : D'=free_9, E'=0, F'=1+F, L'=free_10, [ E>=2 && 0>=D && free_9>=0 && C>=1+F && free_10>=0 && 0>=Q_1 && 1>=free_10 ], cost: 2
     68: f58 -> f22 : D'=free_9, E'=0, F'=1+F, L'=free_11, [ E>=2 && 0>=D && free_9>=0 && C>=1+F && free_11>=0 && Q_1>=2 && 1>=free_11 ], cost: 2
     72: f58 -> f22 : D'=-1+D, L'=free_11, [ D>=1 && C>=F && free_11>=0 && Q_1>=2 && 1>=free_11 ], cost: 2


Applied chaining over branches and pruning:
  Start location: f0
      2: f0 -> f10 : C'=free, D'=free_1, E'=0, F'=1, G'=0, [ free>=1 && free_1>=0 ], cost: 1
     36: f10 -> f22 : H'=1, Q'=1, J'=K, L'=free_2, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_2 && free_2>=0 ], cost: 2
     37: f10 -> f22 : H'=1, Q'=0, J'=K, L'=free_3, [ C>=1+G && 0>=G && C>=2+G && 1>=free_3 && free_3>=0 ], cost: 2
     38: f10 -> f22 : H'=0, Q'=1, J'=K, L'=free_2, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_2 && free_2>=0 ], cost: 2
     39: f10 -> f22 : H'=0, Q'=0, J'=K, L'=free_3, [ C>=1+G && G>=1 && C>=2+G && 1>=free_3 && free_3>=0 ], cost: 2
    133: f22 -> f10 : A'=H, B'=Q, D'=free_4, E'=2, F'=1+F, G'=1+G, K'=1, L'=free_12, M'=1, N'=J, Q_1'=1, [ E>=2 && 0>=D && free_4>=0 && 0>=L && C>=1+F && 1>=free_12 && free_12>=0 && free_12>=1 && 0>=free_4 && 0>=0 && M>=1 && free_12>=1 && free_5>=0 && J>=1+O && 1>=free_5 && 0>=free_4 && free_5>=1 && 1==1 && 0>=K && C>=1+F && free_5==1 ], cost: 7
    134: f22 -> f10 : A'=H, B'=Q, D'=free_4, E'=2, F'=1+F, G'=1+G, K'=1, L'=free_12, M'=1, N'=J, Q_1'=1, [ E>=2 && 0>=D && free_4>=0 && 0>=L && C>=1+F && 1>=free_12 && free_12>=0 && free_12>=1 && 0>=free_4 && 0>=0 && M>=1 && free_12>=1 && free_6>=0 && O>=1+J && 1>=free_6 && 0>=free_4 && free_6>=1 && 1==1 && 0>=K && C>=1+F && free_6==1 ], cost: 7
    135: f22 -> f10 : A'=H, B'=Q, E'=2+E, G'=1+G, K'=0, M'=1, N'=J, Q_1'=1, [ L>=1 && 0>=D && 0>=E && M>=1 && L>=1 && free_6>=0 && O>=1+J && 1>=free_6 && 0>=1+E && 0>=D && free_6>=1 && K>=1 && C>=F && free_6==1 ], cost: 5
    136: f22 -> f10 : A'=H, B'=Q, E'=2+E, G'=1+G, K'=1, M'=1, N'=J, Q_1'=1, [ L>=1 && 0>=D && 0>=E && M>=1 && L>=1 && free_6>=0 && O>=1+J && 1>=free_6 && 0>=1+E && 0>=D && free_6>=1 && 0>=K && C>=F && free_6==1 ], cost: 5
    137: f22 -> f10 : A'=H, B'=Q, E'=2+E, G'=1+G, K'=1, M'=1, N'=J, Q_1'=1, [ L>=1 && 0>=D && 0>=E && M>=1 && L>=1 && free_6>=0 && O>=1+J && 1>=free_6 && 0>=D && free_6>=1 && 1+E==1 && 0>=K && C>=F && free_6==1 ], cost: 5
     78: f22 -> [14] : D'=0, L'=0, [ D>=1 && 0>=L && C>=F && 1>=0 && 0>=0 ], cost: 2*D
     79: f22 -> [15] : D'=0, L'=0, [ D>=1 && 0>=L && C>=F && 1>=0 && 0>=0 ], cost: 2*D
     80: f22 -> [16] : D'=0, L'=0, [ D>=1 && 0>=L && C>=F && 1>=0 && 0>=0 ], cost: 2*D
     81: f22 -> [17] : D'=0, L'=0, [ D>=1 && 0>=L && C>=F && 1>=0 && 0>=0 ], cost: 2*D
     82: f22 -> [18] : D'=0, L'=0, [ D>=1 && 0>=L && C>=F && 1>=0 && 0>=0 ], cost: 2*D


Applied chaining over branches and pruning:
  Start location: f0
      2: f0 -> f10 : C'=free, D'=free_1, E'=0, F'=1, G'=0, [ free>=1 && free_1>=0 ], cost: 1
    140: f10 -> f10 : A'=1, B'=1, D'=free_4, E'=2, F'=1+F, G'=1+G, H'=1, Q'=1, J'=K, K'=1, L'=free_12, M'=1, N'=K, Q_1'=1, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_2 && free_2>=0 && E>=2 && 0>=D && free_4>=0 && 0>=free_2 && C>=1+F && 1>=free_12 && free_12>=0 && free_12>=1 && 0>=free_4 && 0>=0 && M>=1 && free_12>=1 && free_5>=0 && K>=1+O && 1>=free_5 && 0>=free_4 && free_5>=1 && 1==1 && 0>=K && C>=1+F && free_5==1 ], cost: 9
    141: f10 -> f10 : A'=1, B'=1, D'=free_4, E'=2, F'=1+F, G'=1+G, H'=1, Q'=1, J'=K, K'=1, L'=free_12, M'=1, N'=K, Q_1'=1, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_2 && free_2>=0 && E>=2 && 0>=D && free_4>=0 && 0>=free_2 && C>=1+F && 1>=free_12 && free_12>=0 && free_12>=1 && 0>=free_4 && 0>=0 && M>=1 && free_12>=1 && free_6>=0 && O>=1+K && 1>=free_6 && 0>=free_4 && free_6>=1 && 1==1 && 0>=K && C>=1+F && free_6==1 ], cost: 9
    143: f10 -> f10 : A'=1, B'=1, E'=2+E, G'=1+G, H'=1, Q'=1, J'=K, K'=1, L'=free_2, M'=1, N'=K, Q_1'=1, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_2 && free_2>=0 && free_2>=1 && 0>=D && 0>=E && M>=1 && free_2>=1 && free_6>=0 && O>=1+K && 1>=free_6 && 0>=1+E && 0>=D && free_6>=1 && 0>=K && C>=F && free_6==1 ], cost: 7
    152: f10 -> f10 : A'=1, B'=0, E'=2+E, G'=1+G, H'=1, Q'=0, J'=K, K'=0, L'=free_3, M'=1, N'=K, Q_1'=1, [ C>=1+G && 0>=G && C>=2+G && 1>=free_3 && free_3>=0 && free_3>=1 && 0>=D && 0>=E && M>=1 && free_3>=1 && free_6>=0 && O>=1+K && 1>=free_6 && 0>=1+E && 0>=D && free_6>=1 && K>=1 && C>=F && free_6==1 ], cost: 7
    160: f10 -> f10 : A'=0, B'=1, D'=free_4, E'=2, F'=1+F, G'=1+G, H'=0, Q'=1, J'=K, K'=1, L'=free_12, M'=1, N'=K, Q_1'=1, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_2 && free_2>=0 && E>=2 && 0>=D && free_4>=0 && 0>=free_2 && C>=1+F && 1>=free_12 && free_12>=0 && free_12>=1 && 0>=free_4 && 0>=0 && M>=1 && free_12>=1 && free_5>=0 && K>=1+O && 1>=free_5 && 0>=free_4 && free_5>=1 && 1==1 && 0>=K && C>=1+F && free_5==1 ], cost: 9
    145: f10 -> [14] : D'=0, H'=1, Q'=1, J'=K, L'=0, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    155: f10 -> [14] : D'=0, H'=1, Q'=0, J'=K, L'=0, [ C>=1+G && 0>=G && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    165: f10 -> [14] : D'=0, H'=0, Q'=1, J'=K, L'=0, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    175: f10 -> [14] : D'=0, H'=0, Q'=0, J'=K, L'=0, [ C>=1+G && G>=1 && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    146: f10 -> [15] : D'=0, H'=1, Q'=1, J'=K, L'=0, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    156: f10 -> [15] : D'=0, H'=1, Q'=0, J'=K, L'=0, [ C>=1+G && 0>=G && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    166: f10 -> [15] : D'=0, H'=0, Q'=1, J'=K, L'=0, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    176: f10 -> [15] : D'=0, H'=0, Q'=0, J'=K, L'=0, [ C>=1+G && G>=1 && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    147: f10 -> [16] : D'=0, H'=1, Q'=1, J'=K, L'=0, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    157: f10 -> [16] : D'=0, H'=1, Q'=0, J'=K, L'=0, [ C>=1+G && 0>=G && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    167: f10 -> [16] : D'=0, H'=0, Q'=1, J'=K, L'=0, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    177: f10 -> [16] : D'=0, H'=0, Q'=0, J'=K, L'=0, [ C>=1+G && G>=1 && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    148: f10 -> [17] : D'=0, H'=1, Q'=1, J'=K, L'=0, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    158: f10 -> [17] : D'=0, H'=1, Q'=0, J'=K, L'=0, [ C>=1+G && 0>=G && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    168: f10 -> [17] : D'=0, H'=0, Q'=1, J'=K, L'=0, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    178: f10 -> [17] : D'=0, H'=0, Q'=0, J'=K, L'=0, [ C>=1+G && G>=1 && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    149: f10 -> [18] : D'=0, H'=1, Q'=1, J'=K, L'=0, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    159: f10 -> [18] : D'=0, H'=1, Q'=0, J'=K, L'=0, [ C>=1+G && 0>=G && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    169: f10 -> [18] : D'=0, H'=0, Q'=1, J'=K, L'=0, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    179: f10 -> [18] : D'=0, H'=0, Q'=0, J'=K, L'=0, [ C>=1+G && G>=1 && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D

Eliminating 5 self-loops for location f10
  Self-Loop 140 has the metering function: -1+C-G, resulting in the new transition 180.
  Self-Loop 141 has the metering function: -1+C-G, resulting in the new transition 181.
  Self-Loop 143 has the metering function: -1+C-G, resulting in the new transition 182.
  Self-Loop 160 has the metering function: -1+C-G, resulting in the new transition 186.
  Found this metering function when nesting loops: -2+C-G,
  Removing the self-loops: 140 141 143 152 160 183 184.
Adding an epsilon transition (to model nonexecution of the loops): 187.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      2: f0 -> f10 : C'=free, D'=free_1, E'=0, F'=1, G'=0, [ free>=1 && free_1>=0 ], cost: 1
    180: f10 -> [19] : A'=1, B'=1, D'=0, E'=2, F'=-1+F+C-G, G'=-1+C, H'=1, Q'=1, J'=1, K'=1, L'=1, M'=1, N'=1, Q_1'=1, [ 1-C+G==0 && 0>=G && E>=2 && 0>=D && C>=1+F && M>=1 && K>=1+O && 0>=K ], cost: -9+9*C-9*G
    181: f10 -> [19] : A'=1, B'=1, D'=0, E'=2, F'=-1+F+C-G, G'=-1+C, H'=1, Q'=1, J'=1, K'=1, L'=1, M'=1, N'=1, Q_1'=1, [ 1-C+G==0 && 0>=G && E>=2 && 0>=D && C>=1+F && M>=1 && O>=1+K && 0>=K ], cost: -9+9*C-9*G
    182: f10 -> [19] : A'=1, B'=1, E'=-2+E+2*C-2*G, G'=-1+C, H'=1, Q'=1, J'=1, K'=1, L'=1, M'=1, N'=1, Q_1'=1, [ 1-C+G==0 && 0>=G && 0>=D && M>=1 && O>=1+K && 0>=1+E && 0>=K && C>=F ], cost: -7+7*C-7*G
    185: f10 -> [19] : A'=1, B'=0, E'=2+E, G'=1+G, H'=1, Q'=0, J'=K, K'=0, L'=1, M'=1, N'=K, Q_1'=1, [ 0>=G && C>=2+G && 0>=D && M>=1 && O>=1+K && 0>=1+E && K>=1 && C>=F ], cost: 7
    186: f10 -> [19] : A'=0, B'=1, D'=0, E'=2, F'=-1+F+C-G, G'=-1+C, H'=0, Q'=1, J'=1, K'=1, L'=1, M'=1, N'=1, Q_1'=1, [ 1-C+G==0 && G>=1 && E>=2 && 0>=D && C>=1+F && M>=1 && K>=1+O && 0>=K ], cost: -9+9*C-9*G
    187: f10 -> [19] : [], cost: 0
    145: [19] -> [14] : D'=0, H'=1, Q'=1, J'=K, L'=0, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    155: [19] -> [14] : D'=0, H'=1, Q'=0, J'=K, L'=0, [ C>=1+G && 0>=G && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    165: [19] -> [14] : D'=0, H'=0, Q'=1, J'=K, L'=0, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    175: [19] -> [14] : D'=0, H'=0, Q'=0, J'=K, L'=0, [ C>=1+G && G>=1 && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    146: [19] -> [15] : D'=0, H'=1, Q'=1, J'=K, L'=0, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    156: [19] -> [15] : D'=0, H'=1, Q'=0, J'=K, L'=0, [ C>=1+G && 0>=G && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    166: [19] -> [15] : D'=0, H'=0, Q'=1, J'=K, L'=0, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    176: [19] -> [15] : D'=0, H'=0, Q'=0, J'=K, L'=0, [ C>=1+G && G>=1 && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    147: [19] -> [16] : D'=0, H'=1, Q'=1, J'=K, L'=0, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    157: [19] -> [16] : D'=0, H'=1, Q'=0, J'=K, L'=0, [ C>=1+G && 0>=G && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    167: [19] -> [16] : D'=0, H'=0, Q'=1, J'=K, L'=0, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    177: [19] -> [16] : D'=0, H'=0, Q'=0, J'=K, L'=0, [ C>=1+G && G>=1 && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    148: [19] -> [17] : D'=0, H'=1, Q'=1, J'=K, L'=0, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    158: [19] -> [17] : D'=0, H'=1, Q'=0, J'=K, L'=0, [ C>=1+G && 0>=G && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    168: [19] -> [17] : D'=0, H'=0, Q'=1, J'=K, L'=0, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    178: [19] -> [17] : D'=0, H'=0, Q'=0, J'=K, L'=0, [ C>=1+G && G>=1 && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    149: [19] -> [18] : D'=0, H'=1, Q'=1, J'=K, L'=0, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    159: [19] -> [18] : D'=0, H'=1, Q'=0, J'=K, L'=0, [ C>=1+G && 0>=G && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    169: [19] -> [18] : D'=0, H'=0, Q'=1, J'=K, L'=0, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    179: [19] -> [18] : D'=0, H'=0, Q'=0, J'=K, L'=0, [ C>=1+G && G>=1 && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D


Applied chaining over branches and pruning:
  Start location: f0
    188: f0 -> [19] : C'=free, D'=free_1, E'=0, F'=1, G'=0, [ free>=1 && free_1>=0 ], cost: 1
    145: [19] -> [14] : D'=0, H'=1, Q'=1, J'=K, L'=0, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    155: [19] -> [14] : D'=0, H'=1, Q'=0, J'=K, L'=0, [ C>=1+G && 0>=G && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    165: [19] -> [14] : D'=0, H'=0, Q'=1, J'=K, L'=0, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    175: [19] -> [14] : D'=0, H'=0, Q'=0, J'=K, L'=0, [ C>=1+G && G>=1 && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    146: [19] -> [15] : D'=0, H'=1, Q'=1, J'=K, L'=0, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    156: [19] -> [15] : D'=0, H'=1, Q'=0, J'=K, L'=0, [ C>=1+G && 0>=G && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    166: [19] -> [15] : D'=0, H'=0, Q'=1, J'=K, L'=0, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    176: [19] -> [15] : D'=0, H'=0, Q'=0, J'=K, L'=0, [ C>=1+G && G>=1 && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    147: [19] -> [16] : D'=0, H'=1, Q'=1, J'=K, L'=0, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    157: [19] -> [16] : D'=0, H'=1, Q'=0, J'=K, L'=0, [ C>=1+G && 0>=G && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    167: [19] -> [16] : D'=0, H'=0, Q'=1, J'=K, L'=0, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    177: [19] -> [16] : D'=0, H'=0, Q'=0, J'=K, L'=0, [ C>=1+G && G>=1 && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    148: [19] -> [17] : D'=0, H'=1, Q'=1, J'=K, L'=0, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    158: [19] -> [17] : D'=0, H'=1, Q'=0, J'=K, L'=0, [ C>=1+G && 0>=G && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    168: [19] -> [17] : D'=0, H'=0, Q'=1, J'=K, L'=0, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    178: [19] -> [17] : D'=0, H'=0, Q'=0, J'=K, L'=0, [ C>=1+G && G>=1 && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    149: [19] -> [18] : D'=0, H'=1, Q'=1, J'=K, L'=0, [ C>=1+G && 0>=G && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    159: [19] -> [18] : D'=0, H'=1, Q'=0, J'=K, L'=0, [ C>=1+G && 0>=G && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    169: [19] -> [18] : D'=0, H'=0, Q'=1, J'=K, L'=0, [ C>=1+G && G>=1 && 1+G>=C && 1>=free_2 && free_2>=0 && D>=1 && 0>=free_2 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D
    179: [19] -> [18] : D'=0, H'=0, Q'=0, J'=K, L'=0, [ C>=1+G && G>=1 && C>=2+G && 1>=free_3 && free_3>=0 && D>=1 && 0>=free_3 && C>=F && 1>=0 && 0>=0 ], cost: 2+2*D


Applied chaining over branches and pruning:
  Start location: f0
    189: f0 -> [14] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, Q'=1, J'=K, L'=0, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && 1>=free && 1>=free_2 && free_2>=0 && free_1>=1 && 0>=free_2 && free>=1 && 1>=0 && 0>=0 ], cost: 3+2*free_1
    190: f0 -> [14] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, Q'=0, J'=K, L'=0, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && free>=2 && 1>=free_3 && free_3>=0 && free_1>=1 && 0>=free_3 && free>=1 && 1>=0 && 0>=0 ], cost: 3+2*free_1
    191: f0 -> [15] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, Q'=1, J'=K, L'=0, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && 1>=free && 1>=free_2 && free_2>=0 && free_1>=1 && 0>=free_2 && free>=1 && 1>=0 && 0>=0 ], cost: 3+2*free_1
    192: f0 -> [15] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, Q'=0, J'=K, L'=0, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && free>=2 && 1>=free_3 && free_3>=0 && free_1>=1 && 0>=free_3 && free>=1 && 1>=0 && 0>=0 ], cost: 3+2*free_1
    193: f0 -> [16] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, Q'=1, J'=K, L'=0, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && 1>=free && 1>=free_2 && free_2>=0 && free_1>=1 && 0>=free_2 && free>=1 && 1>=0 && 0>=0 ], cost: 3+2*free_1
    194: f0 -> [16] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, Q'=0, J'=K, L'=0, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && free>=2 && 1>=free_3 && free_3>=0 && free_1>=1 && 0>=free_3 && free>=1 && 1>=0 && 0>=0 ], cost: 3+2*free_1
    195: f0 -> [17] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, Q'=1, J'=K, L'=0, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && 1>=free && 1>=free_2 && free_2>=0 && free_1>=1 && 0>=free_2 && free>=1 && 1>=0 && 0>=0 ], cost: 3+2*free_1
    196: f0 -> [17] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, Q'=0, J'=K, L'=0, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && free>=2 && 1>=free_3 && free_3>=0 && free_1>=1 && 0>=free_3 && free>=1 && 1>=0 && 0>=0 ], cost: 3+2*free_1
    197: f0 -> [18] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, Q'=1, J'=K, L'=0, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && 1>=free && 1>=free_2 && free_2>=0 && free_1>=1 && 0>=free_2 && free>=1 && 1>=0 && 0>=0 ], cost: 3+2*free_1
    198: f0 -> [18] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, Q'=0, J'=K, L'=0, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && free>=2 && 1>=free_3 && free_3>=0 && free_1>=1 && 0>=free_3 && free>=1 && 1>=0 && 0>=0 ], cost: 3+2*free_1


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
    189: f0 -> [14] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, Q'=1, J'=K, L'=0, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && 1>=free && 1>=free_2 && free_2>=0 && free_1>=1 && 0>=free_2 && free>=1 && 1>=0 && 0>=0 ], cost: 3+2*free_1
    190: f0 -> [14] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, Q'=0, J'=K, L'=0, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && free>=2 && 1>=free_3 && free_3>=0 && free_1>=1 && 0>=free_3 && free>=1 && 1>=0 && 0>=0 ], cost: 3+2*free_1
    191: f0 -> [15] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, Q'=1, J'=K, L'=0, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && 1>=free && 1>=free_2 && free_2>=0 && free_1>=1 && 0>=free_2 && free>=1 && 1>=0 && 0>=0 ], cost: 3+2*free_1
    192: f0 -> [15] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, Q'=0, J'=K, L'=0, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && free>=2 && 1>=free_3 && free_3>=0 && free_1>=1 && 0>=free_3 && free>=1 && 1>=0 && 0>=0 ], cost: 3+2*free_1
    193: f0 -> [16] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, Q'=1, J'=K, L'=0, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && 1>=free && 1>=free_2 && free_2>=0 && free_1>=1 && 0>=free_2 && free>=1 && 1>=0 && 0>=0 ], cost: 3+2*free_1
    194: f0 -> [16] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, Q'=0, J'=K, L'=0, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && free>=2 && 1>=free_3 && free_3>=0 && free_1>=1 && 0>=free_3 && free>=1 && 1>=0 && 0>=0 ], cost: 3+2*free_1
    195: f0 -> [17] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, Q'=1, J'=K, L'=0, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && 1>=free && 1>=free_2 && free_2>=0 && free_1>=1 && 0>=free_2 && free>=1 && 1>=0 && 0>=0 ], cost: 3+2*free_1
    196: f0 -> [17] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, Q'=0, J'=K, L'=0, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && free>=2 && 1>=free_3 && free_3>=0 && free_1>=1 && 0>=free_3 && free>=1 && 1>=0 && 0>=0 ], cost: 3+2*free_1
    197: f0 -> [18] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, Q'=1, J'=K, L'=0, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && 1>=free && 1>=free_2 && free_2>=0 && free_1>=1 && 0>=free_2 && free>=1 && 1>=0 && 0>=0 ], cost: 3+2*free_1
    198: f0 -> [18] : C'=free, D'=0, E'=0, F'=1, G'=0, H'=1, Q'=0, J'=K, L'=0, [ free>=1 && free_1>=0 && free>=1 && 0>=0 && free>=2 && 1>=free_3 && free_3>=0 && free_1>=1 && 0>=free_3 && free>=1 && 1>=0 && 0>=0 ], cost: 3+2*free_1


Computing complexity for remaining 10 transitions.


The final runtime is determined by this resulting transition:
  Final Guard: 
  Final Cost:  1

Obtained the following complexity w.r.t. the length of the input n:
  Complexity class: const
  Complexity value: 0

WORST_CASE(Omega(1),?)