Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f20 -> f26 : B'=1, C'=D, [ 0>=1+A ], cost: 1
      1: f20 -> f26 : B'=1, C'=D, [ A>=1 ], cost: 1
      2: f20 -> f26 : A'=0, B'=1, C'=0, D'=0, [ D==0 && A==0 ], cost: 1
      3: f20 -> f26 : A'=0, B'=0, C'=D, [ 0>=1+D && A==0 ], cost: 1
      4: f20 -> f26 : A'=0, B'=0, C'=D, [ D>=1 && A==0 ], cost: 1
     25: f26 -> f26 : C'=1+C, F'=0, G'=free_15, [ 0>=1+free_15 && E>=1+C ], cost: 1
     26: f26 -> f26 : C'=1+C, F'=0, G'=free_16, [ free_16>=1 && E>=1+C ], cost: 1
      5: f26 -> f69 : [ C>=E ], cost: 1
      6: f26 -> f33 : F'=free, [ 0>=1+free && E>=1+C ], cost: 1
      7: f26 -> f33 : F'=free_1, [ free_1>=1 && E>=1+C ], cost: 1
      8: f26 -> f33 : F'=0, G'=0, [ E>=1+C ], cost: 1
     35: f69 -> f71 : A'=0, S'=0, [ S==0 ], cost: 1
     38: f69 -> f74 : A'=0, [ 0>=1+S ], cost: 1
     39: f69 -> f74 : A'=0, [ S>=1 ], cost: 1
     11: f33 -> f33 : H'=1+H, [ Q>=1+H && 0>=2+J ], cost: 1
     12: f33 -> f33 : H'=1+H, [ Q>=1+H && J>=0 ], cost: 1
      9: f33 -> f39 : [ H>=Q ], cost: 1
     10: f33 -> f39 : J'=-1, [ Q>=1+H && 1+J==0 ], cost: 1
     27: f39 -> f26 : C'=1+C, K'=free_17, [ Q>=1+H && 0>=1+free_17 ], cost: 1
     28: f39 -> f26 : C'=1+C, K'=free_18, [ Q>=1+H && free_18>=1 ], cost: 1
     13: f39 -> f69 : [ H>=Q ], cost: 1
     14: f39 -> f47 : K'=0, L'=free_3, M'=free_2, [ Q>=1+H && 0>=1+free_3 ], cost: 1
     15: f39 -> f47 : K'=0, L'=free_5, M'=free_4, [ Q>=1+H && free_5>=1 ], cost: 1
     17: f39 -> f50 : K'=0, L'=0, N'=free_7, [ Q>=1+H ], cost: 1
     29: f47 -> f26 : C'=1+C, [ 0>=1+M ], cost: 1
     30: f47 -> f26 : C'=1+C, [ M>=1 ], cost: 1
     16: f47 -> f50 : M'=0, N'=free_6, [ M==0 ], cost: 1
     31: f50 -> f26 : C'=1+C, P'=1, [ 0>=1+N ], cost: 1
     18: f50 -> f69 : O'=3, P'=1, Q_1'=free_8, [ N>=0 && 0>=free_8 && O==3 ], cost: 1
     19: f50 -> f69 : O'=3, P'=1, Q_1'=free_9, [ N>=0 && free_9>=2 && O==3 ], cost: 1
     20: f50 -> f59 : R'=free_10, [ N>=0 && 2>=O ], cost: 1
     21: f50 -> f59 : R'=free_11, [ N>=0 && O>=4 ], cost: 1
     22: f50 -> f59 : O'=3, Q_1'=1, R'=free_12, [ N>=0 && O==3 ], cost: 1
     23: f59 -> f62 : N'=free_13, [ 10>=R ], cost: 1
     24: f59 -> f62 : N'=free_14, R'=10, [ R>=11 ], cost: 1
     32: f62 -> f26 : C'=1+C, P'=1, [ 0>=1+N ], cost: 1
     33: f62 -> f26 : C'=1+C, J'=K, S'=1+S, [ N>=0 ], cost: 1
     34: f71 -> f71 : [], cost: 1
     36: f74 -> f74 : [], cost: 1
     37: f73 -> f74 : A'=0, [], cost: 1
     40: f76 -> f78 : [], cost: 1
     41: f0 -> f20 : A'=free_21, D'=free_19, E'=free_22, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 ], cost: 1
     42: f0 -> f20 : A'=free_25, D'=free_23, E'=free_26, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 ], cost: 1
     43: f0 -> f20 : A'=free_29, D'=free_27, E'=free_30, H'=0, S'=0, U'=1, V'=free_28, [ T>=4 && free_27>=0 && free_28>=1 ], cost: 1


