Trying to load file: main.koat

Initial Control flow graph problem:
  Start location: start
      0: f2 -> f2 : B'=1+B, [ A>=B ], cost: 1
     28: f2 -> f10 : [ B>=1+A ], cost: 1
      1: f75 -> f15 : [ C>=1+D ], cost: 1
      2: f75 -> f15 : [ D>=1+C ], cost: 1
     25: f75 -> f10 : C'=1+C, D'=C, [ C==D ], cost: 1
      6: f15 -> f15 : D'=1+D, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, [ 0>=1+free_2 && A>=1+D ], cost: 1
      7: f15 -> f15 : D'=1+D, F'=free_6, G'=free_7, H'=free_7+free_6, Q'=free_5, [ free_5>=1 && A>=1+D ], cost: 1
      4: f15 -> f24 : [ D>=A ], cost: 1
      5: f15 -> f24 : F'=free, G'=free_1, H'=free_1+free, Q'=0, [ A>=1+D ], cost: 1
      3: f10 -> f15 : E'=0, [ A>=C ], cost: 1
     27: f10 -> f1 : [ C>=1+A ], cost: 1
      8: f24 -> f75 : D'=C, [ C==D ], cost: 1
      9: f24 -> f28 : E'=1+E, J'=E, [ C>=1+D ], cost: 1
     10: f24 -> f28 : E'=1+E, J'=E, [ D>=1+C ], cost: 1
     11: f28 -> f32 : K'=free_8, L'=free_9, [ 29>=J ], cost: 1
     12: f28 -> f32 : K'=free_10, L'=free_11, [ J>=31 ], cost: 1
     13: f28 -> f32 : J'=30, K'=free_12, L'=free_13, [ J==30 ], cost: 1
     14: f32 -> f42 : K'=free_14, M'=free_15, N'=free_15, O'=1, P'=1, Q_1'=0, [ K>=0 ], cost: 1
     15: f32 -> f42 : K'=free_16, N'=-free_17, O'=1, P'=1, Q_1'=0, R'=free_17, [ 0>=1+K ], cost: 1
     16: f42 -> f68 : [ C>=1+B ], cost: 1
     17: f42 -> f68 : L'=0, S'=free_18, T'=free_19, [ B>=C ], cost: 1
     18: f42 -> f60 : K'=free_23, L'=free_26, O'=free_21, P'=free_25, Q_1'=free_20, S'=free_22, T'=free_24, [ B>=C && 0>=1+free_27 ], cost: 1
     19: f42 -> f60 : K'=free_31, L'=free_34, O'=free_29, P'=free_33, Q_1'=free_28, S'=free_30, T'=free_32, [ B>=C && free_35>=1 ], cost: 1
     21: f68 -> f75 : L'=0, [ B>=C && L==0 ], cost: 1
     22: f68 -> f75 : [ 0>=1+L ], cost: 1
     23: f68 -> f75 : [ L>=1 ], cost: 1
     24: f68 -> f75 : L'=0, [ C>=1+B && L==0 ], cost: 1
     26: f60 -> f42 : B'=-1+B, [ U>=1+A ], cost: 1
     20: f60 -> f60 : S'=free_36, U'=1+U, [ A>=U ], cost: 1
     29: start -> f2 : [], cost: 1


Simplified the transitions:
  Start location: start
      0: f2 -> f2 : B'=1+B, [ A>=B ], cost: 1
     28: f2 -> f10 : [ B>=1+A ], cost: 1
      1: f75 -> f15 : [ C>=1+D ], cost: 1
      2: f75 -> f15 : [ D>=1+C ], cost: 1
     25: f75 -> f10 : C'=1+C, D'=C, [ C==D ], cost: 1
      6: f15 -> f15 : D'=1+D, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, [ 0>=1+free_2 && A>=1+D ], cost: 1
      7: f15 -> f15 : D'=1+D, F'=free_6, G'=free_7, H'=free_7+free_6, Q'=free_5, [ free_5>=1 && A>=1+D ], cost: 1
      4: f15 -> f24 : [ D>=A ], cost: 1
      5: f15 -> f24 : F'=free, G'=free_1, H'=free_1+free, Q'=0, [ A>=1+D ], cost: 1
      3: f10 -> f15 : E'=0, [ A>=C ], cost: 1
      8: f24 -> f75 : D'=C, [ C==D ], cost: 1
      9: f24 -> f28 : E'=1+E, J'=E, [ C>=1+D ], cost: 1
     10: f24 -> f28 : E'=1+E, J'=E, [ D>=1+C ], cost: 1
     11: f28 -> f32 : K'=free_8, L'=free_9, [ 29>=J ], cost: 1
     12: f28 -> f32 : K'=free_10, L'=free_11, [ J>=31 ], cost: 1
     13: f28 -> f32 : J'=30, K'=free_12, L'=free_13, [ J==30 ], cost: 1
     14: f32 -> f42 : K'=free_14, M'=free_15, N'=free_15, O'=1, P'=1, Q_1'=0, [ K>=0 ], cost: 1
     15: f32 -> f42 : K'=free_16, N'=-free_17, O'=1, P'=1, Q_1'=0, R'=free_17, [ 0>=1+K ], cost: 1
     16: f42 -> f68 : [ C>=1+B ], cost: 1
     17: f42 -> f68 : L'=0, S'=free_18, T'=free_19, [ B>=C ], cost: 1
     18: f42 -> f60 : K'=free_23, L'=free_26, O'=free_21, P'=free_25, Q_1'=free_20, S'=free_22, T'=free_24, [ B>=C ], cost: 1
     19: f42 -> f60 : K'=free_31, L'=free_34, O'=free_29, P'=free_33, Q_1'=free_28, S'=free_30, T'=free_32, [ B>=C ], cost: 1
     21: f68 -> f75 : L'=0, [ B>=C && L==0 ], cost: 1
     22: f68 -> f75 : [ 0>=1+L ], cost: 1
     23: f68 -> f75 : [ L>=1 ], cost: 1
     24: f68 -> f75 : L'=0, [ C>=1+B && L==0 ], cost: 1
     26: f60 -> f42 : B'=-1+B, [ U>=1+A ], cost: 1
     20: f60 -> f60 : S'=free_36, U'=1+U, [ A>=U ], cost: 1
     29: start -> f2 : [], cost: 1

