Trying to load file: main.koat

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


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

Eliminating 1 self-loops for location f94
  Self-Loop 15 has unbounded runtime, resulting in the new transition 41.
  Removing the self-loops: 15.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f78 -> f80 : A'=0, [ A==0 ], cost: 1
     11: f78 -> f80 : Q'=1, [ 0>=1+A ], cost: 1
     12: f78 -> f80 : Q'=1, [ A>=1 ], cost: 1
      6: f80 -> f84 : [ 0>=1+Q ], cost: 1
      7: f80 -> f84 : [ Q>=1 ], cost: 1
     22: f80 -> f84 : Q'=0, [ Q==0 ], cost: 1
      1: f37 -> f41 : C'=B, D'=free, [ 0>=1+B ], cost: 1
      2: f37 -> f41 : C'=B, D'=free_1, [ B>=1 ], cost: 1
     16: f37 -> f94 : B'=0, C'=0, L'=1, [ B==0 ], cost: 1
     35: f41 -> f48 : E'=free_15, F'=free_16, M'=D, X'=free_15, [ 0>=1+D ], cost: 1
     36: f41 -> f48 : E'=free_17, F'=free_18, M'=D, X'=free_17, [ D>=1 ], cost: 1
     17: f41 -> f94 : D'=0, L'=1, M'=0, [ D==0 ], cost: 1
      3: f89 -> f48 : F'=free_2, [ E>=1 ], cost: 1
     19: f89 -> f94 : L'=1, [ 0>=E ], cost: 1
     28: f48 -> f89 : E'=-1+E, S'=F, T'=0, U'=0, [ F>=0 ], cost: 1
     29: f48 -> f89 : E'=-1+E, S'=F, T'=0, U'=0, [ 0>=2+F ], cost: 1
     34: f48 -> f89 : E'=-1+E, F'=-1, S'=-1, T'=0, U'=0, V'=0, W'=0, [ 1+F==0 ], cost: 1
     32: f48 -> f61 : F'=-1, G'=free_12, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 ], cost: 1
     33: f48 -> f61 : F'=-1, G'=free_14, S'=-1, T'=0, U'=0, V'=free_13, W'=free_13, [ free_13>=1 && 1+F==0 ], cost: 1
     30: f48 -> f94 : L'=1, S'=F, T'=free_9, U'=free_9, [ 0>=1+free_9 ], cost: 1
     31: f48 -> f94 : L'=1, S'=F, T'=free_10, U'=free_10, [ free_10>=1 ], cost: 1
     13: f61 -> f89 : E'=-1+E, G'=0, H'=0, [ G==0 ], cost: 1
      4: f61 -> f66 : H'=G, Q'=0, J'=free_3, [ 0>=1+G ], cost: 1
      5: f61 -> f66 : H'=G, Q'=0, J'=free_4, [ G>=1 ], cost: 1
     25: f66 -> f80 : N'=J, O'=0, P'=0, Q_1'=0, R'=0, [], cost: 1
     23: f66 -> f84 : N'=J, O'=free_5, P'=free_5, [ 0>=1+free_5 ], cost: 1
     24: f66 -> f84 : N'=J, O'=free_6, P'=free_6, [ free_6>=1 ], cost: 1
     26: f66 -> f77 : N'=J, O'=0, P'=0, Q_1'=free_7, R'=free_7, [ 0>=1+free_7 ], cost: 1
     27: f66 -> f77 : N'=J, O'=0, P'=0, Q_1'=free_8, R'=free_8, [ free_8>=1 ], cost: 1
     14: f84 -> f89 : E'=-1+E, Q'=0, [ Q==0 ], cost: 1
     20: f84 -> f89 : E'=-1+E, [ 0>=1+Q ], cost: 1
     21: f84 -> f89 : E'=-1+E, [ Q>=1 ], cost: 1
      8: f77 -> f78 : [ 0>=1+K ], cost: 1
      9: f77 -> f78 : [ K>=1 ], cost: 1
     10: f77 -> f80 : K'=0, [ K==0 ], cost: 1
     41: f94 -> [14] : [], cost: INF
     38: f0 -> f37 : B'=free_24, E'=free_27, L'=free_30, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 ], cost: 1
     39: f0 -> f37 : B'=free_31, E'=free_36, L'=free_32, Y'=free_33, Z'=free_35, A1'=free_37, B1'=free_37, C1'=free_32, D1'=free_34, E1'=free_34, F1'=free_36, G1'=free_35, [ free_37>=1 && 20>=free_35 && free_35>=5 ], cost: 1
     40: f0 -> f37 : B'=free_38, E'=free_41, L'=free_44, Y'=free_40, Z'=20, A1'=free_42, B1'=free_42, C1'=free_44, D1'=free_39, E1'=free_39, F1'=free_41, G1'=free_43, [ free_42>=1 && free_43>=21 ], cost: 1
     37: f0 -> f94 : E'=free_21, L'=1, Y'=free_20, Z'=free_20, A1'=free_22, B1'=free_22, C1'=free_23, D1'=free_19, E1'=free_19, F1'=free_21, [ 0>=free_22 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      0: f78 -> f80 : A'=0, [ A==0 ], cost: 1
     11: f78 -> f80 : Q'=1, [ 0>=1+A ], cost: 1
     12: f78 -> f80 : Q'=1, [ A>=1 ], cost: 1
      6: f80 -> f84 : [ 0>=1+Q ], cost: 1
      7: f80 -> f84 : [ Q>=1 ], cost: 1
     22: f80 -> f84 : Q'=0, [ Q==0 ], cost: 1
     35: f41 -> f48 : E'=free_15, F'=free_16, M'=D, X'=free_15, [ 0>=1+D ], cost: 1
     36: f41 -> f48 : E'=free_17, F'=free_18, M'=D, X'=free_17, [ D>=1 ], cost: 1
     17: f41 -> f94 : D'=0, L'=1, M'=0, [ D==0 ], cost: 1
      3: f89 -> f48 : F'=free_2, [ E>=1 ], cost: 1
     19: f89 -> f94 : L'=1, [ 0>=E ], cost: 1
     28: f48 -> f89 : E'=-1+E, S'=F, T'=0, U'=0, [ F>=0 ], cost: 1
     29: f48 -> f89 : E'=-1+E, S'=F, T'=0, U'=0, [ 0>=2+F ], cost: 1
     34: f48 -> f89 : E'=-1+E, F'=-1, S'=-1, T'=0, U'=0, V'=0, W'=0, [ 1+F==0 ], cost: 1
     51: f48 -> f89 : E'=-1+E, F'=-1, G'=0, H'=0, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && free_12==0 ], cost: 2
     54: f48 -> f89 : E'=-1+E, F'=-1, G'=0, H'=0, S'=-1, T'=0, U'=0, V'=free_13, W'=free_13, [ free_13>=1 && 1+F==0 && free_14==0 ], cost: 2
     52: f48 -> f66 : F'=-1, G'=free_12, H'=free_12, Q'=0, J'=free_3, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && 0>=1+free_12 ], cost: 2
     53: f48 -> f66 : F'=-1, G'=free_12, H'=free_12, Q'=0, J'=free_4, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && free_12>=1 ], cost: 2
     55: f48 -> f66 : F'=-1, G'=free_14, H'=free_14, Q'=0, J'=free_3, S'=-1, T'=0, U'=0, V'=free_13, W'=free_13, [ free_13>=1 && 1+F==0 && 0>=1+free_14 ], cost: 2
     56: f48 -> f66 : F'=-1, G'=free_14, H'=free_14, Q'=0, J'=free_4, S'=-1, T'=0, U'=0, V'=free_13, W'=free_13, [ free_13>=1 && 1+F==0 && free_14>=1 ], cost: 2
     30: f48 -> f94 : L'=1, S'=F, T'=free_9, U'=free_9, [ 0>=1+free_9 ], cost: 1
     31: f48 -> f94 : L'=1, S'=F, T'=free_10, U'=free_10, [ free_10>=1 ], cost: 1
     57: f66 -> f78 : N'=J, O'=0, P'=0, Q_1'=free_7, R'=free_7, [ 0>=1+free_7 && 0>=1+K ], cost: 2
     58: f66 -> f78 : N'=J, O'=0, P'=0, Q_1'=free_7, R'=free_7, [ 0>=1+free_7 && K>=1 ], cost: 2
     60: f66 -> f78 : N'=J, O'=0, P'=0, Q_1'=free_8, R'=free_8, [ free_8>=1 && 0>=1+K ], cost: 2
     61: f66 -> f78 : N'=J, O'=0, P'=0, Q_1'=free_8, R'=free_8, [ free_8>=1 && K>=1 ], cost: 2
     25: f66 -> f80 : N'=J, O'=0, P'=0, Q_1'=0, R'=0, [], cost: 1
     59: f66 -> f80 : K'=0, N'=J, O'=0, P'=0, Q_1'=free_7, R'=free_7, [ 0>=1+free_7 && K==0 ], cost: 2
     62: f66 -> f80 : K'=0, N'=J, O'=0, P'=0, Q_1'=free_8, R'=free_8, [ free_8>=1 && K==0 ], cost: 2
     23: f66 -> f84 : N'=J, O'=free_5, P'=free_5, [ 0>=1+free_5 ], cost: 1
     24: f66 -> f84 : N'=J, O'=free_6, P'=free_6, [ free_6>=1 ], cost: 1
     14: f84 -> f89 : E'=-1+E, Q'=0, [ Q==0 ], cost: 1
     20: f84 -> f89 : E'=-1+E, [ 0>=1+Q ], cost: 1
     21: f84 -> f89 : E'=-1+E, [ Q>=1 ], cost: 1
     41: f94 -> [14] : [], cost: INF
     42: f0 -> f41 : B'=free_24, C'=free_24, D'=free, E'=free_27, L'=free_30, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 ], cost: 2
     43: f0 -> f41 : B'=free_24, C'=free_24, D'=free_1, E'=free_27, L'=free_30, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && free_24>=1 ], cost: 2
     45: f0 -> f41 : B'=free_31, C'=free_31, D'=free, E'=free_36, L'=free_32, Y'=free_33, Z'=free_35, A1'=free_37, B1'=free_37, C1'=free_32, D1'=free_34, E1'=free_34, F1'=free_36, G1'=free_35, [ free_37>=1 && 20>=free_35 && free_35>=5 && 0>=1+free_31 ], cost: 2
     46: f0 -> f41 : B'=free_31, C'=free_31, D'=free_1, E'=free_36, L'=free_32, Y'=free_33, Z'=free_35, A1'=free_37, B1'=free_37, C1'=free_32, D1'=free_34, E1'=free_34, F1'=free_36, G1'=free_35, [ free_37>=1 && 20>=free_35 && free_35>=5 && free_31>=1 ], cost: 2
     49: f0 -> f41 : B'=free_38, C'=free_38, D'=free_1, E'=free_41, L'=free_44, Y'=free_40, Z'=20, A1'=free_42, B1'=free_42, C1'=free_44, D1'=free_39, E1'=free_39, F1'=free_41, G1'=free_43, [ free_42>=1 && free_43>=21 && free_38>=1 ], cost: 2
     37: f0 -> f94 : E'=free_21, L'=1, Y'=free_20, Z'=free_20, A1'=free_22, B1'=free_22, C1'=free_23, D1'=free_19, E1'=free_19, F1'=free_21, [ 0>=free_22 ], cost: 1
     44: f0 -> f94 : B'=0, C'=0, E'=free_27, L'=1, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && free_24==0 ], cost: 2
     47: f0 -> f94 : B'=0, C'=0, E'=free_36, L'=1, Y'=free_33, Z'=free_35, A1'=free_37, B1'=free_37, C1'=free_32, D1'=free_34, E1'=free_34, F1'=free_36, G1'=free_35, [ free_37>=1 && 20>=free_35 && free_35>=5 && free_31==0 ], cost: 2
     50: f0 -> f94 : B'=0, C'=0, E'=free_41, L'=1, Y'=free_40, Z'=20, A1'=free_42, B1'=free_42, C1'=free_44, D1'=free_39, E1'=free_39, F1'=free_41, G1'=free_43, [ free_42>=1 && free_43>=21 && free_38==0 ], cost: 2