Simplified the transitions:
  Start location: f0
      0: f20 -> f26 : B'=1, C'=D, [ 0>=1+A ], cost: 1
      1: f20 -> f26 : B'=1, C'=D, [ A>=1 ], cost: 1
      2: f20 -> f26 : A'=0, B'=1, C'=0, D'=0, [ D==0 && A==0 ], cost: 1
      3: f20 -> f26 : A'=0, B'=0, C'=D, [ 0>=1+D && A==0 ], cost: 1
      4: f20 -> f26 : A'=0, B'=0, C'=D, [ D>=1 && A==0 ], cost: 1
     25: f26 -> f26 : C'=1+C, F'=0, G'=free_15, [ 0>=1+free_15 && E>=1+C ], cost: 1
     26: f26 -> f26 : C'=1+C, F'=0, G'=free_16, [ free_16>=1 && E>=1+C ], cost: 1
      5: f26 -> f69 : [ C>=E ], cost: 1
      6: f26 -> f33 : F'=free, [ 0>=1+free && E>=1+C ], cost: 1
      7: f26 -> f33 : F'=free_1, [ free_1>=1 && E>=1+C ], cost: 1
      8: f26 -> f33 : F'=0, G'=0, [ E>=1+C ], cost: 1
     35: f69 -> f71 : A'=0, S'=0, [ S==0 ], cost: 1
     38: f69 -> f74 : A'=0, [ 0>=1+S ], cost: 1
     39: f69 -> f74 : A'=0, [ S>=1 ], cost: 1
     11: f33 -> f33 : H'=1+H, [ Q>=1+H && 0>=2+J ], cost: 1
     12: f33 -> f33 : H'=1+H, [ Q>=1+H && J>=0 ], cost: 1
      9: f33 -> f39 : [ H>=Q ], cost: 1
     10: f33 -> f39 : J'=-1, [ Q>=1+H && 1+J==0 ], cost: 1
     27: f39 -> f26 : C'=1+C, K'=free_17, [ Q>=1+H && 0>=1+free_17 ], cost: 1
     28: f39 -> f26 : C'=1+C, K'=free_18, [ Q>=1+H && free_18>=1 ], cost: 1
     13: f39 -> f69 : [ H>=Q ], cost: 1
     14: f39 -> f47 : K'=0, L'=free_3, M'=free_2, [ Q>=1+H && 0>=1+free_3 ], cost: 1
     15: f39 -> f47 : K'=0, L'=free_5, M'=free_4, [ Q>=1+H && free_5>=1 ], cost: 1
     17: f39 -> f50 : K'=0, L'=0, N'=free_7, [ Q>=1+H ], cost: 1
     29: f47 -> f26 : C'=1+C, [ 0>=1+M ], cost: 1
     30: f47 -> f26 : C'=1+C, [ M>=1 ], cost: 1
     16: f47 -> f50 : M'=0, N'=free_6, [ M==0 ], cost: 1
     31: f50 -> f26 : C'=1+C, P'=1, [ 0>=1+N ], cost: 1
     18: f50 -> f69 : O'=3, P'=1, Q_1'=free_8, [ N>=0 && 0>=free_8 && O==3 ], cost: 1
     19: f50 -> f69 : O'=3, P'=1, Q_1'=free_9, [ N>=0 && free_9>=2 && O==3 ], cost: 1
     20: f50 -> f59 : R'=free_10, [ N>=0 && 2>=O ], cost: 1
     21: f50 -> f59 : R'=free_11, [ N>=0 && O>=4 ], cost: 1
     22: f50 -> f59 : O'=3, Q_1'=1, R'=free_12, [ N>=0 && O==3 ], cost: 1
     23: f59 -> f62 : N'=free_13, [ 10>=R ], cost: 1
     24: f59 -> f62 : N'=free_14, R'=10, [ R>=11 ], cost: 1
     32: f62 -> f26 : C'=1+C, P'=1, [ 0>=1+N ], cost: 1
     33: f62 -> f26 : C'=1+C, J'=K, S'=1+S, [ N>=0 ], cost: 1
     34: f71 -> f71 : [], cost: 1
     36: f74 -> f74 : [], cost: 1
     41: f0 -> f20 : A'=free_21, D'=free_19, E'=free_22, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 ], cost: 1
     42: f0 -> f20 : A'=free_25, D'=free_23, E'=free_26, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 ], cost: 1
     43: f0 -> f20 : A'=free_29, D'=free_27, E'=free_30, H'=0, S'=0, U'=1, V'=free_28, [ T>=4 && free_27>=0 && free_28>=1 ], cost: 1

Eliminating 2 self-loops for location f26
  Self-Loop 25 has the metering function: E-C, resulting in the new transition 44.
  Self-Loop 26 has the metering function: E-C, resulting in the new transition 45.
  Removing the self-loops: 25 26.
Eliminating 2 self-loops for location f33
  Self-Loop 11 has the metering function: -H+Q, resulting in the new transition 46.
  Self-Loop 12 has the metering function: -H+Q, resulting in the new transition 47.
  Removing the self-loops: 11 12.
Eliminating 1 self-loops for location f71
  Self-Loop 34 has unbounded runtime, resulting in the new transition 48.
  Removing the self-loops: 34.
