Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f0 -> f1 : [], cost: 1
      3: f1 -> f1 : A'=free_9, B'=free_10, C'=free_8, D'=2, E'=free_7, F'=free_9, G'=free_10, H'=free_8, Q'=2, J'=free_7, K'=1, [ free_11>=1 && 7>=free_11 && free_12>=1 && 7>=free_12 && free_7>=1 && 7>=free_7 && 1>=free_9 && free_9>=0 ], cost: 1
      1: f1 -> f2 : A'=0, B'=free_1, C'=free_2, D'=3, E'=free, F'=0, G'=free_1, H'=free_2, Q'=3, J'=free, K'=2, [ 7>=free && free>=1 ], cost: 1
      4: f2 -> f1 : A'=free_15, B'=free_16, C'=free_14, D'=2, E'=free_13, F'=free_15, G'=free_16, H'=free_14, Q'=2, J'=free_13, K'=1, [ free_17>=1 && 7>=free_17 && free_18>=1 && 7>=free_18 && free_13>=1 && 7>=free_13 && 1>=free_15 && free_15>=0 ], cost: 1
      7: f2 -> f4 : A'=free_35, B'=free_36, C'=free_34, D'=free_33, E'=2, F'=free_35, G'=free_36, H'=free_34, Q'=free_33, J'=2, K'=4, [ free_38>=1 && 7>=free_38 && free_39>=1 && 7>=free_39 && free_40>=1 && 7>=free_40 && free_37>=1 && 7>=free_37 && free_33>=1 && 7>=free_33 && 1>=free_35 && free_35>=0 ], cost: 1
      8: f2 -> f4 : A'=free_43, B'=free_44, C'=free_42, D'=free_41, E'=7, F'=free_43, G'=free_44, H'=free_42, Q'=free_41, J'=7, K'=4, [ free_46>=1 && 7>=free_46 && free_47>=1 && 7>=free_47 && free_48>=1 && 7>=free_48 && free_45>=1 && 7>=free_45 && free_41>=1 && 7>=free_41 && 1>=free_43 && free_43>=0 ], cost: 1
      5: f4 -> f1 : A'=free_21, B'=free_22, C'=free_20, D'=2, E'=free_19, F'=free_21, G'=free_22, H'=free_20, Q'=2, J'=free_19, K'=1, [ free_24>=L && free_25>=M && free_26>=1 && 7>=free_26 && free_23>=1 && 7>=free_23 && free_19>=1 && 7>=free_19 && 1>=free_21 && free_21>=0 ], cost: 1
      6: f4 -> f1 : A'=free_29, B'=free_30, C'=free_28, D'=2, E'=free_27, F'=free_29, G'=free_30, H'=free_28, Q'=2, J'=free_27, K'=1, [ free_31>=1 && 7>=free_31 && free_32>=1 && 7>=free_32 && free_27>=1 && 7>=free_27 && 1>=free_29 && free_29>=0 ], cost: 1
      2: f4 -> f2 : A'=0, B'=free_5, C'=free_6, D'=free_4, E'=free_3, F'=0, G'=free_5, H'=free_6, Q'=free_4, J'=free_3, K'=2, [ L>=1 && L>=1+free_6 && M>=1 && M>=1+free_5 && 7>=free_3 && 7>=free_4 && free_3>=1 && free_4>=1 ], cost: 1