Applied chaining over branches and pruning:
  Start location: f0
      0: f78 -> f80 : A'=0, [ A==0 ], cost: 1
     11: f78 -> f80 : Q'=1, [ 0>=1+A ], cost: 1
     12: f78 -> f80 : Q'=1, [ A>=1 ], cost: 1
      6: f80 -> f84 : [ 0>=1+Q ], cost: 1
      7: f80 -> f84 : [ Q>=1 ], cost: 1
     22: f80 -> f84 : Q'=0, [ Q==0 ], cost: 1
      3: f89 -> f48 : F'=free_2, [ E>=1 ], cost: 1
     19: f89 -> f94 : L'=1, [ 0>=E ], cost: 1
     78: f48 -> f78 : F'=-1, G'=free_12, H'=free_12, Q'=0, J'=free_3, N'=free_3, O'=0, P'=0, Q_1'=free_7, R'=free_7, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && 0>=1+free_12 && 0>=1+free_7 && 0>=1+K ], cost: 4
     79: f48 -> f78 : F'=-1, G'=free_12, H'=free_12, Q'=0, J'=free_3, N'=free_3, O'=0, P'=0, Q_1'=free_7, R'=free_7, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && 0>=1+free_12 && 0>=1+free_7 && K>=1 ], cost: 4
     81: f48 -> f78 : F'=-1, G'=free_12, H'=free_12, Q'=0, J'=free_3, N'=free_3, O'=0, P'=0, Q_1'=free_8, R'=free_8, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && 0>=1+free_12 && free_8>=1 && K>=1 ], cost: 4
     90: f48 -> f78 : F'=-1, G'=free_12, H'=free_12, Q'=0, J'=free_4, N'=free_4, O'=0, P'=0, Q_1'=free_8, R'=free_8, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && free_12>=1 && free_8>=1 && K>=1 ], cost: 4
     97: f48 -> f78 : F'=-1, G'=free_14, H'=free_14, Q'=0, J'=free_3, N'=free_3, O'=0, P'=0, Q_1'=free_7, R'=free_7, S'=-1, T'=0, U'=0, V'=free_13, W'=free_13, [ free_13>=1 && 1+F==0 && 0>=1+free_14 && 0>=1+free_7 && K>=1 ], cost: 4
     82: f48 -> f80 : F'=-1, G'=free_12, H'=free_12, Q'=0, J'=free_3, N'=free_3, O'=0, P'=0, Q_1'=0, R'=0, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && 0>=1+free_12 ], cost: 3
     83: f48 -> f80 : F'=-1, G'=free_12, H'=free_12, Q'=0, J'=free_3, K'=0, N'=free_3, O'=0, P'=0, Q_1'=free_7, R'=free_7, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && 0>=1+free_12 && 0>=1+free_7 && K==0 ], cost: 4
     91: f48 -> f80 : F'=-1, G'=free_12, H'=free_12, Q'=0, J'=free_4, N'=free_4, O'=0, P'=0, Q_1'=0, R'=0, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && free_12>=1 ], cost: 3
     93: f48 -> f80 : F'=-1, G'=free_12, H'=free_12, Q'=0, J'=free_4, K'=0, N'=free_4, O'=0, P'=0, Q_1'=free_8, R'=free_8, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && free_12>=1 && free_8>=1 && K==0 ], cost: 4
    100: f48 -> f80 : F'=-1, G'=free_14, H'=free_14, Q'=0, J'=free_3, N'=free_3, O'=0, P'=0, Q_1'=0, R'=0, S'=-1, T'=0, U'=0, V'=free_13, W'=free_13, [ free_13>=1 && 1+F==0 && 0>=1+free_14 ], cost: 3
     28: f48 -> f89 : E'=-1+E, S'=F, T'=0, U'=0, [ F>=0 ], cost: 1
     29: f48 -> f89 : E'=-1+E, S'=F, T'=0, U'=0, [ 0>=2+F ], cost: 1
     34: f48 -> f89 : E'=-1+E, F'=-1, S'=-1, T'=0, U'=0, V'=0, W'=0, [ 1+F==0 ], cost: 1
     51: f48 -> f89 : E'=-1+E, F'=-1, G'=0, H'=0, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && free_12==0 ], cost: 2
     54: f48 -> f89 : E'=-1+E, F'=-1, G'=0, H'=0, S'=-1, T'=0, U'=0, V'=free_13, W'=free_13, [ free_13>=1 && 1+F==0 && free_14==0 ], cost: 2
     85: f48 -> f84 : F'=-1, G'=free_12, H'=free_12, Q'=0, J'=free_3, N'=free_3, O'=free_5, P'=free_5, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && 0>=1+free_12 && 0>=1+free_5 ], cost: 3
     86: f48 -> f84 : F'=-1, G'=free_12, H'=free_12, Q'=0, J'=free_3, N'=free_3, O'=free_6, P'=free_6, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && 0>=1+free_12 && free_6>=1 ], cost: 3
     95: f48 -> f84 : F'=-1, G'=free_12, H'=free_12, Q'=0, J'=free_4, N'=free_4, O'=free_6, P'=free_6, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && free_12>=1 && free_6>=1 ], cost: 3
    103: f48 -> f84 : F'=-1, G'=free_14, H'=free_14, Q'=0, J'=free_3, N'=free_3, O'=free_5, P'=free_5, S'=-1, T'=0, U'=0, V'=free_13, W'=free_13, [ free_13>=1 && 1+F==0 && 0>=1+free_14 && 0>=1+free_5 ], cost: 3
    104: f48 -> f84 : F'=-1, G'=free_14, H'=free_14, Q'=0, J'=free_3, N'=free_3, O'=free_6, P'=free_6, S'=-1, T'=0, U'=0, V'=free_13, W'=free_13, [ free_13>=1 && 1+F==0 && 0>=1+free_14 && free_6>=1 ], cost: 3
     30: f48 -> f94 : L'=1, S'=F, T'=free_9, U'=free_9, [ 0>=1+free_9 ], cost: 1
     31: f48 -> f94 : L'=1, S'=F, T'=free_10, U'=free_10, [ free_10>=1 ], cost: 1
     14: f84 -> f89 : E'=-1+E, Q'=0, [ Q==0 ], cost: 1
     20: f84 -> f89 : E'=-1+E, [ 0>=1+Q ], cost: 1
     21: f84 -> f89 : E'=-1+E, [ Q>=1 ], cost: 1
     41: f94 -> [14] : [], cost: INF
     63: f0 -> f48 : B'=free_24, C'=free_24, D'=free, E'=free_15, F'=free_16, L'=free_30, M'=free, X'=free_15, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && 0>=1+free ], cost: 3
     64: f0 -> f48 : B'=free_24, C'=free_24, D'=free, E'=free_17, F'=free_18, L'=free_30, M'=free, X'=free_17, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && free>=1 ], cost: 3
     67: f0 -> f48 : B'=free_24, C'=free_24, D'=free_1, E'=free_17, F'=free_18, L'=free_30, M'=free_1, X'=free_17, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && free_24>=1 && free_1>=1 ], cost: 3
     69: f0 -> f48 : B'=free_31, C'=free_31, D'=free, E'=free_15, F'=free_16, L'=free_32, M'=free, X'=free_15, Y'=free_33, Z'=free_35, A1'=free_37, B1'=free_37, C1'=free_32, D1'=free_34, E1'=free_34, F1'=free_36, G1'=free_35, [ free_37>=1 && 20>=free_35 && free_35>=5 && 0>=1+free_31 && 0>=1+free ], cost: 3
     70: f0 -> f48 : B'=free_31, C'=free_31, D'=free, E'=free_17, F'=free_18, L'=free_32, M'=free, X'=free_17, Y'=free_33, Z'=free_35, A1'=free_37, B1'=free_37, C1'=free_32, D1'=free_34, E1'=free_34, F1'=free_36, G1'=free_35, [ free_37>=1 && 20>=free_35 && free_35>=5 && 0>=1+free_31 && free>=1 ], cost: 3
     37: f0 -> f94 : E'=free_21, L'=1, Y'=free_20, Z'=free_20, A1'=free_22, B1'=free_22, C1'=free_23, D1'=free_19, E1'=free_19, F1'=free_21, [ 0>=free_22 ], cost: 1
     44: f0 -> f94 : B'=0, C'=0, E'=free_27, L'=1, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && free_24==0 ], cost: 2
     50: f0 -> f94 : B'=0, C'=0, E'=free_41, L'=1, Y'=free_40, Z'=20, A1'=free_42, B1'=free_42, C1'=free_44, D1'=free_39, E1'=free_39, F1'=free_41, G1'=free_43, [ free_42>=1 && free_43>=21 && free_38==0 ], cost: 2
     65: f0 -> f94 : B'=free_24, C'=free_24, D'=0, E'=free_27, L'=1, M'=0, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && free==0 ], cost: 3
     71: f0 -> f94 : B'=free_31, C'=free_31, D'=0, E'=free_36, L'=1, M'=0, Y'=free_33, Z'=free_35, A1'=free_37, B1'=free_37, C1'=free_32, D1'=free_34, E1'=free_34, F1'=free_36, G1'=free_35, [ free_37>=1 && 20>=free_35 && free_35>=5 && 0>=1+free_31 && free==0 ], cost: 3