Eliminating 1 self-loops for location f74
  Self-Loop 36 has unbounded runtime, resulting in the new transition 49.
  Removing the self-loops: 36.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f20 -> f26 : B'=1, C'=D, [ 0>=1+A ], cost: 1
      1: f20 -> f26 : B'=1, C'=D, [ A>=1 ], cost: 1
      2: f20 -> f26 : A'=0, B'=1, C'=0, D'=0, [ D==0 && A==0 ], cost: 1
      3: f20 -> f26 : A'=0, B'=0, C'=D, [ 0>=1+D && A==0 ], cost: 1
      4: f20 -> f26 : A'=0, B'=0, C'=D, [ D>=1 && A==0 ], cost: 1
     44: f26 -> [15] : C'=E, F'=0, G'=free_15, [ 0>=1+free_15 && E>=1+C ], cost: E-C
     45: f26 -> [15] : C'=E, F'=0, G'=free_16, [ free_16>=1 && E>=1+C ], cost: E-C
     35: f69 -> f71 : A'=0, S'=0, [ S==0 ], cost: 1
     38: f69 -> f74 : A'=0, [ 0>=1+S ], cost: 1
     39: f69 -> f74 : A'=0, [ S>=1 ], cost: 1
     46: f33 -> [16] : H'=Q, [ Q>=1+H && 0>=2+J ], cost: -H+Q
     47: f33 -> [16] : H'=Q, [ Q>=1+H && J>=0 ], cost: -H+Q
     27: f39 -> f26 : C'=1+C, K'=free_17, [ Q>=1+H && 0>=1+free_17 ], cost: 1
     28: f39 -> f26 : C'=1+C, K'=free_18, [ Q>=1+H && free_18>=1 ], cost: 1
     13: f39 -> f69 : [ H>=Q ], cost: 1
     14: f39 -> f47 : K'=0, L'=free_3, M'=free_2, [ Q>=1+H && 0>=1+free_3 ], cost: 1
     15: f39 -> f47 : K'=0, L'=free_5, M'=free_4, [ Q>=1+H && free_5>=1 ], cost: 1
     17: f39 -> f50 : K'=0, L'=0, N'=free_7, [ Q>=1+H ], cost: 1
     29: f47 -> f26 : C'=1+C, [ 0>=1+M ], cost: 1
     30: f47 -> f26 : C'=1+C, [ M>=1 ], cost: 1
     16: f47 -> f50 : M'=0, N'=free_6, [ M==0 ], cost: 1
     31: f50 -> f26 : C'=1+C, P'=1, [ 0>=1+N ], cost: 1
     18: f50 -> f69 : O'=3, P'=1, Q_1'=free_8, [ N>=0 && 0>=free_8 && O==3 ], cost: 1
     19: f50 -> f69 : O'=3, P'=1, Q_1'=free_9, [ N>=0 && free_9>=2 && O==3 ], cost: 1
     20: f50 -> f59 : R'=free_10, [ N>=0 && 2>=O ], cost: 1
     21: f50 -> f59 : R'=free_11, [ N>=0 && O>=4 ], cost: 1
     22: f50 -> f59 : O'=3, Q_1'=1, R'=free_12, [ N>=0 && O==3 ], cost: 1
     23: f59 -> f62 : N'=free_13, [ 10>=R ], cost: 1
     24: f59 -> f62 : N'=free_14, R'=10, [ R>=11 ], cost: 1
     32: f62 -> f26 : C'=1+C, P'=1, [ 0>=1+N ], cost: 1
     33: f62 -> f26 : C'=1+C, J'=K, S'=1+S, [ N>=0 ], cost: 1
     48: f71 -> [17] : [], cost: INF
     49: f74 -> [18] : [], cost: INF
     41: f0 -> f20 : A'=free_21, D'=free_19, E'=free_22, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 ], cost: 1
     42: f0 -> f20 : A'=free_25, D'=free_23, E'=free_26, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 ], cost: 1
     43: f0 -> f20 : A'=free_29, D'=free_27, E'=free_30, H'=0, S'=0, U'=1, V'=free_28, [ T>=4 && free_27>=0 && free_28>=1 ], cost: 1
      5: [15] -> f69 : [ C>=E ], cost: 1
      6: [15] -> f33 : F'=free, [ 0>=1+free && E>=1+C ], cost: 1
      7: [15] -> f33 : F'=free_1, [ free_1>=1 && E>=1+C ], cost: 1
      8: [15] -> f33 : F'=0, G'=0, [ E>=1+C ], cost: 1
      9: [16] -> f39 : [ H>=Q ], cost: 1
     10: [16] -> f39 : J'=-1, [ Q>=1+H && 1+J==0 ], cost: 1