Simplified the transitions:
  Start location: f0
      0: f0 -> f1 : [], cost: 1
      3: f1 -> f1 : A'=free_9, B'=free_10, C'=free_8, D'=2, E'=free_7, F'=free_9, G'=free_10, H'=free_8, Q'=2, J'=free_7, K'=1, [ free_7>=1 && 7>=free_7 && 1>=free_9 && free_9>=0 ], cost: 1
      1: f1 -> f2 : A'=0, B'=free_1, C'=free_2, D'=3, E'=free, F'=0, G'=free_1, H'=free_2, Q'=3, J'=free, K'=2, [ 7>=free && free>=1 ], cost: 1
      4: f2 -> f1 : A'=free_15, B'=free_16, C'=free_14, D'=2, E'=free_13, F'=free_15, G'=free_16, H'=free_14, Q'=2, J'=free_13, K'=1, [ free_13>=1 && 7>=free_13 && 1>=free_15 && free_15>=0 ], cost: 1
      7: f2 -> f4 : A'=free_35, B'=free_36, C'=free_34, D'=free_33, E'=2, F'=free_35, G'=free_36, H'=free_34, Q'=free_33, J'=2, K'=4, [ free_33>=1 && 7>=free_33 && 1>=free_35 && free_35>=0 ], cost: 1
      8: f2 -> f4 : A'=free_43, B'=free_44, C'=free_42, D'=free_41, E'=7, F'=free_43, G'=free_44, H'=free_42, Q'=free_41, J'=7, K'=4, [ free_41>=1 && 7>=free_41 && 1>=free_43 && free_43>=0 ], cost: 1
      5: f4 -> f1 : A'=free_21, B'=free_22, C'=free_20, D'=2, E'=free_19, F'=free_21, G'=free_22, H'=free_20, Q'=2, J'=free_19, K'=1, [ free_19>=1 && 7>=free_19 && 1>=free_21 && free_21>=0 ], cost: 1
      6: f4 -> f1 : A'=free_29, B'=free_30, C'=free_28, D'=2, E'=free_27, F'=free_29, G'=free_30, H'=free_28, Q'=2, J'=free_27, K'=1, [ free_27>=1 && 7>=free_27 && 1>=free_29 && free_29>=0 ], cost: 1
      2: f4 -> f2 : A'=0, B'=free_5, C'=free_6, D'=free_4, E'=free_3, F'=0, G'=free_5, H'=free_6, Q'=free_4, J'=free_3, K'=2, [ L>=1 && L>=1+free_6 && M>=1 && M>=1+free_5 && 7>=free_3 && 7>=free_4 && free_3>=1 && free_4>=1 ], cost: 1

Eliminating 1 self-loops for location f1
  Self-Loop 3 has unbounded runtime, resulting in the new transition 9.
  Removing the self-loops: 3.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f1 : [], cost: 1
      9: f1 -> [4] : [ free_7>=1 && 7>=free_7 && 1>=free_9 && free_9>=0 ], cost: INF
      4: f2 -> f1 : A'=free_15, B'=free_16, C'=free_14, D'=2, E'=free_13, F'=free_15, G'=free_16, H'=free_14, Q'=2, J'=free_13, K'=1, [ free_13>=1 && 7>=free_13 && 1>=free_15 && free_15>=0 ], cost: 1
      7: f2 -> f4 : A'=free_35, B'=free_36, C'=free_34, D'=free_33, E'=2, F'=free_35, G'=free_36, H'=free_34, Q'=free_33, J'=2, K'=4, [ free_33>=1 && 7>=free_33 && 1>=free_35 && free_35>=0 ], cost: 1
      8: f2 -> f4 : A'=free_43, B'=free_44, C'=free_42, D'=free_41, E'=7, F'=free_43, G'=free_44, H'=free_42, Q'=free_41, J'=7, K'=4, [ free_41>=1 && 7>=free_41 && 1>=free_43 && free_43>=0 ], cost: 1
      5: f4 -> f1 : A'=free_21, B'=free_22, C'=free_20, D'=2, E'=free_19, F'=free_21, G'=free_22, H'=free_20, Q'=2, J'=free_19, K'=1, [ free_19>=1 && 7>=free_19 && 1>=free_21 && free_21>=0 ], cost: 1
      6: f4 -> f1 : A'=free_29, B'=free_30, C'=free_28, D'=2, E'=free_27, F'=free_29, G'=free_30, H'=free_28, Q'=2, J'=free_27, K'=1, [ free_27>=1 && 7>=free_27 && 1>=free_29 && free_29>=0 ], cost: 1
      2: f4 -> f2 : A'=0, B'=free_5, C'=free_6, D'=free_4, E'=free_3, F'=0, G'=free_5, H'=free_6, Q'=free_4, J'=free_3, K'=2, [ L>=1 && L>=1+free_6 && M>=1 && M>=1+free_5 && 7>=free_3 && 7>=free_4 && free_3>=1 && free_4>=1 ], cost: 1
      1: [4] -> f2 : A'=0, B'=free_1, C'=free_2, D'=3, E'=free, F'=0, G'=free_1, H'=free_2, Q'=3, J'=free, K'=2, [ 7>=free && free>=1 ], cost: 1


