Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f0 -> f1 : [], cost: 1
      1: f1 -> f7 : A'=-1+A, B'=1, C'=D, E'=F, G'=free, H'=free_1, Q'=0, J'=1, K'=free, L'=free_1, M'=7, [ A>=1 && 7>=free_1 && 7>=free && 3>=free_1 && free_1>=1 && free>=1 ], cost: 1
      2: f1 -> f7 : B'=1, C'=D, E'=F, G'=free_2, H'=free_3, Q'=0, J'=1, K'=free_2, L'=free_3, M'=7, [ 7>=free_3 && 7>=free_2 && free_3>=5 && free_2>=1 ], cost: 1
      3: f1 -> f7 : B'=1, C'=1+D, D'=1+D, E'=1+F, F'=1+F, G'=free_4, H'=4, Q'=1, J'=1, K'=free_4, L'=4, M'=7, [ 7>=free_4 && free_4>=1 ], cost: 1
      4: f1 -> f2 : B'=0, C'=D, E'=F, G'=3, H'=free_5, Q'=0, J'=0, K'=3, L'=free_5, M'=2, [ 7>=free_5 && 3>=free_5 && free_5>=1 ], cost: 1
      5: f1 -> f2 : B'=0, C'=D, E'=F, G'=3, H'=free_6, Q'=0, J'=0, K'=3, L'=free_6, M'=2, [ 7>=free_6 && free_6>=5 ], cost: 1
      6: f1 -> f2 : B'=0, C'=1+D, D'=1+D, E'=1+F, F'=1+F, G'=3, H'=4, Q'=1, J'=0, K'=3, L'=4, M'=2, [], cost: 1
      7: f2 -> f7 : B'=1, C'=D, E'=F, G'=free_7, H'=free_8, J'=1, K'=free_7, L'=free_8, M'=7, [ 7>=free_8 && 7>=free_7 && 3>=free_8 && free_8>=1 && free_7>=1 ], cost: 1
      8: f2 -> f7 : B'=1, C'=D, E'=F, G'=free_9, H'=free_10, J'=1, K'=free_9, L'=free_10, M'=7, [ 7>=free_10 && 7>=free_9 && free_10>=5 && free_9>=1 ], cost: 1
      9: f2 -> f7 : B'=1, C'=1+D, D'=1+D, E'=1+F, F'=1+F, G'=free_11, H'=4, Q'=1, J'=1, K'=free_11, L'=4, M'=7, [ 7>=free_11 && free_11>=1 ], cost: 1
     10: f2 -> f3 : B'=0, C'=D, E'=F, G'=free_12, H'=free_13, J'=0, K'=free_12, L'=free_13, M'=3, [ 7>=free_13 && 7>=free_12 && 3>=free_13 && free_13>=1 && free_12>=1 ], cost: 1
     11: f2 -> f3 : B'=0, C'=D, E'=F, G'=free_14, H'=free_15, J'=0, K'=free_14, L'=free_15, M'=3, [ 7>=free_15 && 7>=free_14 && free_15>=5 && free_14>=1 ], cost: 1
     12: f2 -> f3 : B'=0, C'=1+D, D'=1+D, E'=1+F, F'=1+F, G'=free_16, H'=4, Q'=1, J'=0, K'=free_16, L'=4, M'=3, [ 7>=free_16 && free_16>=1 ], cost: 1
     13: f3 -> f6 : B'=1, C'=D, E'=F, G'=free_17, H'=free_18, J'=1, K'=free_17, L'=free_18, M'=6, [ 7>=free_18 && 7>=free_17 && 3>=free_18 && free_18>=1 && free_17>=1 ], cost: 1
     14: f3 -> f6 : B'=1, C'=D, E'=F, G'=free_19, H'=free_20, J'=1, K'=free_19, L'=free_20, M'=6, [ 7>=free_20 && 7>=free_19 && free_20>=5 && free_19>=1 ], cost: 1
     15: f3 -> f6 : B'=1, C'=1+D, D'=1+D, E'=1+F, F'=1+F, G'=free_21, H'=4, Q'=1, J'=1, K'=free_21, L'=4, M'=6, [ 7>=free_21 && free_21>=1 ], cost: 1
     16: f6 -> f4 : B'=1, C'=D, E'=F, G'=free_22, H'=2, Q'=0, J'=1, K'=free_22, L'=2, M'=4, [ free_22>=1 && 7>=free_22 ], cost: 1
     17: f6 -> f4 : B'=free_23, C'=D, E'=F, G'=free_24, H'=7, Q'=1, J'=free_23, K'=free_24, L'=7, M'=4, [ 7>=free_24 && 1>=free_23 && free_23>=0 && free_24>=1 && Q==1 ], cost: 1
     21: f4 -> f7 : B'=0, C'=D, E'=F, G'=free_30, H'=free_31, J'=0, K'=free_30, L'=free_31, M'=7, [ F>=N && D>=O && 7>=free_31 && 7>=free_30 && 3>=free_31 && free_31>=1 && free_30>=1 ], cost: 1
     22: f4 -> f7 : B'=0, C'=D, E'=F, G'=free_32, H'=free_33, J'=0, K'=free_32, L'=free_33, M'=7, [ F>=N && D>=O && 7>=free_33 && 7>=free_32 && free_33>=5 && free_32>=1 ], cost: 1
     23: f4 -> f7 : B'=0, C'=1+D, D'=1+D, E'=1+F, F'=1+F, G'=free_34, H'=4, Q'=1, J'=0, K'=free_34, L'=4, M'=7, [ 1+F>=N && 1+D>=O && 7>=free_34 && free_34>=1 ], cost: 1
     24: f4 -> f7 : B'=1, C'=D, E'=F, G'=free_35, H'=free_36, J'=1, K'=free_35, L'=free_36, M'=7, [ 7>=free_36 && 7>=free_35 && 3>=free_36 && free_36>=1 && free_35>=1 ], cost: 1
     25: f4 -> f7 : B'=1, C'=D, E'=F, G'=free_37, H'=free_38, J'=1, K'=free_37, L'=free_38, M'=7, [ 7>=free_38 && 7>=free_37 && free_38>=5 && free_37>=1 ], cost: 1
     26: f4 -> f7 : B'=1, C'=1+D, D'=1+D, E'=1+F, F'=1+F, G'=free_39, H'=4, Q'=1, J'=1, K'=free_39, L'=4, M'=7, [ 7>=free_39 && free_39>=1 ], cost: 1
     18: f4 -> f2 : B'=0, C'=D, E'=F, G'=free_25, H'=free_26, Q'=1, J'=0, K'=free_25, L'=free_26, M'=2, [ N>=1 && N>=1+F && O>=1 && O>=1+D && 7>=free_26 && 7>=free_25 && 3>=free_26 && free_26>=1 && free_25>=1 && Q==1 ], cost: 1
     19: f4 -> f2 : B'=0, C'=D, E'=F, G'=free_27, H'=free_28, Q'=1, J'=0, K'=free_27, L'=free_28, M'=2, [ N>=1 && N>=1+F && O>=1 && O>=1+D && 7>=free_28 && 7>=free_27 && free_28>=5 && free_27>=1 && Q==1 ], cost: 1
     20: f4 -> f2 : B'=0, C'=1+D, D'=1+D, E'=1+F, F'=1+F, G'=free_29, H'=4, Q'=1, J'=0, K'=free_29, L'=4, M'=2, [ N>=2+F && O>=2+D && N>=1 && O>=1 && 7>=free_29 && free_29>=1 ], cost: 1