Eliminating 1 self-loops for location f2
  Self-Loop 0 has the metering function: 1-B+A, resulting in the new transition 30.
  Removing the self-loops: 0.
Eliminating 2 self-loops for location f15
  Self-Loop 6 has the metering function: -D+A, resulting in the new transition 31.
  Self-Loop 7 has the metering function: -D+A, resulting in the new transition 32.
  Removing the self-loops: 6 7.
Eliminating 1 self-loops for location f60
  Self-Loop 20 has the metering function: 1-U+A, resulting in the new transition 33.
  Removing the self-loops: 20.

Removed all Self-loops using metering functions (where possible):
  Start location: start
     30: f2 -> [12] : B'=1+A, [ A>=B ], cost: 1-B+A
      1: f75 -> f15 : [ C>=1+D ], cost: 1
      2: f75 -> f15 : [ D>=1+C ], cost: 1
     25: f75 -> f10 : C'=1+C, D'=C, [ C==D ], cost: 1
     31: f15 -> [13] : D'=A, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, [ 0>=1+free_2 && A>=1+D ], cost: -D+A
     32: f15 -> [13] : D'=A, F'=free_6, G'=free_7, H'=free_7+free_6, Q'=free_5, [ free_5>=1 && A>=1+D ], cost: -D+A
      3: f10 -> f15 : E'=0, [ A>=C ], cost: 1
      8: f24 -> f75 : D'=C, [ C==D ], cost: 1
      9: f24 -> f28 : E'=1+E, J'=E, [ C>=1+D ], cost: 1
     10: f24 -> f28 : E'=1+E, J'=E, [ D>=1+C ], cost: 1
     11: f28 -> f32 : K'=free_8, L'=free_9, [ 29>=J ], cost: 1
     12: f28 -> f32 : K'=free_10, L'=free_11, [ J>=31 ], cost: 1
     13: f28 -> f32 : J'=30, K'=free_12, L'=free_13, [ J==30 ], cost: 1
     14: f32 -> f42 : K'=free_14, M'=free_15, N'=free_15, O'=1, P'=1, Q_1'=0, [ K>=0 ], cost: 1
     15: f32 -> f42 : K'=free_16, N'=-free_17, O'=1, P'=1, Q_1'=0, R'=free_17, [ 0>=1+K ], cost: 1
     16: f42 -> f68 : [ C>=1+B ], cost: 1
     17: f42 -> f68 : L'=0, S'=free_18, T'=free_19, [ B>=C ], cost: 1
     18: f42 -> f60 : K'=free_23, L'=free_26, O'=free_21, P'=free_25, Q_1'=free_20, S'=free_22, T'=free_24, [ B>=C ], cost: 1
     19: f42 -> f60 : K'=free_31, L'=free_34, O'=free_29, P'=free_33, Q_1'=free_28, S'=free_30, T'=free_32, [ B>=C ], cost: 1
     21: f68 -> f75 : L'=0, [ B>=C && L==0 ], cost: 1
     22: f68 -> f75 : [ 0>=1+L ], cost: 1
     23: f68 -> f75 : [ L>=1 ], cost: 1
     24: f68 -> f75 : L'=0, [ C>=1+B && L==0 ], cost: 1
     33: f60 -> [14] : S'=free_36, U'=1+A, [ A>=U ], cost: 1-U+A
     29: start -> f2 : [], cost: 1
     28: [12] -> f10 : [ B>=1+A ], cost: 1
      4: [13] -> f24 : [ D>=A ], cost: 1
      5: [13] -> f24 : F'=free, G'=free_1, H'=free_1+free, Q'=0, [ A>=1+D ], cost: 1
     26: [14] -> f42 : B'=-1+B, [ U>=1+A ], cost: 1


Applied simple chaining:
  Start location: start
      1: f75 -> f15 : [ C>=1+D ], cost: 1
      2: f75 -> f15 : [ D>=1+C ], cost: 1
     25: f75 -> f10 : C'=1+C, D'=C, [ C==D ], cost: 1
     31: f15 -> [13] : D'=A, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, [ 0>=1+free_2 && A>=1+D ], cost: -D+A
     32: f15 -> [13] : D'=A, F'=free_6, G'=free_7, H'=free_7+free_6, Q'=free_5, [ free_5>=1 && A>=1+D ], cost: -D+A
      3: f10 -> f15 : E'=0, [ A>=C ], cost: 1
      8: f24 -> f75 : D'=C, [ C==D ], cost: 1
      9: f24 -> f28 : E'=1+E, J'=E, [ C>=1+D ], cost: 1
     10: f24 -> f28 : E'=1+E, J'=E, [ D>=1+C ], cost: 1
     11: f28 -> f32 : K'=free_8, L'=free_9, [ 29>=J ], cost: 1
     12: f28 -> f32 : K'=free_10, L'=free_11, [ J>=31 ], cost: 1
     13: f28 -> f32 : J'=30, K'=free_12, L'=free_13, [ J==30 ], cost: 1
     14: f32 -> f42 : K'=free_14, M'=free_15, N'=free_15, O'=1, P'=1, Q_1'=0, [ K>=0 ], cost: 1
     15: f32 -> f42 : K'=free_16, N'=-free_17, O'=1, P'=1, Q_1'=0, R'=free_17, [ 0>=1+K ], cost: 1
     16: f42 -> f68 : [ C>=1+B ], cost: 1
     17: f42 -> f68 : L'=0, S'=free_18, T'=free_19, [ B>=C ], cost: 1
     18: f42 -> f60 : K'=free_23, L'=free_26, O'=free_21, P'=free_25, Q_1'=free_20, S'=free_22, T'=free_24, [ B>=C ], cost: 1
     19: f42 -> f60 : K'=free_31, L'=free_34, O'=free_29, P'=free_33, Q_1'=free_28, S'=free_30, T'=free_32, [ B>=C ], cost: 1
     21: f68 -> f75 : L'=0, [ B>=C && L==0 ], cost: 1
     22: f68 -> f75 : [ 0>=1+L ], cost: 1
     23: f68 -> f75 : [ L>=1 ], cost: 1
     24: f68 -> f75 : L'=0, [ C>=1+B && L==0 ], cost: 1
     33: f60 -> f42 : B'=-1+B, S'=free_36, U'=1+A, [ A>=U && 1+A>=1+A ], cost: 2-U+A
     29: start -> f10 : B'=1+A, [ A>=B && 1+A>=1+A ], cost: 3-B+A
      4: [13] -> f24 : [ D>=A ], cost: 1
      5: [13] -> f24 : F'=free, G'=free_1, H'=free_1+free, Q'=0, [ A>=1+D ], cost: 1