Applied simple chaining:
  Start location: f0
      0: f0 -> f1 : [], cost: 1
      9: f1 -> f2 : A'=0, B'=free_1, C'=free_2, D'=3, E'=free, F'=0, G'=free_1, H'=free_2, Q'=3, J'=free, K'=2, [ free_7>=1 && 7>=free_7 && 1>=free_9 && free_9>=0 && 7>=free && free>=1 ], cost: INF
      4: f2 -> f1 : A'=free_15, B'=free_16, C'=free_14, D'=2, E'=free_13, F'=free_15, G'=free_16, H'=free_14, Q'=2, J'=free_13, K'=1, [ free_13>=1 && 7>=free_13 && 1>=free_15 && free_15>=0 ], cost: 1
      7: f2 -> f4 : A'=free_35, B'=free_36, C'=free_34, D'=free_33, E'=2, F'=free_35, G'=free_36, H'=free_34, Q'=free_33, J'=2, K'=4, [ free_33>=1 && 7>=free_33 && 1>=free_35 && free_35>=0 ], cost: 1
      8: f2 -> f4 : A'=free_43, B'=free_44, C'=free_42, D'=free_41, E'=7, F'=free_43, G'=free_44, H'=free_42, Q'=free_41, J'=7, K'=4, [ free_41>=1 && 7>=free_41 && 1>=free_43 && free_43>=0 ], cost: 1
      5: f4 -> f1 : A'=free_21, B'=free_22, C'=free_20, D'=2, E'=free_19, F'=free_21, G'=free_22, H'=free_20, Q'=2, J'=free_19, K'=1, [ free_19>=1 && 7>=free_19 && 1>=free_21 && free_21>=0 ], cost: 1
      6: f4 -> f1 : A'=free_29, B'=free_30, C'=free_28, D'=2, E'=free_27, F'=free_29, G'=free_30, H'=free_28, Q'=2, J'=free_27, K'=1, [ free_27>=1 && 7>=free_27 && 1>=free_29 && free_29>=0 ], cost: 1
      2: f4 -> f2 : A'=0, B'=free_5, C'=free_6, D'=free_4, E'=free_3, F'=0, G'=free_5, H'=free_6, Q'=free_4, J'=free_3, K'=2, [ L>=1 && L>=1+free_6 && M>=1 && M>=1+free_5 && 7>=free_3 && 7>=free_4 && free_3>=1 && free_4>=1 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f1 : [], cost: 1
      9: f1 -> f2 : A'=0, B'=free_1, C'=free_2, D'=3, E'=free, F'=0, G'=free_1, H'=free_2, Q'=3, J'=free, K'=2, [ free_7>=1 && 7>=free_7 && 1>=free_9 && free_9>=0 && 7>=free && free>=1 ], cost: INF
      4: f2 -> f1 : A'=free_15, B'=free_16, C'=free_14, D'=2, E'=free_13, F'=free_15, G'=free_16, H'=free_14, Q'=2, J'=free_13, K'=1, [ free_13>=1 && 7>=free_13 && 1>=free_15 && free_15>=0 ], cost: 1
     10: f2 -> f1 : A'=free_21, B'=free_22, C'=free_20, D'=2, E'=free_19, F'=free_21, G'=free_22, H'=free_20, Q'=2, J'=free_19, K'=1, [ free_33>=1 && 7>=free_33 && 1>=free_35 && free_35>=0 && free_19>=1 && 7>=free_19 && 1>=free_21 && free_21>=0 ], cost: 2
     11: f2 -> f1 : A'=free_29, B'=free_30, C'=free_28, D'=2, E'=free_27, F'=free_29, G'=free_30, H'=free_28, Q'=2, J'=free_27, K'=1, [ free_33>=1 && 7>=free_33 && 1>=free_35 && free_35>=0 && free_27>=1 && 7>=free_27 && 1>=free_29 && free_29>=0 ], cost: 2
     13: f2 -> f1 : A'=free_21, B'=free_22, C'=free_20, D'=2, E'=free_19, F'=free_21, G'=free_22, H'=free_20, Q'=2, J'=free_19, K'=1, [ free_41>=1 && 7>=free_41 && 1>=free_43 && free_43>=0 && free_19>=1 && 7>=free_19 && 1>=free_21 && free_21>=0 ], cost: 2
     14: f2 -> f1 : A'=free_29, B'=free_30, C'=free_28, D'=2, E'=free_27, F'=free_29, G'=free_30, H'=free_28, Q'=2, J'=free_27, K'=1, [ free_41>=1 && 7>=free_41 && 1>=free_43 && free_43>=0 && free_27>=1 && 7>=free_27 && 1>=free_29 && free_29>=0 ], cost: 2
     12: f2 -> f2 : A'=0, B'=free_5, C'=free_6, D'=free_4, E'=free_3, F'=0, G'=free_5, H'=free_6, Q'=free_4, J'=free_3, K'=2, [ free_33>=1 && 7>=free_33 && 1>=free_35 && free_35>=0 && L>=1 && L>=1+free_6 && M>=1 && M>=1+free_5 && 7>=free_3 && 7>=free_4 && free_3>=1 && free_4>=1 ], cost: 2
     15: f2 -> f2 : A'=0, B'=free_5, C'=free_6, D'=free_4, E'=free_3, F'=0, G'=free_5, H'=free_6, Q'=free_4, J'=free_3, K'=2, [ free_41>=1 && 7>=free_41 && 1>=free_43 && free_43>=0 && L>=1 && L>=1+free_6 && M>=1 && M>=1+free_5 && 7>=free_3 && 7>=free_4 && free_3>=1 && free_4>=1 ], cost: 2

