Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f81 -> f83 : A'=0, [ A==0 ], cost: 1
     12: f81 -> f83 : K'=1, [ 0>=1+A ], cost: 1
     13: f81 -> f83 : K'=1, [ A>=1 ], cost: 1
      7: f83 -> f87 : [ 0>=1+K ], cost: 1
      8: f83 -> f87 : [ K>=1 ], cost: 1
     24: f83 -> f87 : K'=0, [ K==0 ], cost: 1
      1: f34 -> f39 : C'=1, D'=B, E'=free, [ 0>=1+B ], cost: 1
      2: f34 -> f39 : C'=1, D'=B, E'=free_1, [ B>=1 ], cost: 1
     19: f34 -> f96 : B'=0, C'=1, D'=0, [ B==0 ], cost: 1
      3: f39 -> f44 : F'=E, G'=10, H'=free_2, [ 0>=1+E ], cost: 1
      4: f39 -> f44 : F'=E, G'=10, H'=free_3, [ E>=1 ], cost: 1
     20: f39 -> f96 : C'=1, E'=0, F'=0, [ E==0 ], cost: 1
     35: f44 -> f44 : H'=free_21, N'=H, V'=0, W'=0, X'=0, Y'=0, Z'=0, [ V==0 ], cost: 1
     36: f44 -> f44 : C'=0, H'=free_22, N'=H, V'=0, W'=0, X'=0, Y'=free_23, Z'=free_23, [ 0>=1+free_23 && V==0 ], cost: 1
     37: f44 -> f44 : C'=0, H'=free_24, N'=H, V'=0, W'=0, X'=0, Y'=free_25, Z'=free_25, [ free_25>=1 && V==0 ], cost: 1
     33: f44 -> f56 : N'=H, W'=0, X'=0, [ 0>=1+V ], cost: 1
     34: f44 -> f56 : N'=H, W'=0, X'=0, [ V>=1 ], cost: 1
     38: f44 -> f96 : C'=1, N'=H, W'=free_26, X'=free_26, [ 0>=1+free_26 ], cost: 1
     39: f44 -> f96 : C'=1, N'=H, W'=free_27, X'=free_27, [ free_27>=1 ], cost: 1
     16: f64 -> f44 : H'=free_8, Q'=0, J'=0, [ Q==0 ], cost: 1
      5: f64 -> f69 : J'=Q, K'=0, L'=free_4, [ 0>=1+Q ], cost: 1
      6: f64 -> f69 : J'=Q, K'=0, L'=free_5, [ Q>=1 ], cost: 1
     27: f69 -> f83 : O'=L, P'=0, Q_1'=0, R'=0, S'=0, [], cost: 1
     25: f69 -> f87 : O'=L, P'=free_12, Q_1'=free_12, [ 0>=1+free_12 ], cost: 1
     26: f69 -> f87 : O'=L, P'=free_13, Q_1'=free_13, [ free_13>=1 ], cost: 1
     28: f69 -> f80 : O'=L, P'=0, Q_1'=0, R'=free_14, S'=free_14, [ 0>=1+free_14 ], cost: 1
     29: f69 -> f80 : O'=L, P'=0, Q_1'=0, R'=free_15, S'=free_15, [ free_15>=1 ], cost: 1
     17: f87 -> f44 : H'=free_9, K'=0, [ K==0 ], cost: 1
     22: f87 -> f44 : H'=free_10, [ 0>=1+K ], cost: 1
     23: f87 -> f44 : H'=free_11, [ K>=1 ], cost: 1
      9: f80 -> f81 : [ 0>=1+M ], cost: 1
     10: f80 -> f81 : [ M>=1 ], cost: 1
     11: f80 -> f83 : M'=0, [ M==0 ], cost: 1
     14: f56 -> f44 : H'=free_6, [ N>=0 ], cost: 1
     15: f56 -> f44 : H'=free_7, [ 0>=2+N ], cost: 1
     32: f56 -> f44 : H'=free_20, N'=-1, T'=0, U'=0, [ 1+N==0 ], cost: 1
     30: f56 -> f64 : Q'=free_17, N'=-1, T'=free_16, U'=free_16, [ 0>=1+free_16 && 1+N==0 ], cost: 1
     31: f56 -> f64 : Q'=free_19, N'=-1, T'=free_18, U'=free_18, [ free_18>=1 && 1+N==0 ], cost: 1
     18: f96 -> f96 : [], cost: 1
     21: f98 -> f100 : [], cost: 1
     41: f0 -> f34 : B'=free_36, C'=free_37, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 ], cost: 1
     42: f0 -> f34 : B'=free_42, C'=free_38, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 ], cost: 1
     43: f0 -> f34 : B'=free_48, C'=free_49, V'=free_44, A1'=free_45, B1'=20, C1'=free_47, D1'=free_47, E1'=free_49, F1'=free_44, G1'=free_46, [ free_47>=1 && free_46>=21 ], cost: 1
     40: f0 -> f96 : C'=1, V'=free_28, A1'=free_29, B1'=free_29, C1'=free_30, D1'=free_30, E1'=free_31, F1'=free_28, [ 0>=free_30 ], cost: 1


