Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: start
      0: f0 -> f0 : B'=1+B, C'=free, [ A>=B ], cost: 1
     21: f0 -> f17 : A1'=1, [ B>=1+A ], cost: 1
      1: f17 -> f25 : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, [ B>=1 ], cost: 1
     20: f17 -> f93 : [ 0>=B ], cost: 1
      2: f25 -> f28 : [ G>=J && Q>=1+J ], cost: 1
      5: f25 -> f44 : O'=free_7, [ G>=J && J>=Q ], cost: 1
     19: f25 -> f55 : P'=F, [ J>=1+G ], cost: 1
      3: f28 -> f30 : [ F+J>=2+K ], cost: 1
     18: f28 -> f44 : O'=free_19, [ 1+K>=F+J ], cost: 1
     17: f30 -> f28 : K'=2+K, [ L>=1+H ], cost: 1
      4: f30 -> f30 : L'=L+G, M'=L+Q-J, N'=free_6, [ H>=L ], cost: 1
     15: f44 -> f25 : Q'=O+Q, J'=F+J, [ O>=F && O>=Q ], cost: 1
     16: f44 -> f25 : Q'=O+Q, J'=F+J, [ F>=1+O ], cost: 1
      6: f44 -> f44 : Q'=-O+Q, O'=free_8, [ O>=F && Q>=1+O ], cost: 1
     14: f55 -> f17 : B'=-1+B, A1'=free_18, [ P>=G ], cost: 1
      7: f55 -> f64 : Q_1'=free_10, R'=free_12, S'=free_13, T'=free_9, U'=free_11, V'=1, W'=0, [ G>=1+P ], cost: 1
     13: f64 -> f55 : P'=Q_1, [ L>=1+P ], cost: 1
      8: f64 -> f66 : [ P>=L ], cost: 1
     12: f66 -> f64 : L'=L+F, S'=V, V'=free_16, W'=free_17, [ 1+K>=L+F ], cost: 1
      9: f66 -> f68 : [ L+F>=2+K ], cost: 1
     11: f68 -> f66 : K'=2+K, [ J>=1+H ], cost: 1
     10: f68 -> f68 : J'=Q_1+J, N'=free_14, X'=J, Y'=P+J, Z'=free_15, [ H>=J ], cost: 1
     22: start -> f0 : [], cost: 1


Simplified the transitions:
  Start location: start
      0: f0 -> f0 : B'=1+B, C'=free, [ A>=B ], cost: 1
     21: f0 -> f17 : A1'=1, [ B>=1+A ], cost: 1
      1: f17 -> f25 : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, [ B>=1 ], cost: 1
      2: f25 -> f28 : [ G>=J && Q>=1+J ], cost: 1
      5: f25 -> f44 : O'=free_7, [ G>=J && J>=Q ], cost: 1
     19: f25 -> f55 : P'=F, [ J>=1+G ], cost: 1
      3: f28 -> f30 : [ F+J>=2+K ], cost: 1
     18: f28 -> f44 : O'=free_19, [ 1+K>=F+J ], cost: 1
     17: f30 -> f28 : K'=2+K, [ L>=1+H ], cost: 1
      4: f30 -> f30 : L'=L+G, M'=L+Q-J, N'=free_6, [ H>=L ], cost: 1
     15: f44 -> f25 : Q'=O+Q, J'=F+J, [ O>=F && O>=Q ], cost: 1
     16: f44 -> f25 : Q'=O+Q, J'=F+J, [ F>=1+O ], cost: 1
      6: f44 -> f44 : Q'=-O+Q, O'=free_8, [ O>=F && Q>=1+O ], cost: 1
     14: f55 -> f17 : B'=-1+B, A1'=free_18, [ P>=G ], cost: 1
      7: f55 -> f64 : Q_1'=free_10, R'=free_12, S'=free_13, T'=free_9, U'=free_11, V'=1, W'=0, [ G>=1+P ], cost: 1
     13: f64 -> f55 : P'=Q_1, [ L>=1+P ], cost: 1
      8: f64 -> f66 : [ P>=L ], cost: 1
     12: f66 -> f64 : L'=L+F, S'=V, V'=free_16, W'=free_17, [ 1+K>=L+F ], cost: 1
      9: f66 -> f68 : [ L+F>=2+K ], cost: 1
     11: f68 -> f66 : K'=2+K, [ J>=1+H ], cost: 1
     10: f68 -> f68 : J'=Q_1+J, N'=free_14, X'=J, Y'=P+J, Z'=free_15, [ H>=J ], cost: 1
     22: start -> f0 : [], cost: 1

Eliminating 1 self-loops for location f0
  Self-Loop 0 has the metering function: 1-B+A, resulting in the new transition 23.
  Removing the self-loops: 0.
Eliminating 1 self-loops for location f30
  Removing the self-loops: 4.
Adding an epsilon transition (to model nonexecution of the loops): 25.
Eliminating 1 self-loops for location f44
  Removing the self-loops: 6.
Adding an epsilon transition (to model nonexecution of the loops): 27.
Eliminating 1 self-loops for location f68
  Removing the self-loops: 10.
Adding an epsilon transition (to model nonexecution of the loops): 29.

Removed all Self-loops using metering functions (where possible):
  Start location: start
     23: f0 -> [12] : B'=1+A, C'=free, [ A>=B ], cost: 1-B+A
      1: f17 -> f25 : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, [ B>=1 ], cost: 1
      2: f25 -> f28 : [ G>=J && Q>=1+J ], cost: 1
      5: f25 -> f44 : O'=free_7, [ G>=J && J>=Q ], cost: 1
     19: f25 -> f55 : P'=F, [ J>=1+G ], cost: 1
      3: f28 -> f30 : [ F+J>=2+K ], cost: 1
     18: f28 -> f44 : O'=free_19, [ 1+K>=F+J ], cost: 1
     24: f30 -> [13] : L'=L+G, M'=L+Q-J, N'=free_6, [ H>=L ], cost: 1
     25: f30 -> [13] : [], cost: 0
     26: f44 -> [14] : Q'=-O+Q, O'=free_8, [ O>=F && Q>=1+O ], cost: 1
     27: f44 -> [14] : [], cost: 0
     14: f55 -> f17 : B'=-1+B, A1'=free_18, [ P>=G ], cost: 1
      7: f55 -> f64 : Q_1'=free_10, R'=free_12, S'=free_13, T'=free_9, U'=free_11, V'=1, W'=0, [ G>=1+P ], cost: 1
     13: f64 -> f55 : P'=Q_1, [ L>=1+P ], cost: 1
      8: f64 -> f66 : [ P>=L ], cost: 1
     12: f66 -> f64 : L'=L+F, S'=V, V'=free_16, W'=free_17, [ 1+K>=L+F ], cost: 1
      9: f66 -> f68 : [ L+F>=2+K ], cost: 1
     28: f68 -> [15] : J'=Q_1+J, N'=free_14, X'=J, Y'=P+J, Z'=free_15, [ H>=J ], cost: 1
     29: f68 -> [15] : [], cost: 0
     22: start -> f0 : [], cost: 1
     21: [12] -> f17 : A1'=1, [ B>=1+A ], cost: 1
     17: [13] -> f28 : K'=2+K, [ L>=1+H ], cost: 1
     15: [14] -> f25 : Q'=O+Q, J'=F+J, [ O>=F && O>=Q ], cost: 1
     16: [14] -> f25 : Q'=O+Q, J'=F+J, [ F>=1+O ], cost: 1
     11: [15] -> f66 : K'=2+K, [ J>=1+H ], cost: 1