Eliminating 2 self-loops for location f2
  Self-Loop 12 has unbounded runtime, resulting in the new transition 16.
  Self-Loop 15 has unbounded runtime, resulting in the new transition 17.
  Removing the self-loops: 12 15.
Removing duplicate transition: 16.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f1 : [], cost: 1
      9: f1 -> f2 : A'=0, B'=free_1, C'=free_2, D'=3, E'=free, F'=0, G'=free_1, H'=free_2, Q'=3, J'=free, K'=2, [ free_7>=1 && 7>=free_7 && 1>=free_9 && free_9>=0 && 7>=free && free>=1 ], cost: INF
     17: f2 -> [5] : [ L>=1 && L>=1+free_6 && M>=1 && M>=1+free_5 && 7>=free_3 && 7>=free_4 && free_3>=1 && free_4>=1 ], cost: INF
      4: [5] -> f1 : A'=free_15, B'=free_16, C'=free_14, D'=2, E'=free_13, F'=free_15, G'=free_16, H'=free_14, Q'=2, J'=free_13, K'=1, [ free_13>=1 && 7>=free_13 && 1>=free_15 && free_15>=0 ], cost: 1
     10: [5] -> f1 : A'=free_21, B'=free_22, C'=free_20, D'=2, E'=free_19, F'=free_21, G'=free_22, H'=free_20, Q'=2, J'=free_19, K'=1, [ free_33>=1 && 7>=free_33 && 1>=free_35 && free_35>=0 && free_19>=1 && 7>=free_19 && 1>=free_21 && free_21>=0 ], cost: 2
     11: [5] -> f1 : A'=free_29, B'=free_30, C'=free_28, D'=2, E'=free_27, F'=free_29, G'=free_30, H'=free_28, Q'=2, J'=free_27, K'=1, [ free_33>=1 && 7>=free_33 && 1>=free_35 && free_35>=0 && free_27>=1 && 7>=free_27 && 1>=free_29 && free_29>=0 ], cost: 2
     13: [5] -> f1 : A'=free_21, B'=free_22, C'=free_20, D'=2, E'=free_19, F'=free_21, G'=free_22, H'=free_20, Q'=2, J'=free_19, K'=1, [ free_41>=1 && 7>=free_41 && 1>=free_43 && free_43>=0 && free_19>=1 && 7>=free_19 && 1>=free_21 && free_21>=0 ], cost: 2
     14: [5] -> f1 : A'=free_29, B'=free_30, C'=free_28, D'=2, E'=free_27, F'=free_29, G'=free_30, H'=free_28, Q'=2, J'=free_27, K'=1, [ free_41>=1 && 7>=free_41 && 1>=free_43 && free_43>=0 && free_27>=1 && 7>=free_27 && 1>=free_29 && free_29>=0 ], cost: 2


