Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f0
      0: f0 -> f16 : [], cost: 1
      1: f16 -> f18 : [ A>=B ], cost: 1
     41: f16 -> f26 : [ B>=1+A ], cost: 1
     40: f18 -> f16 : B'=1+B, [ C>=1+A ], cost: 1
      2: f18 -> f18 : C'=1+C, [ A>=C ], cost: 1
      3: f26 -> f26 : B'=1+B, D'=free, [ A>=B ], cost: 1
     39: f26 -> f35 : [ B>=1+A ], cost: 1
      4: f35 -> f38 : F'=0, [ 50>=E ], cost: 1
     38: f35 -> f52 : [ E>=51 ], cost: 1
      5: f38 -> f40 : [ A>=1+B ], cost: 1
     35: f38 -> f53 : [ B>=A && 0>=1+F ], cost: 1
     36: f38 -> f53 : [ B>=A && F>=1 ], cost: 1
     37: f38 -> f52 : F'=0, [ B>=A && F==0 ], cost: 1
     34: f40 -> f38 : B'=1+B, [ C>=1+A ], cost: 1
      6: f40 -> f40 : C'=1+C, F'=free_1+F, G'=free_1, [ A>=C ], cost: 1
      7: f53 -> f56 : H'=free_2, [ 3>=E ], cost: 1
      8: f53 -> f56 : H'=0, [ E>=4 ], cost: 1
      9: f56 -> f58 : [ A>=1+B ], cost: 1
     33: f56 -> f132 : [ B>=A ], cost: 1
     32: f58 -> f56 : B'=1+B, [ C>=1+A ], cost: 1
     11: f58 -> f58 : C'=1+C, J'=free_4, K'=free_5, L'=free_6, M'=free_5+free_6, N'=free_3, O'=free_5+free_3, [ A>=C && E>=5 ], cost: 1
     12: f58 -> f74 : Q'=free_9, J'=free_7, K'=free_8, [ A>=C && 4>=E ], cost: 1
     13: f58 -> f74 : Q'=free_14, J'=free_11, K'=free_13, L'=free_15, M'=free_15+free_13, N'=free_10, O'=free_12, [ E>=5 && A>=C && free_12>=1+free_13+free_10 ], cost: 1
     14: f58 -> f74 : Q'=free_20, J'=free_17, K'=free_19, L'=free_21, M'=free_21+free_19, N'=free_16, O'=free_18, [ E>=5 && A>=C && free_19+free_16>=1+free_18 ], cost: 1
     15: f58 -> f74 : Q'=free_24, J'=free_23, K'=free_25, L'=free_26, M'=free_22, [ E>=5 && A>=C && free_22>=1+free_26+free_25 ], cost: 1
     16: f58 -> f74 : Q'=free_29, J'=free_28, K'=free_30, L'=free_31, M'=free_27, [ E>=5 && A>=C && free_30+free_31>=1+free_27 ], cost: 1
     10: f74 -> f58 : C'=1+C, [ H>=Q ], cost: 1
     17: f74 -> f85 : P'=-free_37+free_34, Q_1'=free_39, R'=free_33, S'=free_36, T'=free_38, U'=free_32, V'=free_35, [ Q>=1+H && free_33>=1+K+free_39 ], cost: 1
     18: f74 -> f85 : P'=-free_45+free_42, Q_1'=free_47, R'=free_41, S'=free_44, T'=free_46, U'=free_40, V'=free_43, [ Q>=1+H && K+free_47>=1+free_41 ], cost: 1
     20: f74 -> f96 : P'=free_55, Q_1'=free_57, R'=K+free_57, S'=free_59, W'=free_54, X'=free_56, Y'=free_58, Z'=free_53, [ Q>=1+H ], cost: 1
     19: f85 -> f96 : P'=free_49, W'=free_51, X'=free_52, Y'=free_48, Z'=free_50, [ T>=0 ], cost: 1
     21: f85 -> f96 : P'=free_61, S'=-S, W'=free_63, X'=free_64, Y'=free_60, Z'=free_62, [ 0>=1+T ], cost: 1
     22: f96 -> f96 : K'=free_65, P'=free_66, A1'=1+A1, [ B>=1+A1 ], cost: 1
     31: f96 -> f104 : [ A1>=B ], cost: 1
     23: f104 -> f104 : K'=free_67, P'=free_68, A1'=1+A1, [ C>=1+A1 ], cost: 1
     30: f104 -> f112 : [ A1>=C ], cost: 1
     24: f112 -> f112 : K'=free_69, P'=free_70, A1'=1+A1, [ A>=A1 ], cost: 1
     29: f112 -> f120 : [ A1>=1+A ], cost: 1
     28: f120 -> f58 : C'=1+C, [ A1>=1+A ], cost: 1
     25: f120 -> f120 : K'=free_71, P'=free_72, A1'=1+A1, [ A>=A1 ], cost: 1
     27: f132 -> f35 : E'=1+E, [ B>=1+A ], cost: 1
     26: f132 -> f132 : B'=1+B, [ A>=B ], cost: 1