Applied simple chaining:
  Start location: start
      1: f17 -> f25 : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, [ B>=1 ], cost: 1
      2: f25 -> f28 : [ G>=J && Q>=1+J ], cost: 1
      5: f25 -> f44 : O'=free_7, [ G>=J && J>=Q ], cost: 1
     19: f25 -> f55 : P'=F, [ J>=1+G ], cost: 1
      3: f28 -> f30 : [ F+J>=2+K ], cost: 1
     18: f28 -> f44 : O'=free_19, [ 1+K>=F+J ], cost: 1
     24: f30 -> [13] : L'=L+G, M'=L+Q-J, N'=free_6, [ H>=L ], cost: 1
     25: f30 -> [13] : [], cost: 0
     26: f44 -> [14] : Q'=-O+Q, O'=free_8, [ O>=F && Q>=1+O ], cost: 1
     27: f44 -> [14] : [], cost: 0
     14: f55 -> f17 : B'=-1+B, A1'=free_18, [ P>=G ], cost: 1
      7: f55 -> f64 : Q_1'=free_10, R'=free_12, S'=free_13, T'=free_9, U'=free_11, V'=1, W'=0, [ G>=1+P ], cost: 1
     13: f64 -> f55 : P'=Q_1, [ L>=1+P ], cost: 1
      8: f64 -> f66 : [ P>=L ], cost: 1
     12: f66 -> f64 : L'=L+F, S'=V, V'=free_16, W'=free_17, [ 1+K>=L+F ], cost: 1
      9: f66 -> f68 : [ L+F>=2+K ], cost: 1
     28: f68 -> [15] : J'=Q_1+J, N'=free_14, X'=J, Y'=P+J, Z'=free_15, [ H>=J ], cost: 1
     29: f68 -> [15] : [], cost: 0
     22: start -> f17 : B'=1+A, C'=free, A1'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A
     17: [13] -> f28 : K'=2+K, [ L>=1+H ], cost: 1
     15: [14] -> f25 : Q'=O+Q, J'=F+J, [ O>=F && O>=Q ], cost: 1
     16: [14] -> f25 : Q'=O+Q, J'=F+J, [ F>=1+O ], cost: 1
     11: [15] -> f66 : K'=2+K, [ J>=1+H ], cost: 1


Applied chaining over branches and pruning:
  Start location: start
      1: f17 -> f25 : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, [ B>=1 ], cost: 1
      2: f25 -> f28 : [ G>=J && Q>=1+J ], cost: 1
      5: f25 -> f44 : O'=free_7, [ G>=J && J>=Q ], cost: 1
     19: f25 -> f55 : P'=F, [ J>=1+G ], cost: 1
     18: f28 -> f44 : O'=free_19, [ 1+K>=F+J ], cost: 1
     30: f28 -> [13] : L'=L+G, M'=L+Q-J, N'=free_6, [ F+J>=2+K && H>=L ], cost: 2
     31: f28 -> [13] : [ F+J>=2+K ], cost: 1
     32: f44 -> f25 : Q'=free_8-O+Q, J'=F+J, O'=free_8, [ O>=F && Q>=1+O && free_8>=F && free_8>=-O+Q ], cost: 2
     33: f44 -> f25 : Q'=free_8-O+Q, J'=F+J, O'=free_8, [ O>=F && Q>=1+O && F>=1+free_8 ], cost: 2
     34: f44 -> f25 : Q'=O+Q, J'=F+J, [ O>=F && O>=Q ], cost: 1
     35: f44 -> f25 : Q'=O+Q, J'=F+J, [ F>=1+O ], cost: 1
     14: f55 -> f17 : B'=-1+B, A1'=free_18, [ P>=G ], cost: 1
      7: f55 -> f64 : Q_1'=free_10, R'=free_12, S'=free_13, T'=free_9, U'=free_11, V'=1, W'=0, [ G>=1+P ], cost: 1
     13: f64 -> f55 : P'=Q_1, [ L>=1+P ], cost: 1
      8: f64 -> f66 : [ P>=L ], cost: 1
     12: f66 -> f64 : L'=L+F, S'=V, V'=free_16, W'=free_17, [ 1+K>=L+F ], cost: 1
     36: f66 -> [15] : J'=Q_1+J, N'=free_14, X'=J, Y'=P+J, Z'=free_15, [ L+F>=2+K && H>=J ], cost: 2
     37: f66 -> [15] : [ L+F>=2+K ], cost: 1
     22: start -> f17 : B'=1+A, C'=free, A1'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A
     17: [13] -> f28 : K'=2+K, [ L>=1+H ], cost: 1
     11: [15] -> f66 : K'=2+K, [ J>=1+H ], cost: 1


Applied chaining over branches and pruning:
  Start location: start
      1: f17 -> f25 : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, [ B>=1 ], cost: 1
      2: f25 -> f28 : [ G>=J && Q>=1+J ], cost: 1
      5: f25 -> f44 : O'=free_7, [ G>=J && J>=Q ], cost: 1
     19: f25 -> f55 : P'=F, [ J>=1+G ], cost: 1
     38: f28 -> f28 : K'=2+K, L'=L+G, M'=L+Q-J, N'=free_6, [ F+J>=2+K && H>=L && L+G>=1+H ], cost: 3
     39: f28 -> f28 : K'=2+K, [ F+J>=2+K && L>=1+H ], cost: 2
     18: f28 -> f44 : O'=free_19, [ 1+K>=F+J ], cost: 1
     32: f44 -> f25 : Q'=free_8-O+Q, J'=F+J, O'=free_8, [ O>=F && Q>=1+O && free_8>=F && free_8>=-O+Q ], cost: 2
     33: f44 -> f25 : Q'=free_8-O+Q, J'=F+J, O'=free_8, [ O>=F && Q>=1+O && F>=1+free_8 ], cost: 2
     34: f44 -> f25 : Q'=O+Q, J'=F+J, [ O>=F && O>=Q ], cost: 1
     35: f44 -> f25 : Q'=O+Q, J'=F+J, [ F>=1+O ], cost: 1
     14: f55 -> f17 : B'=-1+B, A1'=free_18, [ P>=G ], cost: 1
      7: f55 -> f64 : Q_1'=free_10, R'=free_12, S'=free_13, T'=free_9, U'=free_11, V'=1, W'=0, [ G>=1+P ], cost: 1
     13: f64 -> f55 : P'=Q_1, [ L>=1+P ], cost: 1
      8: f64 -> f66 : [ P>=L ], cost: 1
     12: f66 -> f64 : L'=L+F, S'=V, V'=free_16, W'=free_17, [ 1+K>=L+F ], cost: 1
     40: f66 -> f66 : J'=Q_1+J, K'=2+K, N'=free_14, X'=J, Y'=P+J, Z'=free_15, [ L+F>=2+K && H>=J && Q_1+J>=1+H ], cost: 3
     41: f66 -> f66 : K'=2+K, [ L+F>=2+K && J>=1+H ], cost: 2
     22: start -> f17 : B'=1+A, C'=free, A1'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A

Eliminating 2 self-loops for location f28
  Self-Loop 39 has the metering function: meter, resulting in the new transition 43.
  Removing the self-loops: 38 39.
Adding an epsilon transition (to model nonexecution of the loops): 44.
Eliminating 2 self-loops for location f66
  Self-Loop 41 has the metering function: meter_1, resulting in the new transition 46.
  Removing the self-loops: 40 41.
Adding an epsilon transition (to model nonexecution of the loops): 47.

Removed all Self-loops using metering functions (where possible):
  Start location: start
      1: f17 -> f25 : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, [ B>=1 ], cost: 1
      2: f25 -> f28 : [ G>=J && Q>=1+J ], cost: 1
      5: f25 -> f44 : O'=free_7, [ G>=J && J>=Q ], cost: 1
     19: f25 -> f55 : P'=F, [ J>=1+G ], cost: 1
     42: f28 -> [16] : K'=2+K, L'=L+G, M'=L+Q-J, N'=free_6, [ F+J>=2+K && H>=L && L+G>=1+H ], cost: 3
     43: f28 -> [16] : K'=K+2*meter, [ F+J>=2+K && L>=1+H && 2*meter==-1-K+F+J ], cost: 2*meter
     44: f28 -> [16] : [], cost: 0
     32: f44 -> f25 : Q'=free_8-O+Q, J'=F+J, O'=free_8, [ O>=F && Q>=1+O && free_8>=F && free_8>=-O+Q ], cost: 2
     33: f44 -> f25 : Q'=free_8-O+Q, J'=F+J, O'=free_8, [ O>=F && Q>=1+O && F>=1+free_8 ], cost: 2
     34: f44 -> f25 : Q'=O+Q, J'=F+J, [ O>=F && O>=Q ], cost: 1
     35: f44 -> f25 : Q'=O+Q, J'=F+J, [ F>=1+O ], cost: 1
     14: f55 -> f17 : B'=-1+B, A1'=free_18, [ P>=G ], cost: 1
      7: f55 -> f64 : Q_1'=free_10, R'=free_12, S'=free_13, T'=free_9, U'=free_11, V'=1, W'=0, [ G>=1+P ], cost: 1
     13: f64 -> f55 : P'=Q_1, [ L>=1+P ], cost: 1
      8: f64 -> f66 : [ P>=L ], cost: 1
     45: f66 -> [17] : J'=Q_1+J, K'=2+K, N'=free_14, X'=J, Y'=P+J, Z'=free_15, [ L+F>=2+K && H>=J && Q_1+J>=1+H ], cost: 3
     46: f66 -> [17] : K'=K+2*meter_1, [ L+F>=2+K && J>=1+H && 2*meter_1==-1-K+L+F ], cost: 2*meter_1
     47: f66 -> [17] : [], cost: 0
     22: start -> f17 : B'=1+A, C'=free, A1'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A
     18: [16] -> f44 : O'=free_19, [ 1+K>=F+J ], cost: 1
     12: [17] -> f64 : L'=L+F, S'=V, V'=free_16, W'=free_17, [ 1+K>=L+F ], cost: 1