Applied simple chaining:
  Start location: f0
      0: f0 -> f1 : [], cost: 1
      9: f1 -> [5] : A'=0, B'=free_1, C'=free_2, D'=3, E'=free, F'=0, G'=free_1, H'=free_2, Q'=3, J'=free, K'=2, [ free_7>=1 && 7>=free_7 && 1>=free_9 && free_9>=0 && 7>=free && free>=1 && L>=1 && L>=1+free_6 && M>=1 && M>=1+free_5 && 7>=free_3 && 7>=free_4 && free_3>=1 && free_4>=1 ], cost: INF
      4: [5] -> f1 : A'=free_15, B'=free_16, C'=free_14, D'=2, E'=free_13, F'=free_15, G'=free_16, H'=free_14, Q'=2, J'=free_13, K'=1, [ free_13>=1 && 7>=free_13 && 1>=free_15 && free_15>=0 ], cost: 1
     10: [5] -> f1 : A'=free_21, B'=free_22, C'=free_20, D'=2, E'=free_19, F'=free_21, G'=free_22, H'=free_20, Q'=2, J'=free_19, K'=1, [ free_33>=1 && 7>=free_33 && 1>=free_35 && free_35>=0 && free_19>=1 && 7>=free_19 && 1>=free_21 && free_21>=0 ], cost: 2
     11: [5] -> f1 : A'=free_29, B'=free_30, C'=free_28, D'=2, E'=free_27, F'=free_29, G'=free_30, H'=free_28, Q'=2, J'=free_27, K'=1, [ free_33>=1 && 7>=free_33 && 1>=free_35 && free_35>=0 && free_27>=1 && 7>=free_27 && 1>=free_29 && free_29>=0 ], cost: 2
     13: [5] -> f1 : A'=free_21, B'=free_22, C'=free_20, D'=2, E'=free_19, F'=free_21, G'=free_22, H'=free_20, Q'=2, J'=free_19, K'=1, [ free_41>=1 && 7>=free_41 && 1>=free_43 && free_43>=0 && free_19>=1 && 7>=free_19 && 1>=free_21 && free_21>=0 ], cost: 2
     14: [5] -> f1 : A'=free_29, B'=free_30, C'=free_28, D'=2, E'=free_27, F'=free_29, G'=free_30, H'=free_28, Q'=2, J'=free_27, K'=1, [ free_41>=1 && 7>=free_41 && 1>=free_43 && free_43>=0 && free_27>=1 && 7>=free_27 && 1>=free_29 && free_29>=0 ], cost: 2