Simplified the transitions:
  Start location: f0
      0: f0 -> f16 : [], cost: 1
      1: f16 -> f18 : [ A>=B ], cost: 1
     41: f16 -> f26 : [ B>=1+A ], cost: 1
     40: f18 -> f16 : B'=1+B, [ C>=1+A ], cost: 1
      2: f18 -> f18 : C'=1+C, [ A>=C ], cost: 1
      3: f26 -> f26 : B'=1+B, D'=free, [ A>=B ], cost: 1
     39: f26 -> f35 : [ B>=1+A ], cost: 1
      4: f35 -> f38 : F'=0, [ 50>=E ], cost: 1
      5: f38 -> f40 : [ A>=1+B ], cost: 1
     35: f38 -> f53 : [ B>=A && 0>=1+F ], cost: 1
     36: f38 -> f53 : [ B>=A && F>=1 ], cost: 1
     34: f40 -> f38 : B'=1+B, [ C>=1+A ], cost: 1
      6: f40 -> f40 : C'=1+C, F'=free_1+F, G'=free_1, [ A>=C ], cost: 1
      7: f53 -> f56 : H'=free_2, [ 3>=E ], cost: 1
      8: f53 -> f56 : H'=0, [ E>=4 ], cost: 1
      9: f56 -> f58 : [ A>=1+B ], cost: 1
     33: f56 -> f132 : [ B>=A ], cost: 1
     32: f58 -> f56 : B'=1+B, [ C>=1+A ], cost: 1
     11: f58 -> f58 : C'=1+C, J'=free_4, K'=free_5, L'=free_6, M'=free_5+free_6, N'=free_3, O'=free_5+free_3, [ A>=C && E>=5 ], cost: 1
     12: f58 -> f74 : Q'=free_9, J'=free_7, K'=free_8, [ A>=C && 4>=E ], cost: 1
     13: f58 -> f74 : Q'=free_14, J'=free_11, K'=free_13, L'=free_15, M'=free_15+free_13, N'=free_10, O'=free_12, [ E>=5 && A>=C && free_12>=1+free_13+free_10 ], cost: 1
     14: f58 -> f74 : Q'=free_20, J'=free_17, K'=free_19, L'=free_21, M'=free_21+free_19, N'=free_16, O'=free_18, [ E>=5 && A>=C && free_19+free_16>=1+free_18 ], cost: 1
     15: f58 -> f74 : Q'=free_24, J'=free_23, K'=free_25, L'=free_26, M'=free_22, [ E>=5 && A>=C && free_22>=1+free_26+free_25 ], cost: 1
     16: f58 -> f74 : Q'=free_29, J'=free_28, K'=free_30, L'=free_31, M'=free_27, [ E>=5 && A>=C && free_30+free_31>=1+free_27 ], cost: 1
     10: f74 -> f58 : C'=1+C, [ H>=Q ], cost: 1
     17: f74 -> f85 : P'=-free_37+free_34, Q_1'=free_39, R'=free_33, S'=free_36, T'=free_38, U'=free_32, V'=free_35, [ Q>=1+H && free_33>=1+K+free_39 ], cost: 1
     18: f74 -> f85 : P'=-free_45+free_42, Q_1'=free_47, R'=free_41, S'=free_44, T'=free_46, U'=free_40, V'=free_43, [ Q>=1+H && K+free_47>=1+free_41 ], cost: 1
     20: f74 -> f96 : P'=free_55, Q_1'=free_57, R'=K+free_57, S'=free_59, W'=free_54, X'=free_56, Y'=free_58, Z'=free_53, [ Q>=1+H ], cost: 1
     19: f85 -> f96 : P'=free_49, W'=free_51, X'=free_52, Y'=free_48, Z'=free_50, [ T>=0 ], cost: 1
     21: f85 -> f96 : P'=free_61, S'=-S, W'=free_63, X'=free_64, Y'=free_60, Z'=free_62, [ 0>=1+T ], cost: 1
     22: f96 -> f96 : K'=free_65, P'=free_66, A1'=1+A1, [ B>=1+A1 ], cost: 1
     31: f96 -> f104 : [ A1>=B ], cost: 1
     23: f104 -> f104 : K'=free_67, P'=free_68, A1'=1+A1, [ C>=1+A1 ], cost: 1
     30: f104 -> f112 : [ A1>=C ], cost: 1
     24: f112 -> f112 : K'=free_69, P'=free_70, A1'=1+A1, [ A>=A1 ], cost: 1
     29: f112 -> f120 : [ A1>=1+A ], cost: 1
     28: f120 -> f58 : C'=1+C, [ A1>=1+A ], cost: 1
     25: f120 -> f120 : K'=free_71, P'=free_72, A1'=1+A1, [ A>=A1 ], cost: 1
     27: f132 -> f35 : E'=1+E, [ B>=1+A ], cost: 1
     26: f132 -> f132 : B'=1+B, [ A>=B ], cost: 1