Applied simple chaining:
  Start location: f0
      0: f20 -> f26 : B'=1, C'=D, [ 0>=1+A ], cost: 1
      1: f20 -> f26 : B'=1, C'=D, [ A>=1 ], cost: 1
      2: f20 -> f26 : A'=0, B'=1, C'=0, D'=0, [ D==0 && A==0 ], cost: 1
      3: f20 -> f26 : A'=0, B'=0, C'=D, [ 0>=1+D && A==0 ], cost: 1
      4: f20 -> f26 : A'=0, B'=0, C'=D, [ D>=1 && A==0 ], cost: 1
     44: f26 -> [15] : C'=E, F'=0, G'=free_15, [ 0>=1+free_15 && E>=1+C ], cost: E-C
     45: f26 -> [15] : C'=E, F'=0, G'=free_16, [ free_16>=1 && E>=1+C ], cost: E-C
     38: f69 -> f74 : A'=0, [ 0>=1+S ], cost: 1
     39: f69 -> f74 : A'=0, [ S>=1 ], cost: 1
     35: f69 -> [17] : A'=0, S'=0, [ S==0 ], cost: INF
     46: f33 -> [16] : H'=Q, [ Q>=1+H && 0>=2+J ], cost: -H+Q
     47: f33 -> [16] : H'=Q, [ Q>=1+H && J>=0 ], cost: -H+Q
     27: f39 -> f26 : C'=1+C, K'=free_17, [ Q>=1+H && 0>=1+free_17 ], cost: 1
     28: f39 -> f26 : C'=1+C, K'=free_18, [ Q>=1+H && free_18>=1 ], cost: 1
     13: f39 -> f69 : [ H>=Q ], cost: 1
     14: f39 -> f47 : K'=0, L'=free_3, M'=free_2, [ Q>=1+H && 0>=1+free_3 ], cost: 1
     15: f39 -> f47 : K'=0, L'=free_5, M'=free_4, [ Q>=1+H && free_5>=1 ], cost: 1
     17: f39 -> f50 : K'=0, L'=0, N'=free_7, [ Q>=1+H ], cost: 1
     29: f47 -> f26 : C'=1+C, [ 0>=1+M ], cost: 1
     30: f47 -> f26 : C'=1+C, [ M>=1 ], cost: 1
     16: f47 -> f50 : M'=0, N'=free_6, [ M==0 ], cost: 1
     31: f50 -> f26 : C'=1+C, P'=1, [ 0>=1+N ], cost: 1
     18: f50 -> f69 : O'=3, P'=1, Q_1'=free_8, [ N>=0 && 0>=free_8 && O==3 ], cost: 1
     19: f50 -> f69 : O'=3, P'=1, Q_1'=free_9, [ N>=0 && free_9>=2 && O==3 ], cost: 1
     20: f50 -> f59 : R'=free_10, [ N>=0 && 2>=O ], cost: 1
     21: f50 -> f59 : R'=free_11, [ N>=0 && O>=4 ], cost: 1
     22: f50 -> f59 : O'=3, Q_1'=1, R'=free_12, [ N>=0 && O==3 ], cost: 1
     23: f59 -> f62 : N'=free_13, [ 10>=R ], cost: 1
     24: f59 -> f62 : N'=free_14, R'=10, [ R>=11 ], cost: 1
     32: f62 -> f26 : C'=1+C, P'=1, [ 0>=1+N ], cost: 1
     33: f62 -> f26 : C'=1+C, J'=K, S'=1+S, [ N>=0 ], cost: 1
     49: f74 -> [18] : [], cost: INF
     41: f0 -> f20 : A'=free_21, D'=free_19, E'=free_22, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 ], cost: 1
     42: f0 -> f20 : A'=free_25, D'=free_23, E'=free_26, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 ], cost: 1
     43: f0 -> f20 : A'=free_29, D'=free_27, E'=free_30, H'=0, S'=0, U'=1, V'=free_28, [ T>=4 && free_27>=0 && free_28>=1 ], cost: 1
      5: [15] -> f69 : [ C>=E ], cost: 1
      6: [15] -> f33 : F'=free, [ 0>=1+free && E>=1+C ], cost: 1
      7: [15] -> f33 : F'=free_1, [ free_1>=1 && E>=1+C ], cost: 1
      8: [15] -> f33 : F'=0, G'=0, [ E>=1+C ], cost: 1
      9: [16] -> f39 : [ H>=Q ], cost: 1
     10: [16] -> f39 : J'=-1, [ Q>=1+H && 1+J==0 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
     62: f26 -> f69 : C'=E, F'=0, G'=free_15, [ 0>=1+free_15 && E>=1+C && E>=E ], cost: 1+E-C
     66: f26 -> f69 : C'=E, F'=0, G'=free_16, [ free_16>=1 && E>=1+C && E>=E ], cost: 1+E-C
     63: f26 -> [19] : C'=E, F'=0, G'=free_15, [ 0>=1+free_15 && E>=1+C ], cost: E-C
     64: f26 -> [20] : C'=E, F'=0, G'=free_15, [ 0>=1+free_15 && E>=1+C ], cost: E-C
     65: f26 -> [21] : C'=E, F'=0, G'=free_15, [ 0>=1+free_15 && E>=1+C ], cost: E-C
     67: f26 -> [22] : C'=E, F'=0, G'=free_16, [ free_16>=1 && E>=1+C ], cost: E-C
     68: f26 -> [23] : C'=E, F'=0, G'=free_16, [ free_16>=1 && E>=1+C ], cost: E-C
     69: f26 -> [24] : C'=E, F'=0, G'=free_16, [ free_16>=1 && E>=1+C ], cost: E-C
     35: f69 -> [17] : A'=0, S'=0, [ S==0 ], cost: INF
     70: f69 -> [18] : A'=0, [ 0>=1+S ], cost: INF
     71: f69 -> [18] : A'=0, [ S>=1 ], cost: INF
     50: f0 -> f26 : A'=free_21, B'=1, C'=free_19, D'=free_19, E'=free_22, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && 0>=1+free_21 ], cost: 2
     51: f0 -> f26 : A'=free_21, B'=1, C'=free_19, D'=free_19, E'=free_22, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_21>=1 ], cost: 2
     53: f0 -> f26 : A'=0, B'=0, C'=free_19, D'=free_19, E'=free_22, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_19>=1 && free_21==0 ], cost: 2
     55: f0 -> f26 : A'=free_25, B'=1, C'=free_23, D'=free_23, E'=free_26, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_25>=1 ], cost: 2
     56: f0 -> f26 : A'=0, B'=1, C'=0, D'=0, E'=free_26, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 ], cost: 2