Applied chaining over branches and pruning:
  Start location: f0
      0: f0 -> f1 : [], cost: 1
     18: f1 -> f1 : A'=free_15, B'=free_16, C'=free_14, D'=2, E'=free_13, F'=free_15, G'=free_16, H'=free_14, Q'=2, J'=free_13, K'=1, [ free_7>=1 && 7>=free_7 && 1>=free_9 && free_9>=0 && 7>=free && free>=1 && L>=1 && L>=1+free_6 && M>=1 && M>=1+free_5 && 7>=free_3 && 7>=free_4 && free_3>=1 && free_4>=1 && free_13>=1 && 7>=free_13 && 1>=free_15 && free_15>=0 ], cost: INF
     19: f1 -> f1 : A'=free_21, B'=free_22, C'=free_20, D'=2, E'=free_19, F'=free_21, G'=free_22, H'=free_20, Q'=2, J'=free_19, K'=1, [ free_7>=1 && 7>=free_7 && 1>=free_9 && free_9>=0 && 7>=free && free>=1 && L>=1 && L>=1+free_6 && M>=1 && M>=1+free_5 && 7>=free_3 && 7>=free_4 && free_3>=1 && free_4>=1 && free_33>=1 && 7>=free_33 && 1>=free_35 && free_35>=0 && free_19>=1 && 7>=free_19 && 1>=free_21 && free_21>=0 ], cost: INF
     20: f1 -> f1 : A'=free_29, B'=free_30, C'=free_28, D'=2, E'=free_27, F'=free_29, G'=free_30, H'=free_28, Q'=2, J'=free_27, K'=1, [ free_7>=1 && 7>=free_7 && 1>=free_9 && free_9>=0 && 7>=free && free>=1 && L>=1 && L>=1+free_6 && M>=1 && M>=1+free_5 && 7>=free_3 && 7>=free_4 && free_3>=1 && free_4>=1 && free_33>=1 && 7>=free_33 && 1>=free_35 && free_35>=0 && free_27>=1 && 7>=free_27 && 1>=free_29 && free_29>=0 ], cost: INF
     21: f1 -> f1 : A'=free_21, B'=free_22, C'=free_20, D'=2, E'=free_19, F'=free_21, G'=free_22, H'=free_20, Q'=2, J'=free_19, K'=1, [ free_7>=1 && 7>=free_7 && 1>=free_9 && free_9>=0 && 7>=free && free>=1 && L>=1 && L>=1+free_6 && M>=1 && M>=1+free_5 && 7>=free_3 && 7>=free_4 && free_3>=1 && free_4>=1 && free_41>=1 && 7>=free_41 && 1>=free_43 && free_43>=0 && free_19>=1 && 7>=free_19 && 1>=free_21 && free_21>=0 ], cost: INF
     22: f1 -> f1 : A'=free_29, B'=free_30, C'=free_28, D'=2, E'=free_27, F'=free_29, G'=free_30, H'=free_28, Q'=2, J'=free_27, K'=1, [ free_7>=1 && 7>=free_7 && 1>=free_9 && free_9>=0 && 7>=free && free>=1 && L>=1 && L>=1+free_6 && M>=1 && M>=1+free_5 && 7>=free_3 && 7>=free_4 && free_3>=1 && free_4>=1 && free_41>=1 && 7>=free_41 && 1>=free_43 && free_43>=0 && free_27>=1 && 7>=free_27 && 1>=free_29 && free_29>=0 ], cost: INF

Eliminating 5 self-loops for location f1
  Removing the self-loops: 18 19 20 21 22.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f1 : [], cost: 1
     23: f1 -> [6] : A'=free_15, B'=free_16, C'=free_14, D'=2, E'=free_13, F'=free_15, G'=free_16, H'=free_14, Q'=2, J'=free_13, K'=1, [ free_7>=1 && 7>=free_7 && 1>=free_9 && free_9>=0 && 7>=free && free>=1 && L>=1 && L>=1+free_6 && M>=1 && M>=1+free_5 && 7>=free_3 && 7>=free_4 && free_3>=1 && free_4>=1 && free_13>=1 && 7>=free_13 && 1>=free_15 && free_15>=0 ], cost: INF
     24: f1 -> [6] : A'=free_21, B'=free_22, C'=free_20, D'=2, E'=free_19, F'=free_21, G'=free_22, H'=free_20, Q'=2, J'=free_19, K'=1, [ free_7>=1 && 7>=free_7 && 1>=free_9 && free_9>=0 && 7>=free && free>=1 && L>=1 && L>=1+free_6 && M>=1 && M>=1+free_5 && 7>=free_3 && 7>=free_4 && free_3>=1 && free_4>=1 && free_33>=1 && 7>=free_33 && 1>=free_35 && free_35>=0 && free_19>=1 && 7>=free_19 && 1>=free_21 && free_21>=0 ], cost: INF
     25: f1 -> [6] : A'=free_29, B'=free_30, C'=free_28, D'=2, E'=free_27, F'=free_29, G'=free_30, H'=free_28, Q'=2, J'=free_27, K'=1, [ free_7>=1 && 7>=free_7 && 1>=free_9 && free_9>=0 && 7>=free && free>=1 && L>=1 && L>=1+free_6 && M>=1 && M>=1+free_5 && 7>=free_3 && 7>=free_4 && free_3>=1 && free_4>=1 && free_33>=1 && 7>=free_33 && 1>=free_35 && free_35>=0 && free_27>=1 && 7>=free_27 && 1>=free_29 && free_29>=0 ], cost: INF
     26: f1 -> [6] : A'=free_21, B'=free_22, C'=free_20, D'=2, E'=free_19, F'=free_21, G'=free_22, H'=free_20, Q'=2, J'=free_19, K'=1, [ free_7>=1 && 7>=free_7 && 1>=free_9 && free_9>=0 && 7>=free && free>=1 && L>=1 && L>=1+free_6 && M>=1 && M>=1+free_5 && 7>=free_3 && 7>=free_4 && free_3>=1 && free_4>=1 && free_41>=1 && 7>=free_41 && 1>=free_43 && free_43>=0 && free_19>=1 && 7>=free_19 && 1>=free_21 && free_21>=0 ], cost: INF
     27: f1 -> [6] : A'=free_29, B'=free_30, C'=free_28, D'=2, E'=free_27, F'=free_29, G'=free_30, H'=free_28, Q'=2, J'=free_27, K'=1, [ free_7>=1 && 7>=free_7 && 1>=free_9 && free_9>=0 && 7>=free && free>=1 && L>=1 && L>=1+free_6 && M>=1 && M>=1+free_5 && 7>=free_3 && 7>=free_4 && free_3>=1 && free_4>=1 && free_41>=1 && 7>=free_41 && 1>=free_43 && free_43>=0 && free_27>=1 && 7>=free_27 && 1>=free_29 && free_29>=0 ], cost: INF


