Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: f2
      0: f2 -> f5 : [], cost: 1
      1: f5 -> f8 : [ A>=B ], cost: 1
     41: f5 -> f17 : [ B>=1+A ], cost: 1
     40: f8 -> f5 : B'=1+B, [ C>=1+A ], cost: 1
      2: f8 -> f8 : C'=1+C, [ A>=C ], cost: 1
      3: f17 -> f17 : B'=1+B, D'=free, [ A>=B ], cost: 1
     39: f17 -> f27 : [ B>=1+A ], cost: 1
      4: f27 -> f31 : F'=0, [ 50>=E ], cost: 1
     38: f27 -> f1 : [ E>=51 ], cost: 1
      5: f31 -> f34 : [ A>=1+B ], cost: 1
     35: f31 -> f46 : [ B>=A && 0>=1+F ], cost: 1
     36: f31 -> f46 : [ B>=A && F>=1 ], cost: 1
     37: f31 -> f1 : F'=0, [ B>=A && F==0 ], cost: 1
     34: f34 -> f31 : B'=1+B, [ C>=1+A ], cost: 1
      6: f34 -> f34 : C'=1+C, F'=free_1+F, G'=free_1, [ A>=C ], cost: 1
      7: f46 -> f50 : H'=free_2, [ 3>=E ], cost: 1
      8: f46 -> f50 : H'=0, [ E>=4 ], cost: 1
      9: f50 -> f53 : [ A>=1+B ], cost: 1
     33: f50 -> f132 : [ B>=A ], cost: 1
     32: f53 -> f50 : B'=1+B, [ C>=1+A ], cost: 1
     11: f53 -> f53 : 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: f53 -> f69 : Q'=free_9, J'=free_7, K'=free_8, [ A>=C && 4>=E ], cost: 1
     13: f53 -> f69 : 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: f53 -> f69 : 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: f53 -> f69 : 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: f53 -> f69 : 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: f69 -> f53 : C'=1+C, [ H>=Q ], cost: 1
     17: f69 -> f80 : 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: f69 -> f80 : 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: f69 -> f92 : 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: f80 -> f92 : P'=free_49, W'=free_51, X'=free_52, Y'=free_48, Z'=free_50, [ T>=0 ], cost: 1
     21: f80 -> f92 : P'=free_61, S'=-S, W'=free_63, X'=free_64, Y'=free_60, Z'=free_62, [ 0>=1+T ], cost: 1
     22: f92 -> f92 : K'=free_65, P'=free_66, A1'=1+A1, [ B>=1+A1 ], cost: 1
     31: f92 -> f101 : [ A1>=B ], cost: 1
     23: f101 -> f101 : K'=free_67, P'=free_68, A1'=1+A1, [ C>=1+A1 ], cost: 1
     30: f101 -> f110 : [ A1>=C ], cost: 1
     24: f110 -> f110 : K'=free_69, P'=free_70, A1'=1+A1, [ A>=A1 ], cost: 1
     29: f110 -> f119 : [ A1>=1+A ], cost: 1
     28: f119 -> f53 : C'=1+C, [ A1>=1+A ], cost: 1
     25: f119 -> f119 : K'=free_71, P'=free_72, A1'=1+A1, [ A>=A1 ], cost: 1
     27: f132 -> f27 : E'=1+E, [ B>=1+A ], cost: 1
     26: f132 -> f132 : B'=1+B, [ A>=B ], cost: 1