Applied chaining over branches and pruning:
  Start location: start
      1: f17 -> f25 : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, [ B>=1 ], cost: 1
      5: f25 -> f44 : O'=free_7, [ G>=J && J>=Q ], cost: 1
     19: f25 -> f55 : P'=F, [ J>=1+G ], cost: 1
     48: f25 -> [16] : K'=2+K, L'=L+G, M'=L+Q-J, N'=free_6, [ G>=J && Q>=1+J && F+J>=2+K && H>=L && L+G>=1+H ], cost: 4
     49: f25 -> [16] : K'=K+2*meter, [ G>=J && Q>=1+J && F+J>=2+K && L>=1+H && 2*meter==-1-K+F+J ], cost: 1+2*meter
     50: f25 -> [16] : [ G>=J && Q>=1+J ], cost: 1
     32: f44 -> f25 : Q'=free_8-O+Q, J'=F+J, O'=free_8, [ O>=F && Q>=1+O && free_8>=F && free_8>=-O+Q ], cost: 2
     33: f44 -> f25 : Q'=free_8-O+Q, J'=F+J, O'=free_8, [ O>=F && Q>=1+O && F>=1+free_8 ], cost: 2
     34: f44 -> f25 : Q'=O+Q, J'=F+J, [ O>=F && O>=Q ], cost: 1
     35: f44 -> f25 : Q'=O+Q, J'=F+J, [ F>=1+O ], cost: 1
     14: f55 -> f17 : B'=-1+B, A1'=free_18, [ P>=G ], cost: 1
      7: f55 -> f64 : Q_1'=free_10, R'=free_12, S'=free_13, T'=free_9, U'=free_11, V'=1, W'=0, [ G>=1+P ], cost: 1
     13: f64 -> f55 : P'=Q_1, [ L>=1+P ], cost: 1
     51: f64 -> [17] : J'=Q_1+J, K'=2+K, N'=free_14, X'=J, Y'=P+J, Z'=free_15, [ P>=L && L+F>=2+K && H>=J && Q_1+J>=1+H ], cost: 4
     52: f64 -> [17] : K'=K+2*meter_1, [ P>=L && L+F>=2+K && J>=1+H && 2*meter_1==-1-K+L+F ], cost: 1+2*meter_1
     53: f64 -> [17] : [ P>=L ], cost: 1
     22: start -> f17 : B'=1+A, C'=free, A1'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A
     18: [16] -> f44 : O'=free_19, [ 1+K>=F+J ], cost: 1
     12: [17] -> f64 : L'=L+F, S'=V, V'=free_16, W'=free_17, [ 1+K>=L+F ], cost: 1


Applied chaining over branches and pruning:
  Start location: start
      1: f17 -> f25 : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, [ B>=1 ], cost: 1
      5: f25 -> f44 : O'=free_7, [ G>=J && J>=Q ], cost: 1
     54: f25 -> f44 : K'=2+K, L'=L+G, M'=L+Q-J, N'=free_6, O'=free_19, [ G>=J && Q>=1+J && F+J>=2+K && H>=L && L+G>=1+H && 3+K>=F+J ], cost: 5
     55: f25 -> f44 : K'=K+2*meter, O'=free_19, [ G>=J && Q>=1+J && F+J>=2+K && L>=1+H && 2*meter==-1-K+F+J && 1+K+2*meter>=F+J ], cost: 2+2*meter
     56: f25 -> f44 : O'=free_19, [ G>=J && Q>=1+J && 1+K>=F+J ], cost: 2
     19: f25 -> f55 : P'=F, [ J>=1+G ], cost: 1
     32: f44 -> f25 : Q'=free_8-O+Q, J'=F+J, O'=free_8, [ O>=F && Q>=1+O && free_8>=F && free_8>=-O+Q ], cost: 2
     33: f44 -> f25 : Q'=free_8-O+Q, J'=F+J, O'=free_8, [ O>=F && Q>=1+O && F>=1+free_8 ], cost: 2
     34: f44 -> f25 : Q'=O+Q, J'=F+J, [ O>=F && O>=Q ], cost: 1
     35: f44 -> f25 : Q'=O+Q, J'=F+J, [ F>=1+O ], cost: 1
     14: f55 -> f17 : B'=-1+B, A1'=free_18, [ P>=G ], cost: 1
      7: f55 -> f64 : Q_1'=free_10, R'=free_12, S'=free_13, T'=free_9, U'=free_11, V'=1, W'=0, [ G>=1+P ], cost: 1
     13: f64 -> f55 : P'=Q_1, [ L>=1+P ], cost: 1
     57: f64 -> f64 : J'=Q_1+J, K'=2+K, L'=L+F, N'=free_14, S'=V, V'=free_16, W'=free_17, X'=J, Y'=P+J, Z'=free_15, [ P>=L && L+F>=2+K && H>=J && Q_1+J>=1+H && 3+K>=L+F ], cost: 5
     58: f64 -> f64 : K'=K+2*meter_1, L'=L+F, S'=V, V'=free_16, W'=free_17, [ P>=L && L+F>=2+K && J>=1+H && 2*meter_1==-1-K+L+F && 1+K+2*meter_1>=L+F ], cost: 2+2*meter_1
     59: f64 -> f64 : L'=L+F, S'=V, V'=free_16, W'=free_17, [ P>=L && 1+K>=L+F ], cost: 2
     22: start -> f17 : B'=1+A, C'=free, A1'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A

Eliminating 3 self-loops for location f64
  Removing the self-loops: 57 58 59.
Adding an epsilon transition (to model nonexecution of the loops): 63.

Removed all Self-loops using metering functions (where possible):
  Start location: start
      1: f17 -> f25 : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, [ B>=1 ], cost: 1
      5: f25 -> f44 : O'=free_7, [ G>=J && J>=Q ], cost: 1
     54: f25 -> f44 : K'=2+K, L'=L+G, M'=L+Q-J, N'=free_6, O'=free_19, [ G>=J && Q>=1+J && F+J>=2+K && H>=L && L+G>=1+H && 3+K>=F+J ], cost: 5
     55: f25 -> f44 : K'=K+2*meter, O'=free_19, [ G>=J && Q>=1+J && F+J>=2+K && L>=1+H && 2*meter==-1-K+F+J && 1+K+2*meter>=F+J ], cost: 2+2*meter
     56: f25 -> f44 : O'=free_19, [ G>=J && Q>=1+J && 1+K>=F+J ], cost: 2
     19: f25 -> f55 : P'=F, [ J>=1+G ], cost: 1
     32: f44 -> f25 : Q'=free_8-O+Q, J'=F+J, O'=free_8, [ O>=F && Q>=1+O && free_8>=F && free_8>=-O+Q ], cost: 2
     33: f44 -> f25 : Q'=free_8-O+Q, J'=F+J, O'=free_8, [ O>=F && Q>=1+O && F>=1+free_8 ], cost: 2
     34: f44 -> f25 : Q'=O+Q, J'=F+J, [ O>=F && O>=Q ], cost: 1
     35: f44 -> f25 : Q'=O+Q, J'=F+J, [ F>=1+O ], cost: 1
     14: f55 -> f17 : B'=-1+B, A1'=free_18, [ P>=G ], cost: 1
      7: f55 -> f64 : Q_1'=free_10, R'=free_12, S'=free_13, T'=free_9, U'=free_11, V'=1, W'=0, [ G>=1+P ], cost: 1
     60: f64 -> [18] : J'=Q_1+J, K'=2+K, L'=L+F, N'=free_14, S'=V, V'=free_16, W'=free_17, X'=J, Y'=P+J, Z'=free_15, [ P>=L && L+F>=2+K && H>=J && Q_1+J>=1+H && 3+K>=L+F ], cost: 5
     61: f64 -> [18] : K'=K+2*meter_1, L'=L+F, S'=V, V'=free_16, W'=free_17, [ P>=L && L+F>=2+K && J>=1+H && 2*meter_1==-1-K+L+F ], cost: 2+2*meter_1
     62: f64 -> [18] : L'=L+F, S'=V, V'=free_16, W'=free_17, [ P>=L && 1+K>=L+F ], cost: 2
     63: f64 -> [18] : [], cost: 0
     22: start -> f17 : B'=1+A, C'=free, A1'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A
     13: [18] -> f55 : P'=Q_1, [ L>=1+P ], cost: 1