Applied chaining over branches and pruning:
  Start location: f0
     28: f0 -> [6] : A'=free_15, B'=free_16, C'=free_14, D'=2, E'=free_13, F'=free_15, G'=free_16, H'=free_14, Q'=2, J'=free_13, K'=1, [ free_7>=1 && 7>=free_7 && 1>=free_9 && free_9>=0 && 7>=free && free>=1 && L>=1 && L>=1+free_6 && M>=1 && M>=1+free_5 && 7>=free_3 && 7>=free_4 && free_3>=1 && free_4>=1 && free_13>=1 && 7>=free_13 && 1>=free_15 && free_15>=0 ], cost: INF
     29: f0 -> [6] : A'=free_21, B'=free_22, C'=free_20, D'=2, E'=free_19, F'=free_21, G'=free_22, H'=free_20, Q'=2, J'=free_19, K'=1, [ free_7>=1 && 7>=free_7 && 1>=free_9 && free_9>=0 && 7>=free && free>=1 && L>=1 && L>=1+free_6 && M>=1 && M>=1+free_5 && 7>=free_3 && 7>=free_4 && free_3>=1 && free_4>=1 && free_33>=1 && 7>=free_33 && 1>=free_35 && free_35>=0 && free_19>=1 && 7>=free_19 && 1>=free_21 && free_21>=0 ], cost: INF
     30: f0 -> [6] : A'=free_29, B'=free_30, C'=free_28, D'=2, E'=free_27, F'=free_29, G'=free_30, H'=free_28, Q'=2, J'=free_27, K'=1, [ free_7>=1 && 7>=free_7 && 1>=free_9 && free_9>=0 && 7>=free && free>=1 && L>=1 && L>=1+free_6 && M>=1 && M>=1+free_5 && 7>=free_3 && 7>=free_4 && free_3>=1 && free_4>=1 && free_33>=1 && 7>=free_33 && 1>=free_35 && free_35>=0 && free_27>=1 && 7>=free_27 && 1>=free_29 && free_29>=0 ], cost: INF
     31: f0 -> [6] : A'=free_21, B'=free_22, C'=free_20, D'=2, E'=free_19, F'=free_21, G'=free_22, H'=free_20, Q'=2, J'=free_19, K'=1, [ free_7>=1 && 7>=free_7 && 1>=free_9 && free_9>=0 && 7>=free && free>=1 && L>=1 && L>=1+free_6 && M>=1 && M>=1+free_5 && 7>=free_3 && 7>=free_4 && free_3>=1 && free_4>=1 && free_41>=1 && 7>=free_41 && 1>=free_43 && free_43>=0 && free_19>=1 && 7>=free_19 && 1>=free_21 && free_21>=0 ], cost: INF
     32: f0 -> [6] : A'=free_29, B'=free_30, C'=free_28, D'=2, E'=free_27, F'=free_29, G'=free_30, H'=free_28, Q'=2, J'=free_27, K'=1, [ free_7>=1 && 7>=free_7 && 1>=free_9 && free_9>=0 && 7>=free && free>=1 && L>=1 && L>=1+free_6 && M>=1 && M>=1+free_5 && 7>=free_3 && 7>=free_4 && free_3>=1 && free_4>=1 && free_41>=1 && 7>=free_41 && 1>=free_43 && free_43>=0 && free_27>=1 && 7>=free_27 && 1>=free_29 && free_29>=0 ], cost: INF


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
     28: f0 -> [6] : A'=free_15, B'=free_16, C'=free_14, D'=2, E'=free_13, F'=free_15, G'=free_16, H'=free_14, Q'=2, J'=free_13, K'=1, [ free_7>=1 && 7>=free_7 && 1>=free_9 && free_9>=0 && 7>=free && free>=1 && L>=1 && L>=1+free_6 && M>=1 && M>=1+free_5 && 7>=free_3 && 7>=free_4 && free_3>=1 && free_4>=1 && free_13>=1 && 7>=free_13 && 1>=free_15 && free_15>=0 ], cost: INF
     29: f0 -> [6] : A'=free_21, B'=free_22, C'=free_20, D'=2, E'=free_19, F'=free_21, G'=free_22, H'=free_20, Q'=2, J'=free_19, K'=1, [ free_7>=1 && 7>=free_7 && 1>=free_9 && free_9>=0 && 7>=free && free>=1 && L>=1 && L>=1+free_6 && M>=1 && M>=1+free_5 && 7>=free_3 && 7>=free_4 && free_3>=1 && free_4>=1 && free_33>=1 && 7>=free_33 && 1>=free_35 && free_35>=0 && free_19>=1 && 7>=free_19 && 1>=free_21 && free_21>=0 ], cost: INF
     30: f0 -> [6] : A'=free_29, B'=free_30, C'=free_28, D'=2, E'=free_27, F'=free_29, G'=free_30, H'=free_28, Q'=2, J'=free_27, K'=1, [ free_7>=1 && 7>=free_7 && 1>=free_9 && free_9>=0 && 7>=free && free>=1 && L>=1 && L>=1+free_6 && M>=1 && M>=1+free_5 && 7>=free_3 && 7>=free_4 && free_3>=1 && free_4>=1 && free_33>=1 && 7>=free_33 && 1>=free_35 && free_35>=0 && free_27>=1 && 7>=free_27 && 1>=free_29 && free_29>=0 ], cost: INF
     31: f0 -> [6] : A'=free_21, B'=free_22, C'=free_20, D'=2, E'=free_19, F'=free_21, G'=free_22, H'=free_20, Q'=2, J'=free_19, K'=1, [ free_7>=1 && 7>=free_7 && 1>=free_9 && free_9>=0 && 7>=free && free>=1 && L>=1 && L>=1+free_6 && M>=1 && M>=1+free_5 && 7>=free_3 && 7>=free_4 && free_3>=1 && free_4>=1 && free_41>=1 && 7>=free_41 && 1>=free_43 && free_43>=0 && free_19>=1 && 7>=free_19 && 1>=free_21 && free_21>=0 ], cost: INF
     32: f0 -> [6] : A'=free_29, B'=free_30, C'=free_28, D'=2, E'=free_27, F'=free_29, G'=free_30, H'=free_28, Q'=2, J'=free_27, K'=1, [ free_7>=1 && 7>=free_7 && 1>=free_9 && free_9>=0 && 7>=free && free>=1 && L>=1 && L>=1+free_6 && M>=1 && M>=1+free_5 && 7>=free_3 && 7>=free_4 && free_3>=1 && free_4>=1 && free_41>=1 && 7>=free_41 && 1>=free_43 && free_43>=0 && free_27>=1 && 7>=free_27 && 1>=free_29 && free_29>=0 ], 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: free_7>=1 && 7>=free_7 && 1>=free_9 && free_9>=0 && 7>=free && free>=1 && L>=1 && L>=1+free_6 && M>=1 && M>=1+free_5 && 7>=free_3 && 7>=free_4 && free_3>=1 && free_4>=1 && free_13>=1 && 7>=free_13 && 1>=free_15 && free_15>=0
  Final Cost:  INF

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

WORST_CASE(INF,?)