Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f0 -> f12 : A'=3, B'=free, C'=3, D'=1, E'=0, [], cost: 1
      1: f12 -> f12 : D'=free_1, E'=1+E, [ C>=1+E ], cost: 1
      6: f12 -> f24 : F'=A, G'=0, H'=1, Q_1'=D, R'=D, S'=free_5, [ E>=C ], cost: 1
      2: f24 -> f24 : G'=1+G, H'=free_2, [ F>=1+G ], cost: 1
      5: f24 -> f36 : Q'=A, J'=0, K'=1, N'=H, O'=H, P'=free_4, [ G>=F ], cost: 1
      3: f36 -> f36 : J'=1+J, K'=free_3, [ Q>=1+J ], cost: 1
      4: f36 -> f46 : L'=K, M'=K, [ J>=Q ], cost: 1


Simplified the transitions:
  Start location: f0
      0: f0 -> f12 : A'=3, B'=free, C'=3, D'=1, E'=0, [], cost: 1
      1: f12 -> f12 : D'=free_1, E'=1+E, [ C>=1+E ], cost: 1
      6: f12 -> f24 : F'=A, G'=0, H'=1, Q_1'=D, R'=D, S'=free_5, [ E>=C ], cost: 1
      2: f24 -> f24 : G'=1+G, H'=free_2, [ F>=1+G ], cost: 1
      5: f24 -> f36 : Q'=A, J'=0, K'=1, N'=H, O'=H, P'=free_4, [ G>=F ], cost: 1
      3: f36 -> f36 : J'=1+J, K'=free_3, [ Q>=1+J ], cost: 1

Eliminating 1 self-loops for location f12
  Self-Loop 1 has the metering function: -E+C, resulting in the new transition 7.
  Removing the self-loops: 1.
Eliminating 1 self-loops for location f24
  Self-Loop 2 has the metering function: F-G, resulting in the new transition 8.
  Removing the self-loops: 2.
Eliminating 1 self-loops for location f36
  Self-Loop 3 has the metering function: Q-J, 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 -> f12 : A'=3, B'=free, C'=3, D'=1, E'=0, [], cost: 1
      7: f12 -> [5] : D'=free_1, E'=C, [ C>=1+E ], cost: -E+C
      8: f24 -> [6] : G'=F, H'=free_2, [ F>=1+G ], cost: F-G
      9: f36 -> [7] : J'=Q, K'=free_3, [ Q>=1+J ], cost: Q-J
      6: [5] -> f24 : F'=A, G'=0, H'=1, Q_1'=D, R'=D, S'=free_5, [ E>=C ], cost: 1
      5: [6] -> f36 : Q'=A, J'=0, K'=1, N'=H, O'=H, P'=free_4, [ G>=F ], cost: 1


Applied simple chaining:
  Start location: f0
      0: f0 -> [7] : A'=3, B'=free, C'=3, D'=free_1, E'=3, F'=3, G'=3, H'=free_2, Q'=3, J'=3, K'=free_3, N'=free_2, O'=free_2, P'=free_4, Q_1'=free_1, R'=free_1, S'=free_5, [ 3>=1 && 3>=3 && 3>=1 && 3>=3 && 3>=1 ], cost: 12


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
      0: f0 -> [7] : A'=3, B'=free, C'=3, D'=free_1, E'=3, F'=3, G'=3, H'=free_2, Q'=3, J'=3, K'=free_3, N'=free_2, O'=free_2, P'=free_4, Q_1'=free_1, R'=free_1, S'=free_5, [ 3>=1 && 3>=3 && 3>=1 && 3>=3 && 3>=1 ], cost: 12


Computing complexity for remaining 1 transitions.

Found new complexity const, because: const cost.


The final runtime is determined by this resulting transition:
  Final Guard: 3>=1 && 3>=3 && 3>=1 && 3>=3 && 3>=1
  Final Cost:  12

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

WORST_CASE(Omega(1),?)