Applied chaining over branches and pruning:
  Start location: start
      1: f75 -> f15 : [ C>=1+D ], cost: 1
      2: f75 -> f15 : [ D>=1+C ], cost: 1
     25: f75 -> f10 : C'=1+C, D'=C, [ C==D ], cost: 1
     34: f15 -> f24 : D'=A, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, [ 0>=1+free_2 && A>=1+D && A>=A ], cost: 1-D+A
     36: f15 -> f24 : D'=A, F'=free_6, G'=free_7, H'=free_7+free_6, Q'=free_5, [ free_5>=1 && A>=1+D && A>=A ], cost: 1-D+A
     35: f15 -> [15] : D'=A, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, [ 0>=1+free_2 && A>=1+D ], cost: -D+A
     37: f15 -> [16] : D'=A, F'=free_6, G'=free_7, H'=free_7+free_6, Q'=free_5, [ free_5>=1 && A>=1+D ], cost: -D+A
      3: f10 -> f15 : E'=0, [ A>=C ], cost: 1
      8: f24 -> f75 : D'=C, [ C==D ], cost: 1
     38: f24 -> f32 : E'=1+E, J'=E, K'=free_8, L'=free_9, [ C>=1+D && 29>=E ], cost: 2
     39: f24 -> f32 : E'=1+E, J'=E, K'=free_10, L'=free_11, [ C>=1+D && E>=31 ], cost: 2
     40: f24 -> f32 : E'=1+E, J'=30, K'=free_12, L'=free_13, [ C>=1+D && E==30 ], cost: 2
     41: f24 -> f32 : E'=1+E, J'=E, K'=free_8, L'=free_9, [ D>=1+C && 29>=E ], cost: 2
     43: f24 -> f32 : E'=1+E, J'=30, K'=free_12, L'=free_13, [ D>=1+C && E==30 ], cost: 2
     14: f32 -> f42 : K'=free_14, M'=free_15, N'=free_15, O'=1, P'=1, Q_1'=0, [ K>=0 ], cost: 1
     15: f32 -> f42 : K'=free_16, N'=-free_17, O'=1, P'=1, Q_1'=0, R'=free_17, [ 0>=1+K ], cost: 1
     44: f42 -> f75 : [ C>=1+B && 0>=1+L ], cost: 2
     45: f42 -> f75 : [ C>=1+B && L>=1 ], cost: 2
     46: f42 -> f75 : L'=0, [ C>=1+B && C>=1+B && L==0 ], cost: 2
     47: f42 -> f75 : L'=0, S'=free_18, T'=free_19, [ B>=C && B>=C && 0==0 ], cost: 2
     48: f42 -> f42 : B'=-1+B, K'=free_23, L'=free_26, O'=free_21, P'=free_25, Q_1'=free_20, S'=free_36, T'=free_24, U'=1+A, [ B>=C && A>=U && 1+A>=1+A ], cost: 3-U+A
     49: f42 -> f42 : B'=-1+B, K'=free_31, L'=free_34, O'=free_29, P'=free_33, Q_1'=free_28, S'=free_36, T'=free_32, U'=1+A, [ B>=C && A>=U && 1+A>=1+A ], cost: 3-U+A
     29: start -> f10 : B'=1+A, [ A>=B && 1+A>=1+A ], cost: 3-B+A

Eliminating 2 self-loops for location f42
  Removing the self-loops: 48 49.
Adding an epsilon transition (to model nonexecution of the loops): 52.