Simplified the transitions:
  Start location: f0
      0: f0 -> f1 : [], cost: 1
      4: f1 -> f2 : B'=0, C'=D, E'=F, G'=3, H'=free_5, Q'=0, J'=0, K'=3, L'=free_5, M'=2, [ 3>=free_5 && free_5>=1 ], cost: 1
      5: f1 -> f2 : B'=0, C'=D, E'=F, G'=3, H'=free_6, Q'=0, J'=0, K'=3, L'=free_6, M'=2, [ 7>=free_6 && free_6>=5 ], cost: 1
      6: f1 -> f2 : B'=0, C'=1+D, D'=1+D, E'=1+F, F'=1+F, G'=3, H'=4, Q'=1, J'=0, K'=3, L'=4, M'=2, [], cost: 1
     10: f2 -> f3 : B'=0, C'=D, E'=F, G'=free_12, H'=free_13, J'=0, K'=free_12, L'=free_13, M'=3, [ 7>=free_12 && 3>=free_13 && free_13>=1 && free_12>=1 ], cost: 1
     11: f2 -> f3 : B'=0, C'=D, E'=F, G'=free_14, H'=free_15, J'=0, K'=free_14, L'=free_15, M'=3, [ 7>=free_15 && 7>=free_14 && free_15>=5 && free_14>=1 ], cost: 1
     12: f2 -> f3 : B'=0, C'=1+D, D'=1+D, E'=1+F, F'=1+F, G'=free_16, H'=4, Q'=1, J'=0, K'=free_16, L'=4, M'=3, [ 7>=free_16 && free_16>=1 ], cost: 1
     13: f3 -> f6 : B'=1, C'=D, E'=F, G'=free_17, H'=free_18, J'=1, K'=free_17, L'=free_18, M'=6, [ 7>=free_17 && 3>=free_18 && free_18>=1 && free_17>=1 ], cost: 1
     14: f3 -> f6 : B'=1, C'=D, E'=F, G'=free_19, H'=free_20, J'=1, K'=free_19, L'=free_20, M'=6, [ 7>=free_20 && 7>=free_19 && free_20>=5 && free_19>=1 ], cost: 1
     15: f3 -> f6 : B'=1, C'=1+D, D'=1+D, E'=1+F, F'=1+F, G'=free_21, H'=4, Q'=1, J'=1, K'=free_21, L'=4, M'=6, [ 7>=free_21 && free_21>=1 ], cost: 1
     16: f6 -> f4 : B'=1, C'=D, E'=F, G'=free_22, H'=2, Q'=0, J'=1, K'=free_22, L'=2, M'=4, [ free_22>=1 && 7>=free_22 ], cost: 1
     17: f6 -> f4 : B'=free_23, C'=D, E'=F, G'=free_24, H'=7, Q'=1, J'=free_23, K'=free_24, L'=7, M'=4, [ 7>=free_24 && 1>=free_23 && free_23>=0 && free_24>=1 && Q==1 ], cost: 1
     18: f4 -> f2 : B'=0, C'=D, E'=F, G'=free_25, H'=free_26, Q'=1, J'=0, K'=free_25, L'=free_26, M'=2, [ N>=1 && N>=1+F && O>=1 && O>=1+D && 7>=free_25 && 3>=free_26 && free_26>=1 && free_25>=1 && Q==1 ], cost: 1
     19: f4 -> f2 : B'=0, C'=D, E'=F, G'=free_27, H'=free_28, Q'=1, J'=0, K'=free_27, L'=free_28, M'=2, [ N>=1 && N>=1+F && O>=1 && O>=1+D && 7>=free_28 && 7>=free_27 && free_28>=5 && free_27>=1 && Q==1 ], cost: 1
     20: f4 -> f2 : B'=0, C'=1+D, D'=1+D, E'=1+F, F'=1+F, G'=free_29, H'=4, Q'=1, J'=0, K'=free_29, L'=4, M'=2, [ N>=2+F && O>=2+D && N>=1 && O>=1 && 7>=free_29 && free_29>=1 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
     27: f0 -> f2 : B'=0, C'=D, E'=F, G'=3, H'=free_5, Q'=0, J'=0, K'=3, L'=free_5, M'=2, [ 3>=free_5 && free_5>=1 ], cost: 2
     28: f0 -> f2 : B'=0, C'=D, E'=F, G'=3, H'=free_6, Q'=0, J'=0, K'=3, L'=free_6, M'=2, [ 7>=free_6 && free_6>=5 ], cost: 2
     29: f0 -> f2 : B'=0, C'=1+D, D'=1+D, E'=1+F, F'=1+F, G'=3, H'=4, Q'=1, J'=0, K'=3, L'=4, M'=2, [], cost: 2
     30: f2 -> f6 : B'=1, C'=D, E'=F, G'=free_17, H'=free_18, J'=1, K'=free_17, L'=free_18, M'=6, [ 7>=free_12 && 3>=free_13 && free_13>=1 && free_12>=1 && 7>=free_17 && 3>=free_18 && free_18>=1 && free_17>=1 ], cost: 2
     31: f2 -> f6 : B'=1, C'=D, E'=F, G'=free_19, H'=free_20, J'=1, K'=free_19, L'=free_20, M'=6, [ 7>=free_12 && 3>=free_13 && free_13>=1 && free_12>=1 && 7>=free_20 && 7>=free_19 && free_20>=5 && free_19>=1 ], cost: 2
     33: f2 -> f6 : B'=1, C'=D, E'=F, G'=free_17, H'=free_18, J'=1, K'=free_17, L'=free_18, M'=6, [ 7>=free_15 && 7>=free_14 && free_15>=5 && free_14>=1 && 7>=free_17 && 3>=free_18 && free_18>=1 && free_17>=1 ], cost: 2
     34: f2 -> f6 : B'=1, C'=D, E'=F, G'=free_19, H'=free_20, J'=1, K'=free_19, L'=free_20, M'=6, [ 7>=free_15 && 7>=free_14 && free_15>=5 && free_14>=1 && 7>=free_20 && 7>=free_19 && free_20>=5 && free_19>=1 ], cost: 2
     36: f2 -> f6 : B'=1, C'=1+D, D'=1+D, E'=1+F, F'=1+F, G'=free_17, H'=free_18, Q'=1, J'=1, K'=free_17, L'=free_18, M'=6, [ 7>=free_16 && free_16>=1 && 7>=free_17 && 3>=free_18 && free_18>=1 && free_17>=1 ], cost: 2
     39: f6 -> f2 : B'=0, C'=1+D, D'=1+D, E'=1+F, F'=1+F, G'=free_29, H'=4, Q'=1, J'=0, K'=free_29, L'=4, M'=2, [ free_22>=1 && 7>=free_22 && N>=2+F && O>=2+D && N>=1 && O>=1 && 7>=free_29 && free_29>=1 ], cost: 2
     40: f6 -> f2 : B'=0, C'=D, E'=F, G'=free_25, H'=free_26, Q'=1, J'=0, K'=free_25, L'=free_26, M'=2, [ 7>=free_24 && 1>=free_23 && free_23>=0 && free_24>=1 && Q==1 && N>=1 && N>=1+F && O>=1 && O>=1+D && 7>=free_25 && 3>=free_26 && free_26>=1 && free_25>=1 && 1==1 ], cost: 2
     41: f6 -> f2 : B'=0, C'=D, E'=F, G'=free_27, H'=free_28, Q'=1, J'=0, K'=free_27, L'=free_28, M'=2, [ 7>=free_24 && 1>=free_23 && free_23>=0 && free_24>=1 && Q==1 && N>=1 && N>=1+F && O>=1 && O>=1+D && 7>=free_28 && 7>=free_27 && free_28>=5 && free_27>=1 && 1==1 ], cost: 2
     42: f6 -> f2 : B'=0, C'=1+D, D'=1+D, E'=1+F, F'=1+F, G'=free_29, H'=4, Q'=1, J'=0, K'=free_29, L'=4, M'=2, [ 7>=free_24 && 1>=free_23 && free_23>=0 && free_24>=1 && Q==1 && N>=2+F && O>=2+D && N>=1 && O>=1 && 7>=free_29 && free_29>=1 ], cost: 2


Applied chaining over branches and pruning:
  Start location: f0
     27: f0 -> f2 : B'=0, C'=D, E'=F, G'=3, H'=free_5, Q'=0, J'=0, K'=3, L'=free_5, M'=2, [ 3>=free_5 && free_5>=1 ], cost: 2
     28: f0 -> f2 : B'=0, C'=D, E'=F, G'=3, H'=free_6, Q'=0, J'=0, K'=3, L'=free_6, M'=2, [ 7>=free_6 && free_6>=5 ], cost: 2
     29: f0 -> f2 : B'=0, C'=1+D, D'=1+D, E'=1+F, F'=1+F, G'=3, H'=4, Q'=1, J'=0, K'=3, L'=4, M'=2, [], cost: 2
     43: f2 -> f2 : B'=0, C'=1+D, D'=1+D, E'=1+F, F'=1+F, G'=free_29, H'=4, Q'=1, J'=0, K'=free_29, L'=4, M'=2, [ 7>=free_12 && 3>=free_13 && free_13>=1 && free_12>=1 && 7>=free_17 && 3>=free_18 && free_18>=1 && free_17>=1 && free_22>=1 && 7>=free_22 && N>=2+F && O>=2+D && N>=1 && O>=1 && 7>=free_29 && free_29>=1 ], cost: 4
     44: f2 -> f2 : B'=0, C'=D, E'=F, G'=free_25, H'=free_26, Q'=1, J'=0, K'=free_25, L'=free_26, M'=2, [ 7>=free_12 && 3>=free_13 && free_13>=1 && free_12>=1 && 7>=free_17 && 3>=free_18 && free_18>=1 && free_17>=1 && 7>=free_24 && 1>=free_23 && free_23>=0 && free_24>=1 && Q==1 && N>=1 && N>=1+F && O>=1 && O>=1+D && 7>=free_25 && 3>=free_26 && free_26>=1 && free_25>=1 && 1==1 ], cost: 4
     46: f2 -> f2 : B'=0, C'=1+D, D'=1+D, E'=1+F, F'=1+F, G'=free_29, H'=4, Q'=1, J'=0, K'=free_29, L'=4, M'=2, [ 7>=free_12 && 3>=free_13 && free_13>=1 && free_12>=1 && 7>=free_17 && 3>=free_18 && free_18>=1 && free_17>=1 && 7>=free_24 && 1>=free_23 && free_23>=0 && free_24>=1 && Q==1 && N>=2+F && O>=2+D && N>=1 && O>=1 && 7>=free_29 && free_29>=1 ], cost: 4
     50: f2 -> f2 : B'=0, C'=1+D, D'=1+D, E'=1+F, F'=1+F, G'=free_29, H'=4, Q'=1, J'=0, K'=free_29, L'=4, M'=2, [ 7>=free_12 && 3>=free_13 && free_13>=1 && free_12>=1 && 7>=free_20 && 7>=free_19 && free_20>=5 && free_19>=1 && 7>=free_24 && 1>=free_23 && free_23>=0 && free_24>=1 && Q==1 && N>=2+F && O>=2+D && N>=1 && O>=1 && 7>=free_29 && free_29>=1 ], cost: 4
     53: f2 -> f2 : B'=0, C'=D, E'=F, G'=free_27, H'=free_28, Q'=1, J'=0, K'=free_27, L'=free_28, M'=2, [ 7>=free_15 && 7>=free_14 && free_15>=5 && free_14>=1 && 7>=free_17 && 3>=free_18 && free_18>=1 && free_17>=1 && 7>=free_24 && 1>=free_23 && free_23>=0 && free_24>=1 && Q==1 && N>=1 && N>=1+F && O>=1 && O>=1+D && 7>=free_28 && 7>=free_27 && free_28>=5 && free_27>=1 && 1==1 ], cost: 4

Eliminating 5 self-loops for location f2
  Self-Loop 44 has unbounded runtime, resulting in the new transition 64.
  Self-Loop 53 has unbounded runtime, resulting in the new transition 67.
  Removing the self-loops: 43 44 46 50 53.
Adding an epsilon transition (to model nonexecution of the loops): 68.
Removing duplicate transition: 65.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
     27: f0 -> f2 : B'=0, C'=D, E'=F, G'=3, H'=free_5, Q'=0, J'=0, K'=3, L'=free_5, M'=2, [ 3>=free_5 && free_5>=1 ], cost: 2
     28: f0 -> f2 : B'=0, C'=D, E'=F, G'=3, H'=free_6, Q'=0, J'=0, K'=3, L'=free_6, M'=2, [ 7>=free_6 && free_6>=5 ], cost: 2
     29: f0 -> f2 : B'=0, C'=1+D, D'=1+D, E'=1+F, F'=1+F, G'=3, H'=4, Q'=1, J'=0, K'=3, L'=4, M'=2, [], cost: 2
     63: f2 -> [7] : B'=0, C'=1+D, D'=1+D, E'=1+F, F'=1+F, G'=free_29, H'=4, Q'=1, J'=0, K'=free_29, L'=4, M'=2, [ N>=2+F && O>=2+D && N>=1 && O>=1 && 7>=free_29 && free_29>=1 ], cost: 4
     64: f2 -> [7] : [ Q==1 && N>=1 && N>=1+F && O>=1 && O>=1+D && 7>=free_25 && 3>=free_26 && free_26>=1 && free_25>=1 ], cost: INF
     66: f2 -> [7] : B'=0, C'=1+D, D'=1+D, E'=1+F, F'=1+F, G'=free_29, H'=4, Q'=1, J'=0, K'=free_29, L'=4, M'=2, [ Q==1 && N>=2+F && O>=2+D && N>=1 && O>=1 && 7>=free_29 && free_29>=1 ], cost: 4
     67: f2 -> [7] : [ Q==1 && N>=1 && N>=1+F && O>=1 && O>=1+D && 7>=free_28 && 7>=free_27 && free_28>=5 && free_27>=1 ], cost: INF
     68: f2 -> [7] : [], cost: 0


Applied chaining over branches and pruning:
  Start location: f0
     74: f0 -> [7] : B'=0, C'=1+D, D'=1+D, E'=1+F, F'=1+F, G'=3, H'=4, Q'=1, J'=0, K'=3, L'=4, M'=2, [ 1==1 && N>=1 && N>=2+F && O>=1 && O>=2+D && 7>=free_25 && 3>=free_26 && free_26>=1 && free_25>=1 ], cost: INF
     76: f0 -> [7] : B'=0, C'=1+D, D'=1+D, E'=1+F, F'=1+F, G'=3, H'=4, Q'=1, J'=0, K'=3, L'=4, M'=2, [ 1==1 && N>=1 && N>=2+F && O>=1 && O>=2+D && 7>=free_28 && 7>=free_27 && free_28>=5 && free_27>=1 ], cost: INF


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
     74: f0 -> [7] : B'=0, C'=1+D, D'=1+D, E'=1+F, F'=1+F, G'=3, H'=4, Q'=1, J'=0, K'=3, L'=4, M'=2, [ 1==1 && N>=1 && N>=2+F && O>=1 && O>=2+D && 7>=free_25 && 3>=free_26 && free_26>=1 && free_25>=1 ], cost: INF
     76: f0 -> [7] : B'=0, C'=1+D, D'=1+D, E'=1+F, F'=1+F, G'=3, H'=4, Q'=1, J'=0, K'=3, L'=4, M'=2, [ 1==1 && N>=1 && N>=2+F && O>=1 && O>=2+D && 7>=free_28 && 7>=free_27 && free_28>=5 && free_27>=1 ], cost: INF


Computing complexity for remaining 2 transitions.

Found new complexity INF, because: INF sat.


The final runtime is determined by this resulting transition:
  Final Guard: 1==1 && N>=1 && N>=2+F && O>=1 && O>=2+D && 7>=free_25 && 3>=free_26 && free_26>=1 && free_25>=1
  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,?)