Simplified the transitions:
  Start location: f2
      0: f2 -> f5 : [], cost: 1
      1: f5 -> f8 : [ A>=B ], cost: 1
     41: f5 -> f17 : [ B>=1+A ], cost: 1
     40: f8 -> f5 : B'=1+B, [ C>=1+A ], cost: 1
      2: f8 -> f8 : C'=1+C, [ A>=C ], cost: 1
      3: f17 -> f17 : B'=1+B, D'=free, [ A>=B ], cost: 1
     39: f17 -> f27 : [ B>=1+A ], cost: 1
      4: f27 -> f31 : F'=0, [ 50>=E ], cost: 1
      5: f31 -> f34 : [ A>=1+B ], cost: 1
     35: f31 -> f46 : [ B>=A && 0>=1+F ], cost: 1
     36: f31 -> f46 : [ B>=A && F>=1 ], cost: 1
     34: f34 -> f31 : B'=1+B, [ C>=1+A ], cost: 1
      6: f34 -> f34 : C'=1+C, F'=free_1+F, G'=free_1, [ A>=C ], cost: 1
      7: f46 -> f50 : H'=free_2, [ 3>=E ], cost: 1
      8: f46 -> f50 : H'=0, [ E>=4 ], cost: 1
      9: f50 -> f53 : [ A>=1+B ], cost: 1
     33: f50 -> f132 : [ B>=A ], cost: 1
     32: f53 -> f50 : B'=1+B, [ C>=1+A ], cost: 1
     11: f53 -> f53 : 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: f53 -> f69 : Q'=free_9, J'=free_7, K'=free_8, [ A>=C && 4>=E ], cost: 1
     13: f53 -> f69 : 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: f53 -> f69 : 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: f53 -> f69 : 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: f53 -> f69 : 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: f69 -> f53 : C'=1+C, [ H>=Q ], cost: 1
     17: f69 -> f80 : 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: f69 -> f80 : 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: f69 -> f92 : 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: f80 -> f92 : P'=free_49, W'=free_51, X'=free_52, Y'=free_48, Z'=free_50, [ T>=0 ], cost: 1
     21: f80 -> f92 : P'=free_61, S'=-S, W'=free_63, X'=free_64, Y'=free_60, Z'=free_62, [ 0>=1+T ], cost: 1
     22: f92 -> f92 : K'=free_65, P'=free_66, A1'=1+A1, [ B>=1+A1 ], cost: 1
     31: f92 -> f101 : [ A1>=B ], cost: 1
     23: f101 -> f101 : K'=free_67, P'=free_68, A1'=1+A1, [ C>=1+A1 ], cost: 1
     30: f101 -> f110 : [ A1>=C ], cost: 1
     24: f110 -> f110 : K'=free_69, P'=free_70, A1'=1+A1, [ A>=A1 ], cost: 1
     29: f110 -> f119 : [ A1>=1+A ], cost: 1
     28: f119 -> f53 : C'=1+C, [ A1>=1+A ], cost: 1
     25: f119 -> f119 : K'=free_71, P'=free_72, A1'=1+A1, [ A>=A1 ], cost: 1
     27: f132 -> f27 : E'=1+E, [ B>=1+A ], cost: 1
     26: f132 -> f132 : B'=1+B, [ A>=B ], cost: 1

Eliminating 1 self-loops for location f8
  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 f17
  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 f34
  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 f53
  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 f92
  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 f101
  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 f110
  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 f119
  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: f2
      0: f2 -> f5 : [], cost: 1
      1: f5 -> f8 : [ A>=B ], cost: 1
     41: f5 -> f17 : [ B>=1+A ], cost: 1
     42: f8 -> [18] : C'=1+A, [ A>=C ], cost: 1-C+A
     43: f17 -> [19] : B'=1+A, D'=free, [ A>=B ], cost: 1-B+A
      4: f27 -> f31 : F'=0, [ 50>=E ], cost: 1
      5: f31 -> f34 : [ A>=1+B ], cost: 1
     35: f31 -> f46 : [ B>=A && 0>=1+F ], cost: 1
     36: f31 -> f46 : [ B>=A && F>=1 ], cost: 1
     44: f34 -> [20] : C'=1+A, F'=F-free_1*(-1+C-A), G'=free_1, [ A>=C ], cost: 1-C+A
      7: f46 -> f50 : H'=free_2, [ 3>=E ], cost: 1
      8: f46 -> f50 : H'=0, [ E>=4 ], cost: 1
      9: f50 -> f53 : [ A>=1+B ], cost: 1
     33: f50 -> f132 : [ B>=A ], cost: 1
     45: f53 -> [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: f69 -> f53 : C'=1+C, [ H>=Q ], cost: 1
     17: f69 -> f80 : 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: f69 -> f80 : 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: f69 -> f92 : 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: f80 -> f92 : P'=free_49, W'=free_51, X'=free_52, Y'=free_48, Z'=free_50, [ T>=0 ], cost: 1
     21: f80 -> f92 : P'=free_61, S'=-S, W'=free_63, X'=free_64, Y'=free_60, Z'=free_62, [ 0>=1+T ], cost: 1
     46: f92 -> [22] : K'=free_65, P'=free_66, A1'=B, [ B>=1+A1 ], cost: -A1+B
     47: f101 -> [23] : K'=free_67, P'=free_68, A1'=C, [ C>=1+A1 ], cost: -A1+C
     48: f110 -> [24] : K'=free_69, P'=free_70, A1'=1+A, [ A>=A1 ], cost: 1-A1+A
     49: f119 -> [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] -> f5 : B'=1+B, [ C>=1+A ], cost: 1
     39: [19] -> f27 : [ B>=1+A ], cost: 1
     34: [20] -> f31 : B'=1+B, [ C>=1+A ], cost: 1
     32: [21] -> f50 : B'=1+B, [ C>=1+A ], cost: 1
     12: [21] -> f69 : Q'=free_9, J'=free_7, K'=free_8, [ A>=C && 4>=E ], cost: 1
     13: [21] -> f69 : 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] -> f69 : 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] -> f69 : 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] -> f69 : 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] -> f101 : [ A1>=B ], cost: 1
     30: [23] -> f110 : [ A1>=C ], cost: 1
     29: [24] -> f119 : [ A1>=1+A ], cost: 1
     28: [25] -> f53 : C'=1+C, [ A1>=1+A ], cost: 1
     27: [26] -> f27 : E'=1+E, [ B>=1+A ], cost: 1