Removed all Self-loops using metering functions (where possible):
  Start location: start
      1: f75 -> f15 : [ C>=1+D ], cost: 1
      2: f75 -> f15 : [ D>=1+C ], cost: 1
     25: f75 -> f10 : C'=1+C, D'=C, [ C==D ], cost: 1
     34: f15 -> f24 : D'=A, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, [ 0>=1+free_2 && A>=1+D && A>=A ], cost: 1-D+A
     36: f15 -> f24 : D'=A, F'=free_6, G'=free_7, H'=free_7+free_6, Q'=free_5, [ free_5>=1 && A>=1+D && A>=A ], cost: 1-D+A
     35: f15 -> [15] : D'=A, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, [ 0>=1+free_2 && A>=1+D ], cost: -D+A
     37: f15 -> [16] : D'=A, F'=free_6, G'=free_7, H'=free_7+free_6, Q'=free_5, [ free_5>=1 && A>=1+D ], cost: -D+A
      3: f10 -> f15 : E'=0, [ A>=C ], cost: 1
      8: f24 -> f75 : D'=C, [ C==D ], cost: 1
     38: f24 -> f32 : E'=1+E, J'=E, K'=free_8, L'=free_9, [ C>=1+D && 29>=E ], cost: 2
     39: f24 -> f32 : E'=1+E, J'=E, K'=free_10, L'=free_11, [ C>=1+D && E>=31 ], cost: 2
     40: f24 -> f32 : E'=1+E, J'=30, K'=free_12, L'=free_13, [ C>=1+D && E==30 ], cost: 2
     41: f24 -> f32 : E'=1+E, J'=E, K'=free_8, L'=free_9, [ D>=1+C && 29>=E ], cost: 2
     43: f24 -> f32 : E'=1+E, J'=30, K'=free_12, L'=free_13, [ D>=1+C && E==30 ], cost: 2
     14: f32 -> f42 : K'=free_14, M'=free_15, N'=free_15, O'=1, P'=1, Q_1'=0, [ K>=0 ], cost: 1
     15: f32 -> f42 : K'=free_16, N'=-free_17, O'=1, P'=1, Q_1'=0, R'=free_17, [ 0>=1+K ], cost: 1
     50: f42 -> [17] : B'=-1+B, K'=free_23, L'=free_26, O'=free_21, P'=free_25, Q_1'=free_20, S'=free_36, T'=free_24, U'=1+A, [ B>=C && A>=U ], cost: 3-U+A
     51: f42 -> [17] : B'=-1+B, K'=free_31, L'=free_34, O'=free_29, P'=free_33, Q_1'=free_28, S'=free_36, T'=free_32, U'=1+A, [ B>=C && A>=U ], cost: 3-U+A
     52: f42 -> [17] : [], cost: 0
     29: start -> f10 : B'=1+A, [ A>=B && 1+A>=1+A ], cost: 3-B+A
     44: [17] -> f75 : [ C>=1+B && 0>=1+L ], cost: 2
     45: [17] -> f75 : [ C>=1+B && L>=1 ], cost: 2
     46: [17] -> f75 : L'=0, [ C>=1+B && C>=1+B && L==0 ], cost: 2
     47: [17] -> f75 : L'=0, S'=free_18, T'=free_19, [ B>=C && B>=C && 0==0 ], cost: 2


Applied chaining over branches and pruning:
  Start location: start
      1: f75 -> f15 : [ C>=1+D ], cost: 1
      2: f75 -> f15 : [ D>=1+C ], cost: 1
     25: f75 -> f10 : C'=1+C, D'=C, [ C==D ], cost: 1
     53: f15 -> f75 : D'=C, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, [ 0>=1+free_2 && A>=1+D && A>=A && C==A ], cost: 2-D+A
     59: f15 -> f75 : D'=C, F'=free_6, G'=free_7, H'=free_7+free_6, Q'=free_5, [ free_5>=1 && A>=1+D && A>=A && C==A ], cost: 2-D+A
     54: f15 -> f32 : D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_8, L'=free_9, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E ], cost: 3-D+A
     55: f15 -> f32 : D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_10, L'=free_11, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && E>=31 ], cost: 3-D+A
     57: f15 -> f32 : D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_8, L'=free_9, [ 0>=1+free_2 && A>=1+D && A>=A && A>=1+C && 29>=E ], cost: 3-D+A
     58: f15 -> f32 : D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=30, K'=free_12, L'=free_13, [ 0>=1+free_2 && A>=1+D && A>=A && A>=1+C && E==30 ], cost: 3-D+A
     60: f15 -> f32 : D'=A, E'=1+E, F'=free_6, G'=free_7, H'=free_7+free_6, Q'=free_5, J'=E, K'=free_8, L'=free_9, [ free_5>=1 && A>=1+D && A>=A && C>=1+A && 29>=E ], cost: 3-D+A
     35: f15 -> [15] : D'=A, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, [ 0>=1+free_2 && A>=1+D ], cost: -D+A
     37: f15 -> [16] : D'=A, F'=free_6, G'=free_7, H'=free_7+free_6, Q'=free_5, [ free_5>=1 && A>=1+D ], cost: -D+A
      3: f10 -> f15 : E'=0, [ A>=C ], cost: 1
     65: f32 -> [17] : B'=-1+B, K'=free_23, L'=free_26, M'=free_15, N'=free_15, O'=free_21, P'=free_25, Q_1'=free_20, S'=free_36, T'=free_24, U'=1+A, [ K>=0 && B>=C && A>=U ], cost: 4-U+A
     66: f32 -> [17] : B'=-1+B, K'=free_31, L'=free_34, M'=free_15, N'=free_15, O'=free_29, P'=free_33, Q_1'=free_28, S'=free_36, T'=free_32, U'=1+A, [ K>=0 && B>=C && A>=U ], cost: 4-U+A
     68: f32 -> [17] : B'=-1+B, K'=free_23, L'=free_26, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_36, T'=free_24, U'=1+A, [ 0>=1+K && B>=C && A>=U ], cost: 4-U+A
     69: f32 -> [17] : B'=-1+B, K'=free_31, L'=free_34, N'=-free_17, O'=free_29, P'=free_33, Q_1'=free_28, R'=free_17, S'=free_36, T'=free_32, U'=1+A, [ 0>=1+K && B>=C && A>=U ], cost: 4-U+A
     70: f32 -> [17] : K'=free_16, N'=-free_17, O'=1, P'=1, Q_1'=0, R'=free_17, [ 0>=1+K ], cost: 1
     29: start -> f10 : B'=1+A, [ A>=B && 1+A>=1+A ], cost: 3-B+A
     44: [17] -> f75 : [ C>=1+B && 0>=1+L ], cost: 2
     45: [17] -> f75 : [ C>=1+B && L>=1 ], cost: 2
     46: [17] -> f75 : L'=0, [ C>=1+B && C>=1+B && L==0 ], cost: 2
     47: [17] -> f75 : L'=0, S'=free_18, T'=free_19, [ B>=C && B>=C && 0==0 ], cost: 2