Simplified the transitions:
  Start location: f0
      0: f81 -> f83 : A'=0, [ A==0 ], cost: 1
     12: f81 -> f83 : K'=1, [ 0>=1+A ], cost: 1
     13: f81 -> f83 : K'=1, [ A>=1 ], cost: 1
      7: f83 -> f87 : [ 0>=1+K ], cost: 1
      8: f83 -> f87 : [ K>=1 ], cost: 1
     24: f83 -> f87 : K'=0, [ K==0 ], cost: 1
      1: f34 -> f39 : C'=1, D'=B, E'=free, [ 0>=1+B ], cost: 1
      2: f34 -> f39 : C'=1, D'=B, E'=free_1, [ B>=1 ], cost: 1
     19: f34 -> f96 : B'=0, C'=1, D'=0, [ B==0 ], cost: 1
      3: f39 -> f44 : F'=E, G'=10, H'=free_2, [ 0>=1+E ], cost: 1
      4: f39 -> f44 : F'=E, G'=10, H'=free_3, [ E>=1 ], cost: 1
     20: f39 -> f96 : C'=1, E'=0, F'=0, [ E==0 ], cost: 1
     35: f44 -> f44 : H'=free_21, N'=H, V'=0, W'=0, X'=0, Y'=0, Z'=0, [ V==0 ], cost: 1
     36: f44 -> f44 : C'=0, H'=free_22, N'=H, V'=0, W'=0, X'=0, Y'=free_23, Z'=free_23, [ 0>=1+free_23 && V==0 ], cost: 1
     37: f44 -> f44 : C'=0, H'=free_24, N'=H, V'=0, W'=0, X'=0, Y'=free_25, Z'=free_25, [ free_25>=1 && V==0 ], cost: 1
     33: f44 -> f56 : N'=H, W'=0, X'=0, [ 0>=1+V ], cost: 1
     34: f44 -> f56 : N'=H, W'=0, X'=0, [ V>=1 ], cost: 1
     38: f44 -> f96 : C'=1, N'=H, W'=free_26, X'=free_26, [ 0>=1+free_26 ], cost: 1
     39: f44 -> f96 : C'=1, N'=H, W'=free_27, X'=free_27, [ free_27>=1 ], cost: 1
     16: f64 -> f44 : H'=free_8, Q'=0, J'=0, [ Q==0 ], cost: 1
      5: f64 -> f69 : J'=Q, K'=0, L'=free_4, [ 0>=1+Q ], cost: 1
      6: f64 -> f69 : J'=Q, K'=0, L'=free_5, [ Q>=1 ], cost: 1
     27: f69 -> f83 : O'=L, P'=0, Q_1'=0, R'=0, S'=0, [], cost: 1
     25: f69 -> f87 : O'=L, P'=free_12, Q_1'=free_12, [ 0>=1+free_12 ], cost: 1
     26: f69 -> f87 : O'=L, P'=free_13, Q_1'=free_13, [ free_13>=1 ], cost: 1
     28: f69 -> f80 : O'=L, P'=0, Q_1'=0, R'=free_14, S'=free_14, [ 0>=1+free_14 ], cost: 1
     29: f69 -> f80 : O'=L, P'=0, Q_1'=0, R'=free_15, S'=free_15, [ free_15>=1 ], cost: 1
     17: f87 -> f44 : H'=free_9, K'=0, [ K==0 ], cost: 1
     22: f87 -> f44 : H'=free_10, [ 0>=1+K ], cost: 1
     23: f87 -> f44 : H'=free_11, [ K>=1 ], cost: 1
      9: f80 -> f81 : [ 0>=1+M ], cost: 1
     10: f80 -> f81 : [ M>=1 ], cost: 1
     11: f80 -> f83 : M'=0, [ M==0 ], cost: 1
     14: f56 -> f44 : H'=free_6, [ N>=0 ], cost: 1
     15: f56 -> f44 : H'=free_7, [ 0>=2+N ], cost: 1
     32: f56 -> f44 : H'=free_20, N'=-1, T'=0, U'=0, [ 1+N==0 ], cost: 1
     30: f56 -> f64 : Q'=free_17, N'=-1, T'=free_16, U'=free_16, [ 0>=1+free_16 && 1+N==0 ], cost: 1
     31: f56 -> f64 : Q'=free_19, N'=-1, T'=free_18, U'=free_18, [ free_18>=1 && 1+N==0 ], cost: 1
     18: f96 -> f96 : [], cost: 1
     41: f0 -> f34 : B'=free_36, C'=free_37, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 ], cost: 1
     42: f0 -> f34 : B'=free_42, C'=free_38, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 ], cost: 1
     43: f0 -> f34 : B'=free_48, C'=free_49, V'=free_44, A1'=free_45, B1'=20, C1'=free_47, D1'=free_47, E1'=free_49, F1'=free_44, G1'=free_46, [ free_47>=1 && free_46>=21 ], cost: 1
     40: f0 -> f96 : C'=1, V'=free_28, A1'=free_29, B1'=free_29, C1'=free_30, D1'=free_30, E1'=free_31, F1'=free_28, [ 0>=free_30 ], cost: 1

