Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f0 -> f23 : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, [], cost: 1
      1: f23 -> f23 : J'=1+J, K'=1, L'=0, M'=0, [ C>=J ], cost: 1
      2: f23 -> f23 : A'=free_1+A, J'=1+J, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && C>=J ], cost: 1
      3: f23 -> f23 : A'=free_3+A, J'=1+J, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && C>=J ], cost: 1
     46: f23 -> f33 : [ J>=1+C ], cost: 1
      4: f33 -> f33 : J'=1+J, [ D>=J ], cost: 1
     43: f33 -> f39 : [ 0>=1+P && J>=1+D ], cost: 1
     44: f33 -> f39 : [ P>=1 && J>=1+D ], cost: 1
     45: f33 -> f44 : P'=0, [ J>=1+D && P==0 ], cost: 1
      5: f39 -> f39 : J'=1+J, [ D>=J ], cost: 1
     42: f39 -> f44 : [ J>=1+D ], cost: 1
      6: f44 -> f46 : [ N>=O ], cost: 1
     41: f44 -> f117 : B'=free_34, [ O>=1+N ], cost: 1
      7: f46 -> f49 : [ 0>=1+P && 0>=Q_1 ], cost: 1
      8: f46 -> f49 : [ P>=1 && 0>=Q_1 ], cost: 1
     12: f46 -> f66 : P'=0, [ 0>=Q_1 && P==0 ], cost: 1
     40: f46 -> f72 : [ Q_1>=1 ], cost: 1
      9: f49 -> f49 : J'=1+J, [ D>=J ], cost: 1
     39: f49 -> f54 : [ J>=1+D ], cost: 1
     10: f54 -> f54 : J'=1+J, [ D>=J ], cost: 1
     38: f54 -> f60 : A1'=Q_1+C, [ J>=1+D ], cost: 1
     37: f60 -> f46 : Q_1'=1+Q_1, [ J>=1+D ], cost: 1
     11: f60 -> f60 : J'=1+J, [ D>=J ], cost: 1
     36: f66 -> f46 : Q_1'=1+Q_1, [ J>=1+E ], cost: 1
     13: f66 -> f66 : J'=2+J, [ E>=J ], cost: 1
     14: f72 -> f72 : J'=1+J, R'=2*J, S'=free_5, T'=1-free_5, [ C>=J ], cost: 1
     33: f72 -> f87 : L'=free_27, Z'=0, [ J>=1+C ], cost: 1
     34: f72 -> f87 : L'=free_28, Z'=free_29, [ 0>=1+free_30 && J>=1+C ], cost: 1
     35: f72 -> f87 : L'=free_31, Z'=free_32, [ free_33>=1 && J>=1+C ], cost: 1
     15: f87 -> f91 : L'=0, U'=0, [ L==0 ], cost: 1
     16: f87 -> f91 : U'=free_6, [ 0>=1+L ], cost: 1
     17: f87 -> f91 : U'=free_7, [ L>=1 ], cost: 1
     32: f91 -> f44 : B'=B+A, O'=1+O, [ J>=1+D ], cost: 1
     18: f91 -> f99 : L'=free_8, R'=2*J, V'=0, [ D>=J ], cost: 1
     19: f91 -> f99 : L'=free_9, R'=2*J, V'=free_10, [ 0>=1+free_11 && D>=J ], cost: 1
     20: f91 -> f99 : L'=free_12, R'=2*J, V'=free_13, [ free_14>=1 && D>=J ], cost: 1
     21: f99 -> f103 : L'=free_15, W'=0, [ L==0 ], cost: 1
     22: f99 -> f103 : L'=free_16, W'=free_17, [ 0>=1+L ], cost: 1
     23: f99 -> f103 : L'=free_18, W'=free_19, [ L>=1 ], cost: 1
     24: f103 -> f107 : L'=free_20, X'=0, [ L==0 ], cost: 1
     25: f103 -> f107 : L'=free_21, X'=free_22, [ 0>=1+L ], cost: 1
     26: f103 -> f107 : L'=free_23, X'=free_24, [ L>=1 ], cost: 1
     27: f107 -> f91 : J'=1+J, L'=0, Y'=0, [ L==0 ], cost: 1
     28: f107 -> f91 : J'=1+J, Y'=free_25, [ 0>=1+L ], cost: 1
     29: f107 -> f91 : J'=1+J, Y'=free_26, [ L>=1 ], cost: 1
     30: f117 -> f117 : J'=1+J, [ D>=J ], cost: 1
     31: f117 -> f125 : [ J>=1+D ], cost: 1