Applied chaining over branches and pruning:
  Start location: start
      1: f75 -> f15 : [ C>=1+D ], cost: 1
      2: f75 -> f15 : [ D>=1+C ], cost: 1
     25: f75 -> f10 : C'=1+C, D'=C, [ C==D ], cost: 1
     53: f15 -> f75 : D'=C, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, [ 0>=1+free_2 && A>=1+D && A>=A && C==A ], cost: 2-D+A
     59: f15 -> f75 : D'=C, F'=free_6, G'=free_7, H'=free_7+free_6, Q'=free_5, [ free_5>=1 && A>=1+D && A>=A && C==A ], cost: 2-D+A
     35: f15 -> [15] : D'=A, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, [ 0>=1+free_2 && A>=1+D ], cost: -D+A
     37: f15 -> [16] : D'=A, F'=free_6, G'=free_7, H'=free_7+free_6, Q'=free_5, [ free_5>=1 && A>=1+D ], cost: -D+A
     71: f15 -> [17] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=free_26, M'=free_15, N'=free_15, O'=free_21, P'=free_25, Q_1'=free_20, S'=free_36, T'=free_24, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && free_8>=0 && B>=C && A>=U ], cost: 7-U-D+2*A
     72: f15 -> [17] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_31, L'=free_34, M'=free_15, N'=free_15, O'=free_29, P'=free_33, Q_1'=free_28, S'=free_36, T'=free_32, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && free_8>=0 && B>=C && A>=U ], cost: 7-U-D+2*A
     74: f15 -> [17] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_31, L'=free_34, N'=-free_17, O'=free_29, P'=free_33, Q_1'=free_28, R'=free_17, S'=free_36, T'=free_32, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && 0>=1+free_8 && B>=C && A>=U ], cost: 7-U-D+2*A
     78: f15 -> [17] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=free_26, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_36, T'=free_24, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && E>=31 && 0>=1+free_10 && B>=C && A>=U ], cost: 7-U-D+2*A
     83: f15 -> [17] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=free_26, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_36, T'=free_24, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && A>=1+C && 29>=E && 0>=1+free_8 && B>=C && A>=U ], cost: 7-U-D+2*A
      3: f10 -> f15 : E'=0, [ A>=C ], cost: 1
     29: start -> f10 : B'=1+A, [ A>=B && 1+A>=1+A ], cost: 3-B+A
     44: [17] -> f75 : [ C>=1+B && 0>=1+L ], cost: 2
     45: [17] -> f75 : [ C>=1+B && L>=1 ], cost: 2
     46: [17] -> f75 : L'=0, [ C>=1+B && C>=1+B && L==0 ], cost: 2
     47: [17] -> f75 : L'=0, S'=free_18, T'=free_19, [ B>=C && B>=C && 0==0 ], cost: 2


Applied chaining over branches and pruning:
  Start location: start
      1: f75 -> f15 : [ C>=1+D ], cost: 1
      2: f75 -> f15 : [ D>=1+C ], cost: 1
     25: f75 -> f10 : C'=1+C, D'=C, [ C==D ], cost: 1
     99: f15 -> f75 : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, M'=free_15, N'=free_15, O'=free_21, P'=free_25, Q_1'=free_20, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && free_8>=0 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    103: f15 -> f75 : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_31, L'=0, M'=free_15, N'=free_15, O'=free_29, P'=free_33, Q_1'=free_28, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && free_8>=0 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    107: f15 -> f75 : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_31, L'=0, N'=-free_17, O'=free_29, P'=free_33, Q_1'=free_28, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && 0>=1+free_8 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    111: f15 -> f75 : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && E>=31 && 0>=1+free_10 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    115: f15 -> f75 : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && A>=1+C && 29>=E && 0>=1+free_8 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
     35: f15 -> [15] : D'=A, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, [ 0>=1+free_2 && A>=1+D ], cost: -D+A
     37: f15 -> [16] : D'=A, F'=free_6, G'=free_7, H'=free_7+free_6, Q'=free_5, [ free_5>=1 && A>=1+D ], cost: -D+A
      3: f10 -> f15 : E'=0, [ A>=C ], cost: 1
     29: start -> f10 : B'=1+A, [ A>=B && 1+A>=1+A ], cost: 3-B+A


Applied chaining over branches and pruning:
  Start location: start
    116: f15 -> f15 : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, M'=free_15, N'=free_15, O'=free_21, P'=free_25, Q_1'=free_20, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && free_8>=0 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 && C>=1+A ], cost: 10-U-D+2*A
    119: f15 -> f15 : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_31, L'=0, M'=free_15, N'=free_15, O'=free_29, P'=free_33, Q_1'=free_28, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && free_8>=0 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 && C>=1+A ], cost: 10-U-D+2*A
    122: f15 -> f15 : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_31, L'=0, N'=-free_17, O'=free_29, P'=free_33, Q_1'=free_28, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && 0>=1+free_8 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 && C>=1+A ], cost: 10-U-D+2*A
    125: f15 -> f15 : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && E>=31 && 0>=1+free_10 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 && C>=1+A ], cost: 10-U-D+2*A
    129: f15 -> f15 : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && A>=1+C && 29>=E && 0>=1+free_8 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 && A>=1+C ], cost: 10-U-D+2*A
     35: f15 -> [15] : D'=A, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, [ 0>=1+free_2 && A>=1+D ], cost: -D+A
     37: f15 -> [16] : D'=A, F'=free_6, G'=free_7, H'=free_7+free_6, Q'=free_5, [ free_5>=1 && A>=1+D ], cost: -D+A
    117: f15 -> [18] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, M'=free_15, N'=free_15, O'=free_21, P'=free_25, Q_1'=free_20, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && free_8>=0 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    118: f15 -> [19] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, M'=free_15, N'=free_15, O'=free_21, P'=free_25, Q_1'=free_20, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && free_8>=0 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    120: f15 -> [20] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_31, L'=0, M'=free_15, N'=free_15, O'=free_29, P'=free_33, Q_1'=free_28, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && free_8>=0 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    121: f15 -> [21] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_31, L'=0, M'=free_15, N'=free_15, O'=free_29, P'=free_33, Q_1'=free_28, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && free_8>=0 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    123: f15 -> [22] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_31, L'=0, N'=-free_17, O'=free_29, P'=free_33, Q_1'=free_28, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && 0>=1+free_8 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    124: f15 -> [23] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_31, L'=0, N'=-free_17, O'=free_29, P'=free_33, Q_1'=free_28, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && 0>=1+free_8 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    126: f15 -> [24] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && E>=31 && 0>=1+free_10 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    127: f15 -> [25] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && E>=31 && 0>=1+free_10 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    128: f15 -> [26] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && A>=1+C && 29>=E && 0>=1+free_8 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    130: f15 -> [27] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && A>=1+C && 29>=E && 0>=1+free_8 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
      3: f10 -> f15 : E'=0, [ A>=C ], cost: 1
     29: start -> f10 : B'=1+A, [ A>=B && 1+A>=1+A ], cost: 3-B+A