Applied chaining over branches and pruning:
  Start location: f0
     35: f69 -> [17] : A'=0, S'=0, [ S==0 ], cost: INF
     70: f69 -> [18] : A'=0, [ 0>=1+S ], cost: INF
     71: f69 -> [18] : A'=0, [ S>=1 ], cost: INF
     73: f0 -> f69 : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && 0>=1+free_21 && free_16>=1 && free_22>=1+free_19 && free_22>=free_22 ], cost: 3+free_22-free_19
     81: f0 -> f69 : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_21>=1 && free_16>=1 && free_22>=1+free_19 && free_22>=free_22 ], cost: 3+free_22-free_19
     88: f0 -> f69 : A'=0, B'=0, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_19>=1 && free_21==0 && 0>=1+free_15 && free_22>=1+free_19 && free_22>=free_22 ], cost: 3+free_22-free_19
    104: f0 -> f69 : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_15, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && 0>=1+free_15 && free_26>=1 && free_26>=free_26 ], cost: 3+free_26
    105: f0 -> f69 : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_16, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && free_16>=1 && free_26>=1 && free_26>=free_26 ], cost: 3+free_26
     74: f0 -> [19] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && 0>=1+free_21 && 0>=1+free_15 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     82: f0 -> [19] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_21>=1 && 0>=1+free_15 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     90: f0 -> [19] : A'=0, B'=0, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_19>=1 && free_21==0 && 0>=1+free_15 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     98: f0 -> [19] : A'=free_25, B'=1, C'=free_26, D'=free_23, E'=free_26, F'=0, G'=free_15, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_25>=1 && 0>=1+free_15 && free_26>=1+free_23 ], cost: 2+free_26-free_23
    106: f0 -> [19] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_15, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && 0>=1+free_15 && free_26>=1 ], cost: 2+free_26
     75: f0 -> [20] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && 0>=1+free_21 && 0>=1+free_15 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     83: f0 -> [20] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_21>=1 && 0>=1+free_15 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     91: f0 -> [20] : A'=0, B'=0, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_19>=1 && free_21==0 && 0>=1+free_15 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     99: f0 -> [20] : A'=free_25, B'=1, C'=free_26, D'=free_23, E'=free_26, F'=0, G'=free_15, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_25>=1 && 0>=1+free_15 && free_26>=1+free_23 ], cost: 2+free_26-free_23
    107: f0 -> [20] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_15, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && 0>=1+free_15 && free_26>=1 ], cost: 2+free_26
     76: f0 -> [21] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && 0>=1+free_21 && 0>=1+free_15 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     84: f0 -> [21] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_21>=1 && 0>=1+free_15 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     92: f0 -> [21] : A'=0, B'=0, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_19>=1 && free_21==0 && 0>=1+free_15 && free_22>=1+free_19 ], cost: 2+free_22-free_19
    100: f0 -> [21] : A'=free_25, B'=1, C'=free_26, D'=free_23, E'=free_26, F'=0, G'=free_15, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_25>=1 && 0>=1+free_15 && free_26>=1+free_23 ], cost: 2+free_26-free_23
    108: f0 -> [21] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_15, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && 0>=1+free_15 && free_26>=1 ], cost: 2+free_26
     77: f0 -> [22] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && 0>=1+free_21 && free_16>=1 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     85: f0 -> [22] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_21>=1 && free_16>=1 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     93: f0 -> [22] : A'=0, B'=0, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_19>=1 && free_21==0 && free_16>=1 && free_22>=1+free_19 ], cost: 2+free_22-free_19
    101: f0 -> [22] : A'=free_25, B'=1, C'=free_26, D'=free_23, E'=free_26, F'=0, G'=free_16, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_25>=1 && free_16>=1 && free_26>=1+free_23 ], cost: 2+free_26-free_23
    109: f0 -> [22] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_16, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && free_16>=1 && free_26>=1 ], cost: 2+free_26
     78: f0 -> [23] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && 0>=1+free_21 && free_16>=1 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     86: f0 -> [23] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_21>=1 && free_16>=1 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     94: f0 -> [23] : A'=0, B'=0, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_19>=1 && free_21==0 && free_16>=1 && free_22>=1+free_19 ], cost: 2+free_22-free_19
    102: f0 -> [23] : A'=free_25, B'=1, C'=free_26, D'=free_23, E'=free_26, F'=0, G'=free_16, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_25>=1 && free_16>=1 && free_26>=1+free_23 ], cost: 2+free_26-free_23
    110: f0 -> [23] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_16, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && free_16>=1 && free_26>=1 ], cost: 2+free_26
     79: f0 -> [24] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && 0>=1+free_21 && free_16>=1 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     87: f0 -> [24] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_21>=1 && free_16>=1 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     95: f0 -> [24] : A'=0, B'=0, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_19>=1 && free_21==0 && free_16>=1 && free_22>=1+free_19 ], cost: 2+free_22-free_19
    103: f0 -> [24] : A'=free_25, B'=1, C'=free_26, D'=free_23, E'=free_26, F'=0, G'=free_16, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_25>=1 && free_16>=1 && free_26>=1+free_23 ], cost: 2+free_26-free_23
    111: f0 -> [24] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_16, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && free_16>=1 && free_26>=1 ], cost: 2+free_26