Simplified the transitions:
  Start location: f0
      0: f0 -> f23 : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, [], cost: 1
      1: f23 -> f23 : J'=1+J, K'=1, L'=0, M'=0, [ C>=J ], cost: 1
      2: f23 -> f23 : A'=free_1+A, J'=1+J, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && C>=J ], cost: 1
      3: f23 -> f23 : A'=free_3+A, J'=1+J, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && C>=J ], cost: 1
     46: f23 -> f33 : [ J>=1+C ], cost: 1
      4: f33 -> f33 : J'=1+J, [ D>=J ], cost: 1
     43: f33 -> f39 : [ 0>=1+P && J>=1+D ], cost: 1
     44: f33 -> f39 : [ P>=1 && J>=1+D ], cost: 1
     45: f33 -> f44 : P'=0, [ J>=1+D && P==0 ], cost: 1
      5: f39 -> f39 : J'=1+J, [ D>=J ], cost: 1
     42: f39 -> f44 : [ J>=1+D ], cost: 1
      6: f44 -> f46 : [ N>=O ], cost: 1
     41: f44 -> f117 : B'=free_34, [ O>=1+N ], cost: 1
      7: f46 -> f49 : [ 0>=1+P && 0>=Q_1 ], cost: 1
      8: f46 -> f49 : [ P>=1 && 0>=Q_1 ], cost: 1
     12: f46 -> f66 : P'=0, [ 0>=Q_1 && P==0 ], cost: 1
     40: f46 -> f72 : [ Q_1>=1 ], cost: 1
      9: f49 -> f49 : J'=1+J, [ D>=J ], cost: 1
     39: f49 -> f54 : [ J>=1+D ], cost: 1
     10: f54 -> f54 : J'=1+J, [ D>=J ], cost: 1
     38: f54 -> f60 : A1'=Q_1+C, [ J>=1+D ], cost: 1
     37: f60 -> f46 : Q_1'=1+Q_1, [ J>=1+D ], cost: 1
     11: f60 -> f60 : J'=1+J, [ D>=J ], cost: 1
     36: f66 -> f46 : Q_1'=1+Q_1, [ J>=1+E ], cost: 1
     13: f66 -> f66 : J'=2+J, [ E>=J ], cost: 1
     14: f72 -> f72 : J'=1+J, R'=2*J, S'=free_5, T'=1-free_5, [ C>=J ], cost: 1
     33: f72 -> f87 : L'=free_27, Z'=0, [ J>=1+C ], cost: 1
     34: f72 -> f87 : L'=free_28, Z'=free_29, [ J>=1+C ], cost: 1
     35: f72 -> f87 : L'=free_31, Z'=free_32, [ J>=1+C ], cost: 1
     15: f87 -> f91 : L'=0, U'=0, [ L==0 ], cost: 1
     16: f87 -> f91 : U'=free_6, [ 0>=1+L ], cost: 1
     17: f87 -> f91 : U'=free_7, [ L>=1 ], cost: 1
     32: f91 -> f44 : B'=B+A, O'=1+O, [ J>=1+D ], cost: 1
     18: f91 -> f99 : L'=free_8, R'=2*J, V'=0, [ D>=J ], cost: 1
     19: f91 -> f99 : L'=free_9, R'=2*J, V'=free_10, [ D>=J ], cost: 1
     20: f91 -> f99 : L'=free_12, R'=2*J, V'=free_13, [ D>=J ], cost: 1
     21: f99 -> f103 : L'=free_15, W'=0, [ L==0 ], cost: 1
     22: f99 -> f103 : L'=free_16, W'=free_17, [ 0>=1+L ], cost: 1
     23: f99 -> f103 : L'=free_18, W'=free_19, [ L>=1 ], cost: 1
     24: f103 -> f107 : L'=free_20, X'=0, [ L==0 ], cost: 1
     25: f103 -> f107 : L'=free_21, X'=free_22, [ 0>=1+L ], cost: 1
     26: f103 -> f107 : L'=free_23, X'=free_24, [ L>=1 ], cost: 1
     27: f107 -> f91 : J'=1+J, L'=0, Y'=0, [ L==0 ], cost: 1
     28: f107 -> f91 : J'=1+J, Y'=free_25, [ 0>=1+L ], cost: 1
     29: f107 -> f91 : J'=1+J, Y'=free_26, [ L>=1 ], cost: 1
     30: f117 -> f117 : J'=1+J, [ D>=J ], cost: 1

Eliminating 3 self-loops for location f23
  Self-Loop 1 has the metering function: 1+C-J, resulting in the new transition 47.
  Self-Loop 2 has the metering function: 1+C-J, resulting in the new transition 48.
  Self-Loop 3 has the metering function: 1+C-J, resulting in the new transition 49.
  Removing the self-loops: 1 2 3.
Eliminating 1 self-loops for location f33
  Self-Loop 4 has the metering function: 1-J+D, resulting in the new transition 50.
  Removing the self-loops: 4.
Eliminating 1 self-loops for location f39
  Self-Loop 5 has the metering function: 1-J+D, resulting in the new transition 51.
  Removing the self-loops: 5.
Eliminating 1 self-loops for location f49
  Self-Loop 9 has the metering function: 1-J+D, resulting in the new transition 52.
  Removing the self-loops: 9.
Eliminating 1 self-loops for location f54
  Self-Loop 10 has the metering function: 1-J+D, resulting in the new transition 53.
  Removing the self-loops: 10.
Eliminating 1 self-loops for location f60
  Self-Loop 11 has the metering function: 1-J+D, resulting in the new transition 54.
  Removing the self-loops: 11.
Eliminating 1 self-loops for location f66
  Self-Loop 13 has the metering function: meter, resulting in the new transition 55.
  Removing the self-loops: 13.
Eliminating 1 self-loops for location f72
  Self-Loop 14 has the metering function: 1+C-J, resulting in the new transition 56.
  Removing the self-loops: 14.