Eliminating 5 self-loops for location f15
  Removing the self-loops: 116 119 122 125 129.
Adding an epsilon transition (to model nonexecution of the loops): 136.

Removed all Self-loops using metering functions (where possible):
  Start location: start
    131: f15 -> [28] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, M'=free_15, N'=free_15, O'=free_21, P'=free_25, Q_1'=free_20, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && C>=1+A && 29>=E && A>=U && -1+B>=C ], cost: 10-U-D+2*A
    132: f15 -> [28] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_31, L'=0, M'=free_15, N'=free_15, O'=free_29, P'=free_33, Q_1'=free_28, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && C>=1+A && 29>=E && A>=U && -1+B>=C ], cost: 10-U-D+2*A
    133: f15 -> [28] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_31, L'=0, N'=-free_17, O'=free_29, P'=free_33, Q_1'=free_28, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && C>=1+A && 29>=E && A>=U && -1+B>=C ], cost: 10-U-D+2*A
    134: f15 -> [28] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && C>=1+A && E>=31 && A>=U && -1+B>=C ], cost: 10-U-D+2*A
    135: f15 -> [28] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=1+C && 29>=E && A>=U && -1+B>=C ], cost: 10-U-D+2*A
    136: f15 -> [28] : [], cost: 0
      3: f10 -> f15 : E'=0, [ A>=C ], cost: 1
     29: start -> f10 : B'=1+A, [ A>=B && 1+A>=1+A ], cost: 3-B+A
     35: [28] -> [15] : D'=A, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, [ 0>=1+free_2 && A>=1+D ], cost: -D+A
     37: [28] -> [16] : D'=A, F'=free_6, G'=free_7, H'=free_7+free_6, Q'=free_5, [ free_5>=1 && A>=1+D ], cost: -D+A
    117: [28] -> [18] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, M'=free_15, N'=free_15, O'=free_21, P'=free_25, Q_1'=free_20, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && free_8>=0 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    118: [28] -> [19] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, M'=free_15, N'=free_15, O'=free_21, P'=free_25, Q_1'=free_20, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && free_8>=0 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    120: [28] -> [20] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_31, L'=0, M'=free_15, N'=free_15, O'=free_29, P'=free_33, Q_1'=free_28, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && free_8>=0 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    121: [28] -> [21] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_31, L'=0, M'=free_15, N'=free_15, O'=free_29, P'=free_33, Q_1'=free_28, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && free_8>=0 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    123: [28] -> [22] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_31, L'=0, N'=-free_17, O'=free_29, P'=free_33, Q_1'=free_28, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && 0>=1+free_8 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    124: [28] -> [23] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_31, L'=0, N'=-free_17, O'=free_29, P'=free_33, Q_1'=free_28, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && 0>=1+free_8 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    126: [28] -> [24] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && E>=31 && 0>=1+free_10 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    127: [28] -> [25] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && E>=31 && 0>=1+free_10 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    128: [28] -> [26] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && A>=1+C && 29>=E && 0>=1+free_8 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    130: [28] -> [27] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && A>=1+C && 29>=E && 0>=1+free_8 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A