Applied chaining over branches and pruning:
  Start location: start
      1: f17 -> f25 : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, [ B>=1 ], cost: 1
     71: f25 -> f25 : Q'=Q+free_19, J'=F+J, K'=2+K, L'=L+G, M'=L+Q-J, N'=free_6, O'=free_19, [ G>=J && Q>=1+J && F+J>=2+K && H>=L && L+G>=1+H && 3+K>=F+J && F>=1+free_19 ], cost: 6
     72: f25 -> f25 : Q'=free_8+Q-free_19, J'=F+J, K'=K+2*meter, O'=free_8, [ G>=J && Q>=1+J && F+J>=2+K && L>=1+H && 2*meter==-1-K+F+J && 1+K+2*meter>=F+J && free_19>=F && Q>=1+free_19 && free_8>=F && free_8>=Q-free_19 ], cost: 4+2*meter
     73: f25 -> f25 : Q'=free_8+Q-free_19, J'=F+J, K'=K+2*meter, O'=free_8, [ G>=J && Q>=1+J && F+J>=2+K && L>=1+H && 2*meter==-1-K+F+J && 1+K+2*meter>=F+J && free_19>=F && Q>=1+free_19 && F>=1+free_8 ], cost: 4+2*meter
     74: f25 -> f25 : Q'=Q+free_19, J'=F+J, K'=K+2*meter, O'=free_19, [ G>=J && Q>=1+J && F+J>=2+K && L>=1+H && 2*meter==-1-K+F+J && 1+K+2*meter>=F+J && free_19>=F && free_19>=Q ], cost: 3+2*meter
     75: f25 -> f25 : Q'=Q+free_19, J'=F+J, K'=K+2*meter, O'=free_19, [ G>=J && Q>=1+J && F+J>=2+K && L>=1+H && 2*meter==-1-K+F+J && 1+K+2*meter>=F+J && F>=1+free_19 ], cost: 3+2*meter
     19: f25 -> f55 : P'=F, [ J>=1+G ], cost: 1
     14: f55 -> f17 : B'=-1+B, A1'=free_18, [ P>=G ], cost: 1
     80: f55 -> [18] : J'=J+free_10, K'=2+K, L'=L+F, N'=free_14, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, X'=J, Y'=P+J, Z'=free_15, [ G>=1+P && P>=L && L+F>=2+K && H>=J && J+free_10>=1+H && 3+K>=L+F ], cost: 6
     81: f55 -> [18] : K'=K+2*meter_1, L'=L+F, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, [ G>=1+P && P>=L && L+F>=2+K && J>=1+H && 2*meter_1==-1-K+L+F ], cost: 3+2*meter_1
     82: f55 -> [18] : L'=L+F, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, [ G>=1+P && P>=L && 1+K>=L+F ], cost: 3
     83: f55 -> [18] : Q_1'=free_10, R'=free_12, S'=free_13, T'=free_9, U'=free_11, V'=1, W'=0, [ G>=1+P ], cost: 1
     22: start -> f17 : B'=1+A, C'=free, A1'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A
     13: [18] -> f55 : P'=Q_1, [ L>=1+P ], cost: 1

Eliminating 5 self-loops for location f25
  Removing the self-loops: 71 72 73 74 75.
Adding an epsilon transition (to model nonexecution of the loops): 89.

Removed all Self-loops using metering functions (where possible):
  Start location: start
      1: f17 -> f25 : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, [ B>=1 ], cost: 1
     84: f25 -> [19] : Q'=Q+free_19, J'=F+J, K'=2+K, L'=L+G, M'=L+Q-J, N'=free_6, O'=free_19, [ G>=J && Q>=1+J && F+J>=2+K && H>=L && L+G>=1+H && 3+K>=F+J && F>=1+free_19 ], cost: 6
     85: f25 -> [19] : Q'=free_8+Q-free_19, J'=F+J, K'=K+2*meter, O'=free_8, [ G>=J && Q>=1+J && F+J>=2+K && L>=1+H && 2*meter==-1-K+F+J && free_19>=F && Q>=1+free_19 && free_8>=F && free_8>=Q-free_19 ], cost: 4+2*meter
     86: f25 -> [19] : Q'=free_8+Q-free_19, J'=F+J, K'=K+2*meter, O'=free_8, [ G>=J && Q>=1+J && F+J>=2+K && L>=1+H && 2*meter==-1-K+F+J && free_19>=F && Q>=1+free_19 && F>=1+free_8 ], cost: 4+2*meter
     87: f25 -> [19] : Q'=Q+free_19, J'=F+J, K'=K+2*meter, O'=free_19, [ G>=J && Q>=1+J && F+J>=2+K && L>=1+H && 2*meter==-1-K+F+J && free_19>=F && free_19>=Q ], cost: 3+2*meter
     88: f25 -> [19] : Q'=Q+free_19, J'=F+J, K'=K+2*meter, O'=free_19, [ G>=J && Q>=1+J && F+J>=2+K && L>=1+H && 2*meter==-1-K+F+J && F>=1+free_19 ], cost: 3+2*meter
     89: f25 -> [19] : [], cost: 0
     14: f55 -> f17 : B'=-1+B, A1'=free_18, [ P>=G ], cost: 1
     80: f55 -> [18] : J'=J+free_10, K'=2+K, L'=L+F, N'=free_14, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, X'=J, Y'=P+J, Z'=free_15, [ G>=1+P && P>=L && L+F>=2+K && H>=J && J+free_10>=1+H && 3+K>=L+F ], cost: 6
     81: f55 -> [18] : K'=K+2*meter_1, L'=L+F, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, [ G>=1+P && P>=L && L+F>=2+K && J>=1+H && 2*meter_1==-1-K+L+F ], cost: 3+2*meter_1
     82: f55 -> [18] : L'=L+F, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, [ G>=1+P && P>=L && 1+K>=L+F ], cost: 3
     83: f55 -> [18] : Q_1'=free_10, R'=free_12, S'=free_13, T'=free_9, U'=free_11, V'=1, W'=0, [ G>=1+P ], cost: 1
     22: start -> f17 : B'=1+A, C'=free, A1'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A
     13: [18] -> f55 : P'=Q_1, [ L>=1+P ], cost: 1
     19: [19] -> f55 : P'=F, [ J>=1+G ], cost: 1


Applied chaining over branches and pruning:
  Start location: start
     90: f17 -> [19] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=2+K, L'=free_1+L, M'=1+L-J, N'=free_6, O'=free_19, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && free_3>=L && free_1+L>=1+free_3 && 3+K>=free_5+J && free_5>=1+free_19 ], cost: 7
     92: f17 -> [19] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_8-free_19, J'=free_5+J, K'=K+2*meter, O'=free_8, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && 1>=1+free_19 && free_5>=1+free_8 ], cost: 5+2*meter
     93: f17 -> [19] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && free_19>=1 ], cost: 4+2*meter
     94: f17 -> [19] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_5>=1+free_19 ], cost: 4+2*meter
     95: f17 -> [19] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, [ B>=1 ], cost: 1
     14: f55 -> f17 : B'=-1+B, A1'=free_18, [ P>=G ], cost: 1
     96: f55 -> f55 : J'=J+free_10, K'=2+K, L'=L+F, N'=free_14, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, X'=J, Y'=P+J, Z'=free_15, [ G>=1+P && P>=L && L+F>=2+K && H>=J && J+free_10>=1+H && 3+K>=L+F && L+F>=1+P ], cost: 7
     97: f55 -> f55 : K'=K+2*meter_1, L'=L+F, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, [ G>=1+P && P>=L && L+F>=2+K && J>=1+H && 2*meter_1==-1-K+L+F && L+F>=1+P ], cost: 4+2*meter_1
     98: f55 -> f55 : L'=L+F, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, [ G>=1+P && P>=L && 1+K>=L+F && L+F>=1+P ], cost: 4
     99: f55 -> f55 : P'=free_10, Q_1'=free_10, R'=free_12, S'=free_13, T'=free_9, U'=free_11, V'=1, W'=0, [ G>=1+P && L>=1+P ], cost: 2
     22: start -> f17 : B'=1+A, C'=free, A1'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A
     19: [19] -> f55 : P'=F, [ J>=1+G ], cost: 1

