Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f4 -> f5 : [ 0>=1+A ], cost: 1
      1: f4 -> f5 : [ A>=1 ], cost: 1
      6: f4 -> f12 : A'=0, [ A==0 ], cost: 1
      3: f5 -> f4 : A'=free_1, B'=1+B, [ 3>=B ], cost: 1
      4: f5 -> f4 : A'=free_2, B'=1+B, [ B>=5 ], cost: 1
      5: f5 -> f4 : A'=free_3, B'=1, [ B==4 ], cost: 1
      2: f0 -> f4 : A'=free, B'=0, [], cost: 1


Simplified the transitions:
  Start location: f0
      0: f4 -> f5 : [ 0>=1+A ], cost: 1
      1: f4 -> f5 : [ A>=1 ], cost: 1
      3: f5 -> f4 : A'=free_1, B'=1+B, [ 3>=B ], cost: 1
      4: f5 -> f4 : A'=free_2, B'=1+B, [ B>=5 ], cost: 1
      5: f5 -> f4 : A'=free_3, B'=1, [ B==4 ], cost: 1
      2: f0 -> f4 : A'=free, B'=0, [], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      7: f4 -> f4 : A'=free_1, B'=1+B, [ 0>=1+A && 3>=B ], cost: 2
      8: f4 -> f4 : A'=free_2, B'=1+B, [ 0>=1+A && B>=5 ], cost: 2
      9: f4 -> f4 : A'=free_3, B'=1, [ 0>=1+A && B==4 ], cost: 2
     10: f4 -> f4 : A'=free_1, B'=1+B, [ A>=1 && 3>=B ], cost: 2
     12: f4 -> f4 : A'=free_3, B'=1, [ A>=1 && B==4 ], cost: 2
      2: f0 -> f4 : A'=free, B'=0, [], cost: 1

