Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f2
      0: f2 -> f13 : A'=1, B'=free_1, C'=free_3, D'=free_5, E'=free, F'=free_2, G'=free_4, [ A==1 ], cost: 1
      3: f2 -> f27 : B'=free_7, C'=free_9, D'=free_11, E'=free_6, F'=free_8, G'=free_10, [ 0>=A ], cost: 1
      4: f2 -> f27 : B'=free_13, C'=free_15, D'=free_17, E'=free_12, F'=free_14, G'=free_16, [ A>=2 ], cost: 1
      1: f13 -> f16 : [ H>=Q ], cost: 1
     23: f13 -> f27 : [ Q>=1+H ], cost: 1
     22: f16 -> f13 : Q'=1+Q, [ K>=1+J ], cost: 1
      2: f16 -> f16 : K'=1+K, L'=2+L, [ J>=K ], cost: 1
      5: f27 -> f35 : M'=2+H-Q, N'=1, O'=0, [ 0>=Q && H>=Q ], cost: 1
      6: f27 -> f35 : M'=2+H-Q, N'=1, O'=0, [ Q>=2 && H>=Q ], cost: 1
      7: f27 -> f35 : Q'=1, M'=1, N'=1, O'=0, [ H>=1 && Q==1 ], cost: 1
     19: f27 -> f1 : [ 0>=2+A && Q>=1+H ], cost: 1
     20: f27 -> f1 : [ A>=0 && Q>=1+H ], cost: 1
     21: f27 -> f1 : A'=-1, [ Q>=1+H && 1+A==0 ], cost: 1
     18: f35 -> f27 : Q'=1+Q, [ P>=2*free_72 && 3*free_72>=1+P && Q_1>=2+free_72 ], cost: 1
      8: f35 -> f38 : [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 ], cost: 1
     17: f38 -> f35 : E'=N, N'=N+N*F-O*G, O'=O+N*G+O*F, Q_1'=1+Q_1, W'=2+W, [ K>=1+J ], cost: 1
     11: f38 -> f38 : K'=1+K, L'=3+free_20, Q_1'=1, R'=free_23*B+B*free_26, S'=-B*free_22+B*free_19, T'=C*free_25-free_27*C, U'=-free_24*C-free_21*C, [ J>=K+4*free_20 && K+5*free_20>=1+J && 0>=K && J>=K && Q_1==1 ], cost: 1
     12: f38 -> f38 : K'=1+K, L'=3+free_29, Q_1'=1, R'=free_32*B+free_35*B, S'=B*free_28-B*free_31, T'=C*free_34-free_36*C, U'=-free_30*C-free_33*C, [ J>=K+4*free_29 && K+5*free_29>=1+J && J>=K && K>=2 && Q_1==1 ], cost: 1
     13: f38 -> f38 : K'=2, L'=1, Q_1'=1, R'=B*free_41+free_38*B, S'=-B*free_37+B*free_43, T'=C*free_40-free_42*C, U'=-free_39*C-C*free_44, [ J>=1 && K==1 && Q_1==1 ], cost: 1
      9: f38 -> f53 : [ 0>=Q_1 && J>=K ], cost: 1
     10: f38 -> f53 : [ Q_1>=2 && J>=K ], cost: 1
     14: f53 -> f38 : K'=1+K, L'=2-K+J, R'=B*free_49+B*free_46, S'=B*free_52-B*free_45, T'=free_48*C-free_51*C, U'=-C*free_53-C*free_47, V'=3+P-free_50, [ Q_1>=2*free_50 && 3*free_50>=1+Q_1 && 0>=K ], cost: 1
     15: f53 -> f38 : K'=1+K, L'=2-K+J, R'=B*free_55+B*free_58, S'=free_61*B-free_54*B, T'=free_57*C-C*free_60, U'=-C*free_56-free_62*C, V'=3-free_59+P, [ Q_1>=2*free_59 && 3*free_59>=1+Q_1 && K>=2 ], cost: 1
     16: f53 -> f38 : K'=2, L'=1, R'=free_64*B+B*free_67, S'=B*free_70-B*free_63, T'=-C*free_69+C*free_66, U'=-free_71*C-free_65*C, V'=3-free_68+P, [ Q_1>=2*free_68 && 3*free_68>=1+Q_1 && K==1 ], cost: 1


Simplified the transitions:
  Start location: f2
      0: f2 -> f13 : A'=1, B'=free_1, C'=free_3, D'=free_5, E'=free, F'=free_2, G'=free_4, [ A==1 ], cost: 1
      3: f2 -> f27 : B'=free_7, C'=free_9, D'=free_11, E'=free_6, F'=free_8, G'=free_10, [ 0>=A ], cost: 1
      4: f2 -> f27 : B'=free_13, C'=free_15, D'=free_17, E'=free_12, F'=free_14, G'=free_16, [ A>=2 ], cost: 1
      1: f13 -> f16 : [ H>=Q ], cost: 1
     23: f13 -> f27 : [ Q>=1+H ], cost: 1
     22: f16 -> f13 : Q'=1+Q, [ K>=1+J ], cost: 1
      2: f16 -> f16 : K'=1+K, L'=2+L, [ J>=K ], cost: 1
      5: f27 -> f35 : M'=2+H-Q, N'=1, O'=0, [ 0>=Q && H>=Q ], cost: 1
      6: f27 -> f35 : M'=2+H-Q, N'=1, O'=0, [ Q>=2 && H>=Q ], cost: 1
      7: f27 -> f35 : Q'=1, M'=1, N'=1, O'=0, [ H>=1 && Q==1 ], cost: 1
     18: f35 -> f27 : Q'=1+Q, [ P>=2*free_72 && 3*free_72>=1+P && Q_1>=2+free_72 ], cost: 1
      8: f35 -> f38 : [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 ], cost: 1
     17: f38 -> f35 : E'=N, N'=N+N*F-O*G, O'=O+N*G+O*F, Q_1'=1+Q_1, W'=2+W, [ K>=1+J ], cost: 1
     11: f38 -> f38 : K'=1+K, L'=3+free_20, Q_1'=1, R'=free_23*B+B*free_26, S'=-B*free_22+B*free_19, T'=C*free_25-free_27*C, U'=-free_24*C-free_21*C, [ J>=K+4*free_20 && K+5*free_20>=1+J && 0>=K && J>=K && Q_1==1 ], cost: 1
     12: f38 -> f38 : K'=1+K, L'=3+free_29, Q_1'=1, R'=free_32*B+free_35*B, S'=B*free_28-B*free_31, T'=C*free_34-free_36*C, U'=-free_30*C-free_33*C, [ J>=K+4*free_29 && K+5*free_29>=1+J && J>=K && K>=2 && Q_1==1 ], cost: 1
     13: f38 -> f38 : K'=2, L'=1, Q_1'=1, R'=B*free_41+free_38*B, S'=-B*free_37+B*free_43, T'=C*free_40-free_42*C, U'=-free_39*C-C*free_44, [ J>=1 && K==1 && Q_1==1 ], cost: 1
      9: f38 -> f53 : [ 0>=Q_1 && J>=K ], cost: 1
     10: f38 -> f53 : [ Q_1>=2 && J>=K ], cost: 1
     14: f53 -> f38 : K'=1+K, L'=2-K+J, R'=B*free_49+B*free_46, S'=B*free_52-B*free_45, T'=free_48*C-free_51*C, U'=-C*free_53-C*free_47, V'=3+P-free_50, [ Q_1>=2*free_50 && 3*free_50>=1+Q_1 && 0>=K ], cost: 1
     15: f53 -> f38 : K'=1+K, L'=2-K+J, R'=B*free_55+B*free_58, S'=free_61*B-free_54*B, T'=free_57*C-C*free_60, U'=-C*free_56-free_62*C, V'=3-free_59+P, [ Q_1>=2*free_59 && 3*free_59>=1+Q_1 && K>=2 ], cost: 1
     16: f53 -> f38 : K'=2, L'=1, R'=free_64*B+B*free_67, S'=B*free_70-B*free_63, T'=-C*free_69+C*free_66, U'=-free_71*C-free_65*C, V'=3-free_68+P, [ Q_1>=2*free_68 && 3*free_68>=1+Q_1 && K==1 ], cost: 1