Eliminating 1 self-loops for location f18
  Self-Loop 2 has the metering function: 1-C+A, resulting in the new transition 42.
  Removing the self-loops: 2.
Eliminating 1 self-loops for location f26
  Self-Loop 3 has the metering function: 1-B+A, resulting in the new transition 43.
  Removing the self-loops: 3.
Eliminating 1 self-loops for location f40
  Self-Loop 6 has the metering function: 1-C+A, resulting in the new transition 44.
  Removing the self-loops: 6.
Eliminating 1 self-loops for location f58
  Self-Loop 11 has the metering function: 1-C+A, resulting in the new transition 45.
  Removing the self-loops: 11.
Eliminating 1 self-loops for location f96
  Self-Loop 22 has the metering function: -A1+B, resulting in the new transition 46.
  Removing the self-loops: 22.
Eliminating 1 self-loops for location f104
  Self-Loop 23 has the metering function: -A1+C, resulting in the new transition 47.
  Removing the self-loops: 23.
Eliminating 1 self-loops for location f112
  Self-Loop 24 has the metering function: 1-A1+A, resulting in the new transition 48.
  Removing the self-loops: 24.
Eliminating 1 self-loops for location f120
  Self-Loop 25 has the metering function: 1-A1+A, resulting in the new transition 49.
  Removing the self-loops: 25.