Applied chaining over branches and pruning:
  Start location: f0
      6: f80 -> f84 : [ 0>=1+Q ], cost: 1
      7: f80 -> f84 : [ Q>=1 ], cost: 1
     22: f80 -> f84 : Q'=0, [ Q==0 ], cost: 1
      3: f89 -> f48 : F'=free_2, [ E>=1 ], cost: 1
     19: f89 -> f94 : L'=1, [ 0>=E ], cost: 1
     82: f48 -> f80 : F'=-1, G'=free_12, H'=free_12, Q'=0, J'=free_3, N'=free_3, O'=0, P'=0, Q_1'=0, R'=0, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && 0>=1+free_12 ], cost: 3
     83: f48 -> f80 : F'=-1, G'=free_12, H'=free_12, Q'=0, J'=free_3, K'=0, N'=free_3, O'=0, P'=0, Q_1'=free_7, R'=free_7, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && 0>=1+free_12 && 0>=1+free_7 && K==0 ], cost: 4
     93: f48 -> f80 : F'=-1, G'=free_12, H'=free_12, Q'=0, J'=free_4, K'=0, N'=free_4, O'=0, P'=0, Q_1'=free_8, R'=free_8, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && free_12>=1 && free_8>=1 && K==0 ], cost: 4
    116: f48 -> f80 : F'=-1, G'=free_12, H'=free_12, Q'=1, J'=free_3, N'=free_3, O'=0, P'=0, Q_1'=free_7, R'=free_7, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && 0>=1+free_12 && 0>=1+free_7 && 0>=1+K && A>=1 ], cost: 5
    119: f48 -> f80 : F'=-1, G'=free_12, H'=free_12, Q'=1, J'=free_3, N'=free_3, O'=0, P'=0, Q_1'=free_7, R'=free_7, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && 0>=1+free_12 && 0>=1+free_7 && K>=1 && A>=1 ], cost: 5
     28: f48 -> f89 : E'=-1+E, S'=F, T'=0, U'=0, [ F>=0 ], cost: 1
     29: f48 -> f89 : E'=-1+E, S'=F, T'=0, U'=0, [ 0>=2+F ], cost: 1
     34: f48 -> f89 : E'=-1+E, F'=-1, S'=-1, T'=0, U'=0, V'=0, W'=0, [ 1+F==0 ], cost: 1
     51: f48 -> f89 : E'=-1+E, F'=-1, G'=0, H'=0, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && free_12==0 ], cost: 2
     54: f48 -> f89 : E'=-1+E, F'=-1, G'=0, H'=0, S'=-1, T'=0, U'=0, V'=free_13, W'=free_13, [ free_13>=1 && 1+F==0 && free_14==0 ], cost: 2
     85: f48 -> f84 : F'=-1, G'=free_12, H'=free_12, Q'=0, J'=free_3, N'=free_3, O'=free_5, P'=free_5, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && 0>=1+free_12 && 0>=1+free_5 ], cost: 3
     86: f48 -> f84 : F'=-1, G'=free_12, H'=free_12, Q'=0, J'=free_3, N'=free_3, O'=free_6, P'=free_6, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && 0>=1+free_12 && free_6>=1 ], cost: 3
     95: f48 -> f84 : F'=-1, G'=free_12, H'=free_12, Q'=0, J'=free_4, N'=free_4, O'=free_6, P'=free_6, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && free_12>=1 && free_6>=1 ], cost: 3
    103: f48 -> f84 : F'=-1, G'=free_14, H'=free_14, Q'=0, J'=free_3, N'=free_3, O'=free_5, P'=free_5, S'=-1, T'=0, U'=0, V'=free_13, W'=free_13, [ free_13>=1 && 1+F==0 && 0>=1+free_14 && 0>=1+free_5 ], cost: 3
    104: f48 -> f84 : F'=-1, G'=free_14, H'=free_14, Q'=0, J'=free_3, N'=free_3, O'=free_6, P'=free_6, S'=-1, T'=0, U'=0, V'=free_13, W'=free_13, [ free_13>=1 && 1+F==0 && 0>=1+free_14 && free_6>=1 ], cost: 3
     30: f48 -> f94 : L'=1, S'=F, T'=free_9, U'=free_9, [ 0>=1+free_9 ], cost: 1
     31: f48 -> f94 : L'=1, S'=F, T'=free_10, U'=free_10, [ free_10>=1 ], cost: 1
     14: f84 -> f89 : E'=-1+E, Q'=0, [ Q==0 ], cost: 1
     20: f84 -> f89 : E'=-1+E, [ 0>=1+Q ], cost: 1
     21: f84 -> f89 : E'=-1+E, [ Q>=1 ], cost: 1
     41: f94 -> [14] : [], cost: INF
     63: f0 -> f48 : B'=free_24, C'=free_24, D'=free, E'=free_15, F'=free_16, L'=free_30, M'=free, X'=free_15, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && 0>=1+free ], cost: 3
     64: f0 -> f48 : B'=free_24, C'=free_24, D'=free, E'=free_17, F'=free_18, L'=free_30, M'=free, X'=free_17, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && free>=1 ], cost: 3
     67: f0 -> f48 : B'=free_24, C'=free_24, D'=free_1, E'=free_17, F'=free_18, L'=free_30, M'=free_1, X'=free_17, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && free_24>=1 && free_1>=1 ], cost: 3
     69: f0 -> f48 : B'=free_31, C'=free_31, D'=free, E'=free_15, F'=free_16, L'=free_32, M'=free, X'=free_15, Y'=free_33, Z'=free_35, A1'=free_37, B1'=free_37, C1'=free_32, D1'=free_34, E1'=free_34, F1'=free_36, G1'=free_35, [ free_37>=1 && 20>=free_35 && free_35>=5 && 0>=1+free_31 && 0>=1+free ], cost: 3
     70: f0 -> f48 : B'=free_31, C'=free_31, D'=free, E'=free_17, F'=free_18, L'=free_32, M'=free, X'=free_17, Y'=free_33, Z'=free_35, A1'=free_37, B1'=free_37, C1'=free_32, D1'=free_34, E1'=free_34, F1'=free_36, G1'=free_35, [ free_37>=1 && 20>=free_35 && free_35>=5 && 0>=1+free_31 && free>=1 ], cost: 3
     37: f0 -> f94 : E'=free_21, L'=1, Y'=free_20, Z'=free_20, A1'=free_22, B1'=free_22, C1'=free_23, D1'=free_19, E1'=free_19, F1'=free_21, [ 0>=free_22 ], cost: 1
     44: f0 -> f94 : B'=0, C'=0, E'=free_27, L'=1, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && free_24==0 ], cost: 2
     50: f0 -> f94 : B'=0, C'=0, E'=free_41, L'=1, Y'=free_40, Z'=20, A1'=free_42, B1'=free_42, C1'=free_44, D1'=free_39, E1'=free_39, F1'=free_41, G1'=free_43, [ free_42>=1 && free_43>=21 && free_38==0 ], cost: 2
     65: f0 -> f94 : B'=free_24, C'=free_24, D'=0, E'=free_27, L'=1, M'=0, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && free==0 ], cost: 3
     71: f0 -> f94 : B'=free_31, C'=free_31, D'=0, E'=free_36, L'=1, M'=0, Y'=free_33, Z'=free_35, A1'=free_37, B1'=free_37, C1'=free_32, D1'=free_34, E1'=free_34, F1'=free_36, G1'=free_35, [ free_37>=1 && 20>=free_35 && free_35>=5 && 0>=1+free_31 && free==0 ], cost: 3