Eliminating 3 self-loops for location f44
  Self-Loop 35 has unbounded runtime, resulting in the new transition 44.
  Self-Loop 36 has unbounded runtime, resulting in the new transition 45.
  Self-Loop 37 has unbounded runtime, resulting in the new transition 46.
  Removing the self-loops: 35 36 37.
Eliminating 1 self-loops for location f96
  Self-Loop 18 has unbounded runtime, resulting in the new transition 47.
  Removing the self-loops: 18.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f81 -> f83 : A'=0, [ A==0 ], cost: 1
     12: f81 -> f83 : K'=1, [ 0>=1+A ], cost: 1
     13: f81 -> f83 : K'=1, [ A>=1 ], cost: 1
      7: f83 -> f87 : [ 0>=1+K ], cost: 1
      8: f83 -> f87 : [ K>=1 ], cost: 1
     24: f83 -> f87 : K'=0, [ K==0 ], cost: 1
      1: f34 -> f39 : C'=1, D'=B, E'=free, [ 0>=1+B ], cost: 1
      2: f34 -> f39 : C'=1, D'=B, E'=free_1, [ B>=1 ], cost: 1
     19: f34 -> f96 : B'=0, C'=1, D'=0, [ B==0 ], cost: 1
      3: f39 -> f44 : F'=E, G'=10, H'=free_2, [ 0>=1+E ], cost: 1
      4: f39 -> f44 : F'=E, G'=10, H'=free_3, [ E>=1 ], cost: 1
     20: f39 -> f96 : C'=1, E'=0, F'=0, [ E==0 ], cost: 1
     44: f44 -> [14] : [ V==0 ], cost: INF
     45: f44 -> [14] : [ 0>=1+free_23 && V==0 ], cost: INF
     46: f44 -> [14] : [ free_25>=1 && V==0 ], cost: INF
     16: f64 -> f44 : H'=free_8, Q'=0, J'=0, [ Q==0 ], cost: 1
      5: f64 -> f69 : J'=Q, K'=0, L'=free_4, [ 0>=1+Q ], cost: 1
      6: f64 -> f69 : J'=Q, K'=0, L'=free_5, [ Q>=1 ], cost: 1
     27: f69 -> f83 : O'=L, P'=0, Q_1'=0, R'=0, S'=0, [], cost: 1
     25: f69 -> f87 : O'=L, P'=free_12, Q_1'=free_12, [ 0>=1+free_12 ], cost: 1
     26: f69 -> f87 : O'=L, P'=free_13, Q_1'=free_13, [ free_13>=1 ], cost: 1
     28: f69 -> f80 : O'=L, P'=0, Q_1'=0, R'=free_14, S'=free_14, [ 0>=1+free_14 ], cost: 1
     29: f69 -> f80 : O'=L, P'=0, Q_1'=0, R'=free_15, S'=free_15, [ free_15>=1 ], cost: 1
     17: f87 -> f44 : H'=free_9, K'=0, [ K==0 ], cost: 1
     22: f87 -> f44 : H'=free_10, [ 0>=1+K ], cost: 1
     23: f87 -> f44 : H'=free_11, [ K>=1 ], cost: 1
      9: f80 -> f81 : [ 0>=1+M ], cost: 1
     10: f80 -> f81 : [ M>=1 ], cost: 1
     11: f80 -> f83 : M'=0, [ M==0 ], cost: 1
     14: f56 -> f44 : H'=free_6, [ N>=0 ], cost: 1
     15: f56 -> f44 : H'=free_7, [ 0>=2+N ], cost: 1
     32: f56 -> f44 : H'=free_20, N'=-1, T'=0, U'=0, [ 1+N==0 ], cost: 1
     30: f56 -> f64 : Q'=free_17, N'=-1, T'=free_16, U'=free_16, [ 0>=1+free_16 && 1+N==0 ], cost: 1
     31: f56 -> f64 : Q'=free_19, N'=-1, T'=free_18, U'=free_18, [ free_18>=1 && 1+N==0 ], cost: 1
     47: f96 -> [15] : [], cost: INF
     41: f0 -> f34 : B'=free_36, C'=free_37, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 ], cost: 1
     42: f0 -> f34 : B'=free_42, C'=free_38, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 ], cost: 1
     43: f0 -> f34 : B'=free_48, C'=free_49, V'=free_44, A1'=free_45, B1'=20, C1'=free_47, D1'=free_47, E1'=free_49, F1'=free_44, G1'=free_46, [ free_47>=1 && free_46>=21 ], cost: 1
     40: f0 -> f96 : C'=1, V'=free_28, A1'=free_29, B1'=free_29, C1'=free_30, D1'=free_30, E1'=free_31, F1'=free_28, [ 0>=free_30 ], cost: 1
     33: [14] -> f56 : N'=H, W'=0, X'=0, [ 0>=1+V ], cost: 1
     34: [14] -> f56 : N'=H, W'=0, X'=0, [ V>=1 ], cost: 1
     38: [14] -> f96 : C'=1, N'=H, W'=free_26, X'=free_26, [ 0>=1+free_26 ], cost: 1
     39: [14] -> f96 : C'=1, N'=H, W'=free_27, X'=free_27, [ free_27>=1 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      3: f39 -> f44 : F'=E, G'=10, H'=free_2, [ 0>=1+E ], cost: 1
      4: f39 -> f44 : F'=E, G'=10, H'=free_3, [ E>=1 ], cost: 1
     20: f39 -> f96 : C'=1, E'=0, F'=0, [ E==0 ], cost: 1
     59: f44 -> f96 : C'=1, N'=H, W'=free_26, X'=free_26, [ V==0 && 0>=1+free_26 ], cost: INF
     60: f44 -> f96 : C'=1, N'=H, W'=free_27, X'=free_27, [ V==0 && free_27>=1 ], cost: INF
     63: f44 -> f96 : C'=1, N'=H, W'=free_26, X'=free_26, [ 0>=1+free_23 && V==0 && 0>=1+free_26 ], cost: INF
     64: f44 -> f96 : C'=1, N'=H, W'=free_27, X'=free_27, [ 0>=1+free_23 && V==0 && free_27>=1 ], cost: INF
     68: f44 -> f96 : C'=1, N'=H, W'=free_27, X'=free_27, [ free_25>=1 && V==0 && free_27>=1 ], cost: INF
     57: f44 -> [16] : [ V==0 ], cost: INF
     58: f44 -> [17] : [ V==0 ], cost: INF
     61: f44 -> [18] : [ 0>=1+free_23 && V==0 ], cost: INF
     62: f44 -> [19] : [ 0>=1+free_23 && V==0 ], cost: INF
     65: f44 -> [20] : [ free_25>=1 && V==0 ], cost: INF
     66: f44 -> [21] : [ free_25>=1 && V==0 ], cost: INF
     47: f96 -> [15] : [], cost: INF
     48: f0 -> f39 : B'=free_36, C'=1, D'=free_36, E'=free, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 ], cost: 2
     49: f0 -> f39 : B'=free_36, C'=1, D'=free_36, E'=free_1, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && free_36>=1 ], cost: 2
     51: f0 -> f39 : B'=free_42, C'=1, D'=free_42, E'=free, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 ], cost: 2
     52: f0 -> f39 : B'=free_42, C'=1, D'=free_42, E'=free_1, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && free_42>=1 ], cost: 2
     55: f0 -> f39 : B'=free_48, C'=1, D'=free_48, E'=free_1, V'=free_44, A1'=free_45, B1'=20, C1'=free_47, D1'=free_47, E1'=free_49, F1'=free_44, G1'=free_46, [ free_47>=1 && free_46>=21 && free_48>=1 ], cost: 2
     40: f0 -> f96 : C'=1, V'=free_28, A1'=free_29, B1'=free_29, C1'=free_30, D1'=free_30, E1'=free_31, F1'=free_28, [ 0>=free_30 ], cost: 1
     50: f0 -> f96 : B'=0, C'=1, D'=0, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && free_36==0 ], cost: 2
     53: f0 -> f96 : B'=0, C'=1, D'=0, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && free_42==0 ], cost: 2
     56: f0 -> f96 : B'=0, C'=1, D'=0, V'=free_44, A1'=free_45, B1'=20, C1'=free_47, D1'=free_47, E1'=free_49, F1'=free_44, G1'=free_46, [ free_47>=1 && free_46>=21 && free_48==0 ], cost: 2