Eliminating 1 self-loops for location f132
  Self-Loop 26 has the metering function: 1-B+A, resulting in the new transition 50.
  Removing the self-loops: 26.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f16 : [], cost: 1
      1: f16 -> f18 : [ A>=B ], cost: 1
     41: f16 -> f26 : [ B>=1+A ], cost: 1
     42: f18 -> [18] : C'=1+A, [ A>=C ], cost: 1-C+A
     43: f26 -> [19] : B'=1+A, D'=free, [ A>=B ], cost: 1-B+A
      4: f35 -> f38 : F'=0, [ 50>=E ], cost: 1
      5: f38 -> f40 : [ A>=1+B ], cost: 1
     35: f38 -> f53 : [ B>=A && 0>=1+F ], cost: 1
     36: f38 -> f53 : [ B>=A && F>=1 ], cost: 1
     44: f40 -> [20] : C'=1+A, F'=F-free_1*(-1+C-A), G'=free_1, [ A>=C ], cost: 1-C+A
      7: f53 -> f56 : H'=free_2, [ 3>=E ], cost: 1
      8: f53 -> f56 : H'=0, [ E>=4 ], cost: 1
      9: f56 -> f58 : [ A>=1+B ], cost: 1
     33: f56 -> f132 : [ B>=A ], cost: 1
     45: f58 -> [21] : C'=1+A, J'=free_4, K'=free_5, L'=free_6, M'=free_5+free_6, N'=free_3, O'=free_5+free_3, [ A>=C && E>=5 ], cost: 1-C+A
     10: f74 -> f58 : C'=1+C, [ H>=Q ], cost: 1
     17: f74 -> f85 : P'=-free_37+free_34, Q_1'=free_39, R'=free_33, S'=free_36, T'=free_38, U'=free_32, V'=free_35, [ Q>=1+H && free_33>=1+K+free_39 ], cost: 1
     18: f74 -> f85 : P'=-free_45+free_42, Q_1'=free_47, R'=free_41, S'=free_44, T'=free_46, U'=free_40, V'=free_43, [ Q>=1+H && K+free_47>=1+free_41 ], cost: 1
     20: f74 -> f96 : P'=free_55, Q_1'=free_57, R'=K+free_57, S'=free_59, W'=free_54, X'=free_56, Y'=free_58, Z'=free_53, [ Q>=1+H ], cost: 1
     19: f85 -> f96 : P'=free_49, W'=free_51, X'=free_52, Y'=free_48, Z'=free_50, [ T>=0 ], cost: 1
     21: f85 -> f96 : P'=free_61, S'=-S, W'=free_63, X'=free_64, Y'=free_60, Z'=free_62, [ 0>=1+T ], cost: 1
     46: f96 -> [22] : K'=free_65, P'=free_66, A1'=B, [ B>=1+A1 ], cost: -A1+B
     47: f104 -> [23] : K'=free_67, P'=free_68, A1'=C, [ C>=1+A1 ], cost: -A1+C
     48: f112 -> [24] : K'=free_69, P'=free_70, A1'=1+A, [ A>=A1 ], cost: 1-A1+A
     49: f120 -> [25] : K'=free_71, P'=free_72, A1'=1+A, [ A>=A1 ], cost: 1-A1+A
     50: f132 -> [26] : B'=1+A, [ A>=B ], cost: 1-B+A
     40: [18] -> f16 : B'=1+B, [ C>=1+A ], cost: 1
     39: [19] -> f35 : [ B>=1+A ], cost: 1
     34: [20] -> f38 : B'=1+B, [ C>=1+A ], cost: 1
     32: [21] -> f56 : B'=1+B, [ C>=1+A ], cost: 1
     12: [21] -> f74 : Q'=free_9, J'=free_7, K'=free_8, [ A>=C && 4>=E ], cost: 1
     13: [21] -> f74 : Q'=free_14, J'=free_11, K'=free_13, L'=free_15, M'=free_15+free_13, N'=free_10, O'=free_12, [ E>=5 && A>=C && free_12>=1+free_13+free_10 ], cost: 1
     14: [21] -> f74 : Q'=free_20, J'=free_17, K'=free_19, L'=free_21, M'=free_21+free_19, N'=free_16, O'=free_18, [ E>=5 && A>=C && free_19+free_16>=1+free_18 ], cost: 1
     15: [21] -> f74 : Q'=free_24, J'=free_23, K'=free_25, L'=free_26, M'=free_22, [ E>=5 && A>=C && free_22>=1+free_26+free_25 ], cost: 1
     16: [21] -> f74 : Q'=free_29, J'=free_28, K'=free_30, L'=free_31, M'=free_27, [ E>=5 && A>=C && free_30+free_31>=1+free_27 ], cost: 1
     31: [22] -> f104 : [ A1>=B ], cost: 1
     30: [23] -> f112 : [ A1>=C ], cost: 1
     29: [24] -> f120 : [ A1>=1+A ], cost: 1
     28: [25] -> f58 : C'=1+C, [ A1>=1+A ], cost: 1
     27: [26] -> f35 : E'=1+E, [ B>=1+A ], cost: 1