Applied chaining over branches and pruning:
  Start location: f0
    112: f0 -> [17] : A'=0, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && 0>=1+free_21 && free_16>=1 && free_22>=1+free_19 && free_22>=free_22 && 0==0 ], cost: INF
    115: f0 -> [17] : A'=0, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_21>=1 && free_16>=1 && free_22>=1+free_19 && free_22>=free_22 && 0==0 ], cost: INF
    118: f0 -> [17] : A'=0, B'=0, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_19>=1 && free_21==0 && 0>=1+free_15 && free_22>=1+free_19 && free_22>=free_22 && 0==0 ], cost: INF
    121: f0 -> [17] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_15, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && 0>=1+free_15 && free_26>=1 && free_26>=free_26 && 0==0 ], cost: INF
    124: f0 -> [17] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_16, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && free_16>=1 && free_26>=1 && free_26>=free_26 && 0==0 ], cost: INF
     74: f0 -> [19] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && 0>=1+free_21 && 0>=1+free_15 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     82: f0 -> [19] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_21>=1 && 0>=1+free_15 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     90: f0 -> [19] : A'=0, B'=0, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_19>=1 && free_21==0 && 0>=1+free_15 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     98: f0 -> [19] : A'=free_25, B'=1, C'=free_26, D'=free_23, E'=free_26, F'=0, G'=free_15, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_25>=1 && 0>=1+free_15 && free_26>=1+free_23 ], cost: 2+free_26-free_23
    106: f0 -> [19] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_15, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && 0>=1+free_15 && free_26>=1 ], cost: 2+free_26
     75: f0 -> [20] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && 0>=1+free_21 && 0>=1+free_15 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     83: f0 -> [20] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_21>=1 && 0>=1+free_15 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     91: f0 -> [20] : A'=0, B'=0, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_19>=1 && free_21==0 && 0>=1+free_15 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     99: f0 -> [20] : A'=free_25, B'=1, C'=free_26, D'=free_23, E'=free_26, F'=0, G'=free_15, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_25>=1 && 0>=1+free_15 && free_26>=1+free_23 ], cost: 2+free_26-free_23
    107: f0 -> [20] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_15, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && 0>=1+free_15 && free_26>=1 ], cost: 2+free_26
     76: f0 -> [21] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && 0>=1+free_21 && 0>=1+free_15 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     84: f0 -> [21] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_21>=1 && 0>=1+free_15 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     92: f0 -> [21] : A'=0, B'=0, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_19>=1 && free_21==0 && 0>=1+free_15 && free_22>=1+free_19 ], cost: 2+free_22-free_19
    100: f0 -> [21] : A'=free_25, B'=1, C'=free_26, D'=free_23, E'=free_26, F'=0, G'=free_15, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_25>=1 && 0>=1+free_15 && free_26>=1+free_23 ], cost: 2+free_26-free_23
    108: f0 -> [21] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_15, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && 0>=1+free_15 && free_26>=1 ], cost: 2+free_26
     77: f0 -> [22] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && 0>=1+free_21 && free_16>=1 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     85: f0 -> [22] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_21>=1 && free_16>=1 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     93: f0 -> [22] : A'=0, B'=0, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_19>=1 && free_21==0 && free_16>=1 && free_22>=1+free_19 ], cost: 2+free_22-free_19
    101: f0 -> [22] : A'=free_25, B'=1, C'=free_26, D'=free_23, E'=free_26, F'=0, G'=free_16, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_25>=1 && free_16>=1 && free_26>=1+free_23 ], cost: 2+free_26-free_23
    109: f0 -> [22] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_16, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && free_16>=1 && free_26>=1 ], cost: 2+free_26
     78: f0 -> [23] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && 0>=1+free_21 && free_16>=1 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     86: f0 -> [23] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_21>=1 && free_16>=1 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     94: f0 -> [23] : A'=0, B'=0, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_19>=1 && free_21==0 && free_16>=1 && free_22>=1+free_19 ], cost: 2+free_22-free_19
    102: f0 -> [23] : A'=free_25, B'=1, C'=free_26, D'=free_23, E'=free_26, F'=0, G'=free_16, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_25>=1 && free_16>=1 && free_26>=1+free_23 ], cost: 2+free_26-free_23
    110: f0 -> [23] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_16, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && free_16>=1 && free_26>=1 ], cost: 2+free_26
     79: f0 -> [24] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && 0>=1+free_21 && free_16>=1 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     87: f0 -> [24] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_21>=1 && free_16>=1 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     95: f0 -> [24] : A'=0, B'=0, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_19>=1 && free_21==0 && free_16>=1 && free_22>=1+free_19 ], cost: 2+free_22-free_19
    103: f0 -> [24] : A'=free_25, B'=1, C'=free_26, D'=free_23, E'=free_26, F'=0, G'=free_16, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_25>=1 && free_16>=1 && free_26>=1+free_23 ], cost: 2+free_26-free_23
    111: f0 -> [24] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_16, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && free_16>=1 && free_26>=1 ], cost: 2+free_26
    113: f0 -> [25] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && 0>=1+free_21 && free_16>=1 && free_22>=1+free_19 && free_22>=free_22 ], cost: 3+free_22-free_19
    114: f0 -> [26] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && 0>=1+free_21 && free_16>=1 && free_22>=1+free_19 && free_22>=free_22 ], cost: 3+free_22-free_19
    116: f0 -> [27] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_21>=1 && free_16>=1 && free_22>=1+free_19 && free_22>=free_22 ], cost: 3+free_22-free_19
    117: f0 -> [28] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_21>=1 && free_16>=1 && free_22>=1+free_19 && free_22>=free_22 ], cost: 3+free_22-free_19
    119: f0 -> [29] : A'=0, B'=0, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_19>=1 && free_21==0 && 0>=1+free_15 && free_22>=1+free_19 && free_22>=free_22 ], cost: 3+free_22-free_19
    120: f0 -> [30] : A'=0, B'=0, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_19>=1 && free_21==0 && 0>=1+free_15 && free_22>=1+free_19 && free_22>=free_22 ], cost: 3+free_22-free_19
    122: f0 -> [31] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_15, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && 0>=1+free_15 && free_26>=1 && free_26>=free_26 ], cost: 3+free_26
    123: f0 -> [32] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_15, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && 0>=1+free_15 && free_26>=1 && free_26>=free_26 ], cost: 3+free_26
    125: f0 -> [33] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_16, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && free_16>=1 && free_26>=1 && free_26>=free_26 ], cost: 3+free_26
    126: f0 -> [34] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_16, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && free_16>=1 && free_26>=1 && free_26>=free_26 ], cost: 3+free_26


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
    112: f0 -> [17] : A'=0, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && 0>=1+free_21 && free_16>=1 && free_22>=1+free_19 && free_22>=free_22 && 0==0 ], cost: INF
    115: f0 -> [17] : A'=0, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_21>=1 && free_16>=1 && free_22>=1+free_19 && free_22>=free_22 && 0==0 ], cost: INF
    118: f0 -> [17] : A'=0, B'=0, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_19>=1 && free_21==0 && 0>=1+free_15 && free_22>=1+free_19 && free_22>=free_22 && 0==0 ], cost: INF
    121: f0 -> [17] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_15, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && 0>=1+free_15 && free_26>=1 && free_26>=free_26 && 0==0 ], cost: INF
    124: f0 -> [17] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_16, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && free_16>=1 && free_26>=1 && free_26>=free_26 && 0==0 ], cost: INF
     74: f0 -> [19] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && 0>=1+free_21 && 0>=1+free_15 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     82: f0 -> [19] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_21>=1 && 0>=1+free_15 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     90: f0 -> [19] : A'=0, B'=0, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_19>=1 && free_21==0 && 0>=1+free_15 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     98: f0 -> [19] : A'=free_25, B'=1, C'=free_26, D'=free_23, E'=free_26, F'=0, G'=free_15, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_25>=1 && 0>=1+free_15 && free_26>=1+free_23 ], cost: 2+free_26-free_23
    106: f0 -> [19] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_15, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && 0>=1+free_15 && free_26>=1 ], cost: 2+free_26
     75: f0 -> [20] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && 0>=1+free_21 && 0>=1+free_15 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     83: f0 -> [20] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_21>=1 && 0>=1+free_15 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     91: f0 -> [20] : A'=0, B'=0, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_19>=1 && free_21==0 && 0>=1+free_15 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     99: f0 -> [20] : A'=free_25, B'=1, C'=free_26, D'=free_23, E'=free_26, F'=0, G'=free_15, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_25>=1 && 0>=1+free_15 && free_26>=1+free_23 ], cost: 2+free_26-free_23
    107: f0 -> [20] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_15, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && 0>=1+free_15 && free_26>=1 ], cost: 2+free_26
     76: f0 -> [21] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && 0>=1+free_21 && 0>=1+free_15 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     84: f0 -> [21] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_21>=1 && 0>=1+free_15 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     92: f0 -> [21] : A'=0, B'=0, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_19>=1 && free_21==0 && 0>=1+free_15 && free_22>=1+free_19 ], cost: 2+free_22-free_19
    100: f0 -> [21] : A'=free_25, B'=1, C'=free_26, D'=free_23, E'=free_26, F'=0, G'=free_15, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_25>=1 && 0>=1+free_15 && free_26>=1+free_23 ], cost: 2+free_26-free_23
    108: f0 -> [21] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_15, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && 0>=1+free_15 && free_26>=1 ], cost: 2+free_26
     77: f0 -> [22] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && 0>=1+free_21 && free_16>=1 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     85: f0 -> [22] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_21>=1 && free_16>=1 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     93: f0 -> [22] : A'=0, B'=0, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_19>=1 && free_21==0 && free_16>=1 && free_22>=1+free_19 ], cost: 2+free_22-free_19
    101: f0 -> [22] : A'=free_25, B'=1, C'=free_26, D'=free_23, E'=free_26, F'=0, G'=free_16, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_25>=1 && free_16>=1 && free_26>=1+free_23 ], cost: 2+free_26-free_23
    109: f0 -> [22] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_16, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && free_16>=1 && free_26>=1 ], cost: 2+free_26
     78: f0 -> [23] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && 0>=1+free_21 && free_16>=1 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     86: f0 -> [23] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_21>=1 && free_16>=1 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     94: f0 -> [23] : A'=0, B'=0, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_19>=1 && free_21==0 && free_16>=1 && free_22>=1+free_19 ], cost: 2+free_22-free_19
    102: f0 -> [23] : A'=free_25, B'=1, C'=free_26, D'=free_23, E'=free_26, F'=0, G'=free_16, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_25>=1 && free_16>=1 && free_26>=1+free_23 ], cost: 2+free_26-free_23
    110: f0 -> [23] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_16, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && free_16>=1 && free_26>=1 ], cost: 2+free_26
     79: f0 -> [24] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && 0>=1+free_21 && free_16>=1 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     87: f0 -> [24] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_21>=1 && free_16>=1 && free_22>=1+free_19 ], cost: 2+free_22-free_19
     95: f0 -> [24] : A'=0, B'=0, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_19>=1 && free_21==0 && free_16>=1 && free_22>=1+free_19 ], cost: 2+free_22-free_19
    103: f0 -> [24] : A'=free_25, B'=1, C'=free_26, D'=free_23, E'=free_26, F'=0, G'=free_16, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_25>=1 && free_16>=1 && free_26>=1+free_23 ], cost: 2+free_26-free_23
    111: f0 -> [24] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_16, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && free_16>=1 && free_26>=1 ], cost: 2+free_26
    113: f0 -> [25] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && 0>=1+free_21 && free_16>=1 && free_22>=1+free_19 && free_22>=free_22 ], cost: 3+free_22-free_19
    114: f0 -> [26] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && 0>=1+free_21 && free_16>=1 && free_22>=1+free_19 && free_22>=free_22 ], cost: 3+free_22-free_19
    116: f0 -> [27] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_21>=1 && free_16>=1 && free_22>=1+free_19 && free_22>=free_22 ], cost: 3+free_22-free_19
    117: f0 -> [28] : A'=free_21, B'=1, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_16, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_21>=1 && free_16>=1 && free_22>=1+free_19 && free_22>=free_22 ], cost: 3+free_22-free_19
    119: f0 -> [29] : A'=0, B'=0, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_19>=1 && free_21==0 && 0>=1+free_15 && free_22>=1+free_19 && free_22>=free_22 ], cost: 3+free_22-free_19
    120: f0 -> [30] : A'=0, B'=0, C'=free_22, D'=free_19, E'=free_22, F'=0, G'=free_15, H'=0, S'=0, T'=3, U'=1, V'=free_20, [ free_19>=0 && free_20>=1 && T==3 && free_19>=1 && free_21==0 && 0>=1+free_15 && free_22>=1+free_19 && free_22>=free_22 ], cost: 3+free_22-free_19
    122: f0 -> [31] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_15, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && 0>=1+free_15 && free_26>=1 && free_26>=free_26 ], cost: 3+free_26
    123: f0 -> [32] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_15, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && 0>=1+free_15 && free_26>=1 && free_26>=free_26 ], cost: 3+free_26
    125: f0 -> [33] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_16, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && free_16>=1 && free_26>=1 && free_26>=free_26 ], cost: 3+free_26
    126: f0 -> [34] : A'=0, B'=1, C'=free_26, D'=0, E'=free_26, F'=0, G'=free_16, H'=0, S'=0, U'=1, V'=free_24, [ 2>=T && free_23>=0 && free_24>=1 && free_23==0 && free_25==0 && free_16>=1 && free_26>=1 && free_26>=free_26 ], cost: 3+free_26


Computing complexity for remaining 45 transitions.

Found new complexity INF, because: INF sat.


The final runtime is determined by this resulting transition:
  Final Guard: free_19>=0 && free_20>=1 && T==3 && 0>=1+free_21 && free_16>=1 && free_22>=1+free_19 && free_22>=free_22 && 0==0
  Final Cost:  INF

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

WORST_CASE(INF,?)