Applied simple chaining:
  Start location: start
    131: f15 -> [28] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, M'=free_15, N'=free_15, O'=free_21, P'=free_25, Q_1'=free_20, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && C>=1+A && 29>=E && A>=U && -1+B>=C ], cost: 10-U-D+2*A
    132: f15 -> [28] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_31, L'=0, M'=free_15, N'=free_15, O'=free_29, P'=free_33, Q_1'=free_28, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && C>=1+A && 29>=E && A>=U && -1+B>=C ], cost: 10-U-D+2*A
    133: f15 -> [28] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_31, L'=0, N'=-free_17, O'=free_29, P'=free_33, Q_1'=free_28, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && C>=1+A && 29>=E && A>=U && -1+B>=C ], cost: 10-U-D+2*A
    134: f15 -> [28] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && C>=1+A && E>=31 && A>=U && -1+B>=C ], cost: 10-U-D+2*A
    135: f15 -> [28] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=1+C && 29>=E && A>=U && -1+B>=C ], cost: 10-U-D+2*A
    136: f15 -> [28] : [], cost: 0
     29: start -> f15 : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A
     35: [28] -> [15] : D'=A, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, [ 0>=1+free_2 && A>=1+D ], cost: -D+A
     37: [28] -> [16] : D'=A, F'=free_6, G'=free_7, H'=free_7+free_6, Q'=free_5, [ free_5>=1 && A>=1+D ], cost: -D+A
    117: [28] -> [18] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, M'=free_15, N'=free_15, O'=free_21, P'=free_25, Q_1'=free_20, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && free_8>=0 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    118: [28] -> [19] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, M'=free_15, N'=free_15, O'=free_21, P'=free_25, Q_1'=free_20, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && free_8>=0 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    120: [28] -> [20] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_31, L'=0, M'=free_15, N'=free_15, O'=free_29, P'=free_33, Q_1'=free_28, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && free_8>=0 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    121: [28] -> [21] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_31, L'=0, M'=free_15, N'=free_15, O'=free_29, P'=free_33, Q_1'=free_28, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && free_8>=0 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    123: [28] -> [22] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_31, L'=0, N'=-free_17, O'=free_29, P'=free_33, Q_1'=free_28, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && 0>=1+free_8 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    124: [28] -> [23] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_31, L'=0, N'=-free_17, O'=free_29, P'=free_33, Q_1'=free_28, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && 0>=1+free_8 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    126: [28] -> [24] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && E>=31 && 0>=1+free_10 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    127: [28] -> [25] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && E>=31 && 0>=1+free_10 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    128: [28] -> [26] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && A>=1+C && 29>=E && 0>=1+free_8 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    130: [28] -> [27] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && A>=1+C && 29>=E && 0>=1+free_8 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A


Applied chaining over branches and pruning:
  Start location: start
    141: start -> [28] : B'=A, D'=A, E'=1, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=0, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D && A>=1+C && 29>=0 && A>=U && A>=C ], cost: 14-U-B-D+3*A
    142: start -> [28] : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A
    137: start -> [29] : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A
    138: start -> [30] : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A
    139: start -> [31] : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A
    140: start -> [32] : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A
     35: [28] -> [15] : D'=A, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, [ 0>=1+free_2 && A>=1+D ], cost: -D+A
     37: [28] -> [16] : D'=A, F'=free_6, G'=free_7, H'=free_7+free_6, Q'=free_5, [ free_5>=1 && A>=1+D ], cost: -D+A
    117: [28] -> [18] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, M'=free_15, N'=free_15, O'=free_21, P'=free_25, Q_1'=free_20, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && free_8>=0 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    118: [28] -> [19] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, M'=free_15, N'=free_15, O'=free_21, P'=free_25, Q_1'=free_20, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && free_8>=0 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    120: [28] -> [20] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_31, L'=0, M'=free_15, N'=free_15, O'=free_29, P'=free_33, Q_1'=free_28, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && free_8>=0 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    121: [28] -> [21] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_31, L'=0, M'=free_15, N'=free_15, O'=free_29, P'=free_33, Q_1'=free_28, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && free_8>=0 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    123: [28] -> [22] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_31, L'=0, N'=-free_17, O'=free_29, P'=free_33, Q_1'=free_28, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && 0>=1+free_8 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    124: [28] -> [23] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_31, L'=0, N'=-free_17, O'=free_29, P'=free_33, Q_1'=free_28, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && 29>=E && 0>=1+free_8 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    126: [28] -> [24] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && E>=31 && 0>=1+free_10 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    127: [28] -> [25] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && C>=1+A && E>=31 && 0>=1+free_10 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    128: [28] -> [26] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && A>=1+C && 29>=E && 0>=1+free_8 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A
    130: [28] -> [27] : B'=-1+B, D'=A, E'=1+E, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=E, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ 0>=1+free_2 && A>=1+D && A>=A && A>=1+C && 29>=E && 0>=1+free_8 && B>=C && A>=U && -1+B>=C && -1+B>=C && 0==0 ], cost: 9-U-D+2*A


Applied chaining over branches and pruning:
  Start location: start
    155: start -> [15] : B'=1+A, D'=A, E'=0, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D ], cost: 4-B-D+2*A
    156: start -> [16] : B'=1+A, D'=A, E'=0, F'=free_6, G'=free_7, H'=free_7+free_6, Q'=free_5, [ A>=B && 1+A>=1+A && A>=C && free_5>=1 && A>=1+D ], cost: 4-B-D+2*A
    165: start -> [26] : B'=A, D'=A, E'=1, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=0, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D && A>=A && A>=1+C && 29>=0 && 0>=1+free_8 && 1+A>=C && A>=U && A>=C && A>=C && 0==0 ], cost: 13-U-B-D+3*A
    166: start -> [27] : B'=A, D'=A, E'=1, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=0, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D && A>=A && A>=1+C && 29>=0 && 0>=1+free_8 && 1+A>=C && A>=U && A>=C && A>=C && 0==0 ], cost: 13-U-B-D+3*A
    137: start -> [29] : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A
    138: start -> [30] : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A
    139: start -> [31] : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A
    140: start -> [32] : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A
    143: start -> [33] : B'=A, D'=A, E'=1, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=0, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D && A>=1+C && 29>=0 && A>=U && A>=C ], cost: 14-U-B-D+3*A
    144: start -> [34] : B'=A, D'=A, E'=1, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=0, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D && A>=1+C && 29>=0 && A>=U && A>=C ], cost: 14-U-B-D+3*A
    145: start -> [35] : B'=A, D'=A, E'=1, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=0, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D && A>=1+C && 29>=0 && A>=U && A>=C ], cost: 14-U-B-D+3*A
    146: start -> [36] : B'=A, D'=A, E'=1, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=0, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D && A>=1+C && 29>=0 && A>=U && A>=C ], cost: 14-U-B-D+3*A
    147: start -> [37] : B'=A, D'=A, E'=1, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=0, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D && A>=1+C && 29>=0 && A>=U && A>=C ], cost: 14-U-B-D+3*A
    148: start -> [38] : B'=A, D'=A, E'=1, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=0, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D && A>=1+C && 29>=0 && A>=U && A>=C ], cost: 14-U-B-D+3*A
    149: start -> [39] : B'=A, D'=A, E'=1, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=0, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D && A>=1+C && 29>=0 && A>=U && A>=C ], cost: 14-U-B-D+3*A
    150: start -> [40] : B'=A, D'=A, E'=1, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=0, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D && A>=1+C && 29>=0 && A>=U && A>=C ], cost: 14-U-B-D+3*A
    151: start -> [41] : B'=A, D'=A, E'=1, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=0, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D && A>=1+C && 29>=0 && A>=U && A>=C ], cost: 14-U-B-D+3*A
    152: start -> [42] : B'=A, D'=A, E'=1, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=0, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D && A>=1+C && 29>=0 && A>=U && A>=C ], cost: 14-U-B-D+3*A
    153: start -> [43] : B'=A, D'=A, E'=1, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=0, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D && A>=1+C && 29>=0 && A>=U && A>=C ], cost: 14-U-B-D+3*A
    154: start -> [44] : B'=A, D'=A, E'=1, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=0, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D && A>=1+C && 29>=0 && A>=U && A>=C ], cost: 14-U-B-D+3*A
    157: start -> [45] : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A
    158: start -> [46] : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A
    159: start -> [47] : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A
    160: start -> [48] : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A
    161: start -> [49] : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A
    162: start -> [50] : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A
    163: start -> [51] : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A
    164: start -> [52] : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A