Eliminating 1 self-loops for location f16
  Self-Loop 2 has the metering function: 1-K+J, resulting in the new transition 24.
  Removing the self-loops: 2.
Eliminating 3 self-loops for location f38
  Self-Loop 13 has the metering function: 2-K, resulting in the new transition 27.
  Found this metering function when nesting loops: meter,
  Found this metering function when nesting loops: meter_1,
  Removing the self-loops: 11 12 13.
Adding an epsilon transition (to model nonexecution of the loops): 28.

Removed all Self-loops using metering functions (where possible):
  Start location: f2
      0: f2 -> f13 : A'=1, B'=free_1, C'=free_3, D'=free_5, E'=free, F'=free_2, G'=free_4, [ A==1 ], cost: 1
      3: f2 -> f27 : B'=free_7, C'=free_9, D'=free_11, E'=free_6, F'=free_8, G'=free_10, [ 0>=A ], cost: 1
      4: f2 -> f27 : B'=free_13, C'=free_15, D'=free_17, E'=free_12, F'=free_14, G'=free_16, [ A>=2 ], cost: 1
      1: f13 -> f16 : [ H>=Q ], cost: 1
     23: f13 -> f27 : [ Q>=1+H ], cost: 1
     24: f16 -> [8] : K'=1+J, L'=2-2*K+L+2*J, [ J>=K ], cost: 1-K+J
      5: f27 -> f35 : M'=2+H-Q, N'=1, O'=0, [ 0>=Q && H>=Q ], cost: 1
      6: f27 -> f35 : M'=2+H-Q, N'=1, O'=0, [ Q>=2 && H>=Q ], cost: 1
      7: f27 -> f35 : Q'=1, M'=1, N'=1, O'=0, [ H>=1 && Q==1 ], cost: 1
     18: f35 -> f27 : Q'=1+Q, [ P>=2*free_72 && 3*free_72>=1+P && Q_1>=2+free_72 ], cost: 1
      8: f35 -> f38 : [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 ], cost: 1
     25: f38 -> [9] : K'=1+K, L'=3+free_20, Q_1'=1, R'=free_23*B+B*free_26, S'=-B*free_22+B*free_19, T'=C*free_25-free_27*C, U'=-free_24*C-free_21*C, [ J>=K+4*free_20 && K+5*free_20>=1+J && 0>=K && J>=K && Q_1==1 ], cost: 1
     26: f38 -> [9] : K'=1+K, L'=3+free_29, Q_1'=1, R'=free_32*B+free_35*B, S'=B*free_28-B*free_31, T'=C*free_34-free_36*C, U'=-free_30*C-free_33*C, [ J>=K+4*free_29 && K+5*free_29>=1+J && J>=K && K>=2 && Q_1==1 ], cost: 1
     27: f38 -> [9] : K'=2, L'=1, Q_1'=1, R'=B*free_41+free_38*B, S'=-B*free_37+B*free_43, T'=C*free_40-free_42*C, U'=-free_39*C-C*free_44, [ J>=1 && K==1 && Q_1==1 ], cost: 2-K
     28: f38 -> [9] : [], cost: 0
     14: f53 -> f38 : K'=1+K, L'=2-K+J, R'=B*free_49+B*free_46, S'=B*free_52-B*free_45, T'=free_48*C-free_51*C, U'=-C*free_53-C*free_47, V'=3+P-free_50, [ Q_1>=2*free_50 && 3*free_50>=1+Q_1 && 0>=K ], cost: 1
     15: f53 -> f38 : K'=1+K, L'=2-K+J, R'=B*free_55+B*free_58, S'=free_61*B-free_54*B, T'=free_57*C-C*free_60, U'=-C*free_56-free_62*C, V'=3-free_59+P, [ Q_1>=2*free_59 && 3*free_59>=1+Q_1 && K>=2 ], cost: 1
     16: f53 -> f38 : K'=2, L'=1, R'=free_64*B+B*free_67, S'=B*free_70-B*free_63, T'=-C*free_69+C*free_66, U'=-free_71*C-free_65*C, V'=3-free_68+P, [ Q_1>=2*free_68 && 3*free_68>=1+Q_1 && K==1 ], cost: 1
     22: [8] -> f13 : Q'=1+Q, [ K>=1+J ], cost: 1
     17: [9] -> f35 : E'=N, N'=N+N*F-O*G, O'=O+N*G+O*F, Q_1'=1+Q_1, W'=2+W, [ K>=1+J ], cost: 1
      9: [9] -> f53 : [ 0>=Q_1 && J>=K ], cost: 1
     10: [9] -> f53 : [ Q_1>=2 && J>=K ], cost: 1