Eliminating 1 self-loops for location f117
  Self-Loop 30 has the metering function: 1-J+D, resulting in the new transition 57.
  Removing the self-loops: 30.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f23 : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, [], cost: 1
     47: f23 -> [18] : J'=1+C, K'=1, L'=0, M'=0, [ C>=J ], cost: 1+C-J
     48: f23 -> [18] : A'=free_1*(1+C-J)+A, J'=1+C, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && C>=J ], cost: 1+C-J
     49: f23 -> [18] : A'=free_3*(1+C-J)+A, J'=1+C, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && C>=J ], cost: 1+C-J
     50: f33 -> [19] : J'=1+D, [ D>=J ], cost: 1-J+D
     51: f39 -> [20] : J'=1+D, [ D>=J ], cost: 1-J+D
      6: f44 -> f46 : [ N>=O ], cost: 1
     41: f44 -> f117 : B'=free_34, [ O>=1+N ], cost: 1
      7: f46 -> f49 : [ 0>=1+P && 0>=Q_1 ], cost: 1
      8: f46 -> f49 : [ P>=1 && 0>=Q_1 ], cost: 1
     12: f46 -> f66 : P'=0, [ 0>=Q_1 && P==0 ], cost: 1
     40: f46 -> f72 : [ Q_1>=1 ], cost: 1
     52: f49 -> [21] : J'=1+D, [ D>=J ], cost: 1-J+D
     53: f54 -> [22] : J'=1+D, [ D>=J ], cost: 1-J+D
     54: f60 -> [23] : J'=1+D, [ D>=J ], cost: 1-J+D
     55: f66 -> [24] : J'=J+2*meter, [ E>=J && 2*meter==E-J ], cost: meter
     56: f72 -> [25] : J'=1+C, R'=2*C, S'=free_5, T'=1-free_5, [ C>=J ], cost: 1+C-J
     15: f87 -> f91 : L'=0, U'=0, [ L==0 ], cost: 1
     16: f87 -> f91 : U'=free_6, [ 0>=1+L ], cost: 1
     17: f87 -> f91 : U'=free_7, [ L>=1 ], cost: 1
     32: f91 -> f44 : B'=B+A, O'=1+O, [ J>=1+D ], cost: 1
     18: f91 -> f99 : L'=free_8, R'=2*J, V'=0, [ D>=J ], cost: 1
     19: f91 -> f99 : L'=free_9, R'=2*J, V'=free_10, [ D>=J ], cost: 1
     20: f91 -> f99 : L'=free_12, R'=2*J, V'=free_13, [ D>=J ], cost: 1
     21: f99 -> f103 : L'=free_15, W'=0, [ L==0 ], cost: 1
     22: f99 -> f103 : L'=free_16, W'=free_17, [ 0>=1+L ], cost: 1
     23: f99 -> f103 : L'=free_18, W'=free_19, [ L>=1 ], cost: 1
     24: f103 -> f107 : L'=free_20, X'=0, [ L==0 ], cost: 1
     25: f103 -> f107 : L'=free_21, X'=free_22, [ 0>=1+L ], cost: 1
     26: f103 -> f107 : L'=free_23, X'=free_24, [ L>=1 ], cost: 1
     27: f107 -> f91 : J'=1+J, L'=0, Y'=0, [ L==0 ], cost: 1
     28: f107 -> f91 : J'=1+J, Y'=free_25, [ 0>=1+L ], cost: 1
     29: f107 -> f91 : J'=1+J, Y'=free_26, [ L>=1 ], cost: 1
     57: f117 -> [26] : J'=1+D, [ D>=J ], cost: 1-J+D
     46: [18] -> f33 : [ J>=1+C ], cost: 1
     43: [19] -> f39 : [ 0>=1+P && J>=1+D ], cost: 1
     44: [19] -> f39 : [ P>=1 && J>=1+D ], cost: 1
     45: [19] -> f44 : P'=0, [ J>=1+D && P==0 ], cost: 1
     42: [20] -> f44 : [ J>=1+D ], cost: 1
     39: [21] -> f54 : [ J>=1+D ], cost: 1
     38: [22] -> f60 : A1'=Q_1+C, [ J>=1+D ], cost: 1
     37: [23] -> f46 : Q_1'=1+Q_1, [ J>=1+D ], cost: 1
     36: [24] -> f46 : Q_1'=1+Q_1, [ J>=1+E ], cost: 1
     33: [25] -> f87 : L'=free_27, Z'=0, [ J>=1+C ], cost: 1
     34: [25] -> f87 : L'=free_28, Z'=free_29, [ J>=1+C ], cost: 1
     35: [25] -> f87 : L'=free_31, Z'=free_32, [ J>=1+C ], cost: 1