Eliminating 5 self-loops for location f4
  Self-Loop 9 has the metering function: meter, resulting in the new transition 15.
  Self-Loop 12 has the metering function: meter_1, resulting in the new transition 17.
  Found this metering function when nesting loops: meter_2,
  and nested parallel self-loops 13 (outer loop) and 15 (inner loop), obtaining the new transitions: 18, 19.
  Found this metering function when nesting loops: meter_3,
  and nested parallel self-loops 13 (outer loop) and 15 (inner loop), obtaining the new transitions: 20.
  Found this metering function when nesting loops: meter_4,
  and nested parallel self-loops 16 (outer loop) and 15 (inner loop), obtaining the new transitions: 21, 22.
  Found this metering function when nesting loops: meter_5,
  and nested parallel self-loops 16 (outer loop) and 15 (inner loop), obtaining the new transitions: 23.
  Found this metering function when nesting loops: meter_6,
  and nested parallel self-loops 13 (outer loop) and 17 (inner loop), obtaining the new transitions: 24, 25.
  Found this metering function when nesting loops: meter_7,
  and nested parallel self-loops 13 (outer loop) and 17 (inner loop), obtaining the new transitions: 26.
  Found this metering function when nesting loops: meter_8,
  and nested parallel self-loops 16 (outer loop) and 17 (inner loop), obtaining the new transitions: 27, 28.
  Found this metering function when nesting loops: meter_9,
  and nested parallel self-loops 16 (outer loop) and 17 (inner loop), obtaining the new transitions: 29.
  Found this metering function when nesting loops: -4+B,
  and nested parallel self-loops 13 (outer loop) and 18 (inner loop), obtaining the new transitions: 30, 31.
  Found this metering function when nesting loops: -3+B,
  and nested parallel self-loops 13 (outer loop) and 18 (inner loop), obtaining the new transitions: 32.
  Found this metering function when nesting loops: -4+B,
  and nested parallel self-loops 16 (outer loop) and 18 (inner loop), obtaining the new transitions: 33.
  Found this metering function when nesting loops: -3+B,
  and nested parallel self-loops 16 (outer loop) and 18 (inner loop), obtaining the new transitions: 34.
  Found this metering function when nesting loops: 3-B,
  and nested parallel self-loops 13 (outer loop) and 19 (inner loop), obtaining the new transitions: 35, 36.
  Found this metering function when nesting loops: 2-B,
  and nested parallel self-loops 13 (outer loop) and 19 (inner loop), obtaining the new transitions: 37, 38.
  Found this metering function when nesting loops: 2-B,
  and nested parallel self-loops 16 (outer loop) and 19 (inner loop), obtaining the new transitions: 39.
  Found this metering function when nesting loops: -3+B,
  and nested parallel self-loops 13 (outer loop) and 20 (inner loop), obtaining the new transitions: 40, 41.
  Found this metering function when nesting loops: meter_10,
  and nested parallel self-loops 13 (outer loop) and 20 (inner loop), obtaining the new transitions: 42.
  Found this metering function when nesting loops: -3+B,
  and nested parallel self-loops 16 (outer loop) and 20 (inner loop), obtaining the new transitions: 43, 44.
  Found this metering function when nesting loops: meter_11,
  and nested parallel self-loops 16 (outer loop) and 20 (inner loop), obtaining the new transitions: 45.
  Found this metering function when nesting loops: -4+B,
  and nested parallel self-loops 13 (outer loop) and 21 (inner loop), obtaining the new transitions: 46, 47.
  Found this metering function when nesting loops: -3+B,
  and nested parallel self-loops 13 (outer loop) and 21 (inner loop), obtaining the new transitions: 48.
  Found this metering function when nesting loops: -4+B,
  and nested parallel self-loops 16 (outer loop) and 21 (inner loop), obtaining the new transitions: 49.
  Found this metering function when nesting loops: -3+B,
  and nested parallel self-loops 16 (outer loop) and 21 (inner loop), obtaining the new transitions: 50.
  Found this metering function when nesting loops: 3-B,
  and nested parallel self-loops 13 (outer loop) and 22 (inner loop), obtaining the new transitions: 51.
  Found this metering function when nesting loops: -3+B,
  and nested parallel self-loops 13 (outer loop) and 23 (inner loop), obtaining the new transitions: 52.
  Found this metering function when nesting loops: -3+B,
  and nested parallel self-loops 16 (outer loop) and 23 (inner loop), obtaining the new transitions: 53.
  Found this metering function when nesting loops: -4+B,
  and nested parallel self-loops 13 (outer loop) and 24 (inner loop), obtaining the new transitions: 54.
  Found this metering function when nesting loops: -3+B,
  and nested parallel self-loops 13 (outer loop) and 24 (inner loop), obtaining the new transitions: 55.
  Found this metering function when nesting loops: -4+B,
  and nested parallel self-loops 16 (outer loop) and 24 (inner loop), obtaining the new transitions: 56, 57.
  Found this metering function when nesting loops: -3+B,
  and nested parallel self-loops 16 (outer loop) and 24 (inner loop), obtaining the new transitions: 58.
  Found this metering function when nesting loops: 3-B,
  and nested parallel self-loops 16 (outer loop) and 25 (inner loop), obtaining the new transitions: 59.
  Found this metering function when nesting loops: -3+B,
  and nested parallel self-loops 13 (outer loop) and 26 (inner loop), obtaining the new transitions: 60.
  Found this metering function when nesting loops: -3+B,
  and nested parallel self-loops 16 (outer loop) and 26 (inner loop), obtaining the new transitions: 61.
  Found this metering function when nesting loops: -4+B,
  and nested parallel self-loops 13 (outer loop) and 27 (inner loop), obtaining the new transitions: 62.
  Found this metering function when nesting loops: -3+B,
  and nested parallel self-loops 13 (outer loop) and 27 (inner loop), obtaining the new transitions: 63.
  Found this metering function when nesting loops: -4+B,
  and nested parallel self-loops 16 (outer loop) and 27 (inner loop), obtaining the new transitions: 64, 65.
  Found this metering function when nesting loops: -3+B,
  and nested parallel self-loops 16 (outer loop) and 27 (inner loop), obtaining the new transitions: 66.
  Found this metering function when nesting loops: 2-B,
  and nested parallel self-loops 13 (outer loop) and 28 (inner loop), obtaining the new transitions: 67.
  Found this metering function when nesting loops: 3-B,
  and nested parallel self-loops 16 (outer loop) and 28 (inner loop), obtaining the new transitions: 68, 69.
  Found this metering function when nesting loops: 2-B,
  and nested parallel self-loops 16 (outer loop) and 28 (inner loop), obtaining the new transitions: 70, 71.
  Found this metering function when nesting loops: -3+B,
  and nested parallel self-loops 13 (outer loop) and 29 (inner loop), obtaining the new transitions: 72, 73.
  Found this metering function when nesting loops: meter_12,
  and nested parallel self-loops 13 (outer loop) and 29 (inner loop), obtaining the new transitions: 74.
  Found this metering function when nesting loops: -3+B,
  and nested parallel self-loops 16 (outer loop) and 29 (inner loop), obtaining the new transitions: 75, 76.
  Found this metering function when nesting loops: meter_13,
  and nested parallel self-loops 16 (outer loop) and 29 (inner loop), obtaining the new transitions: 77.
  Found this metering function when nesting loops: 4-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 4-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: meter_14,
  Found this metering function when nesting loops: meter_15,
  Found this metering function when nesting loops: meter_16,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 1-B,
  Found this metering function when nesting loops: 1-B,
  Found this metering function when nesting loops: 3-B,
  and nested parallel self-loops 13 (outer loop) and 38 (inner loop), obtaining the new transitions: 78, 79.
  Found this metering function when nesting loops: 2-B,
  and nested parallel self-loops 13 (outer loop) and 38 (inner loop), obtaining the new transitions: 80, 81.
  Found this metering function when nesting loops: 2-B,
  and nested parallel self-loops 16 (outer loop) and 38 (inner loop), obtaining the new transitions: 82.
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 1-B,
  Found this metering function when nesting loops: 1-B,
  Found this metering function when nesting loops: 2-B,
  and nested parallel self-loops 13 (outer loop) and 42 (inner loop), obtaining the new transitions: 83, 84.
  Found this metering function when nesting loops: 1-B,
  and nested parallel self-loops 13 (outer loop) and 42 (inner loop), obtaining the new transitions: 85, 86.
  Found this metering function when nesting loops: 2-B,
  and nested parallel self-loops 16 (outer loop) and 42 (inner loop), obtaining the new transitions: 87, 88.
  Found this metering function when nesting loops: 1-B,
  and nested parallel self-loops 16 (outer loop) and 42 (inner loop), obtaining the new transitions: 89, 90.
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 2-B,
  and nested parallel self-loops 13 (outer loop) and 45 (inner loop), obtaining the new transitions: 91.
  Found this metering function when nesting loops: 2-B,
  and nested parallel self-loops 16 (outer loop) and 45 (inner loop), obtaining the new transitions: 92.
  Found this metering function when nesting loops: 4-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 4-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 4-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 4-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 4-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 4-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: meter_17,
  Found this metering function when nesting loops: meter_18,
  Found this metering function when nesting loops: meter_19,
  Found this metering function when nesting loops: 1-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 1-B,
  Found this metering function when nesting loops: 2-B,
  and nested parallel self-loops 13 (outer loop) and 71 (inner loop), obtaining the new transitions: 93.
  Found this metering function when nesting loops: 3-B,
  and nested parallel self-loops 16 (outer loop) and 71 (inner loop), obtaining the new transitions: 94, 95.
  Found this metering function when nesting loops: 2-B,
  and nested parallel self-loops 16 (outer loop) and 71 (inner loop), obtaining the new transitions: 96, 97.
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 2-B,
  and nested parallel self-loops 13 (outer loop) and 74 (inner loop), obtaining the new transitions: 98.
  Found this metering function when nesting loops: 2-B,
  and nested parallel self-loops 16 (outer loop) and 74 (inner loop), obtaining the new transitions: 99.
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 3-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 1-B,
  Found this metering function when nesting loops: 2-B,
  Found this metering function when nesting loops: 1-B,
  Found this metering function when nesting loops: 2-B,
  and nested parallel self-loops 13 (outer loop) and 77 (inner loop), obtaining the new transitions: 100, 101.
  Found this metering function when nesting loops: 1-B,
  and nested parallel self-loops 13 (outer loop) and 77 (inner loop), obtaining the new transitions: 102, 103.
  Found this metering function when nesting loops: 2-B,
  and nested parallel self-loops 16 (outer loop) and 77 (inner loop), obtaining the new transitions: 104, 105.
  Found this metering function when nesting loops: 1-B,
  and nested parallel self-loops 16 (outer loop) and 77 (inner loop), obtaining the new transitions: 106, 107.
  Removing the self-loops: 7 8 9 10 12 13 16.