Applied simple chaining:
  Start location: f2
      0: f2 -> f13 : A'=1, B'=free_1, C'=free_3, D'=free_5, E'=free, F'=free_2, G'=free_4, [ A==1 ], cost: 1
      3: f2 -> f27 : B'=free_7, C'=free_9, D'=free_11, E'=free_6, F'=free_8, G'=free_10, [ 0>=A ], cost: 1
      4: f2 -> f27 : B'=free_13, C'=free_15, D'=free_17, E'=free_12, F'=free_14, G'=free_16, [ A>=2 ], cost: 1
      1: f13 -> f13 : Q'=1+Q, K'=1+J, L'=2-2*K+L+2*J, [ H>=Q && J>=K && 1+J>=1+J ], cost: 3-K+J
     23: f13 -> f27 : [ Q>=1+H ], cost: 1
      5: f27 -> f35 : M'=2+H-Q, N'=1, O'=0, [ 0>=Q && H>=Q ], cost: 1
      6: f27 -> f35 : M'=2+H-Q, N'=1, O'=0, [ Q>=2 && H>=Q ], cost: 1
      7: f27 -> f35 : Q'=1, M'=1, N'=1, O'=0, [ H>=1 && Q==1 ], cost: 1
     18: f35 -> f27 : Q'=1+Q, [ P>=2*free_72 && 3*free_72>=1+P && Q_1>=2+free_72 ], cost: 1
      8: f35 -> f38 : [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 ], cost: 1
     25: f38 -> [9] : K'=1+K, L'=3+free_20, Q_1'=1, R'=free_23*B+B*free_26, S'=-B*free_22+B*free_19, T'=C*free_25-free_27*C, U'=-free_24*C-free_21*C, [ J>=K+4*free_20 && K+5*free_20>=1+J && 0>=K && J>=K && Q_1==1 ], cost: 1
     26: f38 -> [9] : K'=1+K, L'=3+free_29, Q_1'=1, R'=free_32*B+free_35*B, S'=B*free_28-B*free_31, T'=C*free_34-free_36*C, U'=-free_30*C-free_33*C, [ J>=K+4*free_29 && K+5*free_29>=1+J && J>=K && K>=2 && Q_1==1 ], cost: 1
     27: f38 -> [9] : K'=2, L'=1, Q_1'=1, R'=B*free_41+free_38*B, S'=-B*free_37+B*free_43, T'=C*free_40-free_42*C, U'=-free_39*C-C*free_44, [ J>=1 && K==1 && Q_1==1 ], cost: 2-K
     28: f38 -> [9] : [], cost: 0
     14: f53 -> f38 : K'=1+K, L'=2-K+J, R'=B*free_49+B*free_46, S'=B*free_52-B*free_45, T'=free_48*C-free_51*C, U'=-C*free_53-C*free_47, V'=3+P-free_50, [ Q_1>=2*free_50 && 3*free_50>=1+Q_1 && 0>=K ], cost: 1
     15: f53 -> f38 : K'=1+K, L'=2-K+J, R'=B*free_55+B*free_58, S'=free_61*B-free_54*B, T'=free_57*C-C*free_60, U'=-C*free_56-free_62*C, V'=3-free_59+P, [ Q_1>=2*free_59 && 3*free_59>=1+Q_1 && K>=2 ], cost: 1
     16: f53 -> f38 : K'=2, L'=1, R'=free_64*B+B*free_67, S'=B*free_70-B*free_63, T'=-C*free_69+C*free_66, U'=-free_71*C-free_65*C, V'=3-free_68+P, [ Q_1>=2*free_68 && 3*free_68>=1+Q_1 && K==1 ], cost: 1
     17: [9] -> f35 : E'=N, N'=N+N*F-O*G, O'=O+N*G+O*F, Q_1'=1+Q_1, W'=2+W, [ K>=1+J ], cost: 1
      9: [9] -> f53 : [ 0>=Q_1 && J>=K ], cost: 1
     10: [9] -> f53 : [ Q_1>=2 && J>=K ], cost: 1

Eliminating 1 self-loops for location f13
  Removing the self-loops: 1.
Adding an epsilon transition (to model nonexecution of the loops): 30.