Applied simple chaining:
  Start location: f0
      0: f0 -> f23 : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, [], cost: 1
     47: f23 -> [18] : J'=1+C, K'=1, L'=0, M'=0, [ C>=J ], cost: 1+C-J
     48: f23 -> [18] : A'=free_1*(1+C-J)+A, J'=1+C, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && C>=J ], cost: 1+C-J
     49: f23 -> [18] : A'=free_3*(1+C-J)+A, J'=1+C, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && C>=J ], cost: 1+C-J
     51: f39 -> f44 : J'=1+D, [ D>=J && 1+D>=1+D ], cost: 2-J+D
      6: f44 -> f46 : [ N>=O ], cost: 1
     41: f44 -> [26] : B'=free_34, J'=1+D, [ O>=1+N && D>=J ], cost: 2-J+D
      7: f46 -> f49 : [ 0>=1+P && 0>=Q_1 ], cost: 1
      8: f46 -> f49 : [ P>=1 && 0>=Q_1 ], cost: 1
     12: f46 -> [24] : J'=J+2*meter, P'=0, [ 0>=Q_1 && P==0 && E>=J && 2*meter==E-J ], cost: 1+meter
     40: f46 -> [25] : J'=1+C, R'=2*C, S'=free_5, T'=1-free_5, [ Q_1>=1 && C>=J ], cost: 2+C-J
     52: f49 -> f54 : J'=1+D, [ D>=J && 1+D>=1+D ], cost: 2-J+D
     53: f54 -> f60 : J'=1+D, A1'=Q_1+C, [ D>=J && 1+D>=1+D ], cost: 2-J+D
     54: f60 -> f46 : J'=1+D, Q_1'=1+Q_1, [ D>=J && 1+D>=1+D ], cost: 2-J+D
     15: f87 -> f91 : L'=0, U'=0, [ L==0 ], cost: 1
     16: f87 -> f91 : U'=free_6, [ 0>=1+L ], cost: 1
     17: f87 -> f91 : U'=free_7, [ L>=1 ], cost: 1
     32: f91 -> f44 : B'=B+A, O'=1+O, [ J>=1+D ], cost: 1
     18: f91 -> f99 : L'=free_8, R'=2*J, V'=0, [ D>=J ], cost: 1
     19: f91 -> f99 : L'=free_9, R'=2*J, V'=free_10, [ D>=J ], cost: 1
     20: f91 -> f99 : L'=free_12, R'=2*J, V'=free_13, [ D>=J ], cost: 1
     21: f99 -> f103 : L'=free_15, W'=0, [ L==0 ], cost: 1
     22: f99 -> f103 : L'=free_16, W'=free_17, [ 0>=1+L ], cost: 1
     23: f99 -> f103 : L'=free_18, W'=free_19, [ L>=1 ], cost: 1
     24: f103 -> f107 : L'=free_20, X'=0, [ L==0 ], cost: 1
     25: f103 -> f107 : L'=free_21, X'=free_22, [ 0>=1+L ], cost: 1
     26: f103 -> f107 : L'=free_23, X'=free_24, [ L>=1 ], cost: 1
     27: f107 -> f91 : J'=1+J, L'=0, Y'=0, [ L==0 ], cost: 1
     28: f107 -> f91 : J'=1+J, Y'=free_25, [ 0>=1+L ], cost: 1
     29: f107 -> f91 : J'=1+J, Y'=free_26, [ L>=1 ], cost: 1
     46: [18] -> [19] : J'=1+D, [ J>=1+C && D>=J ], cost: 2-J+D
     43: [19] -> f39 : [ 0>=1+P && J>=1+D ], cost: 1
     44: [19] -> f39 : [ P>=1 && J>=1+D ], cost: 1
     45: [19] -> f44 : P'=0, [ J>=1+D && P==0 ], cost: 1
     36: [24] -> f46 : Q_1'=1+Q_1, [ J>=1+E ], cost: 1
     33: [25] -> f87 : L'=free_27, Z'=0, [ J>=1+C ], cost: 1
     34: [25] -> f87 : L'=free_28, Z'=free_29, [ J>=1+C ], cost: 1
     35: [25] -> f87 : L'=free_31, Z'=free_32, [ J>=1+C ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
     58: f0 -> [18] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+2*D, K'=1, L'=0, M'=0, [ 2*D>=J ], cost: 2-J+2*D
     59: f0 -> [18] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+2*D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J ], cost: 2-J+2*D
     60: f0 -> [18] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+2*D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J ], cost: 2-J+2*D
     51: f39 -> f44 : J'=1+D, [ D>=J && 1+D>=1+D ], cost: 2-J+D
      6: f44 -> f46 : [ N>=O ], cost: 1
     41: f44 -> [26] : B'=free_34, J'=1+D, [ O>=1+N && D>=J ], cost: 2-J+D
     64: f46 -> f54 : J'=1+D, [ 0>=1+P && 0>=Q_1 && D>=J && 1+D>=1+D ], cost: 3-J+D
     65: f46 -> f54 : J'=1+D, [ P>=1 && 0>=Q_1 && D>=J && 1+D>=1+D ], cost: 3-J+D
     67: f46 -> f87 : J'=1+C, L'=free_27, R'=2*C, S'=free_5, T'=1-free_5, Z'=0, [ Q_1>=1 && C>=J && 1+C>=1+C ], cost: 3+C-J
     68: f46 -> f87 : J'=1+C, L'=free_28, R'=2*C, S'=free_5, T'=1-free_5, Z'=free_29, [ Q_1>=1 && C>=J && 1+C>=1+C ], cost: 3+C-J
     69: f46 -> f87 : J'=1+C, L'=free_31, R'=2*C, S'=free_5, T'=1-free_5, Z'=free_32, [ Q_1>=1 && C>=J && 1+C>=1+C ], cost: 3+C-J
     66: f46 -> [27] : J'=J+2*meter, P'=0, [ 0>=Q_1 && P==0 && E>=J && 2*meter==E-J ], cost: 1+meter
     70: f54 -> [28] : J'=1+D, A1'=Q_1+C, [ D>=J && 1+D>=1+D ], cost: 2-J+D
     15: f87 -> f91 : L'=0, U'=0, [ L==0 ], cost: 1
     16: f87 -> f91 : U'=free_6, [ 0>=1+L ], cost: 1
     17: f87 -> f91 : U'=free_7, [ L>=1 ], cost: 1
     32: f91 -> f44 : B'=B+A, O'=1+O, [ J>=1+D ], cost: 1
     71: f91 -> f103 : L'=free_15, R'=2*J, V'=0, W'=0, [ D>=J && free_8==0 ], cost: 2
     72: f91 -> f103 : L'=free_16, R'=2*J, V'=0, W'=free_17, [ D>=J && 0>=1+free_8 ], cost: 2
     74: f91 -> f103 : L'=free_15, R'=2*J, V'=free_10, W'=0, [ D>=J && free_9==0 ], cost: 2
     75: f91 -> f103 : L'=free_16, R'=2*J, V'=free_10, W'=free_17, [ D>=J && 0>=1+free_9 ], cost: 2
     77: f91 -> f103 : L'=free_15, R'=2*J, V'=free_13, W'=0, [ D>=J && free_12==0 ], cost: 2
     80: f103 -> f91 : J'=1+J, L'=0, X'=0, Y'=0, [ L==0 && free_20==0 ], cost: 2
     81: f103 -> f91 : J'=1+J, L'=free_20, X'=0, Y'=free_25, [ L==0 && 0>=1+free_20 ], cost: 2
     83: f103 -> f91 : J'=1+J, L'=0, X'=free_22, Y'=0, [ 0>=1+L && free_21==0 ], cost: 2
     84: f103 -> f91 : J'=1+J, L'=free_21, X'=free_22, Y'=free_25, [ 0>=1+L && 0>=1+free_21 ], cost: 2
     86: f103 -> f91 : J'=1+J, L'=0, X'=free_24, Y'=0, [ L>=1 && free_23==0 ], cost: 2
     61: [18] -> f39 : J'=1+D, [ J>=1+C && D>=J && 0>=1+P && 1+D>=1+D ], cost: 3-J+D
     62: [18] -> f39 : J'=1+D, [ J>=1+C && D>=J && P>=1 && 1+D>=1+D ], cost: 3-J+D
     63: [18] -> f44 : J'=1+D, P'=0, [ J>=1+C && D>=J && 1+D>=1+D && P==0 ], cost: 3-J+D