Final control flow graph problem, now checking costs for infinitely many models:
  Start location: start
    155: start -> [15] : B'=1+A, D'=A, E'=0, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D ], cost: 4-B-D+2*A
    156: start -> [16] : B'=1+A, D'=A, E'=0, F'=free_6, G'=free_7, H'=free_7+free_6, Q'=free_5, [ A>=B && 1+A>=1+A && A>=C && free_5>=1 && A>=1+D ], cost: 4-B-D+2*A
    165: start -> [26] : B'=A, D'=A, E'=1, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=0, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D && A>=A && A>=1+C && 29>=0 && 0>=1+free_8 && 1+A>=C && A>=U && A>=C && A>=C && 0==0 ], cost: 13-U-B-D+3*A
    166: start -> [27] : B'=A, D'=A, E'=1, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=0, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D && A>=A && A>=1+C && 29>=0 && 0>=1+free_8 && 1+A>=C && A>=U && A>=C && A>=C && 0==0 ], cost: 13-U-B-D+3*A
    137: start -> [29] : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A
    138: start -> [30] : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A
    139: start -> [31] : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A
    140: start -> [32] : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A
    143: start -> [33] : B'=A, D'=A, E'=1, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=0, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D && A>=1+C && 29>=0 && A>=U && A>=C ], cost: 14-U-B-D+3*A
    144: start -> [34] : B'=A, D'=A, E'=1, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=0, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D && A>=1+C && 29>=0 && A>=U && A>=C ], cost: 14-U-B-D+3*A
    145: start -> [35] : B'=A, D'=A, E'=1, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=0, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D && A>=1+C && 29>=0 && A>=U && A>=C ], cost: 14-U-B-D+3*A
    146: start -> [36] : B'=A, D'=A, E'=1, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=0, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D && A>=1+C && 29>=0 && A>=U && A>=C ], cost: 14-U-B-D+3*A
    147: start -> [37] : B'=A, D'=A, E'=1, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=0, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D && A>=1+C && 29>=0 && A>=U && A>=C ], cost: 14-U-B-D+3*A
    148: start -> [38] : B'=A, D'=A, E'=1, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=0, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D && A>=1+C && 29>=0 && A>=U && A>=C ], cost: 14-U-B-D+3*A
    149: start -> [39] : B'=A, D'=A, E'=1, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=0, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D && A>=1+C && 29>=0 && A>=U && A>=C ], cost: 14-U-B-D+3*A
    150: start -> [40] : B'=A, D'=A, E'=1, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=0, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D && A>=1+C && 29>=0 && A>=U && A>=C ], cost: 14-U-B-D+3*A
    151: start -> [41] : B'=A, D'=A, E'=1, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=0, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D && A>=1+C && 29>=0 && A>=U && A>=C ], cost: 14-U-B-D+3*A
    152: start -> [42] : B'=A, D'=A, E'=1, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=0, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D && A>=1+C && 29>=0 && A>=U && A>=C ], cost: 14-U-B-D+3*A
    153: start -> [43] : B'=A, D'=A, E'=1, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=0, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D && A>=1+C && 29>=0 && A>=U && A>=C ], cost: 14-U-B-D+3*A
    154: start -> [44] : B'=A, D'=A, E'=1, F'=free_3, G'=free_4, H'=free_4+free_3, Q'=free_2, J'=0, K'=free_23, L'=0, N'=-free_17, O'=free_21, P'=free_25, Q_1'=free_20, R'=free_17, S'=free_18, T'=free_19, U'=1+A, [ A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D && A>=1+C && 29>=0 && A>=U && A>=C ], cost: 14-U-B-D+3*A
    157: start -> [45] : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A
    158: start -> [46] : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A
    159: start -> [47] : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A
    160: start -> [48] : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A
    161: start -> [49] : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A
    162: start -> [50] : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A
    163: start -> [51] : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A
    164: start -> [52] : B'=1+A, E'=0, [ A>=B && 1+A>=1+A && A>=C ], cost: 4-B+A


Computing complexity for remaining 28 transitions.

  Found configuration with infinitely models for cost: 4-B-D+2*A
  and guard: A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D:
  B: Neg, free_2: Neg, C: Pos, D: Neg, A: Pos, where: A > C

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


The final runtime is determined by this resulting transition:
  Final Guard: A>=B && 1+A>=1+A && A>=C && 0>=1+free_2 && A>=1+D
  Final Cost:  4-B-D+2*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),?)