Removed all Self-loops using metering functions (where possible):
  Start location: f2
      0: f2 -> f13 : A'=1, B'=free_1, C'=free_3, D'=free_5, E'=free, F'=free_2, G'=free_4, [ A==1 ], cost: 1
      3: f2 -> f27 : B'=free_7, C'=free_9, D'=free_11, E'=free_6, F'=free_8, G'=free_10, [ 0>=A ], cost: 1
      4: f2 -> f27 : B'=free_13, C'=free_15, D'=free_17, E'=free_12, F'=free_14, G'=free_16, [ A>=2 ], cost: 1
     29: f13 -> [10] : Q'=1+Q, K'=1+J, L'=2-2*K+L+2*J, [ H>=Q && J>=K ], cost: 3-K+J
     30: f13 -> [10] : [], cost: 0
      5: f27 -> f35 : M'=2+H-Q, N'=1, O'=0, [ 0>=Q && H>=Q ], cost: 1
      6: f27 -> f35 : M'=2+H-Q, N'=1, O'=0, [ Q>=2 && H>=Q ], cost: 1
      7: f27 -> f35 : Q'=1, M'=1, N'=1, O'=0, [ H>=1 && Q==1 ], cost: 1
     18: f35 -> f27 : Q'=1+Q, [ P>=2*free_72 && 3*free_72>=1+P && Q_1>=2+free_72 ], cost: 1
      8: f35 -> f38 : [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 ], cost: 1
     25: f38 -> [9] : K'=1+K, L'=3+free_20, Q_1'=1, R'=free_23*B+B*free_26, S'=-B*free_22+B*free_19, T'=C*free_25-free_27*C, U'=-free_24*C-free_21*C, [ J>=K+4*free_20 && K+5*free_20>=1+J && 0>=K && J>=K && Q_1==1 ], cost: 1
     26: f38 -> [9] : K'=1+K, L'=3+free_29, Q_1'=1, R'=free_32*B+free_35*B, S'=B*free_28-B*free_31, T'=C*free_34-free_36*C, U'=-free_30*C-free_33*C, [ J>=K+4*free_29 && K+5*free_29>=1+J && J>=K && K>=2 && Q_1==1 ], cost: 1
     27: f38 -> [9] : K'=2, L'=1, Q_1'=1, R'=B*free_41+free_38*B, S'=-B*free_37+B*free_43, T'=C*free_40-free_42*C, U'=-free_39*C-C*free_44, [ J>=1 && K==1 && Q_1==1 ], cost: 2-K
     28: f38 -> [9] : [], cost: 0
     14: f53 -> f38 : K'=1+K, L'=2-K+J, R'=B*free_49+B*free_46, S'=B*free_52-B*free_45, T'=free_48*C-free_51*C, U'=-C*free_53-C*free_47, V'=3+P-free_50, [ Q_1>=2*free_50 && 3*free_50>=1+Q_1 && 0>=K ], cost: 1
     15: f53 -> f38 : K'=1+K, L'=2-K+J, R'=B*free_55+B*free_58, S'=free_61*B-free_54*B, T'=free_57*C-C*free_60, U'=-C*free_56-free_62*C, V'=3-free_59+P, [ Q_1>=2*free_59 && 3*free_59>=1+Q_1 && K>=2 ], cost: 1
     16: f53 -> f38 : K'=2, L'=1, R'=free_64*B+B*free_67, S'=B*free_70-B*free_63, T'=-C*free_69+C*free_66, U'=-free_71*C-free_65*C, V'=3-free_68+P, [ Q_1>=2*free_68 && 3*free_68>=1+Q_1 && K==1 ], cost: 1
     17: [9] -> f35 : E'=N, N'=N+N*F-O*G, O'=O+N*G+O*F, Q_1'=1+Q_1, W'=2+W, [ K>=1+J ], cost: 1
      9: [9] -> f53 : [ 0>=Q_1 && J>=K ], cost: 1
     10: [9] -> f53 : [ Q_1>=2 && J>=K ], cost: 1
     23: [10] -> f27 : [ Q>=1+H ], cost: 1


Applied chaining over branches and pruning:
  Start location: f2
      3: f2 -> f27 : B'=free_7, C'=free_9, D'=free_11, E'=free_6, F'=free_8, G'=free_10, [ 0>=A ], cost: 1
      4: f2 -> f27 : B'=free_13, C'=free_15, D'=free_17, E'=free_12, F'=free_14, G'=free_16, [ A>=2 ], cost: 1
     31: f2 -> [10] : A'=1, B'=free_1, C'=free_3, D'=free_5, E'=free, F'=free_2, G'=free_4, Q'=1+Q, K'=1+J, L'=2-2*K+L+2*J, [ A==1 && H>=Q && J>=K ], cost: 4-K+J
     32: f2 -> [10] : A'=1, B'=free_1, C'=free_3, D'=free_5, E'=free, F'=free_2, G'=free_4, [ A==1 ], cost: 1
      5: f27 -> f35 : M'=2+H-Q, N'=1, O'=0, [ 0>=Q && H>=Q ], cost: 1
      6: f27 -> f35 : M'=2+H-Q, N'=1, O'=0, [ Q>=2 && H>=Q ], cost: 1
      7: f27 -> f35 : Q'=1, M'=1, N'=1, O'=0, [ H>=1 && Q==1 ], cost: 1
     18: f35 -> f27 : Q'=1+Q, [ P>=2*free_72 && 3*free_72>=1+P && Q_1>=2+free_72 ], cost: 1
      8: f35 -> f38 : [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 ], cost: 1
     33: f38 -> f35 : E'=N, K'=2, L'=1, N'=N+N*F-O*G, O'=O+N*G+O*F, Q_1'=2, R'=B*free_41+free_38*B, S'=-B*free_37+B*free_43, T'=C*free_40-free_42*C, U'=-free_39*C-C*free_44, W'=2+W, [ J>=1 && K==1 && Q_1==1 && 2>=1+J ], cost: 3-K
     36: f38 -> f35 : E'=N, N'=N+N*F-O*G, O'=O+N*G+O*F, Q_1'=1+Q_1, W'=2+W, [ K>=1+J ], cost: 1
     37: f38 -> f53 : [ 0>=Q_1 && J>=K ], cost: 1
     38: f38 -> f53 : [ Q_1>=2 && J>=K ], cost: 1
     34: f38 -> [11] : K'=2, L'=1, Q_1'=1, R'=B*free_41+free_38*B, S'=-B*free_37+B*free_43, T'=C*free_40-free_42*C, U'=-free_39*C-C*free_44, [ J>=1 && K==1 && Q_1==1 ], cost: 2-K
     35: f38 -> [12] : K'=2, L'=1, Q_1'=1, R'=B*free_41+free_38*B, S'=-B*free_37+B*free_43, T'=C*free_40-free_42*C, U'=-free_39*C-C*free_44, [ J>=1 && K==1 && Q_1==1 ], cost: 2-K
     14: f53 -> f38 : K'=1+K, L'=2-K+J, R'=B*free_49+B*free_46, S'=B*free_52-B*free_45, T'=free_48*C-free_51*C, U'=-C*free_53-C*free_47, V'=3+P-free_50, [ Q_1>=2*free_50 && 3*free_50>=1+Q_1 && 0>=K ], cost: 1
     15: f53 -> f38 : K'=1+K, L'=2-K+J, R'=B*free_55+B*free_58, S'=free_61*B-free_54*B, T'=free_57*C-C*free_60, U'=-C*free_56-free_62*C, V'=3-free_59+P, [ Q_1>=2*free_59 && 3*free_59>=1+Q_1 && K>=2 ], cost: 1
     16: f53 -> f38 : K'=2, L'=1, R'=free_64*B+B*free_67, S'=B*free_70-B*free_63, T'=-C*free_69+C*free_66, U'=-free_71*C-free_65*C, V'=3-free_68+P, [ Q_1>=2*free_68 && 3*free_68>=1+Q_1 && K==1 ], cost: 1
     23: [10] -> f27 : [ Q>=1+H ], cost: 1