Applied simple chaining:
  Start location: f2
      0: f2 -> f5 : [], cost: 1
      1: f5 -> f5 : B'=1+B, C'=1+A, [ A>=B && A>=C && 1+A>=1+A ], cost: 3-C+A
     41: f5 -> f17 : [ B>=1+A ], cost: 1
     43: f17 -> f27 : B'=1+A, D'=free, [ A>=B && 1+A>=1+A ], cost: 2-B+A
      4: f27 -> f31 : F'=0, [ 50>=E ], cost: 1
      5: f31 -> f31 : 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: f31 -> f46 : [ B>=A && 0>=1+F ], cost: 1
     36: f31 -> f46 : [ B>=A && F>=1 ], cost: 1
      7: f46 -> f50 : H'=free_2, [ 3>=E ], cost: 1
      8: f46 -> f50 : H'=0, [ E>=4 ], cost: 1
     33: f50 -> f27 : B'=1+A, E'=1+E, [ B>=A && A>=B && 1+A>=1+A ], cost: 3-B+A
      9: f50 -> f53 : [ A>=1+B ], cost: 1
     45: f53 -> [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: f69 -> f53 : C'=1+C, [ H>=Q ], cost: 1
     17: f69 -> f80 : 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: f69 -> f80 : 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: f69 -> f92 : 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: f80 -> f92 : P'=free_49, W'=free_51, X'=free_52, Y'=free_48, Z'=free_50, [ T>=0 ], cost: 1
     21: f80 -> f92 : P'=free_61, S'=-S, W'=free_63, X'=free_64, Y'=free_60, Z'=free_62, [ 0>=1+T ], cost: 1
     46: f92 -> f119 : 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: f119 -> f53 : C'=1+C, K'=free_71, P'=free_72, A1'=1+A, [ A>=A1 && 1+A>=1+A ], cost: 2-A1+A
     32: [21] -> f50 : B'=1+B, [ C>=1+A ], cost: 1
     12: [21] -> f69 : Q'=free_9, J'=free_7, K'=free_8, [ A>=C && 4>=E ], cost: 1
     13: [21] -> f69 : 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] -> f69 : 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] -> f69 : 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] -> f69 : 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 f5
  Removing the self-loops: 1.
Adding an epsilon transition (to model nonexecution of the loops): 52.
Eliminating 1 self-loops for location f31
  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: f2
      0: f2 -> f5 : [], cost: 1
     51: f5 -> [27] : B'=1+B, C'=1+A, [ A>=B && A>=C ], cost: 3-C+A
     52: f5 -> [27] : [], cost: 0
     43: f17 -> f27 : B'=1+A, D'=free, [ A>=B && 1+A>=1+A ], cost: 2-B+A
      4: f27 -> f31 : F'=0, [ 50>=E ], cost: 1
     53: f31 -> [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: f31 -> [28] : [], cost: 0
      7: f46 -> f50 : H'=free_2, [ 3>=E ], cost: 1
      8: f46 -> f50 : H'=0, [ E>=4 ], cost: 1
     33: f50 -> f27 : B'=1+A, E'=1+E, [ B>=A && A>=B && 1+A>=1+A ], cost: 3-B+A
      9: f50 -> f53 : [ A>=1+B ], cost: 1
     45: f53 -> [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: f69 -> f53 : C'=1+C, [ H>=Q ], cost: 1
     17: f69 -> f80 : 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: f69 -> f80 : 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: f69 -> f92 : 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: f80 -> f92 : P'=free_49, W'=free_51, X'=free_52, Y'=free_48, Z'=free_50, [ T>=0 ], cost: 1
     21: f80 -> f92 : P'=free_61, S'=-S, W'=free_63, X'=free_64, Y'=free_60, Z'=free_62, [ 0>=1+T ], cost: 1
     46: f92 -> f119 : 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: f119 -> f53 : C'=1+C, K'=free_71, P'=free_72, A1'=1+A, [ A>=A1 && 1+A>=1+A ], cost: 2-A1+A
     32: [21] -> f50 : B'=1+B, [ C>=1+A ], cost: 1
     12: [21] -> f69 : Q'=free_9, J'=free_7, K'=free_8, [ A>=C && 4>=E ], cost: 1
     13: [21] -> f69 : 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] -> f69 : 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] -> f69 : 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] -> f69 : 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] -> f17 : [ B>=1+A ], cost: 1
     35: [28] -> f46 : [ B>=A && 0>=1+F ], cost: 1
     36: [28] -> f46 : [ B>=A && F>=1 ], cost: 1


Applied chaining over branches and pruning:
  Start location: f2
     55: f2 -> [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: f2
     55: f2 -> [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),?)