Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f14
      0: f38 -> f17 : D'=B, E'=C, F'=free_1-G, H'=free_1, Q'=free_1-G, J'=free_1, K'=free_2, L'=free, [ free>=1+A && B>=1+C ], cost: 1
     17: f17 -> f34 : D'=P3, E'=Q3_1, G'=S3, P'=free_90, V'=free_92, W'=-1+W, D1'=free_89, E1'=free_91, P1'=free_93, M4'=free_88, [ W>=1 && S3>=1 && G4>=1+H4 && Q4>=1+J4 && free_94>=1+K4 && free_92>=1+R3 && P3>=1+Q3_1 && free_91>=1+L4 ], cost: 1
      4: f17 -> f0 : D'=free_18, E'=free_20, G'=W, W'=free_21, D1'=free_16, E1'=free_23, H1'=free_19, O1'=free_22, P1'=free_17, [ W>=1 && 0>=W && 0>=free_21 && Q1>=1+J1 && free_24>=1+K1 && L1>=1+M1 && free_23>=1+N1 ], cost: 1
      1: f19 -> f34 : D'=N, E'=O, P'=Q_1, Q_1'=free_4, R'=free_3, [ free_3>=1+M && N>=1+O ], cost: 1
      8: f34 -> f17 : D'=Z1, E'=A2, G'=B2, Q'=free_34, J'=free_35, K'=free_33, L'=free_36, [ B2>=1 && W1>=1 && free_36>=1+Y1 && Z1>=1+A2 ], cost: 1
      6: f34 -> f34 : D'=R1, E'=S1, G'=V1, P'=Q_1, Q_1'=free_28, R'=free_27, [ V1>=1 && R1>=1+S1 && 0>=W1 && free_27>=1+U1 ], cost: 1
      2: f50 -> f34 : D'=T, E'=U, P'=free_5, V'=free_6, [ free_6>=1+S && T>=1+U ], cost: 1
     16: f16 -> f34 : D'=P3, E'=Q3_1, F'=G1, G'=S3, H'=free_86-W, Q'=free_86-W, J'=free_86, P'=free_83, V'=free_85, W'=-1+W, D1'=free_82, E1'=free_84, P1'=G1, M4'=free_81, N4'=free_86, [ W>=1 && S3>=1 && G4>=1+H4 && Q4>=1+J4 && free_87>=1+K4 && free_85>=1+R3 && P3>=1+Q3_1 && free_84>=1+L4 ], cost: 1
      3: f16 -> f0 : D'=free_9, E'=free_11, G'=W, W'=free_12, D1'=free_7, E1'=free_14, F1'=free_13, G1'=free_8, H1'=free_10, [ 0>=W && 0>=free_12 && X>=1+Y && Z>=1+A1 && free_14>=1+B1 && free_15>=1+C1 ], cost: 1
      7: f33 -> f17 : D'=Z1, E'=A2, G'=X1, Q'=free_30, J'=free_31, K'=free_29, L'=free_32, [ X1>=1 && T1>=1 && free_32>=1+Y1 && Z1>=1+A2 ], cost: 1
      5: f33 -> f34 : D'=R1, E'=S1, G'=Q1_1, P'=Q_1, Q_1'=free_26, R'=free_25, [ Q1_1>=1 && R1>=1+S1 && 0>=T1 && free_25>=1+U1 ], cost: 1
     18: f35 -> f34 : D'=P3, E'=Q3_1, F'=O4, G'=S3, H'=-W+free_103, Q'=-W+free_103, J'=free_103, K'=free_100, L'=free_96, P'=free_99, V'=free_97, W'=-1+W, D1'=free_98, E1'=free_101, P1'=O4, T2'=free_102, U2'=free_103, M4'=free_95, N4'=free_103, [ W>=1 && S3>=1 && H2>=1 && F2>=1 && G4>=1+H4 && Q2>=1+J2 && Q4>=1+J4 && free_104>=1+K4 && free_97>=1+R3 && free_96>=1+Q2_1 && P3>=1+Q3_1 && free_101>=1+L4 ], cost: 1
     10: f35 -> f0 : D'=free_43, E'=free_45, G'=W, K'=free_44, L'=free_50, W'=free_47, D1'=free_39, E1'=free_49, H1'=free_46, R2'=free_48, S2'=free_40, T2'=free_41, U2'=free_42, [ 0>=W && 0>=free_47 && H2>=1 && F2>=1 && Q2>=1+J2 && K2>=1+L2 && M2>=1+N2 && free_51>=1+O2 && free_49>=1+P2 && free_50>=1+Q2_1 ], cost: 1
      9: f35 -> f35 : D'=D2, E'=E2, G'=C2, P'=Q_1, Q_1'=free_38, R'=free_37, [ C2>=1 && D2>=1+E2 && 0>=F2 && free_37>=1+G2 ], cost: 1
     19: f36 -> f34 : D'=P3, E'=Q3_1, G'=S3, K'=free_111, L'=free_113, P'=free_110, V'=free_108, W'=-1+W, D1'=free_109, E1'=free_112, K3'=free_114, L3'=free_106, M3'=free_107, N3'=free_115, V4'=free_105, [ W>=1 && 0>=free_115 && S3>=1 && X2>=1 && A3>=1+B3 && P4>=1+Q4_1 && free_116>=1+R4 && free_108>=1+R3 && free_113>=1+Q3 && free_112>=1+S4 && T4>=1+U4 && P3>=1+Q3_1 ], cost: 1
     12: f36 -> f0 : D'=free_59, E'=free_61, G'=W, K'=free_60, L'=free_57, W'=free_63, D1'=free_55, E1'=free_66, H1'=free_64, J3'=free_65, K3'=free_56, L3'=free_67, M3'=free_58, N3'=free_62, [ 0>=W && 0>=free_62 && 0>=free_63 && X2>=1 && A3>=1+B3 && C3>=1+D3 && E3>=1+F3 && free_68>=1+G3 && free_66>=1+H3 && free_57>=1+Q3 ], cost: 1
     11: f36 -> f36 : D'=V2, E'=W2, G'=free_53, P'=Q_1, Q_1'=free_52, R'=free_54, Z2'=free_53, [ 0>=free_53 && V2>=1+W2 && 0>=X2 && free_54>=1+Y2 ], cost: 1
     13: f10 -> f34 : D'=P3, E'=Q3_1, G'=O3, P'=free_69, V'=free_70, W'=-1+W, [ W>=1 && O3>=1 && P3>=1+Q3_1 && free_70>=1+R3 ], cost: 1
     14: f1 -> f34 : D'=P3, E'=Q3_1, G'=S3, P'=free_71, V'=free_72, W'=-1+W, [ W>=1 && S3>=1 && T3>=1+U3 && V3>=1+W3 && free_73>=1+X3 && free_74>=1+Y3 && P3>=1+Q3_1 && free_72>=1+R3 ], cost: 1
     15: f2 -> f34 : D'=P3, E'=Q3_1, G'=S3, P'=free_79, V'=free_77, W'=-1+W, D1'=free_76, E1'=free_75, F4'=free_78, [ W>=1 && S3>=1 && Z3>=1+A4 && B4>=1+C4 && free_80>=1+D4 && free_77>=1+R3 && P3>=1+Q3_1 && free_75>=1+E4 ], cost: 1
     21: f14 -> f35 : D'=P5, E'=Q5_1, G'=M5, P'=free_136, V'=free_129, W'=-1+free_133, O4'=free_133, D5'=free_138, E5'=free_135, F5'=free_137, G5'=free_130, H5'=free_134, Q5'=free_131, J5'=free_139, K5'=free_132, L5'=free_133, [ free_137>=1 && free_133>=1 && M5>=1 && free_135>=1+N5 && free_129>=1+O5 && P5>=1+Q5_1 && R5>=1+S5 ], cost: 1
     20: f14 -> f36 : D'=Y4, E'=Z4, G'=free_125, P'=free_117, V'=free_127, W'=-1+free_121, O4'=free_121, C5'=free_125, D5'=free_123, E5'=free_126, F5'=free_118, G5'=free_122, H5'=free_119, Q5'=free_128, J5'=free_120, K5'=free_124, L5'=free_121, [ 0>=free_118 && 0>=free_125 && free_121>=1 && free_126>=1+W4 && free_127>=1+X4 && Y4>=1+Z4 && A5>=1+B5 ], cost: 1