Applied chaining over branches and pruning:
  Start location: f0
     89: f0 -> f39 : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D
     92: f0 -> f39 : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D
     93: f0 -> f39 : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D
     95: f0 -> f39 : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D
     96: f0 -> f39 : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D
     91: f0 -> f44 : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
     94: f0 -> f44 : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
     97: f0 -> f44 : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
     51: f39 -> f44 : J'=1+D, [ D>=J && 1+D>=1+D ], cost: 2-J+D
     98: f44 -> f54 : J'=1+D, [ N>=O && 0>=1+P && 0>=Q_1 && D>=J && 1+D>=1+D ], cost: 4-J+D
     99: f44 -> f54 : J'=1+D, [ N>=O && P>=1 && 0>=Q_1 && D>=J && 1+D>=1+D ], cost: 4-J+D
    100: f44 -> f87 : J'=1+C, L'=free_27, R'=2*C, S'=free_5, T'=1-free_5, Z'=0, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C ], cost: 4+C-J
    101: f44 -> f87 : J'=1+C, L'=free_28, R'=2*C, S'=free_5, T'=1-free_5, Z'=free_29, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C ], cost: 4+C-J
    102: f44 -> f87 : J'=1+C, L'=free_31, R'=2*C, S'=free_5, T'=1-free_5, Z'=free_32, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C ], cost: 4+C-J
     41: f44 -> [26] : B'=free_34, J'=1+D, [ O>=1+N && D>=J ], cost: 2-J+D
    103: f44 -> [27] : J'=J+2*meter, P'=0, [ N>=O && 0>=Q_1 && P==0 && E>=J && 2*meter==E-J ], cost: 2+meter
     70: f54 -> [28] : J'=1+D, A1'=Q_1+C, [ D>=J && 1+D>=1+D ], cost: 2-J+D
     15: f87 -> f91 : L'=0, U'=0, [ L==0 ], cost: 1
     16: f87 -> f91 : U'=free_6, [ 0>=1+L ], cost: 1
     17: f87 -> f91 : U'=free_7, [ L>=1 ], cost: 1
     32: f91 -> f44 : B'=B+A, O'=1+O, [ J>=1+D ], cost: 1
    104: f91 -> f91 : J'=1+J, L'=0, R'=2*J, V'=0, W'=0, X'=0, Y'=0, [ D>=J && free_8==0 && free_15==0 && free_20==0 ], cost: 4
    105: f91 -> f91 : J'=1+J, L'=free_20, R'=2*J, V'=0, W'=0, X'=0, Y'=free_25, [ D>=J && free_8==0 && free_15==0 && 0>=1+free_20 ], cost: 4
    107: f91 -> f91 : J'=1+J, L'=free_21, R'=2*J, V'=0, W'=0, X'=free_22, Y'=free_25, [ D>=J && free_8==0 && 0>=1+free_15 && 0>=1+free_21 ], cost: 4
    111: f91 -> f91 : J'=1+J, L'=0, R'=2*J, V'=0, W'=free_17, X'=free_22, Y'=0, [ D>=J && 0>=1+free_8 && 0>=1+free_16 && free_21==0 ], cost: 4
    116: f91 -> f91 : J'=1+J, L'=0, R'=2*J, V'=free_10, W'=0, X'=free_22, Y'=0, [ D>=J && free_9==0 && 0>=1+free_15 && free_21==0 ], cost: 4