Applied chaining over branches and pruning:
  Start location: f2
      3: f2 -> f27 : B'=free_7, C'=free_9, D'=free_11, E'=free_6, F'=free_8, G'=free_10, [ 0>=A ], cost: 1
      4: f2 -> f27 : B'=free_13, C'=free_15, D'=free_17, E'=free_12, F'=free_14, G'=free_16, [ A>=2 ], cost: 1
     39: f2 -> f27 : A'=1, B'=free_1, C'=free_3, D'=free_5, E'=free, F'=free_2, G'=free_4, Q'=1+Q, K'=1+J, L'=2-2*K+L+2*J, [ A==1 && H>=Q && J>=K && 1+Q>=1+H ], cost: 5-K+J
     40: f2 -> f27 : A'=1, B'=free_1, C'=free_3, D'=free_5, E'=free, F'=free_2, G'=free_4, [ A==1 && Q>=1+H ], cost: 2
      5: f27 -> f35 : M'=2+H-Q, N'=1, O'=0, [ 0>=Q && H>=Q ], cost: 1
      6: f27 -> f35 : M'=2+H-Q, N'=1, O'=0, [ Q>=2 && H>=Q ], cost: 1
      7: f27 -> f35 : Q'=1, M'=1, N'=1, O'=0, [ H>=1 && Q==1 ], cost: 1
     18: f35 -> f27 : Q'=1+Q, [ P>=2*free_72 && 3*free_72>=1+P && Q_1>=2+free_72 ], cost: 1
      8: f35 -> f38 : [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 ], cost: 1
     33: f38 -> f35 : E'=N, K'=2, L'=1, N'=N+N*F-O*G, O'=O+N*G+O*F, Q_1'=2, R'=B*free_41+free_38*B, S'=-B*free_37+B*free_43, T'=C*free_40-free_42*C, U'=-free_39*C-C*free_44, W'=2+W, [ J>=1 && K==1 && Q_1==1 && 2>=1+J ], cost: 3-K
     36: f38 -> f35 : E'=N, N'=N+N*F-O*G, O'=O+N*G+O*F, Q_1'=1+Q_1, W'=2+W, [ K>=1+J ], cost: 1
     41: f38 -> f38 : K'=1+K, L'=2-K+J, R'=B*free_49+B*free_46, S'=B*free_52-B*free_45, T'=free_48*C-free_51*C, U'=-C*free_53-C*free_47, V'=3+P-free_50, [ Q_1>=2 && J>=K && Q_1>=2*free_50 && 3*free_50>=1+Q_1 && 0>=K ], cost: 2
     42: f38 -> f38 : K'=1+K, L'=2-K+J, R'=B*free_55+B*free_58, S'=free_61*B-free_54*B, T'=free_57*C-C*free_60, U'=-C*free_56-free_62*C, V'=3-free_59+P, [ Q_1>=2 && J>=K && Q_1>=2*free_59 && 3*free_59>=1+Q_1 && K>=2 ], cost: 2
     43: f38 -> f38 : K'=2, L'=1, R'=free_64*B+B*free_67, S'=B*free_70-B*free_63, T'=-C*free_69+C*free_66, U'=-free_71*C-free_65*C, V'=3-free_68+P, [ Q_1>=2 && J>=K && Q_1>=2*free_68 && 3*free_68>=1+Q_1 && K==1 ], cost: 2
     34: f38 -> [11] : K'=2, L'=1, Q_1'=1, R'=B*free_41+free_38*B, S'=-B*free_37+B*free_43, T'=C*free_40-free_42*C, U'=-free_39*C-C*free_44, [ J>=1 && K==1 && Q_1==1 ], cost: 2-K
     35: f38 -> [12] : K'=2, L'=1, Q_1'=1, R'=B*free_41+free_38*B, S'=-B*free_37+B*free_43, T'=C*free_40-free_42*C, U'=-free_39*C-C*free_44, [ J>=1 && K==1 && Q_1==1 ], cost: 2-K

Eliminating 3 self-loops for location f38
  Self-Loop 43 has the metering function: 1-K, resulting in the new transition 46.
  Found this metering function when nesting loops: meter_2,
  Found this metering function when nesting loops: meter_3,
  Removing the self-loops: 41 42 43.
Adding an epsilon transition (to model nonexecution of the loops): 47.

Removed all Self-loops using metering functions (where possible):
  Start location: f2
      3: f2 -> f27 : B'=free_7, C'=free_9, D'=free_11, E'=free_6, F'=free_8, G'=free_10, [ 0>=A ], cost: 1
      4: f2 -> f27 : B'=free_13, C'=free_15, D'=free_17, E'=free_12, F'=free_14, G'=free_16, [ A>=2 ], cost: 1
     39: f2 -> f27 : A'=1, B'=free_1, C'=free_3, D'=free_5, E'=free, F'=free_2, G'=free_4, Q'=1+Q, K'=1+J, L'=2-2*K+L+2*J, [ A==1 && H>=Q && J>=K && 1+Q>=1+H ], cost: 5-K+J
     40: f2 -> f27 : A'=1, B'=free_1, C'=free_3, D'=free_5, E'=free, F'=free_2, G'=free_4, [ A==1 && Q>=1+H ], cost: 2
      5: f27 -> f35 : M'=2+H-Q, N'=1, O'=0, [ 0>=Q && H>=Q ], cost: 1
      6: f27 -> f35 : M'=2+H-Q, N'=1, O'=0, [ Q>=2 && H>=Q ], cost: 1
      7: f27 -> f35 : Q'=1, M'=1, N'=1, O'=0, [ H>=1 && Q==1 ], cost: 1
     18: f35 -> f27 : Q'=1+Q, [ P>=2*free_72 && 3*free_72>=1+P && Q_1>=2+free_72 ], cost: 1
      8: f35 -> f38 : [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 ], cost: 1
     44: f38 -> [13] : K'=1+K, L'=2-K+J, R'=B*free_49+B*free_46, S'=B*free_52-B*free_45, T'=free_48*C-free_51*C, U'=-C*free_53-C*free_47, V'=3+P-free_50, [ Q_1>=2 && J>=K && Q_1>=2*free_50 && 3*free_50>=1+Q_1 && 0>=K ], cost: 2
     45: f38 -> [13] : K'=1+K, L'=2-K+J, R'=B*free_55+B*free_58, S'=free_61*B-free_54*B, T'=free_57*C-C*free_60, U'=-C*free_56-free_62*C, V'=3-free_59+P, [ Q_1>=2 && J>=K && Q_1>=2*free_59 && 3*free_59>=1+Q_1 && K>=2 ], cost: 2
     46: f38 -> [13] : K'=2, L'=1, R'=free_64*B+B*free_67, S'=B*free_70-B*free_63, T'=-C*free_69+C*free_66, U'=-free_71*C-free_65*C, V'=3-free_68+P, [ Q_1>=2 && J>=K && Q_1>=2*free_68 && 3*free_68>=1+Q_1 && K==1 ], cost: 2-2*K
     47: f38 -> [13] : [], cost: 0
     33: [13] -> f35 : E'=N, K'=2, L'=1, N'=N+N*F-O*G, O'=O+N*G+O*F, Q_1'=2, R'=B*free_41+free_38*B, S'=-B*free_37+B*free_43, T'=C*free_40-free_42*C, U'=-free_39*C-C*free_44, W'=2+W, [ J>=1 && K==1 && Q_1==1 && 2>=1+J ], cost: 3-K
     36: [13] -> f35 : E'=N, N'=N+N*F-O*G, O'=O+N*G+O*F, Q_1'=1+Q_1, W'=2+W, [ K>=1+J ], cost: 1
     34: [13] -> [11] : K'=2, L'=1, Q_1'=1, R'=B*free_41+free_38*B, S'=-B*free_37+B*free_43, T'=C*free_40-free_42*C, U'=-free_39*C-C*free_44, [ J>=1 && K==1 && Q_1==1 ], cost: 2-K
     35: [13] -> [12] : K'=2, L'=1, Q_1'=1, R'=B*free_41+free_38*B, S'=-B*free_37+B*free_43, T'=C*free_40-free_42*C, U'=-free_39*C-C*free_44, [ J>=1 && K==1 && Q_1==1 ], cost: 2-K