Applied chaining over branches and pruning:
  Start location: f0
      3: f89 -> f48 : F'=free_2, [ E>=1 ], cost: 1
     19: f89 -> f94 : L'=1, [ 0>=E ], cost: 1
     28: f48 -> f89 : E'=-1+E, S'=F, T'=0, U'=0, [ F>=0 ], cost: 1
     29: f48 -> f89 : E'=-1+E, S'=F, T'=0, U'=0, [ 0>=2+F ], cost: 1
     34: f48 -> f89 : E'=-1+E, F'=-1, S'=-1, T'=0, U'=0, V'=0, W'=0, [ 1+F==0 ], cost: 1
     51: f48 -> f89 : E'=-1+E, F'=-1, G'=0, H'=0, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && free_12==0 ], cost: 2
     54: f48 -> f89 : E'=-1+E, F'=-1, G'=0, H'=0, S'=-1, T'=0, U'=0, V'=free_13, W'=free_13, [ free_13>=1 && 1+F==0 && free_14==0 ], cost: 2
     85: f48 -> f84 : F'=-1, G'=free_12, H'=free_12, Q'=0, J'=free_3, N'=free_3, O'=free_5, P'=free_5, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && 0>=1+free_12 && 0>=1+free_5 ], cost: 3
     86: f48 -> f84 : F'=-1, G'=free_12, H'=free_12, Q'=0, J'=free_3, N'=free_3, O'=free_6, P'=free_6, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && 0>=1+free_12 && free_6>=1 ], cost: 3
    103: f48 -> f84 : F'=-1, G'=free_14, H'=free_14, Q'=0, J'=free_3, N'=free_3, O'=free_5, P'=free_5, S'=-1, T'=0, U'=0, V'=free_13, W'=free_13, [ free_13>=1 && 1+F==0 && 0>=1+free_14 && 0>=1+free_5 ], cost: 3
    104: f48 -> f84 : F'=-1, G'=free_14, H'=free_14, Q'=0, J'=free_3, N'=free_3, O'=free_6, P'=free_6, S'=-1, T'=0, U'=0, V'=free_13, W'=free_13, [ free_13>=1 && 1+F==0 && 0>=1+free_14 && free_6>=1 ], cost: 3
    129: f48 -> f84 : F'=-1, G'=free_12, H'=free_12, Q'=0, J'=free_3, N'=free_3, O'=0, P'=0, Q_1'=0, R'=0, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && 0>=1+free_12 && 0==0 ], cost: 4
     30: f48 -> f94 : L'=1, S'=F, T'=free_9, U'=free_9, [ 0>=1+free_9 ], cost: 1
     31: f48 -> f94 : L'=1, S'=F, T'=free_10, U'=free_10, [ free_10>=1 ], cost: 1
     14: f84 -> f89 : E'=-1+E, Q'=0, [ Q==0 ], cost: 1
     20: f84 -> f89 : E'=-1+E, [ 0>=1+Q ], cost: 1
     21: f84 -> f89 : E'=-1+E, [ Q>=1 ], cost: 1
     41: f94 -> [14] : [], cost: INF
     63: f0 -> f48 : B'=free_24, C'=free_24, D'=free, E'=free_15, F'=free_16, L'=free_30, M'=free, X'=free_15, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && 0>=1+free ], cost: 3
     64: f0 -> f48 : B'=free_24, C'=free_24, D'=free, E'=free_17, F'=free_18, L'=free_30, M'=free, X'=free_17, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && free>=1 ], cost: 3
     67: f0 -> f48 : B'=free_24, C'=free_24, D'=free_1, E'=free_17, F'=free_18, L'=free_30, M'=free_1, X'=free_17, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && free_24>=1 && free_1>=1 ], cost: 3
     69: f0 -> f48 : B'=free_31, C'=free_31, D'=free, E'=free_15, F'=free_16, L'=free_32, M'=free, X'=free_15, Y'=free_33, Z'=free_35, A1'=free_37, B1'=free_37, C1'=free_32, D1'=free_34, E1'=free_34, F1'=free_36, G1'=free_35, [ free_37>=1 && 20>=free_35 && free_35>=5 && 0>=1+free_31 && 0>=1+free ], cost: 3
     70: f0 -> f48 : B'=free_31, C'=free_31, D'=free, E'=free_17, F'=free_18, L'=free_32, M'=free, X'=free_17, Y'=free_33, Z'=free_35, A1'=free_37, B1'=free_37, C1'=free_32, D1'=free_34, E1'=free_34, F1'=free_36, G1'=free_35, [ free_37>=1 && 20>=free_35 && free_35>=5 && 0>=1+free_31 && free>=1 ], cost: 3
     37: f0 -> f94 : E'=free_21, L'=1, Y'=free_20, Z'=free_20, A1'=free_22, B1'=free_22, C1'=free_23, D1'=free_19, E1'=free_19, F1'=free_21, [ 0>=free_22 ], cost: 1
     44: f0 -> f94 : B'=0, C'=0, E'=free_27, L'=1, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && free_24==0 ], cost: 2
     50: f0 -> f94 : B'=0, C'=0, E'=free_41, L'=1, Y'=free_40, Z'=20, A1'=free_42, B1'=free_42, C1'=free_44, D1'=free_39, E1'=free_39, F1'=free_41, G1'=free_43, [ free_42>=1 && free_43>=21 && free_38==0 ], cost: 2
     65: f0 -> f94 : B'=free_24, C'=free_24, D'=0, E'=free_27, L'=1, M'=0, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && free==0 ], cost: 3
     71: f0 -> f94 : B'=free_31, C'=free_31, D'=0, E'=free_36, L'=1, M'=0, Y'=free_33, Z'=free_35, A1'=free_37, B1'=free_37, C1'=free_32, D1'=free_34, E1'=free_34, F1'=free_36, G1'=free_35, [ free_37>=1 && 20>=free_35 && free_35>=5 && 0>=1+free_31 && free==0 ], cost: 3