Simplified the transitions:
  Start location: f14
     17: f17 -> f34 : D'=P3, E'=Q3_1, G'=S3, P'=free_90, V'=free_92, W'=-1+W, D1'=free_89, E1'=free_91, P1'=free_93, M4'=free_88, [ W>=1 && S3>=1 && G4>=1+H4 && Q4>=1+J4 && free_92>=1+R3 && P3>=1+Q3_1 && free_91>=1+L4 ], cost: 1
      8: f34 -> f17 : D'=Z1, E'=A2, G'=B2, Q'=free_34, J'=free_35, K'=free_33, L'=free_36, [ B2>=1 && W1>=1 && free_36>=1+Y1 && Z1>=1+A2 ], cost: 1
      6: f34 -> f34 : D'=R1, E'=S1, G'=V1, P'=Q_1, Q_1'=free_28, R'=free_27, [ V1>=1 && R1>=1+S1 && 0>=W1 && free_27>=1+U1 ], cost: 1
     18: f35 -> f34 : D'=P3, E'=Q3_1, F'=O4, G'=S3, H'=-W+free_103, Q'=-W+free_103, J'=free_103, K'=free_100, L'=free_96, P'=free_99, V'=free_97, W'=-1+W, D1'=free_98, E1'=free_101, P1'=O4, T2'=free_102, U2'=free_103, M4'=free_95, N4'=free_103, [ W>=1 && S3>=1 && H2>=1 && F2>=1 && G4>=1+H4 && Q2>=1+J2 && Q4>=1+J4 && free_97>=1+R3 && free_96>=1+Q2_1 && P3>=1+Q3_1 && free_101>=1+L4 ], cost: 1
      9: f35 -> f35 : D'=D2, E'=E2, G'=C2, P'=Q_1, Q_1'=free_38, R'=free_37, [ C2>=1 && D2>=1+E2 && 0>=F2 && free_37>=1+G2 ], cost: 1
     19: f36 -> f34 : D'=P3, E'=Q3_1, G'=S3, K'=free_111, L'=free_113, P'=free_110, V'=free_108, W'=-1+W, D1'=free_109, E1'=free_112, K3'=free_114, L3'=free_106, M3'=free_107, N3'=free_115, V4'=free_105, [ W>=1 && 0>=free_115 && S3>=1 && X2>=1 && A3>=1+B3 && P4>=1+Q4_1 && free_108>=1+R3 && free_113>=1+Q3 && free_112>=1+S4 && T4>=1+U4 && P3>=1+Q3_1 ], cost: 1
     11: f36 -> f36 : D'=V2, E'=W2, G'=free_53, P'=Q_1, Q_1'=free_52, R'=free_54, Z2'=free_53, [ 0>=free_53 && V2>=1+W2 && 0>=X2 && free_54>=1+Y2 ], cost: 1
     21: f14 -> f35 : D'=P5, E'=Q5_1, G'=M5, P'=free_136, V'=free_129, W'=-1+free_133, O4'=free_133, D5'=free_138, E5'=free_135, F5'=free_137, G5'=free_130, H5'=free_134, Q5'=free_131, J5'=free_139, K5'=free_132, L5'=free_133, [ free_137>=1 && free_133>=1 && M5>=1 && free_135>=1+N5 && free_129>=1+O5 && P5>=1+Q5_1 && R5>=1+S5 ], cost: 1
     20: f14 -> f36 : D'=Y4, E'=Z4, G'=free_125, P'=free_117, V'=free_127, W'=-1+free_121, O4'=free_121, C5'=free_125, D5'=free_123, E5'=free_126, F5'=free_118, G5'=free_122, H5'=free_119, Q5'=free_128, J5'=free_120, K5'=free_124, L5'=free_121, [ 0>=free_118 && 0>=free_125 && free_121>=1 && free_126>=1+W4 && free_127>=1+X4 && Y4>=1+Z4 && A5>=1+B5 ], cost: 1