Eliminating 4 self-loops for location f55
  Removing the self-loops: 96 97 98 99.
Adding an epsilon transition (to model nonexecution of the loops): 104.

Removed all Self-loops using metering functions (where possible):
  Start location: start
     90: f17 -> [19] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=2+K, L'=free_1+L, M'=1+L-J, N'=free_6, O'=free_19, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && free_3>=L && free_1+L>=1+free_3 && 3+K>=free_5+J && free_5>=1+free_19 ], cost: 7
     92: f17 -> [19] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_8-free_19, J'=free_5+J, K'=K+2*meter, O'=free_8, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && 1>=1+free_19 && free_5>=1+free_8 ], cost: 5+2*meter
     93: f17 -> [19] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && free_19>=1 ], cost: 4+2*meter
     94: f17 -> [19] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_5>=1+free_19 ], cost: 4+2*meter
     95: f17 -> [19] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, [ B>=1 ], cost: 1
    100: f55 -> [20] : J'=J+free_10, K'=2+K, L'=L+F, N'=free_14, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, X'=J, Y'=P+J, Z'=free_15, [ G>=1+P && P>=L && L+F>=2+K && H>=J && J+free_10>=1+H && 3+K>=L+F && L+F>=1+P ], cost: 7
    101: f55 -> [20] : K'=K+2*meter_1, L'=L+F, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, [ G>=1+P && P>=L && L+F>=2+K && J>=1+H && 2*meter_1==-1-K+L+F && L+F>=1+P ], cost: 4+2*meter_1
    102: f55 -> [20] : L'=L+F, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, [ G>=1+P && P>=L && 1+K>=L+F && L+F>=1+P ], cost: 4
    103: f55 -> [20] : P'=free_10, Q_1'=free_10, R'=free_12, S'=free_13, T'=free_9, U'=free_11, V'=1, W'=0, [ G>=1+P && L>=1+P ], cost: 2
    104: f55 -> [20] : [], cost: 0
     22: start -> f17 : B'=1+A, C'=free, A1'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A
     19: [19] -> f55 : P'=F, [ J>=1+G ], cost: 1
     14: [20] -> f17 : B'=-1+B, A1'=free_18, [ P>=G ], cost: 1


Applied chaining over branches and pruning:
  Start location: start
    105: f17 -> f55 : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=2+K, L'=free_1+L, M'=1+L-J, N'=free_6, O'=free_19, P'=free_5, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && free_3>=L && free_1+L>=1+free_3 && 3+K>=free_5+J && free_5>=1+free_19 && free_5+J>=1+free_1 ], cost: 8
    107: f17 -> f55 : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && free_19>=1 && free_5+J>=1+free_1 ], cost: 5+2*meter
    108: f17 -> f55 : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_5>=1+free_19 && free_5+J>=1+free_1 ], cost: 5+2*meter
    109: f17 -> f55 : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, P'=free_5, [ B>=1 && J>=1+free_1 ], cost: 2
    106: f17 -> [21] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_8-free_19, J'=free_5+J, K'=K+2*meter, O'=free_8, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && 1>=1+free_19 && free_5>=1+free_8 ], cost: 5+2*meter
    110: f55 -> f17 : B'=-1+B, J'=J+free_10, K'=2+K, L'=L+F, N'=free_14, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, X'=J, Y'=P+J, Z'=free_15, A1'=free_18, [ G>=1+P && P>=L && L+F>=2+K && H>=J && J+free_10>=1+H && 3+K>=L+F && L+F>=1+P && free_10>=G ], cost: 8
    111: f55 -> f17 : B'=-1+B, K'=K+2*meter_1, L'=L+F, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ G>=1+P && P>=L && L+F>=2+K && J>=1+H && 2*meter_1==-1-K+L+F && L+F>=1+P && free_10>=G ], cost: 5+2*meter_1
    112: f55 -> f17 : B'=-1+B, L'=L+F, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ G>=1+P && P>=L && 1+K>=L+F && L+F>=1+P && free_10>=G ], cost: 5
    113: f55 -> f17 : B'=-1+B, P'=free_10, Q_1'=free_10, R'=free_12, S'=free_13, T'=free_9, U'=free_11, V'=1, W'=0, A1'=free_18, [ G>=1+P && L>=1+P && free_10>=G ], cost: 3
    114: f55 -> f17 : B'=-1+B, A1'=free_18, [ P>=G ], cost: 1
     22: start -> f17 : B'=1+A, C'=free, A1'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A


Applied chaining over branches and pruning:
  Start location: start
    115: f17 -> f17 : B'=-1+B, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=2+K, L'=free_1+L, M'=1+L-J, N'=free_6, O'=free_19, P'=free_5, A1'=free_18, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && free_3>=L && free_1+L>=1+free_3 && 3+K>=free_5+J && free_5>=1+free_19 && free_5+J>=1+free_1 && free_5>=free_1 ], cost: 9
    120: f17 -> f17 : B'=-1+B, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, A1'=free_18, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && free_19>=1 && free_5+J>=1+free_1 && free_5>=free_1 ], cost: 6+2*meter
    125: f17 -> f17 : B'=-1+B, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, A1'=free_18, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_5>=1+free_19 && free_5+J>=1+free_1 && free_5>=free_1 ], cost: 6+2*meter
    127: f17 -> f17 : B'=-1+B, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, K'=K+2*meter_1, L'=L+free_5, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ B>=1 && J>=1+free_1 && free_1>=1+free_5 && free_5>=L && L+free_5>=2+K && J>=1+free_3 && 2*meter_1==-1-K+L+free_5 && L+free_5>=1+free_5 && free_10>=free_1 ], cost: 7+2*meter_1
    128: f17 -> f17 : B'=-1+B, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, L'=L+free_5, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ B>=1 && J>=1+free_1 && free_1>=1+free_5 && free_5>=L && 1+K>=L+free_5 && L+free_5>=1+free_5 && free_10>=free_1 ], cost: 7
    106: f17 -> [21] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_8-free_19, J'=free_5+J, K'=K+2*meter, O'=free_8, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && 1>=1+free_19 && free_5>=1+free_8 ], cost: 5+2*meter
    116: f17 -> [22] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && free_19>=1 && free_5+J>=1+free_1 ], cost: 5+2*meter
    117: f17 -> [23] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && free_19>=1 && free_5+J>=1+free_1 ], cost: 5+2*meter
    118: f17 -> [24] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && free_19>=1 && free_5+J>=1+free_1 ], cost: 5+2*meter
    119: f17 -> [25] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && free_19>=1 && free_5+J>=1+free_1 ], cost: 5+2*meter
    121: f17 -> [26] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_5>=1+free_19 && free_5+J>=1+free_1 ], cost: 5+2*meter
    122: f17 -> [27] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_5>=1+free_19 && free_5+J>=1+free_1 ], cost: 5+2*meter
    123: f17 -> [28] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_5>=1+free_19 && free_5+J>=1+free_1 ], cost: 5+2*meter
    124: f17 -> [29] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_5>=1+free_19 && free_5+J>=1+free_1 ], cost: 5+2*meter
     22: start -> f17 : B'=1+A, C'=free, A1'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A

Eliminating 5 self-loops for location f17
  Self-Loop 115 has the metering function: J, resulting in the new transition 131.
  Removing the self-loops: 115 120 125 127 128 135 136.
Adding an epsilon transition (to model nonexecution of the loops): 138.