Applied chaining over branches and pruning:
  Start location: f2
      3: f2 -> f27 : B'=free_7, C'=free_9, D'=free_11, E'=free_6, F'=free_8, G'=free_10, [ 0>=A ], cost: 1
      4: f2 -> f27 : B'=free_13, C'=free_15, D'=free_17, E'=free_12, F'=free_14, G'=free_16, [ A>=2 ], cost: 1
     39: f2 -> f27 : A'=1, B'=free_1, C'=free_3, D'=free_5, E'=free, F'=free_2, G'=free_4, Q'=1+Q, K'=1+J, L'=2-2*K+L+2*J, [ A==1 && H>=Q && J>=K && 1+Q>=1+H ], cost: 5-K+J
     40: f2 -> f27 : A'=1, B'=free_1, C'=free_3, D'=free_5, E'=free, F'=free_2, G'=free_4, [ A==1 && Q>=1+H ], cost: 2
      5: f27 -> f35 : M'=2+H-Q, N'=1, O'=0, [ 0>=Q && H>=Q ], cost: 1
      6: f27 -> f35 : M'=2+H-Q, N'=1, O'=0, [ Q>=2 && H>=Q ], cost: 1
      7: f27 -> f35 : Q'=1, M'=1, N'=1, O'=0, [ H>=1 && Q==1 ], cost: 1
     18: f35 -> f27 : Q'=1+Q, [ P>=2*free_72 && 3*free_72>=1+P && Q_1>=2+free_72 ], cost: 1
     48: f35 -> [13] : K'=1+K, L'=2-K+J, R'=B*free_49+B*free_46, S'=B*free_52-B*free_45, T'=free_48*C-free_51*C, U'=-C*free_53-C*free_47, V'=3+P-free_50, [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 && Q_1>=2 && J>=K && Q_1>=2*free_50 && 3*free_50>=1+Q_1 && 0>=K ], cost: 3
     49: f35 -> [13] : K'=1+K, L'=2-K+J, R'=B*free_55+B*free_58, S'=free_61*B-free_54*B, T'=free_57*C-C*free_60, U'=-C*free_56-free_62*C, V'=3-free_59+P, [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 && Q_1>=2 && J>=K && Q_1>=2*free_59 && 3*free_59>=1+Q_1 && K>=2 ], cost: 3
     50: f35 -> [13] : K'=2, L'=1, R'=free_64*B+B*free_67, S'=B*free_70-B*free_63, T'=-C*free_69+C*free_66, U'=-free_71*C-free_65*C, V'=3-free_68+P, [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 && Q_1>=2 && J>=K && Q_1>=2*free_68 && 3*free_68>=1+Q_1 && K==1 ], cost: 3-2*K
     51: f35 -> [13] : [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 ], cost: 1
     33: [13] -> f35 : E'=N, K'=2, L'=1, N'=N+N*F-O*G, O'=O+N*G+O*F, Q_1'=2, R'=B*free_41+free_38*B, S'=-B*free_37+B*free_43, T'=C*free_40-free_42*C, U'=-free_39*C-C*free_44, W'=2+W, [ J>=1 && K==1 && Q_1==1 && 2>=1+J ], cost: 3-K
     36: [13] -> f35 : E'=N, N'=N+N*F-O*G, O'=O+N*G+O*F, Q_1'=1+Q_1, W'=2+W, [ K>=1+J ], cost: 1
     34: [13] -> [11] : K'=2, L'=1, Q_1'=1, R'=B*free_41+free_38*B, S'=-B*free_37+B*free_43, T'=C*free_40-free_42*C, U'=-free_39*C-C*free_44, [ J>=1 && K==1 && Q_1==1 ], cost: 2-K
     35: [13] -> [12] : K'=2, L'=1, Q_1'=1, R'=B*free_41+free_38*B, S'=-B*free_37+B*free_43, T'=C*free_40-free_42*C, U'=-free_39*C-C*free_44, [ J>=1 && K==1 && Q_1==1 ], cost: 2-K