Applied chaining over branches and pruning:
  Start location: f0
      3: f89 -> f48 : F'=free_2, [ E>=1 ], cost: 1
     19: f89 -> f94 : L'=1, [ 0>=E ], cost: 1
     28: f48 -> f89 : E'=-1+E, S'=F, T'=0, U'=0, [ F>=0 ], cost: 1
     29: f48 -> f89 : E'=-1+E, S'=F, T'=0, U'=0, [ 0>=2+F ], cost: 1
     51: f48 -> f89 : E'=-1+E, F'=-1, G'=0, H'=0, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && free_12==0 ], cost: 2
     54: f48 -> f89 : E'=-1+E, F'=-1, G'=0, H'=0, S'=-1, T'=0, U'=0, V'=free_13, W'=free_13, [ free_13>=1 && 1+F==0 && free_14==0 ], cost: 2
    134: f48 -> f89 : E'=-1+E, F'=-1, G'=free_12, H'=free_12, Q'=0, J'=free_3, N'=free_3, O'=free_5, P'=free_5, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && 0>=1+free_12 && 0>=1+free_5 && 0==0 ], cost: 4
     30: f48 -> f94 : L'=1, S'=F, T'=free_9, U'=free_9, [ 0>=1+free_9 ], cost: 1
     31: f48 -> f94 : L'=1, S'=F, T'=free_10, U'=free_10, [ free_10>=1 ], cost: 1
     41: f94 -> [14] : [], cost: INF
     63: f0 -> f48 : B'=free_24, C'=free_24, D'=free, E'=free_15, F'=free_16, L'=free_30, M'=free, X'=free_15, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && 0>=1+free ], cost: 3
     64: f0 -> f48 : B'=free_24, C'=free_24, D'=free, E'=free_17, F'=free_18, L'=free_30, M'=free, X'=free_17, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && free>=1 ], cost: 3
     67: f0 -> f48 : B'=free_24, C'=free_24, D'=free_1, E'=free_17, F'=free_18, L'=free_30, M'=free_1, X'=free_17, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && free_24>=1 && free_1>=1 ], cost: 3
     69: f0 -> f48 : B'=free_31, C'=free_31, D'=free, E'=free_15, F'=free_16, L'=free_32, M'=free, X'=free_15, Y'=free_33, Z'=free_35, A1'=free_37, B1'=free_37, C1'=free_32, D1'=free_34, E1'=free_34, F1'=free_36, G1'=free_35, [ free_37>=1 && 20>=free_35 && free_35>=5 && 0>=1+free_31 && 0>=1+free ], cost: 3
     70: f0 -> f48 : B'=free_31, C'=free_31, D'=free, E'=free_17, F'=free_18, L'=free_32, M'=free, X'=free_17, Y'=free_33, Z'=free_35, A1'=free_37, B1'=free_37, C1'=free_32, D1'=free_34, E1'=free_34, F1'=free_36, G1'=free_35, [ free_37>=1 && 20>=free_35 && free_35>=5 && 0>=1+free_31 && free>=1 ], cost: 3
     37: f0 -> f94 : E'=free_21, L'=1, Y'=free_20, Z'=free_20, A1'=free_22, B1'=free_22, C1'=free_23, D1'=free_19, E1'=free_19, F1'=free_21, [ 0>=free_22 ], cost: 1
     44: f0 -> f94 : B'=0, C'=0, E'=free_27, L'=1, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && free_24==0 ], cost: 2
     50: f0 -> f94 : B'=0, C'=0, E'=free_41, L'=1, Y'=free_40, Z'=20, A1'=free_42, B1'=free_42, C1'=free_44, D1'=free_39, E1'=free_39, F1'=free_41, G1'=free_43, [ free_42>=1 && free_43>=21 && free_38==0 ], cost: 2
     65: f0 -> f94 : B'=free_24, C'=free_24, D'=0, E'=free_27, L'=1, M'=0, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && free==0 ], cost: 3
     71: f0 -> f94 : B'=free_31, C'=free_31, D'=0, E'=free_36, L'=1, M'=0, Y'=free_33, Z'=free_35, A1'=free_37, B1'=free_37, C1'=free_32, D1'=free_34, E1'=free_34, F1'=free_36, G1'=free_35, [ free_37>=1 && 20>=free_35 && free_35>=5 && 0>=1+free_31 && free==0 ], cost: 3