Applied chaining over branches and pruning:
  Start location: f0
     59: f44 -> f96 : C'=1, N'=H, W'=free_26, X'=free_26, [ V==0 && 0>=1+free_26 ], cost: INF
     60: f44 -> f96 : C'=1, N'=H, W'=free_27, X'=free_27, [ V==0 && free_27>=1 ], cost: INF
     63: f44 -> f96 : C'=1, N'=H, W'=free_26, X'=free_26, [ 0>=1+free_23 && V==0 && 0>=1+free_26 ], cost: INF
     64: f44 -> f96 : C'=1, N'=H, W'=free_27, X'=free_27, [ 0>=1+free_23 && V==0 && free_27>=1 ], cost: INF
     68: f44 -> f96 : C'=1, N'=H, W'=free_27, X'=free_27, [ free_25>=1 && V==0 && free_27>=1 ], cost: INF
     57: f44 -> [16] : [ V==0 ], cost: INF
     58: f44 -> [17] : [ V==0 ], cost: INF
     61: f44 -> [18] : [ 0>=1+free_23 && V==0 ], cost: INF
     62: f44 -> [19] : [ 0>=1+free_23 && V==0 ], cost: INF
     65: f44 -> [20] : [ free_25>=1 && V==0 ], cost: INF
     66: f44 -> [21] : [ free_25>=1 && V==0 ], cost: INF
     47: f96 -> [15] : [], cost: INF
     69: f0 -> f44 : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_2, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && 0>=1+free ], cost: 3
     70: f0 -> f44 : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && free>=1 ], cost: 3
     73: f0 -> f44 : B'=free_36, C'=1, D'=free_36, E'=free_1, F'=free_1, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && free_36>=1 && free_1>=1 ], cost: 3
     75: f0 -> f44 : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_2, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && 0>=1+free ], cost: 3
     76: f0 -> f44 : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_3, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && free>=1 ], cost: 3
     40: f0 -> f96 : C'=1, V'=free_28, A1'=free_29, B1'=free_29, C1'=free_30, D1'=free_30, E1'=free_31, F1'=free_28, [ 0>=free_30 ], cost: 1
     50: f0 -> f96 : B'=0, C'=1, D'=0, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && free_36==0 ], cost: 2
     56: f0 -> f96 : B'=0, C'=1, D'=0, V'=free_44, A1'=free_45, B1'=20, C1'=free_47, D1'=free_47, E1'=free_49, F1'=free_44, G1'=free_46, [ free_47>=1 && free_46>=21 && free_48==0 ], cost: 2
     71: f0 -> f96 : B'=free_36, C'=1, D'=free_36, E'=0, F'=0, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && free==0 ], cost: 3
     77: f0 -> f96 : B'=free_42, C'=1, D'=free_42, E'=0, F'=0, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && free==0 ], cost: 3