Eliminating 1 self-loops for location f34
  Self-Loop 6 has unbounded runtime, resulting in the new transition 22.
  Removing the self-loops: 6.
Eliminating 1 self-loops for location f35
  Self-Loop 9 has unbounded runtime, resulting in the new transition 23.
  Removing the self-loops: 9.
Eliminating 1 self-loops for location f36
  Self-Loop 11 has unbounded runtime, resulting in the new transition 24.
  Removing the self-loops: 11.

Removed all Self-loops using metering functions (where possible):
  Start location: f14
     17: f17 -> f34 : D'=P3, E'=Q3_1, G'=S3, P'=free_90, V'=free_92, W'=-1+W, D1'=free_89, E1'=free_91, P1'=free_93, M4'=free_88, [ W>=1 && S3>=1 && G4>=1+H4 && Q4>=1+J4 && free_92>=1+R3 && P3>=1+Q3_1 && free_91>=1+L4 ], cost: 1
     22: f34 -> [14] : [ V1>=1 && R1>=1+S1 && 0>=W1 && free_27>=1+U1 ], cost: INF
     23: f35 -> [15] : [ C2>=1 && D2>=1+E2 && 0>=F2 && free_37>=1+G2 ], cost: INF
     24: f36 -> [16] : [ 0>=free_53 && V2>=1+W2 && 0>=X2 && free_54>=1+Y2 ], cost: INF
     21: f14 -> f35 : D'=P5, E'=Q5_1, G'=M5, P'=free_136, V'=free_129, W'=-1+free_133, O4'=free_133, D5'=free_138, E5'=free_135, F5'=free_137, G5'=free_130, H5'=free_134, Q5'=free_131, J5'=free_139, K5'=free_132, L5'=free_133, [ free_137>=1 && free_133>=1 && M5>=1 && free_135>=1+N5 && free_129>=1+O5 && P5>=1+Q5_1 && R5>=1+S5 ], cost: 1
     20: f14 -> f36 : D'=Y4, E'=Z4, G'=free_125, P'=free_117, V'=free_127, W'=-1+free_121, O4'=free_121, C5'=free_125, D5'=free_123, E5'=free_126, F5'=free_118, G5'=free_122, H5'=free_119, Q5'=free_128, J5'=free_120, K5'=free_124, L5'=free_121, [ 0>=free_118 && 0>=free_125 && free_121>=1 && free_126>=1+W4 && free_127>=1+X4 && Y4>=1+Z4 && A5>=1+B5 ], cost: 1
      8: [14] -> f17 : D'=Z1, E'=A2, G'=B2, Q'=free_34, J'=free_35, K'=free_33, L'=free_36, [ B2>=1 && W1>=1 && free_36>=1+Y1 && Z1>=1+A2 ], cost: 1
     18: [15] -> f34 : D'=P3, E'=Q3_1, F'=O4, G'=S3, H'=-W+free_103, Q'=-W+free_103, J'=free_103, K'=free_100, L'=free_96, P'=free_99, V'=free_97, W'=-1+W, D1'=free_98, E1'=free_101, P1'=O4, T2'=free_102, U2'=free_103, M4'=free_95, N4'=free_103, [ W>=1 && S3>=1 && H2>=1 && F2>=1 && G4>=1+H4 && Q2>=1+J2 && Q4>=1+J4 && free_97>=1+R3 && free_96>=1+Q2_1 && P3>=1+Q3_1 && free_101>=1+L4 ], cost: 1
     19: [16] -> f34 : D'=P3, E'=Q3_1, G'=S3, K'=free_111, L'=free_113, P'=free_110, V'=free_108, W'=-1+W, D1'=free_109, E1'=free_112, K3'=free_114, L3'=free_106, M3'=free_107, N3'=free_115, V4'=free_105, [ W>=1 && 0>=free_115 && S3>=1 && X2>=1 && A3>=1+B3 && P4>=1+Q4_1 && free_108>=1+R3 && free_113>=1+Q3 && free_112>=1+S4 && T4>=1+U4 && P3>=1+Q3_1 ], cost: 1