Applied chaining over branches and pruning:
  Start location: f0
    139: f48 -> f48 : E'=-1+E, F'=free_2, S'=F, T'=0, U'=0, [ F>=0 && -1+E>=1 ], cost: 2
    141: f48 -> f48 : E'=-1+E, F'=free_2, S'=F, T'=0, U'=0, [ 0>=2+F && -1+E>=1 ], cost: 2
    143: f48 -> f48 : E'=-1+E, F'=free_2, G'=0, H'=0, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && free_12==0 && -1+E>=1 ], cost: 3
    145: f48 -> f48 : E'=-1+E, F'=free_2, G'=0, H'=0, S'=-1, T'=0, U'=0, V'=free_13, W'=free_13, [ free_13>=1 && 1+F==0 && free_14==0 && -1+E>=1 ], cost: 3
    147: f48 -> f48 : E'=-1+E, F'=free_2, G'=free_12, H'=free_12, Q'=0, J'=free_3, N'=free_3, O'=free_5, P'=free_5, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && 0>=1+free_12 && 0>=1+free_5 && 0==0 && -1+E>=1 ], cost: 5
     30: f48 -> f94 : L'=1, S'=F, T'=free_9, U'=free_9, [ 0>=1+free_9 ], cost: 1
     31: f48 -> f94 : L'=1, S'=F, T'=free_10, U'=free_10, [ free_10>=1 ], cost: 1
    140: f48 -> f94 : E'=-1+E, L'=1, S'=F, T'=0, U'=0, [ F>=0 && 0>=-1+E ], cost: 2
    142: f48 -> f94 : E'=-1+E, L'=1, S'=F, T'=0, U'=0, [ 0>=2+F && 0>=-1+E ], cost: 2
    144: f48 -> f94 : E'=-1+E, F'=-1, G'=0, H'=0, L'=1, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && free_12==0 && 0>=-1+E ], cost: 3
     41: f94 -> [14] : [], cost: INF
     63: f0 -> f48 : B'=free_24, C'=free_24, D'=free, E'=free_15, F'=free_16, L'=free_30, M'=free, X'=free_15, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && 0>=1+free ], cost: 3
     64: f0 -> f48 : B'=free_24, C'=free_24, D'=free, E'=free_17, F'=free_18, L'=free_30, M'=free, X'=free_17, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && free>=1 ], cost: 3
     67: f0 -> f48 : B'=free_24, C'=free_24, D'=free_1, E'=free_17, F'=free_18, L'=free_30, M'=free_1, X'=free_17, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && free_24>=1 && free_1>=1 ], cost: 3
     69: f0 -> f48 : B'=free_31, C'=free_31, D'=free, E'=free_15, F'=free_16, L'=free_32, M'=free, X'=free_15, Y'=free_33, Z'=free_35, A1'=free_37, B1'=free_37, C1'=free_32, D1'=free_34, E1'=free_34, F1'=free_36, G1'=free_35, [ free_37>=1 && 20>=free_35 && free_35>=5 && 0>=1+free_31 && 0>=1+free ], cost: 3
     70: f0 -> f48 : B'=free_31, C'=free_31, D'=free, E'=free_17, F'=free_18, L'=free_32, M'=free, X'=free_17, Y'=free_33, Z'=free_35, A1'=free_37, B1'=free_37, C1'=free_32, D1'=free_34, E1'=free_34, F1'=free_36, G1'=free_35, [ free_37>=1 && 20>=free_35 && free_35>=5 && 0>=1+free_31 && free>=1 ], cost: 3
     37: f0 -> f94 : E'=free_21, L'=1, Y'=free_20, Z'=free_20, A1'=free_22, B1'=free_22, C1'=free_23, D1'=free_19, E1'=free_19, F1'=free_21, [ 0>=free_22 ], cost: 1
     44: f0 -> f94 : B'=0, C'=0, E'=free_27, L'=1, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && free_24==0 ], cost: 2
     50: f0 -> f94 : B'=0, C'=0, E'=free_41, L'=1, Y'=free_40, Z'=20, A1'=free_42, B1'=free_42, C1'=free_44, D1'=free_39, E1'=free_39, F1'=free_41, G1'=free_43, [ free_42>=1 && free_43>=21 && free_38==0 ], cost: 2
     65: f0 -> f94 : B'=free_24, C'=free_24, D'=0, E'=free_27, L'=1, M'=0, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && free==0 ], cost: 3
     71: f0 -> f94 : B'=free_31, C'=free_31, D'=0, E'=free_36, L'=1, M'=0, Y'=free_33, Z'=free_35, A1'=free_37, B1'=free_37, C1'=free_32, D1'=free_34, E1'=free_34, F1'=free_36, G1'=free_35, [ free_37>=1 && 20>=free_35 && free_35>=5 && 0>=1+free_31 && free==0 ], cost: 3