Applied chaining over branches and pruning:
  Start location: f0
     47: f96 -> [15] : [], cost: INF
     86: f0 -> f96 : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_2, N'=free_2, V'=free_32, W'=free_26, X'=free_26, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && 0>=1+free && 0>=1+free_23 && free_32==0 && 0>=1+free_26 ], cost: INF
    106: f0 -> f96 : B'=free_36, C'=1, D'=free_36, E'=free_1, F'=free_1, G'=10, H'=free_3, N'=free_3, V'=free_32, W'=free_26, X'=free_26, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && free_36>=1 && free_1>=1 && free_32==0 && 0>=1+free_26 ], cost: INF
    120: f0 -> f96 : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_2, N'=free_2, V'=free_40, W'=free_27, X'=free_27, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && 0>=1+free && 0>=1+free_23 && free_40==0 && free_27>=1 ], cost: INF
    130: f0 -> f96 : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_3, N'=free_3, V'=free_40, W'=free_26, X'=free_26, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && free>=1 && 0>=1+free_23 && free_40==0 && 0>=1+free_26 ], cost: INF
    132: f0 -> f96 : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_3, N'=free_3, V'=free_40, W'=free_27, X'=free_27, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && free>=1 && free_25>=1 && free_40==0 && free_27>=1 ], cost: INF
     89: f0 -> [16] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_2, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && 0>=1+free && free_32==0 ], cost: INF
    100: f0 -> [16] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && free>=1 && free_32==0 ], cost: INF
    111: f0 -> [16] : B'=free_36, C'=1, D'=free_36, E'=free_1, F'=free_1, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && free_36>=1 && free_1>=1 && free_32==0 ], cost: INF
    122: f0 -> [16] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_2, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && 0>=1+free && free_40==0 ], cost: INF
    133: f0 -> [16] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_3, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && free>=1 && free_40==0 ], cost: INF
     90: f0 -> [17] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_2, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && 0>=1+free && free_32==0 ], cost: INF
    101: f0 -> [17] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && free>=1 && free_32==0 ], cost: INF
    112: f0 -> [17] : B'=free_36, C'=1, D'=free_36, E'=free_1, F'=free_1, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && free_36>=1 && free_1>=1 && free_32==0 ], cost: INF
    123: f0 -> [17] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_2, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && 0>=1+free && free_40==0 ], cost: INF
    134: f0 -> [17] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_3, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && free>=1 && free_40==0 ], cost: INF
     91: f0 -> [18] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_2, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && 0>=1+free && 0>=1+free_23 && free_32==0 ], cost: INF
    102: f0 -> [18] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && free>=1 && 0>=1+free_23 && free_32==0 ], cost: INF
    113: f0 -> [18] : B'=free_36, C'=1, D'=free_36, E'=free_1, F'=free_1, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && free_36>=1 && free_1>=1 && 0>=1+free_23 && free_32==0 ], cost: INF
    124: f0 -> [18] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_2, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && 0>=1+free && 0>=1+free_23 && free_40==0 ], cost: INF
    135: f0 -> [18] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_3, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && free>=1 && 0>=1+free_23 && free_40==0 ], cost: INF
     92: f0 -> [19] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_2, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && 0>=1+free && 0>=1+free_23 && free_32==0 ], cost: INF
    103: f0 -> [19] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && free>=1 && 0>=1+free_23 && free_32==0 ], cost: INF
    114: f0 -> [19] : B'=free_36, C'=1, D'=free_36, E'=free_1, F'=free_1, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && free_36>=1 && free_1>=1 && 0>=1+free_23 && free_32==0 ], cost: INF
    125: f0 -> [19] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_2, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && 0>=1+free && 0>=1+free_23 && free_40==0 ], cost: INF
    136: f0 -> [19] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_3, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && free>=1 && 0>=1+free_23 && free_40==0 ], cost: INF
     93: f0 -> [20] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_2, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && 0>=1+free && free_25>=1 && free_32==0 ], cost: INF
    104: f0 -> [20] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && free>=1 && free_25>=1 && free_32==0 ], cost: INF
    115: f0 -> [20] : B'=free_36, C'=1, D'=free_36, E'=free_1, F'=free_1, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && free_36>=1 && free_1>=1 && free_25>=1 && free_32==0 ], cost: INF
    126: f0 -> [20] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_2, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && 0>=1+free && free_25>=1 && free_40==0 ], cost: INF
    137: f0 -> [20] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_3, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && free>=1 && free_25>=1 && free_40==0 ], cost: INF
     94: f0 -> [21] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_2, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && 0>=1+free && free_25>=1 && free_32==0 ], cost: INF
    105: f0 -> [21] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && free>=1 && free_25>=1 && free_32==0 ], cost: INF
    116: f0 -> [21] : B'=free_36, C'=1, D'=free_36, E'=free_1, F'=free_1, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && free_36>=1 && free_1>=1 && free_25>=1 && free_32==0 ], cost: INF
    127: f0 -> [21] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_2, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && 0>=1+free && free_25>=1 && free_40==0 ], cost: INF
    138: f0 -> [21] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_3, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && free>=1 && free_25>=1 && free_40==0 ], cost: INF