Removed all Self-loops using metering functions (where possible):
  Start location: start
    131: f17 -> [30] : B'=B-J, D'=free_2, E'=free_4, F'=0, G'=1+free_1, H'=free_3, Q'=1+free_19, J'=1+free_1, K'=K+2*J, L'=L+free_1*J+J, M'=-1-2*free_1+L+free_1*J+J, N'=free_6, O'=free_19, P'=0, A1'=free_18, [ B>=1 && J>=J && 1>=1+J && 1+free_1>=2+K && free_3>=L && L+J>=1+free_3 && 3+K>=1+free_1 && 1+free_1-J>=1+free_19 && 1+free_1>=1+J && 1+free_1-J>=J ], cost: 9*J
    132: f17 -> [30] : B'=-1+B, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ B>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && free_19>=1+K+2*meter-J && free_19>=1 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 6+2*meter
    133: f17 -> [30] : B'=-1+B, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ B>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && 1+K+2*meter-J>=1+free_19 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 6+2*meter
    134: f17 -> [30] : B'=-1+B, D'=free_2, E'=free_4, F'=1+K+2*meter_1-L, G'=free_1, H'=free_3, Q'=1, K'=K+2*meter_1, L'=1+K+2*meter_1, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ B>=1 && J>=1+free_1 && free_1>=2+K+2*meter_1-L && 1+K+2*meter_1-L>=L && 1+K+2*meter_1>=2+K && J>=1+free_3 && 1+K+2*meter_1>=2+K+2*meter_1-L && free_10>=free_1 ], cost: 7+2*meter_1
    137: f17 -> [30] : B'=-1+B, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, L'=L+free_5, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ B>=1 && J>=1+free_1 && free_1>=1+free_5 && free_5>=L && 1+K>=L+free_5 && L+free_5>=1+free_5 && free_10>=free_1 ], cost: 7
    138: f17 -> [30] : [], cost: 0
     22: start -> f17 : B'=1+A, C'=free, A1'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A
    106: [30] -> [21] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_8-free_19, J'=free_5+J, K'=K+2*meter, O'=free_8, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && 1>=1+free_19 && free_5>=1+free_8 ], cost: 5+2*meter
    116: [30] -> [22] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && free_19>=1 && free_5+J>=1+free_1 ], cost: 5+2*meter
    117: [30] -> [23] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && free_19>=1 && free_5+J>=1+free_1 ], cost: 5+2*meter
    118: [30] -> [24] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && free_19>=1 && free_5+J>=1+free_1 ], cost: 5+2*meter
    119: [30] -> [25] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && free_19>=1 && free_5+J>=1+free_1 ], cost: 5+2*meter
    121: [30] -> [26] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_5>=1+free_19 && free_5+J>=1+free_1 ], cost: 5+2*meter
    122: [30] -> [27] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_5>=1+free_19 && free_5+J>=1+free_1 ], cost: 5+2*meter
    123: [30] -> [28] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_5>=1+free_19 && free_5+J>=1+free_1 ], cost: 5+2*meter
    124: [30] -> [29] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_5>=1+free_19 && free_5+J>=1+free_1 ], cost: 5+2*meter


Applied chaining over branches and pruning:
  Start location: start
    140: start -> [30] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && free_19>=1+K+2*meter-J && free_19>=1 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    141: start -> [30] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && 1+K+2*meter-J>=1+free_19 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    142: start -> [30] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter_1-L, G'=free_1, H'=free_3, Q'=1, K'=K+2*meter_1, L'=1+K+2*meter_1, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=2+K+2*meter_1-L && 1+K+2*meter_1-L>=L && 1+K+2*meter_1>=2+K && J>=1+free_3 && 1+K+2*meter_1>=2+K+2*meter_1-L && free_10>=free_1 ], cost: 10+2*meter_1-B+A
    143: start -> [30] : B'=A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, L'=L+free_5, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=1+free_5 && free_5>=L && 1+K>=L+free_5 && L+free_5>=1+free_5 && free_10>=free_1 ], cost: 10-B+A
    144: start -> [30] : B'=1+A, C'=free, A1'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A
    139: start -> [31] : B'=1+A, C'=free, A1'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A
    106: [30] -> [21] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_8-free_19, J'=free_5+J, K'=K+2*meter, O'=free_8, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && 1>=1+free_19 && free_5>=1+free_8 ], cost: 5+2*meter
    116: [30] -> [22] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && free_19>=1 && free_5+J>=1+free_1 ], cost: 5+2*meter
    117: [30] -> [23] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && free_19>=1 && free_5+J>=1+free_1 ], cost: 5+2*meter
    118: [30] -> [24] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && free_19>=1 && free_5+J>=1+free_1 ], cost: 5+2*meter
    119: [30] -> [25] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && free_19>=1 && free_5+J>=1+free_1 ], cost: 5+2*meter
    121: [30] -> [26] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_5>=1+free_19 && free_5+J>=1+free_1 ], cost: 5+2*meter
    122: [30] -> [27] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_5>=1+free_19 && free_5+J>=1+free_1 ], cost: 5+2*meter
    123: [30] -> [28] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_5>=1+free_19 && free_5+J>=1+free_1 ], cost: 5+2*meter
    124: [30] -> [29] : D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, [ B>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_5>=1+free_19 && free_5+J>=1+free_1 ], cost: 5+2*meter


