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


Simplified the transitions:
  Start location: f14
     17: f17 -> f34 : D'=W3, E'=X3, G'=Z3, P'=free_104, V'=free_105, W'=-1+W, D1'=free_106, E1'=free_108, F1'=free_103, H1'=free_103, Q1'=free_107, U1'=free_102, U4'=free_101, [ W>=1 && Z3>=1 && O4>=1+P4 && free_105>=1+Y3 && free_107>=1+Q4_1 && free_108>=1+R4 && S4>=1+T4 && W3>=1+X3 ], cost: 1
      8: f34 -> f17 : D'=E2, E'=F2, G'=G2, Q'=free_38, J'=free_40, K'=free_37, L'=free_39, [ G2>=1 && B2>=1 && free_39>=1+D2 && E2>=1+F2 ], cost: 1
      6: f34 -> f34 : D'=Y1, E'=Z1, G'=A2, P'=Q_1, Q_1'=free_32, R'=free_31, [ A2>=1 && free_31>=1+W1 && 0>=B2 && Y1>=1+Z1 ], cost: 1
     18: f35 -> f34 : D'=W3, E'=X3, F'=W4, G'=Z3, H'=free_111-W, Q'=free_111-W, J'=free_111, K'=free_114, L'=free_117, P'=free_109, V'=free_113, W'=-1+W, D1'=free_116, E1'=free_119, F1'=free_112, H1'=free_112, Q1'=free_118, U1'=W4, Z2'=free_115, A3'=free_111, U4'=free_110, V4'=free_111, [ W>=1 && Z3>=1 && M2>=1 && J2>=1 && N2>=1+O2 && O4>=1+P4 && free_113>=1+Y3 && free_117>=1+T2 && free_118>=1+Q4_1 && free_119>=1+R4 && S4>=1+T4 && W3>=1+X3 ], cost: 1
      9: f35 -> f35 : D'=K2, E'=L2, G'=H2, P'=Q_1, Q_1'=free_42, R'=free_41, [ H2>=1 && free_41>=1+Q2 && 0>=J2 && K2>=1+L2 ], cost: 1
     19: f36 -> f34 : D'=W3, E'=X3, G'=Z3, K'=free_126, L'=free_127, P'=free_121, V'=free_129, W'=-1+W, D1'=free_128, E1'=free_132, F1'=free_124, H1'=free_124, Q1'=free_131, R3'=free_123, S3'=free_130, T3'=free_125, U3'=free_120, D5'=free_122, [ W>=1 && 0>=free_120 && Z3>=1 && C3>=1 && G3>=1+H3 && X4>=1+Y4 && free_129>=1+Y3 && free_127>=1+M3 && free_131>=1+Z4 && free_132>=1+A5 && W3>=1+X3 && B5>=1+C5 ], cost: 1
     11: f36 -> f36 : D'=D3, E'=E3, G'=free_59, P'=Q_1, Q_1'=free_58, R'=free_60, F3'=free_59, [ 0>=free_59 && free_60>=1+B3 && 0>=C3 && D3>=1+E3 ], cost: 1
     21: f14 -> f35 : D'=X5, E'=Y5, G'=U5, P'=free_155, V'=free_148, W'=-1+free_152, W4'=free_152, L5'=free_154, M5'=free_146, N5'=free_147, O5'=free_150, P5'=free_151, Q5_1'=free_153, R5'=free_145, S5'=free_149, T5'=free_152, [ free_147>=1 && free_152>=1 && U5>=1 && free_146>=1+V5 && free_148>=1+W5 && X5>=1+Y5 && Z5>=1+A6 ], cost: 1
     20: f14 -> f36 : D'=G5, E'=H5, G'=free_141, P'=free_137, V'=free_143, W'=-1+free_144, W4'=free_144, K5'=free_141, L5'=free_135, M5'=free_136, N5'=free_139, O5'=free_140, P5'=free_142, Q5_1'=free_134, R5'=free_138, S5'=free_133, T5'=free_144, [ 0>=free_139 && free_144>=1 && 0>=free_141 && free_136>=1+E5 && free_143>=1+F5 && G5>=1+H5 && Q5>=1+J5 ], 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'=W3, E'=X3, G'=Z3, P'=free_104, V'=free_105, W'=-1+W, D1'=free_106, E1'=free_108, F1'=free_103, H1'=free_103, Q1'=free_107, U1'=free_102, U4'=free_101, [ W>=1 && Z3>=1 && O4>=1+P4 && free_105>=1+Y3 && free_107>=1+Q4_1 && free_108>=1+R4 && S4>=1+T4 && W3>=1+X3 ], cost: 1
     22: f34 -> [14] : [ A2>=1 && free_31>=1+W1 && 0>=B2 && Y1>=1+Z1 ], cost: INF
     23: f35 -> [15] : [ H2>=1 && free_41>=1+Q2 && 0>=J2 && K2>=1+L2 ], cost: INF
     24: f36 -> [16] : [ 0>=free_59 && free_60>=1+B3 && 0>=C3 && D3>=1+E3 ], cost: INF
     21: f14 -> f35 : D'=X5, E'=Y5, G'=U5, P'=free_155, V'=free_148, W'=-1+free_152, W4'=free_152, L5'=free_154, M5'=free_146, N5'=free_147, O5'=free_150, P5'=free_151, Q5_1'=free_153, R5'=free_145, S5'=free_149, T5'=free_152, [ free_147>=1 && free_152>=1 && U5>=1 && free_146>=1+V5 && free_148>=1+W5 && X5>=1+Y5 && Z5>=1+A6 ], cost: 1
     20: f14 -> f36 : D'=G5, E'=H5, G'=free_141, P'=free_137, V'=free_143, W'=-1+free_144, W4'=free_144, K5'=free_141, L5'=free_135, M5'=free_136, N5'=free_139, O5'=free_140, P5'=free_142, Q5_1'=free_134, R5'=free_138, S5'=free_133, T5'=free_144, [ 0>=free_139 && free_144>=1 && 0>=free_141 && free_136>=1+E5 && free_143>=1+F5 && G5>=1+H5 && Q5>=1+J5 ], cost: 1
      8: [14] -> f17 : D'=E2, E'=F2, G'=G2, Q'=free_38, J'=free_40, K'=free_37, L'=free_39, [ G2>=1 && B2>=1 && free_39>=1+D2 && E2>=1+F2 ], cost: 1
     18: [15] -> f34 : D'=W3, E'=X3, F'=W4, G'=Z3, H'=free_111-W, Q'=free_111-W, J'=free_111, K'=free_114, L'=free_117, P'=free_109, V'=free_113, W'=-1+W, D1'=free_116, E1'=free_119, F1'=free_112, H1'=free_112, Q1'=free_118, U1'=W4, Z2'=free_115, A3'=free_111, U4'=free_110, V4'=free_111, [ W>=1 && Z3>=1 && M2>=1 && J2>=1 && N2>=1+O2 && O4>=1+P4 && free_113>=1+Y3 && free_117>=1+T2 && free_118>=1+Q4_1 && free_119>=1+R4 && S4>=1+T4 && W3>=1+X3 ], cost: 1
     19: [16] -> f34 : D'=W3, E'=X3, G'=Z3, K'=free_126, L'=free_127, P'=free_121, V'=free_129, W'=-1+W, D1'=free_128, E1'=free_132, F1'=free_124, H1'=free_124, Q1'=free_131, R3'=free_123, S3'=free_130, T3'=free_125, U3'=free_120, D5'=free_122, [ W>=1 && 0>=free_120 && Z3>=1 && C3>=1 && G3>=1+H3 && X4>=1+Y4 && free_129>=1+Y3 && free_127>=1+M3 && free_131>=1+Z4 && free_132>=1+A5 && W3>=1+X3 && B5>=1+C5 ], cost: 1