Applied chaining over branches and pruning:
  Start location: f0
    139: f0 -> [15] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_2, N'=free_2, V'=free_32, W'=free_26, X'=free_26, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && 0>=1+free && 0>=1+free_23 && free_32==0 && 0>=1+free_26 ], cost: INF
    140: f0 -> [15] : B'=free_36, C'=1, D'=free_36, E'=free_1, F'=free_1, G'=10, H'=free_3, N'=free_3, V'=free_32, W'=free_26, X'=free_26, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && free_36>=1 && free_1>=1 && free_32==0 && 0>=1+free_26 ], cost: INF
    141: f0 -> [15] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_2, N'=free_2, V'=free_40, W'=free_27, X'=free_27, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && 0>=1+free && 0>=1+free_23 && free_40==0 && free_27>=1 ], cost: INF
    142: f0 -> [15] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_3, N'=free_3, V'=free_40, W'=free_26, X'=free_26, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && free>=1 && 0>=1+free_23 && free_40==0 && 0>=1+free_26 ], cost: INF
    143: f0 -> [15] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_3, N'=free_3, V'=free_40, W'=free_27, X'=free_27, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && free>=1 && free_25>=1 && free_40==0 && free_27>=1 ], cost: INF
     89: f0 -> [16] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_2, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && 0>=1+free && free_32==0 ], cost: INF
    100: f0 -> [16] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && free>=1 && free_32==0 ], cost: INF
    111: f0 -> [16] : B'=free_36, C'=1, D'=free_36, E'=free_1, F'=free_1, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && free_36>=1 && free_1>=1 && free_32==0 ], cost: INF
    122: f0 -> [16] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_2, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && 0>=1+free && free_40==0 ], cost: INF
    133: f0 -> [16] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_3, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && free>=1 && free_40==0 ], cost: INF
     90: f0 -> [17] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_2, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && 0>=1+free && free_32==0 ], cost: INF
    101: f0 -> [17] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && free>=1 && free_32==0 ], cost: INF
    112: f0 -> [17] : B'=free_36, C'=1, D'=free_36, E'=free_1, F'=free_1, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && free_36>=1 && free_1>=1 && free_32==0 ], cost: INF
    123: f0 -> [17] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_2, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && 0>=1+free && free_40==0 ], cost: INF
    134: f0 -> [17] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_3, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && free>=1 && free_40==0 ], cost: INF
     91: f0 -> [18] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_2, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && 0>=1+free && 0>=1+free_23 && free_32==0 ], cost: INF
    102: f0 -> [18] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && free>=1 && 0>=1+free_23 && free_32==0 ], cost: INF
    113: f0 -> [18] : B'=free_36, C'=1, D'=free_36, E'=free_1, F'=free_1, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && free_36>=1 && free_1>=1 && 0>=1+free_23 && free_32==0 ], cost: INF
    124: f0 -> [18] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_2, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && 0>=1+free && 0>=1+free_23 && free_40==0 ], cost: INF
    135: f0 -> [18] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_3, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && free>=1 && 0>=1+free_23 && free_40==0 ], cost: INF
     92: f0 -> [19] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_2, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && 0>=1+free && 0>=1+free_23 && free_32==0 ], cost: INF
    103: f0 -> [19] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && free>=1 && 0>=1+free_23 && free_32==0 ], cost: INF
    114: f0 -> [19] : B'=free_36, C'=1, D'=free_36, E'=free_1, F'=free_1, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && free_36>=1 && free_1>=1 && 0>=1+free_23 && free_32==0 ], cost: INF
    125: f0 -> [19] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_2, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && 0>=1+free && 0>=1+free_23 && free_40==0 ], cost: INF
    136: f0 -> [19] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_3, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && free>=1 && 0>=1+free_23 && free_40==0 ], cost: INF
     93: f0 -> [20] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_2, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && 0>=1+free && free_25>=1 && free_32==0 ], cost: INF
    104: f0 -> [20] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && free>=1 && free_25>=1 && free_32==0 ], cost: INF
    115: f0 -> [20] : B'=free_36, C'=1, D'=free_36, E'=free_1, F'=free_1, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && free_36>=1 && free_1>=1 && free_25>=1 && free_32==0 ], cost: INF
    126: f0 -> [20] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_2, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && 0>=1+free && free_25>=1 && free_40==0 ], cost: INF
    137: f0 -> [20] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_3, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && free>=1 && free_25>=1 && free_40==0 ], cost: INF
     94: f0 -> [21] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_2, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && 0>=1+free && free_25>=1 && free_32==0 ], cost: INF
    105: f0 -> [21] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && free>=1 && free_25>=1 && free_32==0 ], cost: INF
    116: f0 -> [21] : B'=free_36, C'=1, D'=free_36, E'=free_1, F'=free_1, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && free_36>=1 && free_1>=1 && free_25>=1 && free_32==0 ], cost: INF
    127: f0 -> [21] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_2, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && 0>=1+free && free_25>=1 && free_40==0 ], cost: INF
    138: f0 -> [21] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_3, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && free>=1 && free_25>=1 && free_40==0 ], cost: INF


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
    139: f0 -> [15] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_2, N'=free_2, V'=free_32, W'=free_26, X'=free_26, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && 0>=1+free && 0>=1+free_23 && free_32==0 && 0>=1+free_26 ], cost: INF
    140: f0 -> [15] : B'=free_36, C'=1, D'=free_36, E'=free_1, F'=free_1, G'=10, H'=free_3, N'=free_3, V'=free_32, W'=free_26, X'=free_26, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && free_36>=1 && free_1>=1 && free_32==0 && 0>=1+free_26 ], cost: INF
    141: f0 -> [15] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_2, N'=free_2, V'=free_40, W'=free_27, X'=free_27, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && 0>=1+free && 0>=1+free_23 && free_40==0 && free_27>=1 ], cost: INF
    142: f0 -> [15] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_3, N'=free_3, V'=free_40, W'=free_26, X'=free_26, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && free>=1 && 0>=1+free_23 && free_40==0 && 0>=1+free_26 ], cost: INF
    143: f0 -> [15] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_3, N'=free_3, V'=free_40, W'=free_27, X'=free_27, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && free>=1 && free_25>=1 && free_40==0 && free_27>=1 ], cost: INF
     89: f0 -> [16] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_2, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && 0>=1+free && free_32==0 ], cost: INF
    100: f0 -> [16] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && free>=1 && free_32==0 ], cost: INF
    111: f0 -> [16] : B'=free_36, C'=1, D'=free_36, E'=free_1, F'=free_1, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && free_36>=1 && free_1>=1 && free_32==0 ], cost: INF
    122: f0 -> [16] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_2, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && 0>=1+free && free_40==0 ], cost: INF
    133: f0 -> [16] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_3, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && free>=1 && free_40==0 ], cost: INF
     90: f0 -> [17] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_2, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && 0>=1+free && free_32==0 ], cost: INF
    101: f0 -> [17] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && free>=1 && free_32==0 ], cost: INF
    112: f0 -> [17] : B'=free_36, C'=1, D'=free_36, E'=free_1, F'=free_1, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && free_36>=1 && free_1>=1 && free_32==0 ], cost: INF
    123: f0 -> [17] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_2, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && 0>=1+free && free_40==0 ], cost: INF
    134: f0 -> [17] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_3, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && free>=1 && free_40==0 ], cost: INF
     91: f0 -> [18] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_2, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && 0>=1+free && 0>=1+free_23 && free_32==0 ], cost: INF
    102: f0 -> [18] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && free>=1 && 0>=1+free_23 && free_32==0 ], cost: INF
    113: f0 -> [18] : B'=free_36, C'=1, D'=free_36, E'=free_1, F'=free_1, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && free_36>=1 && free_1>=1 && 0>=1+free_23 && free_32==0 ], cost: INF
    124: f0 -> [18] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_2, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && 0>=1+free && 0>=1+free_23 && free_40==0 ], cost: INF
    135: f0 -> [18] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_3, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && free>=1 && 0>=1+free_23 && free_40==0 ], cost: INF
     92: f0 -> [19] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_2, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && 0>=1+free && 0>=1+free_23 && free_32==0 ], cost: INF
    103: f0 -> [19] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && free>=1 && 0>=1+free_23 && free_32==0 ], cost: INF
    114: f0 -> [19] : B'=free_36, C'=1, D'=free_36, E'=free_1, F'=free_1, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && free_36>=1 && free_1>=1 && 0>=1+free_23 && free_32==0 ], cost: INF
    125: f0 -> [19] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_2, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && 0>=1+free && 0>=1+free_23 && free_40==0 ], cost: INF
    136: f0 -> [19] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_3, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && free>=1 && 0>=1+free_23 && free_40==0 ], cost: INF
     93: f0 -> [20] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_2, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && 0>=1+free && free_25>=1 && free_32==0 ], cost: INF
    104: f0 -> [20] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && free>=1 && free_25>=1 && free_32==0 ], cost: INF
    115: f0 -> [20] : B'=free_36, C'=1, D'=free_36, E'=free_1, F'=free_1, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && free_36>=1 && free_1>=1 && free_25>=1 && free_32==0 ], cost: INF
    126: f0 -> [20] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_2, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && 0>=1+free && free_25>=1 && free_40==0 ], cost: INF
    137: f0 -> [20] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_3, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && free>=1 && free_25>=1 && free_40==0 ], cost: INF
     94: f0 -> [21] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_2, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && 0>=1+free && free_25>=1 && free_32==0 ], cost: INF
    105: f0 -> [21] : B'=free_36, C'=1, D'=free_36, E'=free, F'=free, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && 0>=1+free_36 && free>=1 && free_25>=1 && free_32==0 ], cost: INF
    116: f0 -> [21] : B'=free_36, C'=1, D'=free_36, E'=free_1, F'=free_1, G'=10, H'=free_3, V'=free_32, A1'=free_33, B1'=5, C1'=free_35, D1'=free_35, E1'=free_37, F1'=free_32, G1'=free_34, [ free_35>=1 && 4>=free_34 && free_36>=1 && free_1>=1 && free_25>=1 && free_32==0 ], cost: INF
    127: f0 -> [21] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_2, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && 0>=1+free && free_25>=1 && free_40==0 ], cost: INF
    138: f0 -> [21] : B'=free_42, C'=1, D'=free_42, E'=free, F'=free, G'=10, H'=free_3, V'=free_40, A1'=free_39, B1'=free_41, C1'=free_43, D1'=free_43, E1'=free_38, F1'=free_40, G1'=free_41, [ free_43>=1 && 20>=free_41 && free_41>=5 && 0>=1+free_42 && free>=1 && free_25>=1 && free_40==0 ], cost: INF


Computing complexity for remaining 35 transitions.

Found new complexity INF, because: INF sat.


The final runtime is determined by this resulting transition:
  Final Guard: free_35>=1 && 4>=free_34 && 0>=1+free_36 && 0>=1+free && 0>=1+free_23 && free_32==0 && 0>=1+free_26
  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,?)