Applied chaining over branches and pruning:
  Start location: start
    181: start -> [21] : B'=1+A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_8-free_19, J'=free_5+J, K'=K+2*meter, O'=free_8, A1'=1, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && 1>=1+free_19 && free_5>=1+free_8 ], cost: 8+2*meter-B+A
    182: start -> [22] : B'=1+A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, A1'=1, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && free_19>=1 && free_5+J>=1+free_1 ], cost: 8+2*meter-B+A
    183: start -> [23] : B'=1+A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, A1'=1, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && free_19>=1 && free_5+J>=1+free_1 ], cost: 8+2*meter-B+A
    184: start -> [24] : B'=1+A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, A1'=1, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && free_19>=1 && free_5+J>=1+free_1 ], cost: 8+2*meter-B+A
    185: start -> [25] : B'=1+A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, A1'=1, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && free_19>=1 && free_5+J>=1+free_1 ], cost: 8+2*meter-B+A
    186: start -> [26] : B'=1+A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, A1'=1, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_5>=1+free_19 && free_5+J>=1+free_1 ], cost: 8+2*meter-B+A
    187: start -> [27] : B'=1+A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, A1'=1, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_5>=1+free_19 && free_5+J>=1+free_1 ], cost: 8+2*meter-B+A
    188: start -> [28] : B'=1+A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, A1'=1, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_5>=1+free_19 && free_5+J>=1+free_1 ], cost: 8+2*meter-B+A
    189: start -> [29] : B'=1+A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, A1'=1, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_5>=1+free_19 && free_5+J>=1+free_1 ], cost: 8+2*meter-B+A
    139: start -> [31] : B'=1+A, C'=free, A1'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A
    145: start -> [32] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && free_19>=1+K+2*meter-J && free_19>=1 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    146: start -> [33] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && free_19>=1+K+2*meter-J && free_19>=1 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    147: start -> [34] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && free_19>=1+K+2*meter-J && free_19>=1 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    148: start -> [35] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && free_19>=1+K+2*meter-J && free_19>=1 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    149: start -> [36] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && free_19>=1+K+2*meter-J && free_19>=1 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    150: start -> [37] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && free_19>=1+K+2*meter-J && free_19>=1 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    151: start -> [38] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && free_19>=1+K+2*meter-J && free_19>=1 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    152: start -> [39] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && free_19>=1+K+2*meter-J && free_19>=1 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    153: start -> [40] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && free_19>=1+K+2*meter-J && free_19>=1 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    154: start -> [41] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && 1+K+2*meter-J>=1+free_19 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    155: start -> [42] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && 1+K+2*meter-J>=1+free_19 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    156: start -> [43] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && 1+K+2*meter-J>=1+free_19 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    157: start -> [44] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && 1+K+2*meter-J>=1+free_19 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    158: start -> [45] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && 1+K+2*meter-J>=1+free_19 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    159: start -> [46] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && 1+K+2*meter-J>=1+free_19 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    160: start -> [47] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && 1+K+2*meter-J>=1+free_19 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    161: start -> [48] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && 1+K+2*meter-J>=1+free_19 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    162: start -> [49] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && 1+K+2*meter-J>=1+free_19 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    163: start -> [50] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter_1-L, G'=free_1, H'=free_3, Q'=1, K'=K+2*meter_1, L'=1+K+2*meter_1, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=2+K+2*meter_1-L && 1+K+2*meter_1-L>=L && 1+K+2*meter_1>=2+K && J>=1+free_3 && 1+K+2*meter_1>=2+K+2*meter_1-L && free_10>=free_1 ], cost: 10+2*meter_1-B+A
    164: start -> [51] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter_1-L, G'=free_1, H'=free_3, Q'=1, K'=K+2*meter_1, L'=1+K+2*meter_1, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=2+K+2*meter_1-L && 1+K+2*meter_1-L>=L && 1+K+2*meter_1>=2+K && J>=1+free_3 && 1+K+2*meter_1>=2+K+2*meter_1-L && free_10>=free_1 ], cost: 10+2*meter_1-B+A
    165: start -> [52] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter_1-L, G'=free_1, H'=free_3, Q'=1, K'=K+2*meter_1, L'=1+K+2*meter_1, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=2+K+2*meter_1-L && 1+K+2*meter_1-L>=L && 1+K+2*meter_1>=2+K && J>=1+free_3 && 1+K+2*meter_1>=2+K+2*meter_1-L && free_10>=free_1 ], cost: 10+2*meter_1-B+A
    166: start -> [53] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter_1-L, G'=free_1, H'=free_3, Q'=1, K'=K+2*meter_1, L'=1+K+2*meter_1, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=2+K+2*meter_1-L && 1+K+2*meter_1-L>=L && 1+K+2*meter_1>=2+K && J>=1+free_3 && 1+K+2*meter_1>=2+K+2*meter_1-L && free_10>=free_1 ], cost: 10+2*meter_1-B+A
    167: start -> [54] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter_1-L, G'=free_1, H'=free_3, Q'=1, K'=K+2*meter_1, L'=1+K+2*meter_1, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=2+K+2*meter_1-L && 1+K+2*meter_1-L>=L && 1+K+2*meter_1>=2+K && J>=1+free_3 && 1+K+2*meter_1>=2+K+2*meter_1-L && free_10>=free_1 ], cost: 10+2*meter_1-B+A
    168: start -> [55] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter_1-L, G'=free_1, H'=free_3, Q'=1, K'=K+2*meter_1, L'=1+K+2*meter_1, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=2+K+2*meter_1-L && 1+K+2*meter_1-L>=L && 1+K+2*meter_1>=2+K && J>=1+free_3 && 1+K+2*meter_1>=2+K+2*meter_1-L && free_10>=free_1 ], cost: 10+2*meter_1-B+A
    169: start -> [56] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter_1-L, G'=free_1, H'=free_3, Q'=1, K'=K+2*meter_1, L'=1+K+2*meter_1, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=2+K+2*meter_1-L && 1+K+2*meter_1-L>=L && 1+K+2*meter_1>=2+K && J>=1+free_3 && 1+K+2*meter_1>=2+K+2*meter_1-L && free_10>=free_1 ], cost: 10+2*meter_1-B+A
    170: start -> [57] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter_1-L, G'=free_1, H'=free_3, Q'=1, K'=K+2*meter_1, L'=1+K+2*meter_1, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=2+K+2*meter_1-L && 1+K+2*meter_1-L>=L && 1+K+2*meter_1>=2+K && J>=1+free_3 && 1+K+2*meter_1>=2+K+2*meter_1-L && free_10>=free_1 ], cost: 10+2*meter_1-B+A
    171: start -> [58] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter_1-L, G'=free_1, H'=free_3, Q'=1, K'=K+2*meter_1, L'=1+K+2*meter_1, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=2+K+2*meter_1-L && 1+K+2*meter_1-L>=L && 1+K+2*meter_1>=2+K && J>=1+free_3 && 1+K+2*meter_1>=2+K+2*meter_1-L && free_10>=free_1 ], cost: 10+2*meter_1-B+A
    172: start -> [59] : B'=A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, L'=L+free_5, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=1+free_5 && free_5>=L && 1+K>=L+free_5 && L+free_5>=1+free_5 && free_10>=free_1 ], cost: 10-B+A
    173: start -> [60] : B'=A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, L'=L+free_5, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=1+free_5 && free_5>=L && 1+K>=L+free_5 && L+free_5>=1+free_5 && free_10>=free_1 ], cost: 10-B+A
    174: start -> [61] : B'=A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, L'=L+free_5, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=1+free_5 && free_5>=L && 1+K>=L+free_5 && L+free_5>=1+free_5 && free_10>=free_1 ], cost: 10-B+A
    175: start -> [62] : B'=A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, L'=L+free_5, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=1+free_5 && free_5>=L && 1+K>=L+free_5 && L+free_5>=1+free_5 && free_10>=free_1 ], cost: 10-B+A
    176: start -> [63] : B'=A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, L'=L+free_5, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=1+free_5 && free_5>=L && 1+K>=L+free_5 && L+free_5>=1+free_5 && free_10>=free_1 ], cost: 10-B+A
    177: start -> [64] : B'=A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, L'=L+free_5, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=1+free_5 && free_5>=L && 1+K>=L+free_5 && L+free_5>=1+free_5 && free_10>=free_1 ], cost: 10-B+A
    178: start -> [65] : B'=A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, L'=L+free_5, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=1+free_5 && free_5>=L && 1+K>=L+free_5 && L+free_5>=1+free_5 && free_10>=free_1 ], cost: 10-B+A
    179: start -> [66] : B'=A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, L'=L+free_5, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=1+free_5 && free_5>=L && 1+K>=L+free_5 && L+free_5>=1+free_5 && free_10>=free_1 ], cost: 10-B+A
    180: start -> [67] : B'=A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, L'=L+free_5, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=1+free_5 && free_5>=L && 1+K>=L+free_5 && L+free_5>=1+free_5 && free_10>=free_1 ], cost: 10-B+A


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: start
    181: start -> [21] : B'=1+A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_8-free_19, J'=free_5+J, K'=K+2*meter, O'=free_8, A1'=1, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && 1>=1+free_19 && free_5>=1+free_8 ], cost: 8+2*meter-B+A
    182: start -> [22] : B'=1+A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, A1'=1, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && free_19>=1 && free_5+J>=1+free_1 ], cost: 8+2*meter-B+A
    183: start -> [23] : B'=1+A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, A1'=1, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && free_19>=1 && free_5+J>=1+free_1 ], cost: 8+2*meter-B+A
    184: start -> [24] : B'=1+A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, A1'=1, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && free_19>=1 && free_5+J>=1+free_1 ], cost: 8+2*meter-B+A
    185: start -> [25] : B'=1+A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, A1'=1, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && free_19>=1 && free_5+J>=1+free_1 ], cost: 8+2*meter-B+A
    186: start -> [26] : B'=1+A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, A1'=1, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_5>=1+free_19 && free_5+J>=1+free_1 ], cost: 8+2*meter-B+A
    187: start -> [27] : B'=1+A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, A1'=1, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_5>=1+free_19 && free_5+J>=1+free_1 ], cost: 8+2*meter-B+A
    188: start -> [28] : B'=1+A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, A1'=1, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_5>=1+free_19 && free_5+J>=1+free_1 ], cost: 8+2*meter-B+A
    189: start -> [29] : B'=1+A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1+free_19, J'=free_5+J, K'=K+2*meter, O'=free_19, P'=free_5, A1'=1, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_5>=1+free_19 && free_5+J>=1+free_1 ], cost: 8+2*meter-B+A
    139: start -> [31] : B'=1+A, C'=free, A1'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A
    145: start -> [32] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && free_19>=1+K+2*meter-J && free_19>=1 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    146: start -> [33] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && free_19>=1+K+2*meter-J && free_19>=1 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    147: start -> [34] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && free_19>=1+K+2*meter-J && free_19>=1 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    148: start -> [35] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && free_19>=1+K+2*meter-J && free_19>=1 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    149: start -> [36] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && free_19>=1+K+2*meter-J && free_19>=1 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    150: start -> [37] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && free_19>=1+K+2*meter-J && free_19>=1 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    151: start -> [38] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && free_19>=1+K+2*meter-J && free_19>=1 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    152: start -> [39] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && free_19>=1+K+2*meter-J && free_19>=1 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    153: start -> [40] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && free_19>=1+K+2*meter-J && free_19>=1 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    154: start -> [41] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && 1+K+2*meter-J>=1+free_19 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    155: start -> [42] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && 1+K+2*meter-J>=1+free_19 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    156: start -> [43] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && 1+K+2*meter-J>=1+free_19 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    157: start -> [44] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && 1+K+2*meter-J>=1+free_19 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    158: start -> [45] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && 1+K+2*meter-J>=1+free_19 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    159: start -> [46] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && 1+K+2*meter-J>=1+free_19 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    160: start -> [47] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && 1+K+2*meter-J>=1+free_19 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    161: start -> [48] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && 1+K+2*meter-J>=1+free_19 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    162: start -> [49] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter-J, G'=free_1, H'=free_3, Q'=1+free_19, J'=1+K+2*meter, K'=K+2*meter, O'=free_19, P'=1+K+2*meter-J, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && 1+K+2*meter>=2+K && L>=1+free_3 && 1+K+2*meter-J>=1+free_19 && 1+K+2*meter>=1+free_1 && 1+K+2*meter-J>=free_1 ], cost: 9+2*meter-B+A
    163: start -> [50] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter_1-L, G'=free_1, H'=free_3, Q'=1, K'=K+2*meter_1, L'=1+K+2*meter_1, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=2+K+2*meter_1-L && 1+K+2*meter_1-L>=L && 1+K+2*meter_1>=2+K && J>=1+free_3 && 1+K+2*meter_1>=2+K+2*meter_1-L && free_10>=free_1 ], cost: 10+2*meter_1-B+A
    164: start -> [51] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter_1-L, G'=free_1, H'=free_3, Q'=1, K'=K+2*meter_1, L'=1+K+2*meter_1, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=2+K+2*meter_1-L && 1+K+2*meter_1-L>=L && 1+K+2*meter_1>=2+K && J>=1+free_3 && 1+K+2*meter_1>=2+K+2*meter_1-L && free_10>=free_1 ], cost: 10+2*meter_1-B+A
    165: start -> [52] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter_1-L, G'=free_1, H'=free_3, Q'=1, K'=K+2*meter_1, L'=1+K+2*meter_1, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=2+K+2*meter_1-L && 1+K+2*meter_1-L>=L && 1+K+2*meter_1>=2+K && J>=1+free_3 && 1+K+2*meter_1>=2+K+2*meter_1-L && free_10>=free_1 ], cost: 10+2*meter_1-B+A
    166: start -> [53] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter_1-L, G'=free_1, H'=free_3, Q'=1, K'=K+2*meter_1, L'=1+K+2*meter_1, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=2+K+2*meter_1-L && 1+K+2*meter_1-L>=L && 1+K+2*meter_1>=2+K && J>=1+free_3 && 1+K+2*meter_1>=2+K+2*meter_1-L && free_10>=free_1 ], cost: 10+2*meter_1-B+A
    167: start -> [54] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter_1-L, G'=free_1, H'=free_3, Q'=1, K'=K+2*meter_1, L'=1+K+2*meter_1, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=2+K+2*meter_1-L && 1+K+2*meter_1-L>=L && 1+K+2*meter_1>=2+K && J>=1+free_3 && 1+K+2*meter_1>=2+K+2*meter_1-L && free_10>=free_1 ], cost: 10+2*meter_1-B+A
    168: start -> [55] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter_1-L, G'=free_1, H'=free_3, Q'=1, K'=K+2*meter_1, L'=1+K+2*meter_1, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=2+K+2*meter_1-L && 1+K+2*meter_1-L>=L && 1+K+2*meter_1>=2+K && J>=1+free_3 && 1+K+2*meter_1>=2+K+2*meter_1-L && free_10>=free_1 ], cost: 10+2*meter_1-B+A
    169: start -> [56] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter_1-L, G'=free_1, H'=free_3, Q'=1, K'=K+2*meter_1, L'=1+K+2*meter_1, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=2+K+2*meter_1-L && 1+K+2*meter_1-L>=L && 1+K+2*meter_1>=2+K && J>=1+free_3 && 1+K+2*meter_1>=2+K+2*meter_1-L && free_10>=free_1 ], cost: 10+2*meter_1-B+A
    170: start -> [57] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter_1-L, G'=free_1, H'=free_3, Q'=1, K'=K+2*meter_1, L'=1+K+2*meter_1, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=2+K+2*meter_1-L && 1+K+2*meter_1-L>=L && 1+K+2*meter_1>=2+K && J>=1+free_3 && 1+K+2*meter_1>=2+K+2*meter_1-L && free_10>=free_1 ], cost: 10+2*meter_1-B+A
    171: start -> [58] : B'=A, C'=free, D'=free_2, E'=free_4, F'=1+K+2*meter_1-L, G'=free_1, H'=free_3, Q'=1, K'=K+2*meter_1, L'=1+K+2*meter_1, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=2+K+2*meter_1-L && 1+K+2*meter_1-L>=L && 1+K+2*meter_1>=2+K && J>=1+free_3 && 1+K+2*meter_1>=2+K+2*meter_1-L && free_10>=free_1 ], cost: 10+2*meter_1-B+A
    172: start -> [59] : B'=A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, L'=L+free_5, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=1+free_5 && free_5>=L && 1+K>=L+free_5 && L+free_5>=1+free_5 && free_10>=free_1 ], cost: 10-B+A
    173: start -> [60] : B'=A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, L'=L+free_5, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=1+free_5 && free_5>=L && 1+K>=L+free_5 && L+free_5>=1+free_5 && free_10>=free_1 ], cost: 10-B+A
    174: start -> [61] : B'=A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, L'=L+free_5, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=1+free_5 && free_5>=L && 1+K>=L+free_5 && L+free_5>=1+free_5 && free_10>=free_1 ], cost: 10-B+A
    175: start -> [62] : B'=A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, L'=L+free_5, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=1+free_5 && free_5>=L && 1+K>=L+free_5 && L+free_5>=1+free_5 && free_10>=free_1 ], cost: 10-B+A
    176: start -> [63] : B'=A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, L'=L+free_5, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=1+free_5 && free_5>=L && 1+K>=L+free_5 && L+free_5>=1+free_5 && free_10>=free_1 ], cost: 10-B+A
    177: start -> [64] : B'=A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, L'=L+free_5, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=1+free_5 && free_5>=L && 1+K>=L+free_5 && L+free_5>=1+free_5 && free_10>=free_1 ], cost: 10-B+A
    178: start -> [65] : B'=A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, L'=L+free_5, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=1+free_5 && free_5>=L && 1+K>=L+free_5 && L+free_5>=1+free_5 && free_10>=free_1 ], cost: 10-B+A
    179: start -> [66] : B'=A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, L'=L+free_5, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=1+free_5 && free_5>=L && 1+K>=L+free_5 && L+free_5>=1+free_5 && free_10>=free_1 ], cost: 10-B+A
    180: start -> [67] : B'=A, C'=free, D'=free_2, E'=free_4, F'=free_5, G'=free_1, H'=free_3, Q'=1, L'=L+free_5, P'=free_10, Q_1'=free_10, R'=free_12, S'=1, T'=free_9, U'=free_11, V'=free_16, W'=free_17, A1'=free_18, [ A>=B && 1+A>=1+A && 1+A>=1 && J>=1+free_1 && free_1>=1+free_5 && free_5>=L && 1+K>=L+free_5 && L+free_5>=1+free_5 && free_10>=free_1 ], cost: 10-B+A


Computing complexity for remaining 46 transitions.

  Found configuration with infinitely models for cost: 8+2*meter-B+A
  and guard: A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && 1>=1+free_19 && free_5>=1+free_8:
  K: Both, meter: Pos, free_1: Pos, B: Pos, free_8: Neg, L: Both, free_5: Neg, J: Neg, free_3: Neg, free_19: Neg, A: Pos, where: free_8 > free_5 free_5 > free_19 A > B

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


The final runtime is determined by this resulting transition:
  Final Guard: A>=B && 1+A>=1+A && 1+A>=1 && free_1>=J && 1>=1+J && free_5+J>=2+K && L>=1+free_3 && 2*meter==-1-K+free_5+J && free_19>=free_5 && 1>=1+free_19 && free_5>=1+free_8
  Final Cost:  8+2*meter-B+A

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),?)