Applied simple chaining:
  Start location: f14
     22: f34 -> [14] : [ V1>=1 && R1>=1+S1 && 0>=W1 && free_27>=1+U1 ], cost: INF
     21: f14 -> [15] : D'=P5, E'=Q5_1, G'=M5, P'=free_136, V'=free_129, W'=-1+free_133, O4'=free_133, D5'=free_138, E5'=free_135, F5'=free_137, G5'=free_130, H5'=free_134, Q5'=free_131, J5'=free_139, K5'=free_132, L5'=free_133, [ free_137>=1 && free_133>=1 && M5>=1 && free_135>=1+N5 && free_129>=1+O5 && P5>=1+Q5_1 && R5>=1+S5 && C2>=1 && D2>=1+E2 && 0>=F2 && free_37>=1+G2 ], cost: INF
     20: f14 -> [16] : D'=Y4, E'=Z4, G'=free_125, P'=free_117, V'=free_127, W'=-1+free_121, O4'=free_121, C5'=free_125, D5'=free_123, E5'=free_126, F5'=free_118, G5'=free_122, H5'=free_119, Q5'=free_128, J5'=free_120, K5'=free_124, L5'=free_121, [ 0>=free_118 && 0>=free_125 && free_121>=1 && free_126>=1+W4 && free_127>=1+X4 && Y4>=1+Z4 && A5>=1+B5 && 0>=free_53 && V2>=1+W2 && 0>=X2 && free_54>=1+Y2 ], cost: INF
      8: [14] -> f34 : D'=P3, E'=Q3_1, G'=S3, Q'=free_34, J'=free_35, K'=free_33, L'=free_36, P'=free_90, V'=free_92, W'=-1+W, D1'=free_89, E1'=free_91, P1'=free_93, M4'=free_88, [ B2>=1 && W1>=1 && free_36>=1+Y1 && Z1>=1+A2 && W>=1 && S3>=1 && G4>=1+H4 && Q4>=1+J4 && free_92>=1+R3 && P3>=1+Q3_1 && free_91>=1+L4 ], cost: 2
     18: [15] -> f34 : D'=P3, E'=Q3_1, F'=O4, G'=S3, H'=-W+free_103, Q'=-W+free_103, J'=free_103, K'=free_100, L'=free_96, P'=free_99, V'=free_97, W'=-1+W, D1'=free_98, E1'=free_101, P1'=O4, T2'=free_102, U2'=free_103, M4'=free_95, N4'=free_103, [ W>=1 && S3>=1 && H2>=1 && F2>=1 && G4>=1+H4 && Q2>=1+J2 && Q4>=1+J4 && free_97>=1+R3 && free_96>=1+Q2_1 && P3>=1+Q3_1 && free_101>=1+L4 ], cost: 1
     19: [16] -> f34 : D'=P3, E'=Q3_1, G'=S3, K'=free_111, L'=free_113, P'=free_110, V'=free_108, W'=-1+W, D1'=free_109, E1'=free_112, K3'=free_114, L3'=free_106, M3'=free_107, N3'=free_115, V4'=free_105, [ W>=1 && 0>=free_115 && S3>=1 && X2>=1 && A3>=1+B3 && P4>=1+Q4_1 && free_108>=1+R3 && free_113>=1+Q3 && free_112>=1+S4 && T4>=1+U4 && P3>=1+Q3_1 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f14
     25: f14 -> [17] : D'=P5, E'=Q5_1, G'=M5, P'=free_136, V'=free_129, W'=-1+free_133, O4'=free_133, D5'=free_138, E5'=free_135, F5'=free_137, G5'=free_130, H5'=free_134, Q5'=free_131, J5'=free_139, K5'=free_132, L5'=free_133, [ free_137>=1 && free_133>=1 && M5>=1 && free_135>=1+N5 && free_129>=1+O5 && P5>=1+Q5_1 && R5>=1+S5 && C2>=1 && D2>=1+E2 && 0>=F2 && free_37>=1+G2 ], cost: INF
     26: f14 -> [18] : D'=Y4, E'=Z4, G'=free_125, P'=free_117, V'=free_127, W'=-1+free_121, O4'=free_121, C5'=free_125, D5'=free_123, E5'=free_126, F5'=free_118, G5'=free_122, H5'=free_119, Q5'=free_128, J5'=free_120, K5'=free_124, L5'=free_121, [ 0>=free_118 && 0>=free_125 && free_121>=1 && free_126>=1+W4 && free_127>=1+X4 && Y4>=1+Z4 && A5>=1+B5 && 0>=free_53 && V2>=1+W2 && 0>=X2 && free_54>=1+Y2 ], cost: INF


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f14
     25: f14 -> [17] : D'=P5, E'=Q5_1, G'=M5, P'=free_136, V'=free_129, W'=-1+free_133, O4'=free_133, D5'=free_138, E5'=free_135, F5'=free_137, G5'=free_130, H5'=free_134, Q5'=free_131, J5'=free_139, K5'=free_132, L5'=free_133, [ free_137>=1 && free_133>=1 && M5>=1 && free_135>=1+N5 && free_129>=1+O5 && P5>=1+Q5_1 && R5>=1+S5 && C2>=1 && D2>=1+E2 && 0>=F2 && free_37>=1+G2 ], cost: INF
     26: f14 -> [18] : D'=Y4, E'=Z4, G'=free_125, P'=free_117, V'=free_127, W'=-1+free_121, O4'=free_121, C5'=free_125, D5'=free_123, E5'=free_126, F5'=free_118, G5'=free_122, H5'=free_119, Q5'=free_128, J5'=free_120, K5'=free_124, L5'=free_121, [ 0>=free_118 && 0>=free_125 && free_121>=1 && free_126>=1+W4 && free_127>=1+X4 && Y4>=1+Z4 && A5>=1+B5 && 0>=free_53 && V2>=1+W2 && 0>=X2 && free_54>=1+Y2 ], 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: free_137>=1 && free_133>=1 && M5>=1 && free_135>=1+N5 && free_129>=1+O5 && P5>=1+Q5_1 && R5>=1+S5 && C2>=1 && D2>=1+E2 && 0>=F2 && free_37>=1+G2
  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,?)