Adding an epsilon transition (to model nonexecution of the loops): 108.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
     14: f4 -> [4] : A'=free_2, B'=1+B, [ 0>=1+A && B>=5 ], cost: 2
     15: f4 -> [4] : A'=free_3, B'=1, [ 0>=1+A && B==4 && 3*meter==-4+B ], cost: 2*meter
     17: f4 -> [4] : A'=free_3, B'=1, [ A>=1 && B==4 && 3*meter_1==-4+B ], cost: 2*meter_1
     18: f4 -> [4] : A'=free_1, B'=2, [ 0>=1+A && B==4 && 3*meter==-4+B && 0>=1+free_3 && 3>=1 && 2*meter_2==-4+B ], cost: 2*meter_2+2*meter_2*meter
     19: f4 -> [4] : A'=free_1, B'=2, [ 0>=1+A && 3>=B && 0>=1+free_1 && 1+B==4 && 3*meter==-3+B && 0>=1+free_3 && 3>=1 && 2*meter_2==-3+B ], cost: 2+2*meter_2+2*meter_2*meter
     20: f4 -> [4] : A'=free_3, B'=1, [ 0>=1+A && 3>=B && 0>=1+free_1 && 1+B==4 && 3*meter==-3+B && 2*meter_3==-3+B ], cost: 2*meter_3+2*meter_3*meter
     21: f4 -> [4] : A'=free_1, B'=2, [ 0>=1+A && B==4 && 3*meter==-4+B && free_3>=1 && 3>=1 && 2*meter_4==-4+B ], cost: 2*meter_4*meter+2*meter_4
     22: f4 -> [4] : A'=free_1, B'=2, [ A>=1 && 3>=B && 0>=1+free_1 && 1+B==4 && 3*meter==-3+B && free_3>=1 && 3>=1 && 2*meter_4==-3+B ], cost: 2+2*meter_4*meter+2*meter_4
     23: f4 -> [4] : A'=free_3, B'=1, [ A>=1 && 3>=B && 0>=1+free_1 && 1+B==4 && 3*meter==-3+B && 2*meter_5==-3+B ], cost: 2*meter_5*meter+2*meter_5
     24: f4 -> [4] : A'=free_1, B'=2, [ A>=1 && B==4 && 3*meter_1==-4+B && 0>=1+free_3 && 3>=1 && 2*meter_6==-4+B ], cost: 2*meter_6*meter_1+2*meter_6
     25: f4 -> [4] : A'=free_1, B'=2, [ 0>=1+A && 3>=B && free_1>=1 && 1+B==4 && 3*meter_1==-3+B && 0>=1+free_3 && 3>=1 && 2*meter_6==-3+B ], cost: 2+2*meter_6*meter_1+2*meter_6
     26: f4 -> [4] : A'=free_3, B'=1, [ 0>=1+A && 3>=B && free_1>=1 && 1+B==4 && 3*meter_1==-3+B && 2*meter_7==-3+B ], cost: 2*meter_7+2*meter_7*meter_1
     27: f4 -> [4] : A'=free_1, B'=2, [ A>=1 && B==4 && 3*meter_1==-4+B && free_3>=1 && 3>=1 && 2*meter_8==-4+B ], cost: 2*meter_8*meter_1+2*meter_8
     28: f4 -> [4] : A'=free_1, B'=2, [ A>=1 && 3>=B && free_1>=1 && 1+B==4 && 3*meter_1==-3+B && free_3>=1 && 3>=1 && 2*meter_8==-3+B ], cost: 2+2*meter_8*meter_1+2*meter_8
     29: f4 -> [4] : A'=free_3, B'=1, [ A>=1 && 3>=B && free_1>=1 && 1+B==4 && 3*meter_1==-3+B && 2*meter_9==-3+B ], cost: 2*meter_9*meter_1+2*meter_9
     30: f4 -> [4] : A'=free_1, B'=3, [ 0>=1+A && B==4 && 3*meter==-4+B && 0>=1+free_3 && 3>=1 && 2*meter_2==-4+B && 0>=1+free_1 && 3>=2 ], cost: -8+2*(-4+B)*meter_2*meter+2*B+2*(-4+B)*meter_2
     31: f4 -> [4] : A'=free_1, B'=3, [ 0>=1+A && 3>=B && 0>=1+free_1 && 1+B==4 && 3*meter==-3+B && 0>=1+free_3 && 3>=1 && 2*meter_2==-3+B && 0>=1+free_1 && 3>=2 ], cost: -4+2*(-3+B)*meter_2+2*B+2*(-3+B)*meter_2*meter
     32: f4 -> [4] : A'=free_1, B'=2, [ 0>=1+A && 3>=B && 0>=1+free_1 && 1+B==4 && 3*meter==-3+B && 0>=1+free_3 && 3>=1 && 2*meter_2==-3+B ], cost: -6+2*(-3+B)*meter_2+2*B+2*(-3+B)*meter_2*meter
     33: f4 -> [4] : A'=free_1, B'=3, [ 0>=1+A && B==4 && 3*meter==-4+B && 0>=1+free_3 && 3>=1 && 2*meter_2==-4+B && free_1>=1 && 3>=2 ], cost: -8+2*(-4+B)*meter_2*meter+2*B+2*(-4+B)*meter_2
     34: f4 -> [4] : A'=free_1, B'=2, [ A>=1 && 3>=B && 0>=1+free_1 && 1+B==4 && 3*meter==-3+B && 0>=1+free_3 && 3>=1 && 2*meter_2==-3+B ], cost: -6+2*(-3+B)*meter_2+2*B+2*(-3+B)*meter_2*meter
     35: f4 -> [4] : A'=free_1, B'=3, [ 0>=1+A && 3>=B && 0>=1+free_1 && 1+B==4 && 3*meter==-3+B && 0>=1+free_3 && 3>=1 && 2*meter_2==-3+B && 0>=1+free_1 && 3>=2 ], cost: 12-2*(-3+B)*meter_2-4*B-2*(-3+B)*meter_2*meter
     36: f4 -> [4] : A'=free_1, B'=3, [ 0>=1+A && 3>=B && 0>=1+free_1 && 3>=1+B && 0>=1+free_1 && 2+B==4 && 3*meter==-2+B && 0>=1+free_3 && 3>=1 && 2*meter_2==-2+B && 0>=1+free_1 && 3>=2 ], cost: 10-4*B-2*(-2+B)*meter_2-2*(-2+B)*meter_2*meter
     37: f4 -> [4] : A'=free_1, B'=2, [ 0>=1+A && 3>=B && 0>=1+free_1 && 3>=1+B && 0>=1+free_1 && 2+B==4 && 3*meter==-2+B && 0>=1+free_3 && 3>=1 && 2*meter_2==-2+B ], cost: 8-4*B-2*(-2+B)*meter_2-2*(-2+B)*meter_2*meter
     38: f4 -> [4] : A'=free_1, B'=2, [ 0>=1+A && 3>=B && 0>=1+free_1 && 1+B==4 && 3*meter==-3+B && 0>=1+free_3 && 3>=1 && 2*meter_2==-3+B && 0>=1+free_1 && 3>=2 && 0>=1+free_1 && 3>=3 && 0>=1+free_1 && 4==4 && 3*meter==0 && 0>=1+free_3 && 3>=1 && 2*meter_2==0 ], cost: 2+2*meter_2+2*meter_2*meter
     39: f4 -> [4] : A'=free_1, B'=2, [ A>=1 && 3>=B && 0>=1+free_1 && 3>=1+B && 0>=1+free_1 && 2+B==4 && 3*meter==-2+B && 0>=1+free_3 && 3>=1 && 2*meter_2==-2+B ], cost: 8-4*B-2*(-2+B)*meter_2-2*(-2+B)*meter_2*meter
     40: f4 -> [4] : A'=free_1, B'=2, [ 0>=1+A && 3>=B && 0>=1+free_1 && 1+B==4 && 3*meter==-3+B && 2*meter_3==-3+B && 0>=1+free_3 && 3>=1 ], cost: -6+2*B+2*(-3+B)*meter_3+2*(-3+B)*meter_3*meter
     41: f4 -> [4] : A'=free_1, B'=2, [ 0>=1+A && 3>=B && 0>=1+free_1 && 3>=1+B && 0>=1+free_1 && 2+B==4 && 3*meter==-2+B && 2*meter_3==-2+B && 0>=1+free_3 && 3>=1 ], cost: -2+2*(-2+B)*meter_3+2*B+2*(-2+B)*meter_3*meter
     42: f4 -> [4] : A'=free_3, B'=1, [ 0>=1+A && 3>=B && 0>=1+free_1 && 3>=1+B && 0>=1+free_1 && 2+B==4 && 3*meter==-2+B && 2*meter_3==-2+B && 2*meter_10==-2+B ], cost: 2*meter_3*meter_10+2*meter_3*meter_10*meter+2*meter_10
     43: f4 -> [4] : A'=free_1, B'=2, [ 0>=1+A && 3>=B && 0>=1+free_1 && 1+B==4 && 3*meter==-3+B && 2*meter_3==-3+B && free_3>=1 && 3>=1 ], cost: -6+2*B+2*(-3+B)*meter_3+2*(-3+B)*meter_3*meter
     44: f4 -> [4] : A'=free_1, B'=2, [ A>=1 && 3>=B && 0>=1+free_1 && 3>=1+B && 0>=1+free_1 && 2+B==4 && 3*meter==-2+B && 2*meter_3==-2+B && free_3>=1 && 3>=1 ], cost: -2+2*(-2+B)*meter_3+2*B+2*(-2+B)*meter_3*meter
     45: f4 -> [4] : A'=free_3, B'=1, [ A>=1 && 3>=B && 0>=1+free_1 && 3>=1+B && 0>=1+free_1 && 2+B==4 && 3*meter==-2+B && 2*meter_3==-2+B && 2*meter_11==-2+B ], cost: 2*meter_11+2*meter_11*meter_3*meter+2*meter_11*meter_3
     46: f4 -> [4] : A'=free_1, B'=3, [ 0>=1+A && B==4 && 3*meter==-4+B && free_3>=1 && 3>=1 && 2*meter_4==-4+B && 0>=1+free_1 && 3>=2 ], cost: -8+2*B+2*(-4+B)*meter_4*meter+2*(-4+B)*meter_4
     47: f4 -> [4] : A'=free_1, B'=3, [ 0>=1+A && 3>=B && 0>=1+free_1 && 1+B==4 && 3*meter==-3+B && free_3>=1 && 3>=1 && 2*meter_4==-3+B && 0>=1+free_1 && 3>=2 ], cost: -4+2*B+2*(-3+B)*meter_4*meter+2*(-3+B)*meter_4
     48: f4 -> [4] : A'=free_1, B'=2, [ 0>=1+A && 3>=B && 0>=1+free_1 && 1+B==4 && 3*meter==-3+B && free_3>=1 && 3>=1 && 2*meter_4==-3+B ], cost: -6+2*B+2*(-3+B)*meter_4*meter+2*(-3+B)*meter_4
     49: f4 -> [4] : A'=free_1, B'=3, [ 0>=1+A && B==4 && 3*meter==-4+B && free_3>=1 && 3>=1 && 2*meter_4==-4+B && free_1>=1 && 3>=2 ], cost: -8+2*B+2*(-4+B)*meter_4*meter+2*(-4+B)*meter_4
     50: f4 -> [4] : A'=free_1, B'=2, [ A>=1 && 3>=B && 0>=1+free_1 && 1+B==4 && 3*meter==-3+B && free_3>=1 && 3>=1 && 2*meter_4==-3+B ], cost: -6+2*B+2*(-3+B)*meter_4*meter+2*(-3+B)*meter_4
     51: f4 -> [4] : A'=free_1, B'=3, [ A>=1 && 3>=B && 0>=1+free_1 && 1+B==4 && 3*meter==-3+B && free_3>=1 && 3>=1 && 2*meter_4==-3+B && 0>=1+free_1 && 3>=2 ], cost: 12-4*B-2*(-3+B)*meter_4*meter-2*(-3+B)*meter_4
     52: f4 -> [4] : A'=free_1, B'=2, [ A>=1 && 3>=B && 0>=1+free_1 && 1+B==4 && 3*meter==-3+B && 2*meter_5==-3+B && 0>=1+free_3 && 3>=1 ], cost: -6+2*(-3+B)*meter_5*meter+2*B+2*(-3+B)*meter_5
     53: f4 -> [4] : A'=free_1, B'=2, [ A>=1 && 3>=B && 0>=1+free_1 && 1+B==4 && 3*meter==-3+B && 2*meter_5==-3+B && free_3>=1 && 3>=1 ], cost: -6+2*(-3+B)*meter_5*meter+2*B+2*(-3+B)*meter_5
     54: f4 -> [4] : A'=free_1, B'=3, [ A>=1 && B==4 && 3*meter_1==-4+B && 0>=1+free_3 && 3>=1 && 2*meter_6==-4+B && 0>=1+free_1 && 3>=2 ], cost: -8+2*(-4+B)*meter_6+2*B+2*(-4+B)*meter_6*meter_1
     55: f4 -> [4] : A'=free_1, B'=2, [ 0>=1+A && 3>=B && free_1>=1 && 1+B==4 && 3*meter_1==-3+B && 0>=1+free_3 && 3>=1 && 2*meter_6==-3+B ], cost: -6+2*B+2*(-3+B)*meter_6*meter_1+2*(-3+B)*meter_6
     56: f4 -> [4] : A'=free_1, B'=3, [ A>=1 && B==4 && 3*meter_1==-4+B && 0>=1+free_3 && 3>=1 && 2*meter_6==-4+B && free_1>=1 && 3>=2 ], cost: -8+2*(-4+B)*meter_6+2*B+2*(-4+B)*meter_6*meter_1
     57: f4 -> [4] : A'=free_1, B'=3, [ A>=1 && 3>=B && free_1>=1 && 1+B==4 && 3*meter_1==-3+B && 0>=1+free_3 && 3>=1 && 2*meter_6==-3+B && free_1>=1 && 3>=2 ], cost: -4+2*B+2*(-3+B)*meter_6*meter_1+2*(-3+B)*meter_6
     58: f4 -> [4] : A'=free_1, B'=2, [ A>=1 && 3>=B && free_1>=1 && 1+B==4 && 3*meter_1==-3+B && 0>=1+free_3 && 3>=1 && 2*meter_6==-3+B ], cost: -6+2*B+2*(-3+B)*meter_6*meter_1+2*(-3+B)*meter_6
     59: f4 -> [4] : A'=free_1, B'=3, [ 0>=1+A && 3>=B && free_1>=1 && 1+B==4 && 3*meter_1==-3+B && 0>=1+free_3 && 3>=1 && 2*meter_6==-3+B && free_1>=1 && 3>=2 ], cost: 12-4*B-2*(-3+B)*meter_6*meter_1-2*(-3+B)*meter_6
     60: f4 -> [4] : A'=free_1, B'=2, [ 0>=1+A && 3>=B && free_1>=1 && 1+B==4 && 3*meter_1==-3+B && 2*meter_7==-3+B && 0>=1+free_3 && 3>=1 ], cost: -6+2*B+2*(-3+B)*meter_7+2*(-3+B)*meter_7*meter_1
     61: f4 -> [4] : A'=free_1, B'=2, [ 0>=1+A && 3>=B && free_1>=1 && 1+B==4 && 3*meter_1==-3+B && 2*meter_7==-3+B && free_3>=1 && 3>=1 ], cost: -6+2*B+2*(-3+B)*meter_7+2*(-3+B)*meter_7*meter_1
     62: f4 -> [4] : A'=free_1, B'=3, [ A>=1 && B==4 && 3*meter_1==-4+B && free_3>=1 && 3>=1 && 2*meter_8==-4+B && 0>=1+free_1 && 3>=2 ], cost: -8+2*B+2*(-4+B)*meter_8*meter_1+2*(-4+B)*meter_8
     63: f4 -> [4] : A'=free_1, B'=2, [ 0>=1+A && 3>=B && free_1>=1 && 1+B==4 && 3*meter_1==-3+B && free_3>=1 && 3>=1 && 2*meter_8==-3+B ], cost: -6+2*(-3+B)*meter_8*meter_1+2*B+2*(-3+B)*meter_8
     64: f4 -> [4] : A'=free_1, B'=3, [ A>=1 && B==4 && 3*meter_1==-4+B && free_3>=1 && 3>=1 && 2*meter_8==-4+B && free_1>=1 && 3>=2 ], cost: -8+2*B+2*(-4+B)*meter_8*meter_1+2*(-4+B)*meter_8
     65: f4 -> [4] : A'=free_1, B'=3, [ A>=1 && 3>=B && free_1>=1 && 1+B==4 && 3*meter_1==-3+B && free_3>=1 && 3>=1 && 2*meter_8==-3+B && free_1>=1 && 3>=2 ], cost: -4+2*(-3+B)*meter_8*meter_1+2*B+2*(-3+B)*meter_8
     66: f4 -> [4] : A'=free_1, B'=2, [ A>=1 && 3>=B && free_1>=1 && 1+B==4 && 3*meter_1==-3+B && free_3>=1 && 3>=1 && 2*meter_8==-3+B ], cost: -6+2*(-3+B)*meter_8*meter_1+2*B+2*(-3+B)*meter_8
     67: f4 -> [4] : A'=free_1, B'=2, [ 0>=1+A && 3>=B && free_1>=1 && 3>=1+B && free_1>=1 && 2+B==4 && 3*meter_1==-2+B && free_3>=1 && 3>=1 && 2*meter_8==-2+B ], cost: 8-2*(-2+B)*meter_8*meter_1-4*B-2*(-2+B)*meter_8
     68: f4 -> [4] : A'=free_1, B'=3, [ A>=1 && 3>=B && free_1>=1 && 1+B==4 && 3*meter_1==-3+B && free_3>=1 && 3>=1 && 2*meter_8==-3+B && free_1>=1 && 3>=2 ], cost: 12-2*(-3+B)*meter_8*meter_1-4*B-2*(-3+B)*meter_8
     69: f4 -> [4] : A'=free_1, B'=3, [ A>=1 && 3>=B && free_1>=1 && 3>=1+B && free_1>=1 && 2+B==4 && 3*meter_1==-2+B && free_3>=1 && 3>=1 && 2*meter_8==-2+B && free_1>=1 && 3>=2 ], cost: 10-2*(-2+B)*meter_8*meter_1-4*B-2*(-2+B)*meter_8
     70: f4 -> [4] : A'=free_1, B'=2, [ A>=1 && 3>=B && free_1>=1 && 3>=1+B && free_1>=1 && 2+B==4 && 3*meter_1==-2+B && free_3>=1 && 3>=1 && 2*meter_8==-2+B ], cost: 8-2*(-2+B)*meter_8*meter_1-4*B-2*(-2+B)*meter_8
     71: f4 -> [4] : A'=free_1, B'=2, [ A>=1 && 3>=B && free_1>=1 && 1+B==4 && 3*meter_1==-3+B && free_3>=1 && 3>=1 && 2*meter_8==-3+B && free_1>=1 && 3>=2 && free_1>=1 && 3>=3 && free_1>=1 && 4==4 && 3*meter_1==0 && free_3>=1 && 3>=1 && 2*meter_8==0 ], cost: 2+2*meter_8*meter_1+2*meter_8
     72: f4 -> [4] : A'=free_1, B'=2, [ A>=1 && 3>=B && free_1>=1 && 1+B==4 && 3*meter_1==-3+B && 2*meter_9==-3+B && 0>=1+free_3 && 3>=1 ], cost: -6+2*(-3+B)*meter_9*meter_1+2*B+2*(-3+B)*meter_9
     73: f4 -> [4] : A'=free_1, B'=2, [ 0>=1+A && 3>=B && free_1>=1 && 3>=1+B && free_1>=1 && 2+B==4 && 3*meter_1==-2+B && 2*meter_9==-2+B && 0>=1+free_3 && 3>=1 ], cost: -2+2*B+2*(-2+B)*meter_9+2*(-2+B)*meter_9*meter_1
     74: f4 -> [4] : A'=free_3, B'=1, [ 0>=1+A && 3>=B && free_1>=1 && 3>=1+B && free_1>=1 && 2+B==4 && 3*meter_1==-2+B && 2*meter_9==-2+B && 2*meter_12==-2+B ], cost: 2*meter_12+2*meter_12*meter_9*meter_1+2*meter_12*meter_9
     75: f4 -> [4] : A'=free_1, B'=2, [ A>=1 && 3>=B && free_1>=1 && 1+B==4 && 3*meter_1==-3+B && 2*meter_9==-3+B && free_3>=1 && 3>=1 ], cost: -6+2*(-3+B)*meter_9*meter_1+2*B+2*(-3+B)*meter_9
     76: f4 -> [4] : A'=free_1, B'=2, [ A>=1 && 3>=B && free_1>=1 && 3>=1+B && free_1>=1 && 2+B==4 && 3*meter_1==-2+B && 2*meter_9==-2+B && free_3>=1 && 3>=1 ], cost: -2+2*B+2*(-2+B)*meter_9+2*(-2+B)*meter_9*meter_1
     77: f4 -> [4] : A'=free_3, B'=1, [ A>=1 && 3>=B && free_1>=1 && 3>=1+B && free_1>=1 && 2+B==4 && 3*meter_1==-2+B && 2*meter_9==-2+B && 2*meter_13==-2+B ], cost: 2*meter_9*meter_13*meter_1+2*meter_13+2*meter_9*meter_13
     78: f4 -> [4] : A'=free_1, B'=3, [ 0>=1+A && 3>=B && 0>=1+free_1 && 1+B==4 && 3*meter==-3+B && 0>=1+free_3 && 3>=1 && 2*meter_2==-3+B && 0>=1+free_1 && 3>=2 && 0>=1+free_1 && 3>=3 && 0>=1+free_1 && 4==4 && 3*meter==0 && 0>=1+free_3 && 3>=1 && 2*meter_2==0 && 0>=1+free_1 && 3>=2 ], cost: 12-2*(-3+B)*meter_2-4*B-2*(-3+B)*meter_2*meter
     79: f4 -> [4] : A'=free_1, B'=3, [ 0>=1+A && 3>=B && 0>=1+free_1 && 3>=1+B && 0>=1+free_1 && 2+B==4 && 3*meter==-2+B && 0>=1+free_3 && 3>=1 && 2*meter_2==-2+B && 0>=1+free_1 && 3>=2 && 0>=1+free_1 && 3>=3 && 0>=1+free_1 && 4==4 && 3*meter==0 && 0>=1+free_3 && 3>=1 && 2*meter_2==0 && 0>=1+free_1 && 3>=2 ], cost: 10-4*B-2*(-2+B)*meter_2-2*(-2+B)*meter_2*meter
     80: f4 -> [4] : A'=free_1, B'=2, [ 0>=1+A && 3>=B && 0>=1+free_1 && 3>=1+B && 0>=1+free_1 && 2+B==4 && 3*meter==-2+B && 0>=1+free_3 && 3>=1 && 2*meter_2==-2+B && 0>=1+free_1 && 3>=2 && 0>=1+free_1 && 3>=3 && 0>=1+free_1 && 4==4 && 3*meter==0 && 0>=1+free_3 && 3>=1 && 2*meter_2==0 ], cost: 8-4*B-2*(-2+B)*meter_2-2*(-2+B)*meter_2*meter
     81: f4 -> [4] : A'=free_1, B'=2, [ 0>=1+A && 3>=B && 0>=1+free_1 && 1+B==4 && 3*meter==-3+B && 0>=1+free_3 && 3>=1 && 2*meter_2==-3+B && 0>=1+free_1 && 3>=2 && 0>=1+free_1 && 3>=3 && 0>=1+free_1 && 4==4 && 3*meter==0 && 0>=1+free_3 && 3>=1 && 2*meter_2==0 && 0>=1+free_1 && 3>=2 && 0>=1+free_1 && 3>=3 && 0>=1+free_1 && 4==4 && 3*meter==0 && 0>=1+free_3 && 3>=1 && 2*meter_2==0 && 0>=1+free_1 && 3>=2 && 0>=1+free_1 && 3>=3 && 0>=1+free_1 && 4==4 && 3*meter==0 && 0>=1+free_3 && 3>=1 && 2*meter_2==0 ], cost: 2+2*meter_2+2*meter_2*meter
     82: f4 -> [4] : A'=free_1, B'=2, [ A>=1 && 3>=B && 0>=1+free_1 && 3>=1+B && 0>=1+free_1 && 2+B==4 && 3*meter==-2+B && 0>=1+free_3 && 3>=1 && 2*meter_2==-2+B && 0>=1+free_1 && 3>=2 && 0>=1+free_1 && 3>=3 && 0>=1+free_1 && 4==4 && 3*meter==0 && 0>=1+free_3 && 3>=1 && 2*meter_2==0 ], cost: 8-4*B-2*(-2+B)*meter_2-2*(-2+B)*meter_2*meter
     83: f4 -> [4] : A'=free_1, B'=2, [ 0>=1+A && 3>=B && 0>=1+free_1 && 3>=1+B && 0>=1+free_1 && 2+B==4 && 3*meter==-2+B && 2*meter_3==-2+B && 2*meter_10==-2+B && 0>=1+free_3 && 3>=1 ], cost: 4-2*B-2*(-2+B)*meter_10-2*(-2+B)*meter_3*meter_10-2*(-2+B)*meter_3*meter_10*meter
     84: f4 -> [4] : A'=free_1, B'=2, [ 0>=1+A && 3>=B && 0>=1+free_1 && 3>=1+B && 0>=1+free_1 && 3>=2+B && 0>=1+free_1 && 3+B==4 && 3*meter==-1+B && 2*meter_3==-1+B && 2*meter_10==-1+B && 0>=1+free_3 && 3>=1 ], cost: 4-2*B-2*meter_10*(-1+B)-2*meter_3*meter_10*meter*(-1+B)-2*meter_3*meter_10*(-1+B)
     85: f4 -> [4] : A'=free_3, B'=1, [ 0>=1+A && 3>=B && 0>=1+free_1 && 3>=1+B && 0>=1+free_1 && 3>=2+B && 0>=1+free_1 && 3+B==4 && 3*meter==-1+B && 2*meter_3==-1+B && 2*meter_10==-1+B ], cost: 2-2*B-2*meter_10*(-1+B)-2*meter_3*meter_10*meter*(-1+B)-2*meter_3*meter_10*(-1+B)
     86: f4 -> [4] : A'=free_3, B'=1, [ 0>=1+A && 3>=B && 0>=1+free_1 && 3>=1+B && 0>=1+free_1 && 2+B==4 && 3*meter==-2+B && 2*meter_3==-2+B && 2*meter_10==-2+B && 0>=1+free_3 && 3>=1 && 0>=1+free_1 && 3>=2 && 0>=1+free_1 && 3>=3 && 0>=1+free_1 && 4==4 && 3*meter==0 && 2*meter_3==0 && 2*meter_10==0 ], cost: 2*meter_3*meter_10+2*meter_3*meter_10*meter+2*meter_10
     87: f4 -> [4] : A'=free_1, B'=2, [ 0>=1+A && 3>=B && 0>=1+free_1 && 3>=1+B && 0>=1+free_1 && 2+B==4 && 3*meter==-2+B && 2*meter_3==-2+B && 2*meter_10==-2+B && free_3>=1 && 3>=1 ], cost: 4-2*B-2*(-2+B)*meter_10-2*(-2+B)*meter_3*meter_10-2*(-2+B)*meter_3*meter_10*meter
     88: f4 -> [4] : A'=free_1, B'=2, [ A>=1 && 3>=B && 0>=1+free_1 && 3>=1+B && 0>=1+free_1 && 3>=2+B && 0>=1+free_1 && 3+B==4 && 3*meter==-1+B && 2*meter_3==-1+B && 2*meter_10==-1+B && free_3>=1 && 3>=1 ], cost: 4-2*B-2*meter_10*(-1+B)-2*meter_3*meter_10*meter*(-1+B)-2*meter_3*meter_10*(-1+B)
     89: f4 -> [4] : A'=free_3, B'=1, [ A>=1 && 3>=B && 0>=1+free_1 && 3>=1+B && 0>=1+free_1 && 3>=2+B && 0>=1+free_1 && 3+B==4 && 3*meter==-1+B && 2*meter_3==-1+B && 2*meter_10==-1+B ], cost: 2-2*B-2*meter_10*(-1+B)-2*meter_3*meter_10*meter*(-1+B)-2*meter_3*meter_10*(-1+B)
     90: f4 -> [4] : A'=free_3, B'=1, [ 0>=1+A && 3>=B && 0>=1+free_1 && 3>=1+B && 0>=1+free_1 && 2+B==4 && 3*meter==-2+B && 2*meter_3==-2+B && 2*meter_10==-2+B && free_3>=1 && 3>=1 && 0>=1+free_1 && 3>=2 && 0>=1+free_1 && 3>=3 && 0>=1+free_1 && 4==4 && 3*meter==0 && 2*meter_3==0 && 2*meter_10==0 ], cost: 2*meter_3*meter_10+2*meter_3*meter_10*meter+2*meter_10
     91: f4 -> [4] : A'=free_1, B'=2, [ A>=1 && 3>=B && 0>=1+free_1 && 3>=1+B && 0>=1+free_1 && 2+B==4 && 3*meter==-2+B && 2*meter_3==-2+B && 2*meter_11==-2+B && 0>=1+free_3 && 3>=1 ], cost: 4-2*(-2+B)*meter_11*meter_3*meter-2*B-2*(-2+B)*meter_11*meter_3-2*(-2+B)*meter_11
     92: f4 -> [4] : A'=free_1, B'=2, [ A>=1 && 3>=B && 0>=1+free_1 && 3>=1+B && 0>=1+free_1 && 2+B==4 && 3*meter==-2+B && 2*meter_3==-2+B && 2*meter_11==-2+B && free_3>=1 && 3>=1 ], cost: 4-2*(-2+B)*meter_11*meter_3*meter-2*B-2*(-2+B)*meter_11*meter_3-2*(-2+B)*meter_11
     93: f4 -> [4] : A'=free_1, B'=2, [ 0>=1+A && 3>=B && free_1>=1 && 3>=1+B && free_1>=1 && 2+B==4 && 3*meter_1==-2+B && free_3>=1 && 3>=1 && 2*meter_8==-2+B && free_1>=1 && 3>=2 && free_1>=1 && 3>=3 && free_1>=1 && 4==4 && 3*meter_1==0 && free_3>=1 && 3>=1 && 2*meter_8==0 ], cost: 8-2*(-2+B)*meter_8*meter_1-4*B-2*(-2+B)*meter_8
     94: f4 -> [4] : A'=free_1, B'=3, [ A>=1 && 3>=B && free_1>=1 && 1+B==4 && 3*meter_1==-3+B && free_3>=1 && 3>=1 && 2*meter_8==-3+B && free_1>=1 && 3>=2 && free_1>=1 && 3>=3 && free_1>=1 && 4==4 && 3*meter_1==0 && free_3>=1 && 3>=1 && 2*meter_8==0 && free_1>=1 && 3>=2 ], cost: 12-2*(-3+B)*meter_8*meter_1-4*B-2*(-3+B)*meter_8
     95: f4 -> [4] : A'=free_1, B'=3, [ A>=1 && 3>=B && free_1>=1 && 3>=1+B && free_1>=1 && 2+B==4 && 3*meter_1==-2+B && free_3>=1 && 3>=1 && 2*meter_8==-2+B && free_1>=1 && 3>=2 && free_1>=1 && 3>=3 && free_1>=1 && 4==4 && 3*meter_1==0 && free_3>=1 && 3>=1 && 2*meter_8==0 && free_1>=1 && 3>=2 ], cost: 10-2*(-2+B)*meter_8*meter_1-4*B-2*(-2+B)*meter_8
     96: f4 -> [4] : A'=free_1, B'=2, [ A>=1 && 3>=B && free_1>=1 && 3>=1+B && free_1>=1 && 2+B==4 && 3*meter_1==-2+B && free_3>=1 && 3>=1 && 2*meter_8==-2+B && free_1>=1 && 3>=2 && free_1>=1 && 3>=3 && free_1>=1 && 4==4 && 3*meter_1==0 && free_3>=1 && 3>=1 && 2*meter_8==0 ], cost: 8-2*(-2+B)*meter_8*meter_1-4*B-2*(-2+B)*meter_8
     97: f4 -> [4] : A'=free_1, B'=2, [ A>=1 && 3>=B && free_1>=1 && 1+B==4 && 3*meter_1==-3+B && free_3>=1 && 3>=1 && 2*meter_8==-3+B && free_1>=1 && 3>=2 && free_1>=1 && 3>=3 && free_1>=1 && 4==4 && 3*meter_1==0 && free_3>=1 && 3>=1 && 2*meter_8==0 && free_1>=1 && 3>=2 && free_1>=1 && 3>=3 && free_1>=1 && 4==4 && 3*meter_1==0 && free_3>=1 && 3>=1 && 2*meter_8==0 && free_1>=1 && 3>=2 && free_1>=1 && 3>=3 && free_1>=1 && 4==4 && 3*meter_1==0 && free_3>=1 && 3>=1 && 2*meter_8==0 ], cost: 2+2*meter_8*meter_1+2*meter_8
     98: f4 -> [4] : A'=free_1, B'=2, [ 0>=1+A && 3>=B && free_1>=1 && 3>=1+B && free_1>=1 && 2+B==4 && 3*meter_1==-2+B && 2*meter_9==-2+B && 2*meter_12==-2+B && 0>=1+free_3 && 3>=1 ], cost: 4-2*meter_12*(-2+B)*meter_9-2*meter_12*(-2+B)-2*B-2*meter_12*(-2+B)*meter_9*meter_1
     99: f4 -> [4] : A'=free_1, B'=2, [ 0>=1+A && 3>=B && free_1>=1 && 3>=1+B && free_1>=1 && 2+B==4 && 3*meter_1==-2+B && 2*meter_9==-2+B && 2*meter_12==-2+B && free_3>=1 && 3>=1 ], cost: 4-2*meter_12*(-2+B)*meter_9-2*meter_12*(-2+B)-2*B-2*meter_12*(-2+B)*meter_9*meter_1
    100: f4 -> [4] : A'=free_1, B'=2, [ A>=1 && 3>=B && free_1>=1 && 3>=1+B && free_1>=1 && 2+B==4 && 3*meter_1==-2+B && 2*meter_9==-2+B && 2*meter_13==-2+B && 0>=1+free_3 && 3>=1 ], cost: 4-2*(-2+B)*meter_13-2*B-2*(-2+B)*meter_9*meter_13*meter_1-2*(-2+B)*meter_9*meter_13
    101: f4 -> [4] : A'=free_1, B'=2, [ 0>=1+A && 3>=B && free_1>=1 && 3>=1+B && free_1>=1 && 3>=2+B && free_1>=1 && 3+B==4 && 3*meter_1==-1+B && 2*meter_9==-1+B && 2*meter_13==-1+B && 0>=1+free_3 && 3>=1 ], cost: 4-2*meter_9*meter_13*(-1+B)-2*B-2*meter_13*(-1+B)-2*meter_9*meter_13*(-1+B)*meter_1
    102: f4 -> [4] : A'=free_3, B'=1, [ 0>=1+A && 3>=B && free_1>=1 && 3>=1+B && free_1>=1 && 3>=2+B && free_1>=1 && 3+B==4 && 3*meter_1==-1+B && 2*meter_9==-1+B && 2*meter_13==-1+B ], cost: 2-2*meter_9*meter_13*(-1+B)-2*B-2*meter_13*(-1+B)-2*meter_9*meter_13*(-1+B)*meter_1
    103: f4 -> [4] : A'=free_3, B'=1, [ A>=1 && 3>=B && free_1>=1 && 3>=1+B && free_1>=1 && 2+B==4 && 3*meter_1==-2+B && 2*meter_9==-2+B && 2*meter_13==-2+B && 0>=1+free_3 && 3>=1 && free_1>=1 && 3>=2 && free_1>=1 && 3>=3 && free_1>=1 && 4==4 && 3*meter_1==0 && 2*meter_9==0 && 2*meter_13==0 ], cost: 2*meter_9*meter_13*meter_1+2*meter_13+2*meter_9*meter_13
    104: f4 -> [4] : A'=free_1, B'=2, [ A>=1 && 3>=B && free_1>=1 && 3>=1+B && free_1>=1 && 2+B==4 && 3*meter_1==-2+B && 2*meter_9==-2+B && 2*meter_13==-2+B && free_3>=1 && 3>=1 ], cost: 4-2*(-2+B)*meter_13-2*B-2*(-2+B)*meter_9*meter_13*meter_1-2*(-2+B)*meter_9*meter_13
    105: f4 -> [4] : A'=free_1, B'=2, [ A>=1 && 3>=B && free_1>=1 && 3>=1+B && free_1>=1 && 3>=2+B && free_1>=1 && 3+B==4 && 3*meter_1==-1+B && 2*meter_9==-1+B && 2*meter_13==-1+B && free_3>=1 && 3>=1 ], cost: 4-2*meter_9*meter_13*(-1+B)-2*B-2*meter_13*(-1+B)-2*meter_9*meter_13*(-1+B)*meter_1
    106: f4 -> [4] : A'=free_3, B'=1, [ A>=1 && 3>=B && free_1>=1 && 3>=1+B && free_1>=1 && 3>=2+B && free_1>=1 && 3+B==4 && 3*meter_1==-1+B && 2*meter_9==-1+B && 2*meter_13==-1+B ], cost: 2-2*meter_9*meter_13*(-1+B)-2*B-2*meter_13*(-1+B)-2*meter_9*meter_13*(-1+B)*meter_1
    107: f4 -> [4] : A'=free_3, B'=1, [ A>=1 && 3>=B && free_1>=1 && 3>=1+B && free_1>=1 && 2+B==4 && 3*meter_1==-2+B && 2*meter_9==-2+B && 2*meter_13==-2+B && free_3>=1 && 3>=1 && free_1>=1 && 3>=2 && free_1>=1 && 3>=3 && free_1>=1 && 4==4 && 3*meter_1==0 && 2*meter_9==0 && 2*meter_13==0 ], cost: 2*meter_9*meter_13*meter_1+2*meter_13+2*meter_9*meter_13
    108: f4 -> [4] : [], cost: 0
      2: f0 -> f4 : A'=free, B'=0, [], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
    <empty>


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
    <empty>


Computing complexity for remaining 0 transitions.


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

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

WORST_CASE(Omega(1),?)