Applied simple chaining:
  Start location: f0
      0: f0 -> f16 : [], cost: 1
      1: f16 -> f16 : B'=1+B, C'=1+A, [ A>=B && A>=C && 1+A>=1+A ], cost: 3-C+A
     41: f16 -> f26 : [ B>=1+A ], cost: 1
     43: f26 -> f35 : B'=1+A, D'=free, [ A>=B && 1+A>=1+A ], cost: 2-B+A
      4: f35 -> f38 : F'=0, [ 50>=E ], cost: 1
      5: f38 -> f38 : B'=1+B, C'=1+A, F'=F-free_1*(-1+C-A), G'=free_1, [ A>=1+B && A>=C && 1+A>=1+A ], cost: 3-C+A
     35: f38 -> f53 : [ B>=A && 0>=1+F ], cost: 1
     36: f38 -> f53 : [ B>=A && F>=1 ], cost: 1
      7: f53 -> f56 : H'=free_2, [ 3>=E ], cost: 1
      8: f53 -> f56 : H'=0, [ E>=4 ], cost: 1
     33: f56 -> f35 : B'=1+A, E'=1+E, [ B>=A && A>=B && 1+A>=1+A ], cost: 3-B+A
      9: f56 -> f58 : [ A>=1+B ], cost: 1
     45: f58 -> [21] : C'=1+A, J'=free_4, K'=free_5, L'=free_6, M'=free_5+free_6, N'=free_3, O'=free_5+free_3, [ A>=C && E>=5 ], cost: 1-C+A
     10: f74 -> f58 : C'=1+C, [ H>=Q ], cost: 1
     17: f74 -> f85 : P'=-free_37+free_34, Q_1'=free_39, R'=free_33, S'=free_36, T'=free_38, U'=free_32, V'=free_35, [ Q>=1+H && free_33>=1+K+free_39 ], cost: 1
     18: f74 -> f85 : P'=-free_45+free_42, Q_1'=free_47, R'=free_41, S'=free_44, T'=free_46, U'=free_40, V'=free_43, [ Q>=1+H && K+free_47>=1+free_41 ], cost: 1
     20: f74 -> f96 : P'=free_55, Q_1'=free_57, R'=K+free_57, S'=free_59, W'=free_54, X'=free_56, Y'=free_58, Z'=free_53, [ Q>=1+H ], cost: 1
     19: f85 -> f96 : P'=free_49, W'=free_51, X'=free_52, Y'=free_48, Z'=free_50, [ T>=0 ], cost: 1
     21: f85 -> f96 : P'=free_61, S'=-S, W'=free_63, X'=free_64, Y'=free_60, Z'=free_62, [ 0>=1+T ], cost: 1
     46: f96 -> f120 : K'=free_69, P'=free_70, A1'=1+A, [ B>=1+A1 && B>=B && C>=1+B && C>=C && A>=C && 1+A>=1+A ], cost: 4-A1+A
     49: f120 -> f58 : C'=1+C, K'=free_71, P'=free_72, A1'=1+A, [ A>=A1 && 1+A>=1+A ], cost: 2-A1+A
     32: [21] -> f56 : B'=1+B, [ C>=1+A ], cost: 1
     12: [21] -> f74 : Q'=free_9, J'=free_7, K'=free_8, [ A>=C && 4>=E ], cost: 1
     13: [21] -> f74 : Q'=free_14, J'=free_11, K'=free_13, L'=free_15, M'=free_15+free_13, N'=free_10, O'=free_12, [ E>=5 && A>=C && free_12>=1+free_13+free_10 ], cost: 1
     14: [21] -> f74 : Q'=free_20, J'=free_17, K'=free_19, L'=free_21, M'=free_21+free_19, N'=free_16, O'=free_18, [ E>=5 && A>=C && free_19+free_16>=1+free_18 ], cost: 1
     15: [21] -> f74 : Q'=free_24, J'=free_23, K'=free_25, L'=free_26, M'=free_22, [ E>=5 && A>=C && free_22>=1+free_26+free_25 ], cost: 1
     16: [21] -> f74 : Q'=free_29, J'=free_28, K'=free_30, L'=free_31, M'=free_27, [ E>=5 && A>=C && free_30+free_31>=1+free_27 ], cost: 1

Eliminating 1 self-loops for location f16
  Removing the self-loops: 1.
Adding an epsilon transition (to model nonexecution of the loops): 52.
Eliminating 1 self-loops for location f38
  Removing the self-loops: 5.
Adding an epsilon transition (to model nonexecution of the loops): 54.