Eliminating 5 self-loops for location f48
  Removing the self-loops: 139 141 143 145 147.
Adding an epsilon transition (to model nonexecution of the loops): 154.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
    149: f48 -> [15] : E'=-1+E, F'=free_2, S'=F, T'=0, U'=0, [ F>=0 && -1+E>=1 ], cost: 2
    150: f48 -> [15] : E'=-1+E, F'=free_2, S'=F, T'=0, U'=0, [ 0>=2+F && -1+E>=1 ], cost: 2
    151: f48 -> [15] : E'=-1+E, F'=free_2, G'=0, H'=0, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && -1+E>=1 ], cost: 3
    152: f48 -> [15] : E'=-1+E, F'=free_2, G'=0, H'=0, S'=-1, T'=0, U'=0, V'=free_13, W'=free_13, [ free_13>=1 && 1+F==0 && -1+E>=1 ], cost: 3
    153: f48 -> [15] : E'=-1+E, F'=free_2, G'=free_12, H'=free_12, Q'=0, J'=free_3, N'=free_3, O'=free_5, P'=free_5, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && 0>=1+free_12 && 0>=1+free_5 && -1+E>=1 ], cost: 5
    154: f48 -> [15] : [], cost: 0
     41: f94 -> [14] : [], cost: INF
     63: f0 -> f48 : B'=free_24, C'=free_24, D'=free, E'=free_15, F'=free_16, L'=free_30, M'=free, X'=free_15, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && 0>=1+free ], cost: 3
     64: f0 -> f48 : B'=free_24, C'=free_24, D'=free, E'=free_17, F'=free_18, L'=free_30, M'=free, X'=free_17, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && free>=1 ], cost: 3
     67: f0 -> f48 : B'=free_24, C'=free_24, D'=free_1, E'=free_17, F'=free_18, L'=free_30, M'=free_1, X'=free_17, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && free_24>=1 && free_1>=1 ], cost: 3
     69: f0 -> f48 : B'=free_31, C'=free_31, D'=free, E'=free_15, F'=free_16, L'=free_32, M'=free, X'=free_15, Y'=free_33, Z'=free_35, A1'=free_37, B1'=free_37, C1'=free_32, D1'=free_34, E1'=free_34, F1'=free_36, G1'=free_35, [ free_37>=1 && 20>=free_35 && free_35>=5 && 0>=1+free_31 && 0>=1+free ], cost: 3
     70: f0 -> f48 : B'=free_31, C'=free_31, D'=free, E'=free_17, F'=free_18, L'=free_32, M'=free, X'=free_17, Y'=free_33, Z'=free_35, A1'=free_37, B1'=free_37, C1'=free_32, D1'=free_34, E1'=free_34, F1'=free_36, G1'=free_35, [ free_37>=1 && 20>=free_35 && free_35>=5 && 0>=1+free_31 && free>=1 ], cost: 3
     37: f0 -> f94 : E'=free_21, L'=1, Y'=free_20, Z'=free_20, A1'=free_22, B1'=free_22, C1'=free_23, D1'=free_19, E1'=free_19, F1'=free_21, [ 0>=free_22 ], cost: 1
     44: f0 -> f94 : B'=0, C'=0, E'=free_27, L'=1, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && free_24==0 ], cost: 2
     50: f0 -> f94 : B'=0, C'=0, E'=free_41, L'=1, Y'=free_40, Z'=20, A1'=free_42, B1'=free_42, C1'=free_44, D1'=free_39, E1'=free_39, F1'=free_41, G1'=free_43, [ free_42>=1 && free_43>=21 && free_38==0 ], cost: 2
     65: f0 -> f94 : B'=free_24, C'=free_24, D'=0, E'=free_27, L'=1, M'=0, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && free==0 ], cost: 3
     71: f0 -> f94 : B'=free_31, C'=free_31, D'=0, E'=free_36, L'=1, M'=0, Y'=free_33, Z'=free_35, A1'=free_37, B1'=free_37, C1'=free_32, D1'=free_34, E1'=free_34, F1'=free_36, G1'=free_35, [ free_37>=1 && 20>=free_35 && free_35>=5 && 0>=1+free_31 && free==0 ], cost: 3
     30: [15] -> f94 : L'=1, S'=F, T'=free_9, U'=free_9, [ 0>=1+free_9 ], cost: 1
     31: [15] -> f94 : L'=1, S'=F, T'=free_10, U'=free_10, [ free_10>=1 ], cost: 1
    140: [15] -> f94 : E'=-1+E, L'=1, S'=F, T'=0, U'=0, [ F>=0 && 0>=-1+E ], cost: 2
    142: [15] -> f94 : E'=-1+E, L'=1, S'=F, T'=0, U'=0, [ 0>=2+F && 0>=-1+E ], cost: 2
    144: [15] -> f94 : E'=-1+E, F'=-1, G'=0, H'=0, L'=1, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && free_12==0 && 0>=-1+E ], cost: 3