Applied chaining over branches and pruning:
  Start location: f2
      3: f2 -> f27 : B'=free_7, C'=free_9, D'=free_11, E'=free_6, F'=free_8, G'=free_10, [ 0>=A ], cost: 1
      4: f2 -> f27 : B'=free_13, C'=free_15, D'=free_17, E'=free_12, F'=free_14, G'=free_16, [ A>=2 ], cost: 1
     39: f2 -> f27 : A'=1, B'=free_1, C'=free_3, D'=free_5, E'=free, F'=free_2, G'=free_4, Q'=1+Q, K'=1+J, L'=2-2*K+L+2*J, [ A==1 && H>=Q && J>=K && 1+Q>=1+H ], cost: 5-K+J
     40: f2 -> f27 : A'=1, B'=free_1, C'=free_3, D'=free_5, E'=free, F'=free_2, G'=free_4, [ A==1 && Q>=1+H ], cost: 2
      5: f27 -> f35 : M'=2+H-Q, N'=1, O'=0, [ 0>=Q && H>=Q ], cost: 1
      6: f27 -> f35 : M'=2+H-Q, N'=1, O'=0, [ Q>=2 && H>=Q ], cost: 1
      7: f27 -> f35 : Q'=1, M'=1, N'=1, O'=0, [ H>=1 && Q==1 ], cost: 1
     18: f35 -> f27 : Q'=1+Q, [ P>=2*free_72 && 3*free_72>=1+P && Q_1>=2+free_72 ], cost: 1
     52: f35 -> f35 : E'=N, K'=1+K, L'=2-K+J, N'=N+N*F-O*G, O'=O+N*G+O*F, Q_1'=1+Q_1, R'=B*free_49+B*free_46, S'=B*free_52-B*free_45, T'=free_48*C-free_51*C, U'=-C*free_53-C*free_47, V'=3+P-free_50, W'=2+W, [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 && Q_1>=2 && J>=K && Q_1>=2*free_50 && 3*free_50>=1+Q_1 && 0>=K && 1+K>=1+J ], cost: 4
     53: f35 -> f35 : E'=N, K'=1+K, L'=2-K+J, N'=N+N*F-O*G, O'=O+N*G+O*F, Q_1'=1+Q_1, R'=B*free_55+B*free_58, S'=free_61*B-free_54*B, T'=free_57*C-C*free_60, U'=-C*free_56-free_62*C, V'=3-free_59+P, W'=2+W, [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 && Q_1>=2 && J>=K && Q_1>=2*free_59 && 3*free_59>=1+Q_1 && K>=2 && 1+K>=1+J ], cost: 4
     55: f35 -> f35 : E'=N, K'=2, L'=1, N'=N+N*F-O*G, O'=O+N*G+O*F, Q_1'=1+Q_1, R'=free_64*B+B*free_67, S'=B*free_70-B*free_63, T'=-C*free_69+C*free_66, U'=-free_71*C-free_65*C, V'=3-free_68+P, W'=2+W, [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 && Q_1>=2 && J>=K && Q_1>=2*free_68 && 3*free_68>=1+Q_1 && K==1 && 2>=1+J ], cost: 4-2*K
     58: f35 -> f35 : E'=N, K'=2, L'=1, N'=N+N*F-O*G, O'=O+N*G+O*F, Q_1'=2, R'=B*free_41+free_38*B, S'=-B*free_37+B*free_43, T'=C*free_40-free_42*C, U'=-free_39*C-C*free_44, W'=2+W, [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 && J>=1 && K==1 && Q_1==1 && 2>=1+J ], cost: 4-K
     59: f35 -> f35 : E'=N, N'=N+N*F-O*G, O'=O+N*G+O*F, Q_1'=1+Q_1, W'=2+W, [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 && K>=1+J ], cost: 2
     60: f35 -> [11] : K'=2, L'=1, Q_1'=1, R'=B*free_41+free_38*B, S'=-B*free_37+B*free_43, T'=C*free_40-free_42*C, U'=-free_39*C-C*free_44, [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 && J>=1 && K==1 && Q_1==1 ], cost: 3-K
     61: f35 -> [12] : K'=2, L'=1, Q_1'=1, R'=B*free_41+free_38*B, S'=-B*free_37+B*free_43, T'=C*free_40-free_42*C, U'=-free_39*C-C*free_44, [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 && J>=1 && K==1 && Q_1==1 ], cost: 3-K
     54: f35 -> [14] : K'=2, L'=1, R'=free_64*B+B*free_67, S'=B*free_70-B*free_63, T'=-C*free_69+C*free_66, U'=-free_71*C-free_65*C, V'=3-free_68+P, [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 && Q_1>=2 && J>=K && Q_1>=2*free_68 && 3*free_68>=1+Q_1 && K==1 ], cost: 3-2*K
     56: f35 -> [15] : K'=2, L'=1, R'=free_64*B+B*free_67, S'=B*free_70-B*free_63, T'=-C*free_69+C*free_66, U'=-free_71*C-free_65*C, V'=3-free_68+P, [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 && Q_1>=2 && J>=K && Q_1>=2*free_68 && 3*free_68>=1+Q_1 && K==1 ], cost: 3-2*K
     57: f35 -> [16] : K'=2, L'=1, R'=free_64*B+B*free_67, S'=B*free_70-B*free_63, T'=-C*free_69+C*free_66, U'=-free_71*C-free_65*C, V'=3-free_68+P, [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 && Q_1>=2 && J>=K && Q_1>=2*free_68 && 3*free_68>=1+Q_1 && K==1 ], cost: 3-2*K

Eliminating 5 self-loops for location f35
  Self-Loop 52 has the metering function: -K+J, resulting in the new transition 62.
  Self-Loop 53 has the metering function: -K+J, resulting in the new transition 63.
  Self-Loop 55 has the metering function: -K+J, resulting in the new transition 64.
  Self-Loop 58 has the metering function: meter_4, resulting in the new transition 65.
  Self-Loop 59 has the metering function: meter_5, resulting in the new transition 66.
  Removing the self-loops: 52 53 55 58 59.