Removed all Self-loops using metering functions (where possible):
  Start location: f0
      0: f0 -> f16 : [], cost: 1
     51: f16 -> [27] : B'=1+B, C'=1+A, [ A>=B && A>=C ], cost: 3-C+A
     52: f16 -> [27] : [], cost: 0
     43: f26 -> f35 : B'=1+A, D'=free, [ A>=B && 1+A>=1+A ], cost: 2-B+A
      4: f35 -> f38 : F'=0, [ 50>=E ], cost: 1
     53: f38 -> [28] : B'=1+B, C'=1+A, F'=F-free_1*(-1+C-A), G'=free_1, [ A>=1+B && A>=C ], cost: 3-C+A
     54: f38 -> [28] : [], cost: 0
      7: f53 -> f56 : H'=free_2, [ 3>=E ], cost: 1
      8: f53 -> f56 : H'=0, [ E>=4 ], cost: 1
     33: f56 -> f35 : B'=1+A, E'=1+E, [ B>=A && A>=B && 1+A>=1+A ], cost: 3-B+A
      9: f56 -> f58 : [ A>=1+B ], cost: 1
     45: f58 -> [21] : C'=1+A, J'=free_4, K'=free_5, L'=free_6, M'=free_5+free_6, N'=free_3, O'=free_5+free_3, [ A>=C && E>=5 ], cost: 1-C+A
     10: f74 -> f58 : C'=1+C, [ H>=Q ], cost: 1
     17: f74 -> f85 : P'=-free_37+free_34, Q_1'=free_39, R'=free_33, S'=free_36, T'=free_38, U'=free_32, V'=free_35, [ Q>=1+H && free_33>=1+K+free_39 ], cost: 1
     18: f74 -> f85 : P'=-free_45+free_42, Q_1'=free_47, R'=free_41, S'=free_44, T'=free_46, U'=free_40, V'=free_43, [ Q>=1+H && K+free_47>=1+free_41 ], cost: 1
     20: f74 -> f96 : P'=free_55, Q_1'=free_57, R'=K+free_57, S'=free_59, W'=free_54, X'=free_56, Y'=free_58, Z'=free_53, [ Q>=1+H ], cost: 1
     19: f85 -> f96 : P'=free_49, W'=free_51, X'=free_52, Y'=free_48, Z'=free_50, [ T>=0 ], cost: 1
     21: f85 -> f96 : P'=free_61, S'=-S, W'=free_63, X'=free_64, Y'=free_60, Z'=free_62, [ 0>=1+T ], cost: 1
     46: f96 -> f120 : K'=free_69, P'=free_70, A1'=1+A, [ B>=1+A1 && B>=B && C>=1+B && C>=C && A>=C && 1+A>=1+A ], cost: 4-A1+A
     49: f120 -> f58 : C'=1+C, K'=free_71, P'=free_72, A1'=1+A, [ A>=A1 && 1+A>=1+A ], cost: 2-A1+A
     32: [21] -> f56 : B'=1+B, [ C>=1+A ], cost: 1
     12: [21] -> f74 : Q'=free_9, J'=free_7, K'=free_8, [ A>=C && 4>=E ], cost: 1
     13: [21] -> f74 : Q'=free_14, J'=free_11, K'=free_13, L'=free_15, M'=free_15+free_13, N'=free_10, O'=free_12, [ E>=5 && A>=C && free_12>=1+free_13+free_10 ], cost: 1
     14: [21] -> f74 : Q'=free_20, J'=free_17, K'=free_19, L'=free_21, M'=free_21+free_19, N'=free_16, O'=free_18, [ E>=5 && A>=C && free_19+free_16>=1+free_18 ], cost: 1
     15: [21] -> f74 : Q'=free_24, J'=free_23, K'=free_25, L'=free_26, M'=free_22, [ E>=5 && A>=C && free_22>=1+free_26+free_25 ], cost: 1
     16: [21] -> f74 : Q'=free_29, J'=free_28, K'=free_30, L'=free_31, M'=free_27, [ E>=5 && A>=C && free_30+free_31>=1+free_27 ], cost: 1
     41: [27] -> f26 : [ B>=1+A ], cost: 1
     35: [28] -> f53 : [ B>=A && 0>=1+F ], cost: 1
     36: [28] -> f53 : [ B>=A && F>=1 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f0
     55: f0 -> [27] : B'=1+B, C'=1+A, [ A>=B && A>=C ], cost: 4-C+A


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: f0
     55: f0 -> [27] : B'=1+B, C'=1+A, [ A>=B && A>=C ], cost: 4-C+A


Computing complexity for remaining 1 transitions.

  Found configuration with infinitely models for cost: 4-C+A
  and guard: A>=B && A>=C:
  B: Pos, C: Pos, A: Pos, where: A > B A > C

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


The final runtime is determined by this resulting transition:
  Final Guard: A>=B && A>=C
  Final Cost:  4-C+A

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),?)