Eliminating 5 self-loops for location f91
  Self-Loop 104 has the metering function: 1-J+D, resulting in the new transition 129.
  Self-Loop 105 has the metering function: 1-J+D, resulting in the new transition 130.
  Self-Loop 107 has the metering function: 1-J+D, resulting in the new transition 131.
  Self-Loop 111 has the metering function: 1-J+D, resulting in the new transition 132.
  Self-Loop 116 has the metering function: 1-J+D, resulting in the new transition 133.
  Removing the self-loops: 104 105 107 111 116.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
     89: f0 -> f39 : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D
     92: f0 -> f39 : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D
     93: f0 -> f39 : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D
     95: f0 -> f39 : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D
     96: f0 -> f39 : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D
     91: f0 -> f44 : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
     94: f0 -> f44 : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
     97: f0 -> f44 : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
     51: f39 -> f44 : J'=1+D, [ D>=J && 1+D>=1+D ], cost: 2-J+D
     98: f44 -> f54 : J'=1+D, [ N>=O && 0>=1+P && 0>=Q_1 && D>=J && 1+D>=1+D ], cost: 4-J+D
     99: f44 -> f54 : J'=1+D, [ N>=O && P>=1 && 0>=Q_1 && D>=J && 1+D>=1+D ], cost: 4-J+D
    100: f44 -> f87 : J'=1+C, L'=free_27, R'=2*C, S'=free_5, T'=1-free_5, Z'=0, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C ], cost: 4+C-J
    101: f44 -> f87 : J'=1+C, L'=free_28, R'=2*C, S'=free_5, T'=1-free_5, Z'=free_29, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C ], cost: 4+C-J
    102: f44 -> f87 : J'=1+C, L'=free_31, R'=2*C, S'=free_5, T'=1-free_5, Z'=free_32, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C ], cost: 4+C-J
     41: f44 -> [26] : B'=free_34, J'=1+D, [ O>=1+N && D>=J ], cost: 2-J+D
    103: f44 -> [27] : J'=J+2*meter, P'=0, [ N>=O && 0>=Q_1 && P==0 && E>=J && 2*meter==E-J ], cost: 2+meter
     70: f54 -> [28] : J'=1+D, A1'=Q_1+C, [ D>=J && 1+D>=1+D ], cost: 2-J+D
     15: f87 -> f91 : L'=0, U'=0, [ L==0 ], cost: 1
     16: f87 -> f91 : U'=free_6, [ 0>=1+L ], cost: 1
     17: f87 -> f91 : U'=free_7, [ L>=1 ], cost: 1
    129: f91 -> [29] : J'=1+D, L'=0, R'=2*D, V'=0, W'=0, X'=0, Y'=0, [ D>=J ], cost: 4-4*J+4*D
    130: f91 -> [29] : J'=1+D, L'=free_20, R'=2*D, V'=0, W'=0, X'=0, Y'=free_25, [ D>=J && 0>=1+free_20 ], cost: 4-4*J+4*D
    131: f91 -> [29] : J'=1+D, L'=free_21, R'=2*D, V'=0, W'=0, X'=free_22, Y'=free_25, [ D>=J && 0>=1+free_21 ], cost: 4-4*J+4*D
    132: f91 -> [29] : J'=1+D, L'=0, R'=2*D, V'=0, W'=free_17, X'=free_22, Y'=0, [ D>=J ], cost: 4-4*J+4*D
    133: f91 -> [29] : J'=1+D, L'=0, R'=2*D, V'=free_10, W'=0, X'=free_22, Y'=0, [ D>=J ], cost: 4-4*J+4*D
     32: [29] -> f44 : B'=B+A, O'=1+O, [ J>=1+D ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
     91: f0 -> f44 : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
     94: f0 -> f44 : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
     97: f0 -> f44 : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    134: f0 -> [30] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D
    135: f0 -> [31] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D
    136: f0 -> [32] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D
    137: f0 -> [33] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D
    138: f0 -> [34] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D
    141: f44 -> f91 : J'=1+C, L'=0, R'=2*C, S'=free_5, T'=1-free_5, U'=0, Z'=0, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C && free_27==0 ], cost: 5+C-J
    142: f44 -> f91 : J'=1+C, L'=free_27, R'=2*C, S'=free_5, T'=1-free_5, U'=free_6, Z'=0, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C && 0>=1+free_27 ], cost: 5+C-J
    144: f44 -> f91 : J'=1+C, L'=0, R'=2*C, S'=free_5, T'=1-free_5, U'=0, Z'=free_29, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C && free_28==0 ], cost: 5+C-J
    145: f44 -> f91 : J'=1+C, L'=free_28, R'=2*C, S'=free_5, T'=1-free_5, U'=free_6, Z'=free_29, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C && 0>=1+free_28 ], cost: 5+C-J
    147: f44 -> f91 : J'=1+C, L'=0, R'=2*C, S'=free_5, T'=1-free_5, U'=0, Z'=free_32, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C && free_31==0 ], cost: 5+C-J
     41: f44 -> [26] : B'=free_34, J'=1+D, [ O>=1+N && D>=J ], cost: 2-J+D
    103: f44 -> [27] : J'=J+2*meter, P'=0, [ N>=O && 0>=Q_1 && P==0 && E>=J && 2*meter==E-J ], cost: 2+meter
    139: f44 -> [35] : J'=1+D, [ N>=O && 0>=1+P && 0>=Q_1 && D>=J && 1+D>=1+D ], cost: 4-J+D
    140: f44 -> [36] : J'=1+D, [ N>=O && P>=1 && 0>=Q_1 && D>=J && 1+D>=1+D ], cost: 4-J+D
    150: f91 -> f44 : B'=B+A, J'=1+D, L'=0, O'=1+O, R'=2*D, V'=0, W'=0, X'=0, Y'=0, [ D>=J && 1+D>=1+D ], cost: 5-4*J+4*D
    151: f91 -> f44 : B'=B+A, J'=1+D, L'=free_20, O'=1+O, R'=2*D, V'=0, W'=0, X'=0, Y'=free_25, [ D>=J && 0>=1+free_20 && 1+D>=1+D ], cost: 5-4*J+4*D
    152: f91 -> f44 : B'=B+A, J'=1+D, L'=free_21, O'=1+O, R'=2*D, V'=0, W'=0, X'=free_22, Y'=free_25, [ D>=J && 0>=1+free_21 && 1+D>=1+D ], cost: 5-4*J+4*D
    153: f91 -> f44 : B'=B+A, J'=1+D, L'=0, O'=1+O, R'=2*D, V'=0, W'=free_17, X'=free_22, Y'=0, [ D>=J && 1+D>=1+D ], cost: 5-4*J+4*D
    154: f91 -> f44 : B'=B+A, J'=1+D, L'=0, O'=1+O, R'=2*D, V'=free_10, W'=0, X'=free_22, Y'=0, [ D>=J && 1+D>=1+D ], cost: 5-4*J+4*D


Applied chaining over branches and pruning:
  Start location: f0
     91: f0 -> f44 : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
     94: f0 -> f44 : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
     97: f0 -> f44 : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    134: f0 -> [30] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D
    135: f0 -> [31] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D
    136: f0 -> [32] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D
    137: f0 -> [33] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D
    138: f0 -> [34] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D
    156: f44 -> f44 : B'=B+A, J'=1+D, L'=free_20, O'=1+O, R'=2*D, S'=free_5, T'=1-free_5, U'=0, V'=0, W'=0, X'=0, Y'=free_25, Z'=0, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C && free_27==0 && D>=1+C && 0>=1+free_20 && 1+D>=1+D ], cost: 6-3*C-J+4*D
    161: f44 -> f44 : B'=B+A, J'=1+D, L'=free_20, O'=1+O, R'=2*D, S'=free_5, T'=1-free_5, U'=free_6, V'=0, W'=0, X'=0, Y'=free_25, Z'=0, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C && 0>=1+free_27 && D>=1+C && 0>=1+free_20 && 1+D>=1+D ], cost: 6-3*C-J+4*D
    162: f44 -> f44 : B'=B+A, J'=1+D, L'=free_21, O'=1+O, R'=2*D, S'=free_5, T'=1-free_5, U'=free_6, V'=0, W'=0, X'=free_22, Y'=free_25, Z'=0, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C && 0>=1+free_27 && D>=1+C && 0>=1+free_21 && 1+D>=1+D ], cost: 6-3*C-J+4*D
    167: f44 -> f44 : B'=B+A, J'=1+D, L'=free_21, O'=1+O, R'=2*D, S'=free_5, T'=1-free_5, U'=0, V'=0, W'=0, X'=free_22, Y'=free_25, Z'=free_29, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C && free_28==0 && D>=1+C && 0>=1+free_21 && 1+D>=1+D ], cost: 6-3*C-J+4*D
    177: f44 -> f44 : B'=B+A, J'=1+D, L'=free_21, O'=1+O, R'=2*D, S'=free_5, T'=1-free_5, U'=0, V'=0, W'=0, X'=free_22, Y'=free_25, Z'=free_32, [ N>=O && Q_1>=1 && C>=J && 1+C>=1+C && free_31==0 && D>=1+C && 0>=1+free_21 && 1+D>=1+D ], cost: 6-3*C-J+4*D
     41: f44 -> [26] : B'=free_34, J'=1+D, [ O>=1+N && D>=J ], cost: 2-J+D
    103: f44 -> [27] : J'=J+2*meter, P'=0, [ N>=O && 0>=Q_1 && P==0 && E>=J && 2*meter==E-J ], cost: 2+meter
    139: f44 -> [35] : J'=1+D, [ N>=O && 0>=1+P && 0>=Q_1 && D>=J && 1+D>=1+D ], cost: 4-J+D
    140: f44 -> [36] : J'=1+D, [ N>=O && P>=1 && 0>=Q_1 && D>=J && 1+D>=1+D ], cost: 4-J+D

Eliminating 5 self-loops for location f44
  Removing the self-loops: 156 161 162 167 177.
Adding an epsilon transition (to model nonexecution of the loops): 185.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
     91: f0 -> f44 : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
     94: f0 -> f44 : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
     97: f0 -> f44 : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    134: f0 -> [30] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D
    135: f0 -> [31] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D
    136: f0 -> [32] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D
    137: f0 -> [33] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D
    138: f0 -> [34] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D
    180: f44 -> [37] : B'=B+A, J'=1+D, L'=free_20, O'=1+O, R'=2*D, S'=free_5, T'=1-free_5, U'=0, V'=0, W'=0, X'=0, Y'=free_25, Z'=0, [ N>=O && Q_1>=1 && C>=J && D>=1+C && 0>=1+free_20 ], cost: 6-3*C-J+4*D
    181: f44 -> [37] : B'=B+A, J'=1+D, L'=free_20, O'=1+O, R'=2*D, S'=free_5, T'=1-free_5, U'=free_6, V'=0, W'=0, X'=0, Y'=free_25, Z'=0, [ N>=O && Q_1>=1 && C>=J && D>=1+C && 0>=1+free_20 ], cost: 6-3*C-J+4*D
    182: f44 -> [37] : B'=B+A, J'=1+D, L'=free_21, O'=1+O, R'=2*D, S'=free_5, T'=1-free_5, U'=free_6, V'=0, W'=0, X'=free_22, Y'=free_25, Z'=0, [ N>=O && Q_1>=1 && C>=J && D>=1+C && 0>=1+free_21 ], cost: 6-3*C-J+4*D
    183: f44 -> [37] : B'=B+A, J'=1+D, L'=free_21, O'=1+O, R'=2*D, S'=free_5, T'=1-free_5, U'=0, V'=0, W'=0, X'=free_22, Y'=free_25, Z'=free_29, [ N>=O && Q_1>=1 && C>=J && D>=1+C && 0>=1+free_21 ], cost: 6-3*C-J+4*D
    184: f44 -> [37] : B'=B+A, J'=1+D, L'=free_21, O'=1+O, R'=2*D, S'=free_5, T'=1-free_5, U'=0, V'=0, W'=0, X'=free_22, Y'=free_25, Z'=free_32, [ N>=O && Q_1>=1 && C>=J && D>=1+C && 0>=1+free_21 ], cost: 6-3*C-J+4*D
    185: f44 -> [37] : [], cost: 0
     41: [37] -> [26] : B'=free_34, J'=1+D, [ O>=1+N && D>=J ], cost: 2-J+D
    103: [37] -> [27] : J'=J+2*meter, P'=0, [ N>=O && 0>=Q_1 && P==0 && E>=J && 2*meter==E-J ], cost: 2+meter
    139: [37] -> [35] : J'=1+D, [ N>=O && 0>=1+P && 0>=Q_1 && D>=J && 1+D>=1+D ], cost: 4-J+D
    140: [37] -> [36] : J'=1+D, [ N>=O && P>=1 && 0>=Q_1 && D>=J && 1+D>=1+D ], cost: 4-J+D


Applied chaining over branches and pruning:
  Start location: f0
    134: f0 -> [30] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D
    135: f0 -> [31] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D
    136: f0 -> [32] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D
    137: f0 -> [33] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D
    138: f0 -> [34] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D
    191: f0 -> [37] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    197: f0 -> [37] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    203: f0 -> [37] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    186: f0 -> [38] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    187: f0 -> [39] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    188: f0 -> [40] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    189: f0 -> [41] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    190: f0 -> [42] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    192: f0 -> [43] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    193: f0 -> [44] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    194: f0 -> [45] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    195: f0 -> [46] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    196: f0 -> [47] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    198: f0 -> [48] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    199: f0 -> [49] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    200: f0 -> [50] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    201: f0 -> [51] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    202: f0 -> [52] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
     41: [37] -> [26] : B'=free_34, J'=1+D, [ O>=1+N && D>=J ], cost: 2-J+D
    103: [37] -> [27] : J'=J+2*meter, P'=0, [ N>=O && 0>=Q_1 && P==0 && E>=J && 2*meter==E-J ], cost: 2+meter
    139: [37] -> [35] : J'=1+D, [ N>=O && 0>=1+P && 0>=Q_1 && D>=J && 1+D>=1+D ], cost: 4-J+D
    140: [37] -> [36] : J'=1+D, [ N>=O && P>=1 && 0>=Q_1 && D>=J && 1+D>=1+D ], cost: 4-J+D


Applied chaining over branches and pruning:
  Start location: f0
    134: f0 -> [30] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D
    135: f0 -> [31] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D
    136: f0 -> [32] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D
    137: f0 -> [33] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D
    138: f0 -> [34] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D
    186: f0 -> [38] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    187: f0 -> [39] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    188: f0 -> [40] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    189: f0 -> [41] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    190: f0 -> [42] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    192: f0 -> [43] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    193: f0 -> [44] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    194: f0 -> [45] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    195: f0 -> [46] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    196: f0 -> [47] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    198: f0 -> [48] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    199: f0 -> [49] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    200: f0 -> [50] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    201: f0 -> [51] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    202: f0 -> [52] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    204: f0 -> [53] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    205: f0 -> [54] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    206: f0 -> [55] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    207: f0 -> [56] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    208: f0 -> [57] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    209: f0 -> [58] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    210: f0 -> [59] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    211: f0 -> [60] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    212: f0 -> [61] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    213: f0 -> [62] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    214: f0 -> [63] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    215: f0 -> [64] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
    134: f0 -> [30] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D
    135: f0 -> [31] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D
    136: f0 -> [32] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D
    137: f0 -> [33] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D ], cost: 4-J+D
    138: f0 -> [34] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && P>=1 && 1+D>=1+D ], cost: 4-J+D
    186: f0 -> [38] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    187: f0 -> [39] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    188: f0 -> [40] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    189: f0 -> [41] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    190: f0 -> [42] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    192: f0 -> [43] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    193: f0 -> [44] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    194: f0 -> [45] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    195: f0 -> [46] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    196: f0 -> [47] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    198: f0 -> [48] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    199: f0 -> [49] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    200: f0 -> [50] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    201: f0 -> [51] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    202: f0 -> [52] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    204: f0 -> [53] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    205: f0 -> [54] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    206: f0 -> [55] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    207: f0 -> [56] : A'=0, B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=1, L'=0, M'=0, P'=0, [ 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    208: f0 -> [57] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    209: f0 -> [58] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    210: f0 -> [59] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    211: f0 -> [60] : A'=-free_1*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_2, L'=1-free_2, M'=free_1, P'=0, [ free_2>=2 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    212: f0 -> [61] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    213: f0 -> [62] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    214: f0 -> [63] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D
    215: f0 -> [64] : A'=-free_3*(-1+J-2*D), B'=0, C'=2*D, E'=4*D, F'=3+4*D, G'=4+4*D, H'=D, Q'=free, J'=1+D, K'=free_4, L'=1-free_4, M'=free_3, P'=0, [ 0>=free_4 && 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 1+D>=1+D && P==0 ], cost: 4-J+D


Computing complexity for remaining 32 transitions.

  Found configuration with infinitely models for cost: 4-J+D
  and guard: 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D:
  P: Neg, J: Neg, D: Neg, where: J > D

Found new complexity n^1, because: Found infinity configuration.


The final runtime is determined by this resulting transition:
  Final Guard: 2*D>=J && 1+2*D>=1+2*D && D>=1+2*D && 0>=1+P && 1+D>=1+D
  Final Cost:  4-J+D

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

WORST_CASE(Omega(n^1),?)