Applied chaining over branches and pruning:
  Start location: f0
     41: f94 -> [14] : [], cost: INF
     37: f0 -> f94 : E'=free_21, L'=1, Y'=free_20, Z'=free_20, A1'=free_22, B1'=free_22, C1'=free_23, D1'=free_19, E1'=free_19, F1'=free_21, [ 0>=free_22 ], cost: 1
     44: f0 -> f94 : B'=0, C'=0, E'=free_27, L'=1, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && free_24==0 ], cost: 2
     50: f0 -> f94 : B'=0, C'=0, E'=free_41, L'=1, Y'=free_40, Z'=20, A1'=free_42, B1'=free_42, C1'=free_44, D1'=free_39, E1'=free_39, F1'=free_41, G1'=free_43, [ free_42>=1 && free_43>=21 && free_38==0 ], cost: 2
     65: f0 -> f94 : B'=free_24, C'=free_24, D'=0, E'=free_27, L'=1, M'=0, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && free==0 ], cost: 3
     71: f0 -> f94 : B'=free_31, C'=free_31, D'=0, E'=free_36, L'=1, M'=0, Y'=free_33, Z'=free_35, A1'=free_37, B1'=free_37, C1'=free_32, D1'=free_34, E1'=free_34, F1'=free_36, G1'=free_35, [ free_37>=1 && 20>=free_35 && free_35>=5 && 0>=1+free_31 && free==0 ], cost: 3
    155: f0 -> [15] : B'=free_24, C'=free_24, D'=free, E'=-1+free_15, F'=free_2, L'=free_30, M'=free, S'=free_16, T'=0, U'=0, X'=free_15, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && 0>=1+free && free_16>=0 && -1+free_15>=1 ], cost: 5
    156: f0 -> [15] : B'=free_24, C'=free_24, D'=free, E'=-1+free_15, F'=free_2, L'=free_30, M'=free, S'=free_16, T'=0, U'=0, X'=free_15, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && 0>=1+free && 0>=2+free_16 && -1+free_15>=1 ], cost: 5
    158: f0 -> [15] : B'=free_24, C'=free_24, D'=free, E'=-1+free_15, F'=free_2, G'=0, H'=0, L'=free_30, M'=free, S'=-1, T'=0, U'=0, V'=free_13, W'=free_13, X'=free_15, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && 0>=1+free && free_13>=1 && 1+free_16==0 && -1+free_15>=1 ], cost: 6
    162: f0 -> [15] : B'=free_24, C'=free_24, D'=free, E'=-1+free_17, F'=free_2, L'=free_30, M'=free, S'=free_18, T'=0, U'=0, X'=free_17, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && free>=1 && 0>=2+free_18 && -1+free_17>=1 ], cost: 5
    170: f0 -> [15] : B'=free_24, C'=free_24, D'=free_1, E'=-1+free_17, F'=free_2, G'=0, H'=0, L'=free_30, M'=free_1, S'=-1, T'=0, U'=0, V'=free_13, W'=free_13, X'=free_17, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && free_24>=1 && free_1>=1 && free_13>=1 && 1+free_18==0 && -1+free_17>=1 ], cost: 6
     30: [15] -> f94 : L'=1, S'=F, T'=free_9, U'=free_9, [ 0>=1+free_9 ], cost: 1
     31: [15] -> f94 : L'=1, S'=F, T'=free_10, U'=free_10, [ free_10>=1 ], cost: 1
    140: [15] -> f94 : E'=-1+E, L'=1, S'=F, T'=0, U'=0, [ F>=0 && 0>=-1+E ], cost: 2
    142: [15] -> f94 : E'=-1+E, L'=1, S'=F, T'=0, U'=0, [ 0>=2+F && 0>=-1+E ], cost: 2
    144: [15] -> f94 : E'=-1+E, F'=-1, G'=0, H'=0, L'=1, S'=-1, T'=0, U'=0, V'=free_11, W'=free_11, [ 0>=1+free_11 && 1+F==0 && free_12==0 && 0>=-1+E ], cost: 3


Applied chaining over branches and pruning:
  Start location: f0
     41: f94 -> [14] : [], cost: INF
     37: f0 -> f94 : E'=free_21, L'=1, Y'=free_20, Z'=free_20, A1'=free_22, B1'=free_22, C1'=free_23, D1'=free_19, E1'=free_19, F1'=free_21, [ 0>=free_22 ], cost: 1
     44: f0 -> f94 : B'=0, C'=0, E'=free_27, L'=1, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && free_24==0 ], cost: 2
     65: f0 -> f94 : B'=free_24, C'=free_24, D'=0, E'=free_27, L'=1, M'=0, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && free==0 ], cost: 3
    187: f0 -> f94 : B'=free_24, C'=free_24, D'=free, E'=-2+free_15, F'=free_2, L'=1, M'=free, S'=free_2, T'=0, U'=0, X'=free_15, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && 0>=1+free && free_16>=0 && -1+free_15>=1 && free_2>=0 && 0>=-2+free_15 ], cost: 7
    195: f0 -> f94 : B'=free_24, C'=free_24, D'=free, E'=-1+free_15, F'=free_2, G'=0, H'=0, L'=1, M'=free, S'=free_2, T'=free_9, U'=free_9, V'=free_13, W'=free_13, X'=free_15, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && 0>=1+free && free_13>=1 && 1+free_16==0 && -1+free_15>=1 && 0>=1+free_9 ], cost: 7


Applied chaining over branches and pruning:
  Start location: f0
    210: f0 -> [14] : E'=free_21, L'=1, Y'=free_20, Z'=free_20, A1'=free_22, B1'=free_22, C1'=free_23, D1'=free_19, E1'=free_19, F1'=free_21, [ 0>=free_22 ], cost: INF
    211: f0 -> [14] : B'=0, C'=0, E'=free_27, L'=1, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && free_24==0 ], cost: INF
    212: f0 -> [14] : B'=free_24, C'=free_24, D'=0, E'=free_27, L'=1, M'=0, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && free==0 ], cost: INF
    213: f0 -> [14] : B'=free_24, C'=free_24, D'=free, E'=-2+free_15, F'=free_2, L'=1, M'=free, S'=free_2, T'=0, U'=0, X'=free_15, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && 0>=1+free && free_16>=0 && -1+free_15>=1 && free_2>=0 && 0>=-2+free_15 ], cost: INF
    214: f0 -> [14] : B'=free_24, C'=free_24, D'=free, E'=-1+free_15, F'=free_2, G'=0, H'=0, L'=1, M'=free, S'=free_2, T'=free_9, U'=free_9, V'=free_13, W'=free_13, X'=free_15, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && 0>=1+free && free_13>=1 && 1+free_16==0 && -1+free_15>=1 && 0>=1+free_9 ], cost: INF


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
    210: f0 -> [14] : E'=free_21, L'=1, Y'=free_20, Z'=free_20, A1'=free_22, B1'=free_22, C1'=free_23, D1'=free_19, E1'=free_19, F1'=free_21, [ 0>=free_22 ], cost: INF
    211: f0 -> [14] : B'=0, C'=0, E'=free_27, L'=1, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && free_24==0 ], cost: INF
    212: f0 -> [14] : B'=free_24, C'=free_24, D'=0, E'=free_27, L'=1, M'=0, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && free==0 ], cost: INF
    213: f0 -> [14] : B'=free_24, C'=free_24, D'=free, E'=-2+free_15, F'=free_2, L'=1, M'=free, S'=free_2, T'=0, U'=0, X'=free_15, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && 0>=1+free && free_16>=0 && -1+free_15>=1 && free_2>=0 && 0>=-2+free_15 ], cost: INF
    214: f0 -> [14] : B'=free_24, C'=free_24, D'=free, E'=-1+free_15, F'=free_2, G'=0, H'=0, L'=1, M'=free, S'=free_2, T'=free_9, U'=free_9, V'=free_13, W'=free_13, X'=free_15, Y'=free_26, Z'=5, A1'=free_28, B1'=free_28, C1'=free_30, D1'=free_25, E1'=free_25, F1'=free_27, G1'=free_29, [ free_28>=1 && 4>=free_29 && 0>=1+free_24 && 0>=1+free && free_13>=1 && 1+free_16==0 && -1+free_15>=1 && 0>=1+free_9 ], cost: INF


Computing complexity for remaining 5 transitions.

Found new complexity INF, because: INF sat.


The final runtime is determined by this resulting transition:
  Final Guard: 0>=free_22
  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,?)