Applied simple chaining:
  Start location: f14
     22: f34 -> [14] : [ A2>=1 && free_31>=1+W1 && 0>=B2 && Y1>=1+Z1 ], cost: INF
     21: f14 -> [15] : D'=X5, E'=Y5, G'=U5, P'=free_155, V'=free_148, W'=-1+free_152, W4'=free_152, L5'=free_154, M5'=free_146, N5'=free_147, O5'=free_150, P5'=free_151, Q5_1'=free_153, R5'=free_145, S5'=free_149, T5'=free_152, [ free_147>=1 && free_152>=1 && U5>=1 && free_146>=1+V5 && free_148>=1+W5 && X5>=1+Y5 && Z5>=1+A6 && H2>=1 && free_41>=1+Q2 && 0>=J2 && K2>=1+L2 ], cost: INF
     20: f14 -> [16] : D'=G5, E'=H5, G'=free_141, P'=free_137, V'=free_143, W'=-1+free_144, W4'=free_144, K5'=free_141, L5'=free_135, M5'=free_136, N5'=free_139, O5'=free_140, P5'=free_142, Q5_1'=free_134, R5'=free_138, S5'=free_133, T5'=free_144, [ 0>=free_139 && free_144>=1 && 0>=free_141 && free_136>=1+E5 && free_143>=1+F5 && G5>=1+H5 && Q5>=1+J5 && 0>=free_59 && free_60>=1+B3 && 0>=C3 && D3>=1+E3 ], cost: INF
      8: [14] -> f34 : D'=W3, E'=X3, G'=Z3, Q'=free_38, J'=free_40, K'=free_37, L'=free_39, P'=free_104, V'=free_105, W'=-1+W, D1'=free_106, E1'=free_108, F1'=free_103, H1'=free_103, Q1'=free_107, U1'=free_102, U4'=free_101, [ G2>=1 && B2>=1 && free_39>=1+D2 && E2>=1+F2 && W>=1 && Z3>=1 && O4>=1+P4 && free_105>=1+Y3 && free_107>=1+Q4_1 && free_108>=1+R4 && S4>=1+T4 && W3>=1+X3 ], cost: 2
     18: [15] -> f34 : D'=W3, E'=X3, F'=W4, G'=Z3, H'=free_111-W, Q'=free_111-W, J'=free_111, K'=free_114, L'=free_117, P'=free_109, V'=free_113, W'=-1+W, D1'=free_116, E1'=free_119, F1'=free_112, H1'=free_112, Q1'=free_118, U1'=W4, Z2'=free_115, A3'=free_111, U4'=free_110, V4'=free_111, [ W>=1 && Z3>=1 && M2>=1 && J2>=1 && N2>=1+O2 && O4>=1+P4 && free_113>=1+Y3 && free_117>=1+T2 && free_118>=1+Q4_1 && free_119>=1+R4 && S4>=1+T4 && W3>=1+X3 ], cost: 1
     19: [16] -> f34 : D'=W3, E'=X3, G'=Z3, K'=free_126, L'=free_127, P'=free_121, V'=free_129, W'=-1+W, D1'=free_128, E1'=free_132, F1'=free_124, H1'=free_124, Q1'=free_131, R3'=free_123, S3'=free_130, T3'=free_125, U3'=free_120, D5'=free_122, [ W>=1 && 0>=free_120 && Z3>=1 && C3>=1 && G3>=1+H3 && X4>=1+Y4 && free_129>=1+Y3 && free_127>=1+M3 && free_131>=1+Z4 && free_132>=1+A5 && W3>=1+X3 && B5>=1+C5 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f14
     25: f14 -> [17] : D'=X5, E'=Y5, G'=U5, P'=free_155, V'=free_148, W'=-1+free_152, W4'=free_152, L5'=free_154, M5'=free_146, N5'=free_147, O5'=free_150, P5'=free_151, Q5_1'=free_153, R5'=free_145, S5'=free_149, T5'=free_152, [ free_147>=1 && free_152>=1 && U5>=1 && free_146>=1+V5 && free_148>=1+W5 && X5>=1+Y5 && Z5>=1+A6 && H2>=1 && free_41>=1+Q2 && 0>=J2 && K2>=1+L2 ], cost: INF
     26: f14 -> [18] : D'=G5, E'=H5, G'=free_141, P'=free_137, V'=free_143, W'=-1+free_144, W4'=free_144, K5'=free_141, L5'=free_135, M5'=free_136, N5'=free_139, O5'=free_140, P5'=free_142, Q5_1'=free_134, R5'=free_138, S5'=free_133, T5'=free_144, [ 0>=free_139 && free_144>=1 && 0>=free_141 && free_136>=1+E5 && free_143>=1+F5 && G5>=1+H5 && Q5>=1+J5 && 0>=free_59 && free_60>=1+B3 && 0>=C3 && D3>=1+E3 ], cost: INF


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f14
     25: f14 -> [17] : D'=X5, E'=Y5, G'=U5, P'=free_155, V'=free_148, W'=-1+free_152, W4'=free_152, L5'=free_154, M5'=free_146, N5'=free_147, O5'=free_150, P5'=free_151, Q5_1'=free_153, R5'=free_145, S5'=free_149, T5'=free_152, [ free_147>=1 && free_152>=1 && U5>=1 && free_146>=1+V5 && free_148>=1+W5 && X5>=1+Y5 && Z5>=1+A6 && H2>=1 && free_41>=1+Q2 && 0>=J2 && K2>=1+L2 ], cost: INF
     26: f14 -> [18] : D'=G5, E'=H5, G'=free_141, P'=free_137, V'=free_143, W'=-1+free_144, W4'=free_144, K5'=free_141, L5'=free_135, M5'=free_136, N5'=free_139, O5'=free_140, P5'=free_142, Q5_1'=free_134, R5'=free_138, S5'=free_133, T5'=free_144, [ 0>=free_139 && free_144>=1 && 0>=free_141 && free_136>=1+E5 && free_143>=1+F5 && G5>=1+H5 && Q5>=1+J5 && 0>=free_59 && free_60>=1+B3 && 0>=C3 && D3>=1+E3 ], 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_147>=1 && free_152>=1 && U5>=1 && free_146>=1+V5 && free_148>=1+W5 && X5>=1+Y5 && Z5>=1+A6 && H2>=1 && free_41>=1+Q2 && 0>=J2 && K2>=1+L2
  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,?)