Removed all Self-loops using metering functions (where possible):
  Start location: f2
      3: f2 -> f27 : B'=free_7, C'=free_9, D'=free_11, E'=free_6, F'=free_8, G'=free_10, [ 0>=A ], cost: 1
      4: f2 -> f27 : B'=free_13, C'=free_15, D'=free_17, E'=free_12, F'=free_14, G'=free_16, [ A>=2 ], cost: 1
     39: f2 -> f27 : A'=1, B'=free_1, C'=free_3, D'=free_5, E'=free, F'=free_2, G'=free_4, Q'=1+Q, K'=1+J, L'=2-2*K+L+2*J, [ A==1 && H>=Q && J>=K && 1+Q>=1+H ], cost: 5-K+J
     40: f2 -> f27 : A'=1, B'=free_1, C'=free_3, D'=free_5, E'=free, F'=free_2, G'=free_4, [ A==1 && Q>=1+H ], cost: 2
      5: f27 -> f35 : M'=2+H-Q, N'=1, O'=0, [ 0>=Q && H>=Q ], cost: 1
      6: f27 -> f35 : M'=2+H-Q, N'=1, O'=0, [ Q>=2 && H>=Q ], cost: 1
      7: f27 -> f35 : Q'=1, M'=1, N'=1, O'=0, [ H>=1 && Q==1 ], cost: 1
     62: f35 -> [17] : E'=E, K'=J, L'=3, N'=-E*G+E+E*F, O'=E*G+E+E*F, Q_1'=Q_1-K+J, R'=B*free_49+B*free_46, S'=B*free_52-B*free_45, T'=free_48*C-free_51*C, U'=-C*free_53-C*free_47, V'=3+P-free_50, W'=-2*K+2*J+W, [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 && Q_1>=2 && K-J==0 && Q_1>=2*free_50 && 3*free_50>=1+Q_1 && 0>=K && E==N && E==O ], cost: -4*K+4*J
     63: f35 -> [17] : E'=E, K'=J, L'=3, N'=-E*G+E+E*F, O'=E*G+E+E*F, Q_1'=Q_1-K+J, R'=B*free_55+B*free_58, S'=free_61*B-free_54*B, T'=free_57*C-C*free_60, U'=-C*free_56-free_62*C, V'=3-free_59+P, W'=-2*K+2*J+W, [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 && Q_1>=2 && K-J==0 && Q_1>=2*free_59 && 3*free_59>=1+Q_1 && K>=2 && E==N && E==O ], cost: -4*K+4*J
     64: f35 -> [17] : E'=E, K'=2, L'=1, N'=-E*G+E+E*F, O'=E*G+E+E*F, Q_1'=Q_1-K+J, R'=free_64*B+B*free_67, S'=B*free_70-B*free_63, T'=-C*free_69+C*free_66, U'=-free_71*C-free_65*C, V'=3-free_68+P, W'=-2*K+2*J+W, [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 && Q_1>=2 && J>=K && Q_1>=2*free_68 && 3*free_68>=1+Q_1 && K==1 && 2>=1+J && E==N && E==O ], cost: 0
     65: f35 -> [17] : E'=E, K'=2, L'=1, N'=-E*G+E+E*F, O'=E*G+E+E*F, Q_1'=2, R'=B*free_41+free_38*B, S'=-B*free_37+B*free_43, T'=C*free_40-free_42*C, U'=-free_39*C-C*free_44, W'=2*meter_4+W, [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 && 1-J==0 && K==1 && Q_1==1 && 2*meter_4==2-Q_1-K && E==N && E==O ], cost: 2*meter_4
     66: f35 -> [17] : E'=E, N'=-E*G+E+E*F, O'=E*G+E+E*F, Q_1'=Q_1+meter_5, W'=2*meter_5+W, [ P>=-2+2*Q_1 && -3+3*Q_1>=1+P && Q_1>=Q_1 && K>=1+J && 2*meter_5==3-2*Q_1+P && E==N && E==O ], cost: 2*meter_5
     18: [17] -> f27 : Q'=1+Q, [ P>=2*free_72 && 3*free_72>=1+P && Q_1>=2+free_72 ], cost: 1
     60: [17] -> [11] : K'=2, L'=1, Q_1'=1, R'=B*free_41+free_38*B, S'=-B*free_37+B*free_43, T'=C*free_40-free_42*C, U'=-free_39*C-C*free_44, [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 && J>=1 && K==1 && Q_1==1 ], cost: 3-K
     61: [17] -> [12] : K'=2, L'=1, Q_1'=1, R'=B*free_41+free_38*B, S'=-B*free_37+B*free_43, T'=C*free_40-free_42*C, U'=-free_39*C-C*free_44, [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 && J>=1 && K==1 && Q_1==1 ], cost: 3-K
     54: [17] -> [14] : K'=2, L'=1, R'=free_64*B+B*free_67, S'=B*free_70-B*free_63, T'=-C*free_69+C*free_66, U'=-free_71*C-free_65*C, V'=3-free_68+P, [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 && Q_1>=2 && J>=K && Q_1>=2*free_68 && 3*free_68>=1+Q_1 && K==1 ], cost: 3-2*K
     56: [17] -> [15] : K'=2, L'=1, R'=free_64*B+B*free_67, S'=B*free_70-B*free_63, T'=-C*free_69+C*free_66, U'=-free_71*C-free_65*C, V'=3-free_68+P, [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 && Q_1>=2 && J>=K && Q_1>=2*free_68 && 3*free_68>=1+Q_1 && K==1 ], cost: 3-2*K
     57: [17] -> [16] : K'=2, L'=1, R'=free_64*B+B*free_67, S'=B*free_70-B*free_63, T'=-C*free_69+C*free_66, U'=-free_71*C-free_65*C, V'=3-free_68+P, [ P>=2*free_18 && 3*free_18>=1+P && 1+free_18>=Q_1 && Q_1>=2 && J>=K && Q_1>=2*free_68 && 3*free_68>=1+Q_1 && K==1 ], cost: 3-2*K


Applied chaining over branches and pruning:
  Start location: f2
     39: f2 -> f27 : A'=1, B'=free_1, C'=free_3, D'=free_5, E'=free, F'=free_2, G'=free_4, Q'=1+Q, K'=1+J, L'=2-2*K+L+2*J, [ A==1 && H>=Q && J>=K && 1+Q>=1+H ], cost: 5-K+J


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f2
     39: f2 -> f27 : A'=1, B'=free_1, C'=free_3, D'=free_5, E'=free, F'=free_2, G'=free_4, Q'=1+Q, K'=1+J, L'=2-2*K+L+2*J, [ A==1 && H>=Q && J>=K && 1+Q>=1+H ], cost: 5-K+J


Computing complexity for remaining 1 transitions.

  Found configuration with infinitely models for cost: 5-K+J
  and guard: A==1 && H>=Q && J>=K && 1+Q>=1+H:
  K: Pos, H: Const, Q: Const, J: Pos, A: Both, where: J > K

Found new complexity n^1, because: Found infinity configuration.


The final runtime is determined by this resulting transition:
  Final Guard: A==1 && H>=Q && J>=K && 1+Q>=1+H
  Final Cost:  5-K+J

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

WORST_CASE(Omega(n^1),?)