Trying to load file: main.koat Initial Control flow graph problem: Start location: start 0: f2 -> f2 : B'=1+B, C'=free*C, [ A>=B ], cost: 1 21: f2 -> f10 : D'=1, [ B>=1+A ], cost: 1 1: f10 -> f19 : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 ], cost: 1 20: f10 -> f1 : [ 0>=B ], cost: 1 2: f19 -> f23 : [ H>=K && J>=1+K ], cost: 1 5: f19 -> f41 : P'=free_19, [ K>=J && H>=2*free_21 && 3*free_21>=1+H && free_21>=free_19 && H>=2*free_20 && 3*free_20>=1+H && free_19>=free_20 && H>=K ], cost: 1 19: f19 -> f53 : Q_1'=G, [ K>=1+H ], cost: 1 3: f23 -> f26 : [ K+G>=2+L ], cost: 1 18: f23 -> f41 : P'=free_33, [ 1+L>=K+G && H>=2*free_35 && 3*free_35>=1+H && free_35>=free_33 && H>=2*free_34 && 3*free_34>=1+H && free_33>=free_34 ], cost: 1 17: f26 -> f23 : L'=2+L, [ M>=1+Q ], cost: 1 4: f26 -> f26 : M'=H+M, N'=-K+M+J, O'=free_18, [ Q>=M ], cost: 1 15: f41 -> f19 : J'=P+J, K'=K+G, [ P>=G && P>=J ], cost: 1 16: f41 -> f19 : J'=P+J, K'=K+G, [ G>=1+P ], cost: 1 6: f41 -> f41 : J'=-P+J, P'=free_22, [ J>=1+P && P>=2*free_24 && 3*free_24>=1+P && free_24>=free_22 && P>=2*free_23 && 3*free_23>=1+P && free_22>=free_23 && P>=G ], cost: 1 14: f53 -> f10 : B'=-1+B, D'=E*D, [ Q_1>=H ], cost: 1 7: f53 -> f63 : R'=2*Q_1, S'=free_25, T'=free_28, U'=free_27, V'=free_26, W'=1, X'=0, [ H>=1+Q_1 ], cost: 1 13: f63 -> f53 : Q_1'=R, [ M>=1+Q_1 ], cost: 1 8: f63 -> f66 : [ Q_1>=M ], cost: 1 12: f66 -> f63 : M'=M+G, T'=W, W'=U*W+W-X*V, X'=X+X*U+V*W, [ 1+L>=M+G ], cost: 1 9: f66 -> f69 : [ M+G>=2+L ], cost: 1 11: f69 -> f66 : L'=2+L, [ K>=1+Q ], cost: 1 10: f69 -> f69 : K'=K+R, O'=-X*free_32+W*free_29, Y'=K, Z'=Q_1+K, A1'=X*free_30+free_31*W, [ Q>=K ], cost: 1 22: start -> f2 : [], cost: 1 Simplified the transitions: Start location: start 0: f2 -> f2 : B'=1+B, C'=free*C, [ A>=B ], cost: 1 21: f2 -> f10 : D'=1, [ B>=1+A ], cost: 1 1: f10 -> f19 : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 ], cost: 1 2: f19 -> f23 : [ H>=K && J>=1+K ], cost: 1 5: f19 -> f41 : P'=free_19, [ K>=J && H>=2*free_21 && 3*free_21>=1+H && free_21>=free_19 && H>=2*free_20 && 3*free_20>=1+H && free_19>=free_20 && H>=K ], cost: 1 19: f19 -> f53 : Q_1'=G, [ K>=1+H ], cost: 1 3: f23 -> f26 : [ K+G>=2+L ], cost: 1 18: f23 -> f41 : P'=free_33, [ 1+L>=K+G && H>=2*free_35 && 3*free_35>=1+H && free_35>=free_33 && H>=2*free_34 && 3*free_34>=1+H && free_33>=free_34 ], cost: 1 17: f26 -> f23 : L'=2+L, [ M>=1+Q ], cost: 1 4: f26 -> f26 : M'=H+M, N'=-K+M+J, O'=free_18, [ Q>=M ], cost: 1 15: f41 -> f19 : J'=P+J, K'=K+G, [ P>=G && P>=J ], cost: 1 16: f41 -> f19 : J'=P+J, K'=K+G, [ G>=1+P ], cost: 1 6: f41 -> f41 : J'=-P+J, P'=free_22, [ J>=1+P && P>=2*free_24 && 3*free_24>=1+P && free_24>=free_22 && P>=2*free_23 && 3*free_23>=1+P && free_22>=free_23 && P>=G ], cost: 1 14: f53 -> f10 : B'=-1+B, D'=E*D, [ Q_1>=H ], cost: 1 7: f53 -> f63 : R'=2*Q_1, S'=free_25, T'=free_28, U'=free_27, V'=free_26, W'=1, X'=0, [ H>=1+Q_1 ], cost: 1 13: f63 -> f53 : Q_1'=R, [ M>=1+Q_1 ], cost: 1 8: f63 -> f66 : [ Q_1>=M ], cost: 1 12: f66 -> f63 : M'=M+G, T'=W, W'=U*W+W-X*V, X'=X+X*U+V*W, [ 1+L>=M+G ], cost: 1 9: f66 -> f69 : [ M+G>=2+L ], cost: 1 11: f69 -> f66 : L'=2+L, [ K>=1+Q ], cost: 1 10: f69 -> f69 : K'=K+R, O'=-X*free_32+W*free_29, Y'=K, Z'=Q_1+K, A1'=X*free_30+free_31*W, [ Q>=K ], cost: 1 22: 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 23. Removing the self-loops: 0. Eliminating 1 self-loops for location f26 Removing the self-loops: 4. Adding an epsilon transition (to model nonexecution of the loops): 25. Eliminating 1 self-loops for location f41 Removing the self-loops: 6. Adding an epsilon transition (to model nonexecution of the loops): 27. Eliminating 1 self-loops for location f69 Removing the self-loops: 10. Adding an epsilon transition (to model nonexecution of the loops): 29. Removed all Self-loops using metering functions (where possible): Start location: start 23: f2 -> [12] : B'=1+A, C'=C*free^(1-B+A), [ A>=B ], cost: 1-B+A 1: f10 -> f19 : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 ], cost: 1 2: f19 -> f23 : [ H>=K && J>=1+K ], cost: 1 5: f19 -> f41 : P'=free_19, [ K>=J && H>=2*free_21 && 3*free_21>=1+H && free_21>=free_19 && H>=2*free_20 && 3*free_20>=1+H && free_19>=free_20 && H>=K ], cost: 1 19: f19 -> f53 : Q_1'=G, [ K>=1+H ], cost: 1 3: f23 -> f26 : [ K+G>=2+L ], cost: 1 18: f23 -> f41 : P'=free_33, [ 1+L>=K+G && H>=2*free_35 && 3*free_35>=1+H && free_35>=free_33 && H>=2*free_34 && 3*free_34>=1+H && free_33>=free_34 ], cost: 1 24: f26 -> [13] : M'=H+M, N'=-K+M+J, O'=free_18, [ Q>=M ], cost: 1 25: f26 -> [13] : [], cost: 0 26: f41 -> [14] : J'=-P+J, P'=free_22, [ J>=1+P && P>=2*free_24 && 3*free_24>=1+P && free_24>=free_22 && P>=2*free_23 && 3*free_23>=1+P && free_22>=free_23 && P>=G ], cost: 1 27: f41 -> [14] : [], cost: 0 14: f53 -> f10 : B'=-1+B, D'=E*D, [ Q_1>=H ], cost: 1 7: f53 -> f63 : R'=2*Q_1, S'=free_25, T'=free_28, U'=free_27, V'=free_26, W'=1, X'=0, [ H>=1+Q_1 ], cost: 1 13: f63 -> f53 : Q_1'=R, [ M>=1+Q_1 ], cost: 1 8: f63 -> f66 : [ Q_1>=M ], cost: 1 12: f66 -> f63 : M'=M+G, T'=W, W'=U*W+W-X*V, X'=X+X*U+V*W, [ 1+L>=M+G ], cost: 1 9: f66 -> f69 : [ M+G>=2+L ], cost: 1 28: f69 -> [15] : K'=K+R, O'=-X*free_32+W*free_29, Y'=K, Z'=Q_1+K, A1'=X*free_30+free_31*W, [ Q>=K ], cost: 1 29: f69 -> [15] : [], cost: 0 22: start -> f2 : [], cost: 1 21: [12] -> f10 : D'=1, [ B>=1+A ], cost: 1 17: [13] -> f23 : L'=2+L, [ M>=1+Q ], cost: 1 15: [14] -> f19 : J'=P+J, K'=K+G, [ P>=G && P>=J ], cost: 1 16: [14] -> f19 : J'=P+J, K'=K+G, [ G>=1+P ], cost: 1 11: [15] -> f66 : L'=2+L, [ K>=1+Q ], cost: 1 Applied simple chaining: Start location: start 1: f10 -> f19 : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 ], cost: 1 2: f19 -> f23 : [ H>=K && J>=1+K ], cost: 1 5: f19 -> f41 : P'=free_19, [ K>=J && H>=2*free_21 && 3*free_21>=1+H && free_21>=free_19 && H>=2*free_20 && 3*free_20>=1+H && free_19>=free_20 && H>=K ], cost: 1 19: f19 -> f53 : Q_1'=G, [ K>=1+H ], cost: 1 3: f23 -> f26 : [ K+G>=2+L ], cost: 1 18: f23 -> f41 : P'=free_33, [ 1+L>=K+G && H>=2*free_35 && 3*free_35>=1+H && free_35>=free_33 && H>=2*free_34 && 3*free_34>=1+H && free_33>=free_34 ], cost: 1 24: f26 -> [13] : M'=H+M, N'=-K+M+J, O'=free_18, [ Q>=M ], cost: 1 25: f26 -> [13] : [], cost: 0 26: f41 -> [14] : J'=-P+J, P'=free_22, [ J>=1+P && P>=2*free_24 && 3*free_24>=1+P && free_24>=free_22 && P>=2*free_23 && 3*free_23>=1+P && free_22>=free_23 && P>=G ], cost: 1 27: f41 -> [14] : [], cost: 0 14: f53 -> f10 : B'=-1+B, D'=E*D, [ Q_1>=H ], cost: 1 7: f53 -> f63 : R'=2*Q_1, S'=free_25, T'=free_28, U'=free_27, V'=free_26, W'=1, X'=0, [ H>=1+Q_1 ], cost: 1 13: f63 -> f53 : Q_1'=R, [ M>=1+Q_1 ], cost: 1 8: f63 -> f66 : [ Q_1>=M ], cost: 1 12: f66 -> f63 : M'=M+G, T'=W, W'=U*W+W-X*V, X'=X+X*U+V*W, [ 1+L>=M+G ], cost: 1 9: f66 -> f69 : [ M+G>=2+L ], cost: 1 28: f69 -> [15] : K'=K+R, O'=-X*free_32+W*free_29, Y'=K, Z'=Q_1+K, A1'=X*free_30+free_31*W, [ Q>=K ], cost: 1 29: f69 -> [15] : [], cost: 0 22: start -> f10 : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 17: [13] -> f23 : L'=2+L, [ M>=1+Q ], cost: 1 15: [14] -> f19 : J'=P+J, K'=K+G, [ P>=G && P>=J ], cost: 1 16: [14] -> f19 : J'=P+J, K'=K+G, [ G>=1+P ], cost: 1 11: [15] -> f66 : L'=2+L, [ K>=1+Q ], cost: 1 Applied chaining over branches and pruning: Start location: start 1: f10 -> f19 : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 ], cost: 1 2: f19 -> f23 : [ H>=K && J>=1+K ], cost: 1 5: f19 -> f41 : P'=free_19, [ K>=J && H>=2*free_21 && 3*free_21>=1+H && free_21>=free_19 && H>=2*free_20 && 3*free_20>=1+H && free_19>=free_20 && H>=K ], cost: 1 19: f19 -> f53 : Q_1'=G, [ K>=1+H ], cost: 1 18: f23 -> f41 : P'=free_33, [ 1+L>=K+G && H>=2*free_35 && 3*free_35>=1+H && free_35>=free_33 && H>=2*free_34 && 3*free_34>=1+H && free_33>=free_34 ], cost: 1 30: f23 -> [13] : M'=H+M, N'=-K+M+J, O'=free_18, [ K+G>=2+L && Q>=M ], cost: 2 31: f23 -> [13] : [ K+G>=2+L ], cost: 1 32: f41 -> f19 : J'=-P+J+free_22, K'=K+G, P'=free_22, [ J>=1+P && P>=2*free_24 && 3*free_24>=1+P && free_24>=free_22 && P>=2*free_23 && 3*free_23>=1+P && free_22>=free_23 && P>=G && free_22>=G && free_22>=-P+J ], cost: 2 33: f41 -> f19 : J'=-P+J+free_22, K'=K+G, P'=free_22, [ J>=1+P && P>=2*free_24 && 3*free_24>=1+P && free_24>=free_22 && P>=2*free_23 && 3*free_23>=1+P && free_22>=free_23 && P>=G && G>=1+free_22 ], cost: 2 34: f41 -> f19 : J'=P+J, K'=K+G, [ P>=G && P>=J ], cost: 1 35: f41 -> f19 : J'=P+J, K'=K+G, [ G>=1+P ], cost: 1 14: f53 -> f10 : B'=-1+B, D'=E*D, [ Q_1>=H ], cost: 1 7: f53 -> f63 : R'=2*Q_1, S'=free_25, T'=free_28, U'=free_27, V'=free_26, W'=1, X'=0, [ H>=1+Q_1 ], cost: 1 13: f63 -> f53 : Q_1'=R, [ M>=1+Q_1 ], cost: 1 8: f63 -> f66 : [ Q_1>=M ], cost: 1 12: f66 -> f63 : M'=M+G, T'=W, W'=U*W+W-X*V, X'=X+X*U+V*W, [ 1+L>=M+G ], cost: 1 36: f66 -> [15] : K'=K+R, O'=-X*free_32+W*free_29, Y'=K, Z'=Q_1+K, A1'=X*free_30+free_31*W, [ M+G>=2+L && Q>=K ], cost: 2 37: f66 -> [15] : [ M+G>=2+L ], cost: 1 22: start -> f10 : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 17: [13] -> f23 : L'=2+L, [ M>=1+Q ], cost: 1 11: [15] -> f66 : L'=2+L, [ K>=1+Q ], cost: 1 Applied chaining over branches and pruning: Start location: start 1: f10 -> f19 : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 ], cost: 1 2: f19 -> f23 : [ H>=K && J>=1+K ], cost: 1 5: f19 -> f41 : P'=free_19, [ K>=J && H>=2*free_21 && 3*free_21>=1+H && free_21>=free_19 && H>=2*free_20 && 3*free_20>=1+H && free_19>=free_20 && H>=K ], cost: 1 19: f19 -> f53 : Q_1'=G, [ K>=1+H ], cost: 1 38: f23 -> f23 : L'=2+L, M'=H+M, N'=-K+M+J, O'=free_18, [ K+G>=2+L && Q>=M && H+M>=1+Q ], cost: 3 39: f23 -> f23 : L'=2+L, [ K+G>=2+L && M>=1+Q ], cost: 2 18: f23 -> f41 : P'=free_33, [ 1+L>=K+G && H>=2*free_35 && 3*free_35>=1+H && free_35>=free_33 && H>=2*free_34 && 3*free_34>=1+H && free_33>=free_34 ], cost: 1 32: f41 -> f19 : J'=-P+J+free_22, K'=K+G, P'=free_22, [ J>=1+P && P>=2*free_24 && 3*free_24>=1+P && free_24>=free_22 && P>=2*free_23 && 3*free_23>=1+P && free_22>=free_23 && P>=G && free_22>=G && free_22>=-P+J ], cost: 2 33: f41 -> f19 : J'=-P+J+free_22, K'=K+G, P'=free_22, [ J>=1+P && P>=2*free_24 && 3*free_24>=1+P && free_24>=free_22 && P>=2*free_23 && 3*free_23>=1+P && free_22>=free_23 && P>=G && G>=1+free_22 ], cost: 2 34: f41 -> f19 : J'=P+J, K'=K+G, [ P>=G && P>=J ], cost: 1 35: f41 -> f19 : J'=P+J, K'=K+G, [ G>=1+P ], cost: 1 14: f53 -> f10 : B'=-1+B, D'=E*D, [ Q_1>=H ], cost: 1 7: f53 -> f63 : R'=2*Q_1, S'=free_25, T'=free_28, U'=free_27, V'=free_26, W'=1, X'=0, [ H>=1+Q_1 ], cost: 1 13: f63 -> f53 : Q_1'=R, [ M>=1+Q_1 ], cost: 1 8: f63 -> f66 : [ Q_1>=M ], cost: 1 12: f66 -> f63 : M'=M+G, T'=W, W'=U*W+W-X*V, X'=X+X*U+V*W, [ 1+L>=M+G ], cost: 1 40: f66 -> f66 : K'=K+R, L'=2+L, O'=-X*free_32+W*free_29, Y'=K, Z'=Q_1+K, A1'=X*free_30+free_31*W, [ M+G>=2+L && Q>=K && K+R>=1+Q ], cost: 3 41: f66 -> f66 : L'=2+L, [ M+G>=2+L && K>=1+Q ], cost: 2 22: start -> f10 : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A Eliminating 2 self-loops for location f23 Self-Loop 39 has the metering function: meter, resulting in the new transition 43. Removing the self-loops: 38 39. Adding an epsilon transition (to model nonexecution of the loops): 44. Eliminating 2 self-loops for location f66 Self-Loop 41 has the metering function: meter_1, resulting in the new transition 46. Removing the self-loops: 40 41. Adding an epsilon transition (to model nonexecution of the loops): 47. Removed all Self-loops using metering functions (where possible): Start location: start 1: f10 -> f19 : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 ], cost: 1 2: f19 -> f23 : [ H>=K && J>=1+K ], cost: 1 5: f19 -> f41 : P'=free_19, [ K>=J && H>=2*free_21 && 3*free_21>=1+H && free_21>=free_19 && H>=2*free_20 && 3*free_20>=1+H && free_19>=free_20 && H>=K ], cost: 1 19: f19 -> f53 : Q_1'=G, [ K>=1+H ], cost: 1 42: f23 -> [16] : L'=2+L, M'=H+M, N'=-K+M+J, O'=free_18, [ K+G>=2+L && Q>=M && H+M>=1+Q ], cost: 3 43: f23 -> [16] : L'=2*meter+L, [ K+G>=2+L && M>=1+Q && 2*meter==-1+K-L+G ], cost: 2*meter 44: f23 -> [16] : [], cost: 0 32: f41 -> f19 : J'=-P+J+free_22, K'=K+G, P'=free_22, [ J>=1+P && P>=2*free_24 && 3*free_24>=1+P && free_24>=free_22 && P>=2*free_23 && 3*free_23>=1+P && free_22>=free_23 && P>=G && free_22>=G && free_22>=-P+J ], cost: 2 33: f41 -> f19 : J'=-P+J+free_22, K'=K+G, P'=free_22, [ J>=1+P && P>=2*free_24 && 3*free_24>=1+P && free_24>=free_22 && P>=2*free_23 && 3*free_23>=1+P && free_22>=free_23 && P>=G && G>=1+free_22 ], cost: 2 34: f41 -> f19 : J'=P+J, K'=K+G, [ P>=G && P>=J ], cost: 1 35: f41 -> f19 : J'=P+J, K'=K+G, [ G>=1+P ], cost: 1 14: f53 -> f10 : B'=-1+B, D'=E*D, [ Q_1>=H ], cost: 1 7: f53 -> f63 : R'=2*Q_1, S'=free_25, T'=free_28, U'=free_27, V'=free_26, W'=1, X'=0, [ H>=1+Q_1 ], cost: 1 13: f63 -> f53 : Q_1'=R, [ M>=1+Q_1 ], cost: 1 8: f63 -> f66 : [ Q_1>=M ], cost: 1 45: f66 -> [17] : K'=K+R, L'=2+L, O'=-X*free_32+W*free_29, Y'=K, Z'=Q_1+K, A1'=X*free_30+free_31*W, [ M+G>=2+L && Q>=K && K+R>=1+Q ], cost: 3 46: f66 -> [17] : L'=2*meter_1+L, [ M+G>=2+L && K>=1+Q && 2*meter_1==-1-L+M+G ], cost: 2*meter_1 47: f66 -> [17] : [], cost: 0 22: start -> f10 : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 18: [16] -> f41 : P'=free_33, [ 1+L>=K+G && H>=2*free_35 && 3*free_35>=1+H && free_35>=free_33 && H>=2*free_34 && 3*free_34>=1+H && free_33>=free_34 ], cost: 1 12: [17] -> f63 : M'=M+G, T'=W, W'=U*W+W-X*V, X'=X+X*U+V*W, [ 1+L>=M+G ], cost: 1 Applied chaining over branches and pruning: Start location: start 1: f10 -> f19 : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 ], cost: 1 5: f19 -> f41 : P'=free_19, [ K>=J && H>=2*free_21 && 3*free_21>=1+H && free_21>=free_19 && H>=2*free_20 && 3*free_20>=1+H && free_19>=free_20 && H>=K ], cost: 1 19: f19 -> f53 : Q_1'=G, [ K>=1+H ], cost: 1 48: f19 -> [16] : L'=2+L, M'=H+M, N'=-K+M+J, O'=free_18, [ H>=K && J>=1+K && K+G>=2+L && Q>=M && H+M>=1+Q ], cost: 4 49: f19 -> [16] : L'=2*meter+L, [ H>=K && J>=1+K && K+G>=2+L && M>=1+Q && 2*meter==-1+K-L+G ], cost: 1+2*meter 50: f19 -> [16] : [ H>=K && J>=1+K ], cost: 1 32: f41 -> f19 : J'=-P+J+free_22, K'=K+G, P'=free_22, [ J>=1+P && P>=2*free_24 && 3*free_24>=1+P && free_24>=free_22 && P>=2*free_23 && 3*free_23>=1+P && free_22>=free_23 && P>=G && free_22>=G && free_22>=-P+J ], cost: 2 33: f41 -> f19 : J'=-P+J+free_22, K'=K+G, P'=free_22, [ J>=1+P && P>=2*free_24 && 3*free_24>=1+P && free_24>=free_22 && P>=2*free_23 && 3*free_23>=1+P && free_22>=free_23 && P>=G && G>=1+free_22 ], cost: 2 34: f41 -> f19 : J'=P+J, K'=K+G, [ P>=G && P>=J ], cost: 1 35: f41 -> f19 : J'=P+J, K'=K+G, [ G>=1+P ], cost: 1 14: f53 -> f10 : B'=-1+B, D'=E*D, [ Q_1>=H ], cost: 1 7: f53 -> f63 : R'=2*Q_1, S'=free_25, T'=free_28, U'=free_27, V'=free_26, W'=1, X'=0, [ H>=1+Q_1 ], cost: 1 13: f63 -> f53 : Q_1'=R, [ M>=1+Q_1 ], cost: 1 51: f63 -> [17] : K'=K+R, L'=2+L, O'=-X*free_32+W*free_29, Y'=K, Z'=Q_1+K, A1'=X*free_30+free_31*W, [ Q_1>=M && M+G>=2+L && Q>=K && K+R>=1+Q ], cost: 4 52: f63 -> [17] : L'=2*meter_1+L, [ Q_1>=M && M+G>=2+L && K>=1+Q && 2*meter_1==-1-L+M+G ], cost: 1+2*meter_1 53: f63 -> [17] : [ Q_1>=M ], cost: 1 22: start -> f10 : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 18: [16] -> f41 : P'=free_33, [ 1+L>=K+G && H>=2*free_35 && 3*free_35>=1+H && free_35>=free_33 && H>=2*free_34 && 3*free_34>=1+H && free_33>=free_34 ], cost: 1 12: [17] -> f63 : M'=M+G, T'=W, W'=U*W+W-X*V, X'=X+X*U+V*W, [ 1+L>=M+G ], cost: 1 Applied chaining over branches and pruning: Start location: start 1: f10 -> f19 : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 ], cost: 1 5: f19 -> f41 : P'=free_19, [ K>=J && H>=2*free_21 && 3*free_21>=1+H && free_21>=free_19 && H>=2*free_20 && 3*free_20>=1+H && free_19>=free_20 && H>=K ], cost: 1 54: f19 -> f41 : L'=2+L, M'=H+M, N'=-K+M+J, O'=free_18, P'=free_33, [ H>=K && J>=1+K && K+G>=2+L && Q>=M && H+M>=1+Q && 3+L>=K+G && H>=2*free_35 && 3*free_35>=1+H && free_35>=free_33 && H>=2*free_34 && 3*free_34>=1+H && free_33>=free_34 ], cost: 5 55: f19 -> f41 : L'=2*meter+L, P'=free_33, [ H>=K && J>=1+K && K+G>=2+L && M>=1+Q && 2*meter==-1+K-L+G && 1+2*meter+L>=K+G && H>=2*free_35 && 3*free_35>=1+H && free_35>=free_33 && H>=2*free_34 && 3*free_34>=1+H && free_33>=free_34 ], cost: 2+2*meter 56: f19 -> f41 : P'=free_33, [ H>=K && J>=1+K && 1+L>=K+G && H>=2*free_35 && 3*free_35>=1+H && free_35>=free_33 && H>=2*free_34 && 3*free_34>=1+H && free_33>=free_34 ], cost: 2 19: f19 -> f53 : Q_1'=G, [ K>=1+H ], cost: 1 32: f41 -> f19 : J'=-P+J+free_22, K'=K+G, P'=free_22, [ J>=1+P && P>=2*free_24 && 3*free_24>=1+P && free_24>=free_22 && P>=2*free_23 && 3*free_23>=1+P && free_22>=free_23 && P>=G && free_22>=G && free_22>=-P+J ], cost: 2 33: f41 -> f19 : J'=-P+J+free_22, K'=K+G, P'=free_22, [ J>=1+P && P>=2*free_24 && 3*free_24>=1+P && free_24>=free_22 && P>=2*free_23 && 3*free_23>=1+P && free_22>=free_23 && P>=G && G>=1+free_22 ], cost: 2 34: f41 -> f19 : J'=P+J, K'=K+G, [ P>=G && P>=J ], cost: 1 35: f41 -> f19 : J'=P+J, K'=K+G, [ G>=1+P ], cost: 1 14: f53 -> f10 : B'=-1+B, D'=E*D, [ Q_1>=H ], cost: 1 7: f53 -> f63 : R'=2*Q_1, S'=free_25, T'=free_28, U'=free_27, V'=free_26, W'=1, X'=0, [ H>=1+Q_1 ], cost: 1 13: f63 -> f53 : Q_1'=R, [ M>=1+Q_1 ], cost: 1 57: f63 -> f63 : K'=K+R, L'=2+L, M'=M+G, O'=-X*free_32+W*free_29, T'=W, W'=U*W+W-X*V, X'=X+X*U+V*W, Y'=K, Z'=Q_1+K, A1'=X*free_30+free_31*W, [ Q_1>=M && M+G>=2+L && Q>=K && K+R>=1+Q && 3+L>=M+G ], cost: 5 58: f63 -> f63 : L'=2*meter_1+L, M'=M+G, T'=W, W'=U*W+W-X*V, X'=X+X*U+V*W, [ Q_1>=M && M+G>=2+L && K>=1+Q && 2*meter_1==-1-L+M+G && 1+2*meter_1+L>=M+G ], cost: 2+2*meter_1 59: f63 -> f63 : M'=M+G, T'=W, W'=U*W+W-X*V, X'=X+X*U+V*W, [ Q_1>=M && 1+L>=M+G ], cost: 2 22: start -> f10 : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A Eliminating 3 self-loops for location f63 Removing the self-loops: 57 58 59. Adding an epsilon transition (to model nonexecution of the loops): 63. Removed all Self-loops using metering functions (where possible): Start location: start 1: f10 -> f19 : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 ], cost: 1 5: f19 -> f41 : P'=free_19, [ K>=J && H>=2*free_21 && 3*free_21>=1+H && free_21>=free_19 && H>=2*free_20 && 3*free_20>=1+H && free_19>=free_20 && H>=K ], cost: 1 54: f19 -> f41 : L'=2+L, M'=H+M, N'=-K+M+J, O'=free_18, P'=free_33, [ H>=K && J>=1+K && K+G>=2+L && Q>=M && H+M>=1+Q && 3+L>=K+G && H>=2*free_35 && 3*free_35>=1+H && free_35>=free_33 && H>=2*free_34 && 3*free_34>=1+H && free_33>=free_34 ], cost: 5 55: f19 -> f41 : L'=2*meter+L, P'=free_33, [ H>=K && J>=1+K && K+G>=2+L && M>=1+Q && 2*meter==-1+K-L+G && 1+2*meter+L>=K+G && H>=2*free_35 && 3*free_35>=1+H && free_35>=free_33 && H>=2*free_34 && 3*free_34>=1+H && free_33>=free_34 ], cost: 2+2*meter 56: f19 -> f41 : P'=free_33, [ H>=K && J>=1+K && 1+L>=K+G && H>=2*free_35 && 3*free_35>=1+H && free_35>=free_33 && H>=2*free_34 && 3*free_34>=1+H && free_33>=free_34 ], cost: 2 19: f19 -> f53 : Q_1'=G, [ K>=1+H ], cost: 1 32: f41 -> f19 : J'=-P+J+free_22, K'=K+G, P'=free_22, [ J>=1+P && P>=2*free_24 && 3*free_24>=1+P && free_24>=free_22 && P>=2*free_23 && 3*free_23>=1+P && free_22>=free_23 && P>=G && free_22>=G && free_22>=-P+J ], cost: 2 33: f41 -> f19 : J'=-P+J+free_22, K'=K+G, P'=free_22, [ J>=1+P && P>=2*free_24 && 3*free_24>=1+P && free_24>=free_22 && P>=2*free_23 && 3*free_23>=1+P && free_22>=free_23 && P>=G && G>=1+free_22 ], cost: 2 34: f41 -> f19 : J'=P+J, K'=K+G, [ P>=G && P>=J ], cost: 1 35: f41 -> f19 : J'=P+J, K'=K+G, [ G>=1+P ], cost: 1 14: f53 -> f10 : B'=-1+B, D'=E*D, [ Q_1>=H ], cost: 1 7: f53 -> f63 : R'=2*Q_1, S'=free_25, T'=free_28, U'=free_27, V'=free_26, W'=1, X'=0, [ H>=1+Q_1 ], cost: 1 60: f63 -> [18] : K'=K+R, L'=2+L, M'=M+G, O'=-X*free_32+W*free_29, T'=W, W'=U*W+W-X*V, X'=X+X*U+V*W, Y'=K, Z'=Q_1+K, A1'=X*free_30+free_31*W, [ Q_1>=M && M+G>=2+L && Q>=K && K+R>=1+Q && 3+L>=M+G ], cost: 5 61: f63 -> [18] : L'=2*meter_1+L, M'=M+G, T'=W, W'=U*W+W-X*V, X'=X+X*U+V*W, [ Q_1>=M && M+G>=2+L && K>=1+Q && 2*meter_1==-1-L+M+G ], cost: 2+2*meter_1 62: f63 -> [18] : M'=M+G, T'=W, W'=U*W+W-X*V, X'=X+X*U+V*W, [ Q_1>=M && 1+L>=M+G ], cost: 2 63: f63 -> [18] : [], cost: 0 22: start -> f10 : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 13: [18] -> f53 : Q_1'=R, [ M>=1+Q_1 ], cost: 1 Applied chaining over branches and pruning: Start location: start 1: f10 -> f19 : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 ], cost: 1 71: f19 -> f19 : J'=free_33+J, K'=K+G, L'=2+L, M'=H+M, N'=-K+M+J, O'=free_18, P'=free_33, [ H>=K && J>=1+K && K+G>=2+L && Q>=M && H+M>=1+Q && 3+L>=K+G && H>=2*free_35 && 3*free_35>=1+H && free_35>=free_33 && H>=2*free_34 && 3*free_34>=1+H && free_33>=free_34 && G>=1+free_33 ], cost: 6 72: f19 -> f19 : J'=-free_33+J+free_22, K'=K+G, L'=2*meter+L, P'=free_22, [ H>=K && J>=1+K && K+G>=2+L && M>=1+Q && 2*meter==-1+K-L+G && 1+2*meter+L>=K+G && H>=2*free_35 && 3*free_35>=1+H && free_35>=free_33 && H>=2*free_34 && 3*free_34>=1+H && free_33>=free_34 && J>=1+free_33 && free_33>=2*free_24 && 3*free_24>=1+free_33 && free_24>=free_22 && free_33>=2*free_23 && 3*free_23>=1+free_33 && free_22>=free_23 && free_33>=G && free_22>=G && free_22>=-free_33+J ], cost: 4+2*meter 73: f19 -> f19 : J'=-free_33+J+free_22, K'=K+G, L'=2*meter+L, P'=free_22, [ H>=K && J>=1+K && K+G>=2+L && M>=1+Q && 2*meter==-1+K-L+G && 1+2*meter+L>=K+G && H>=2*free_35 && 3*free_35>=1+H && free_35>=free_33 && H>=2*free_34 && 3*free_34>=1+H && free_33>=free_34 && J>=1+free_33 && free_33>=2*free_24 && 3*free_24>=1+free_33 && free_24>=free_22 && free_33>=2*free_23 && 3*free_23>=1+free_33 && free_22>=free_23 && free_33>=G && G>=1+free_22 ], cost: 4+2*meter 74: f19 -> f19 : J'=free_33+J, K'=K+G, L'=2*meter+L, P'=free_33, [ H>=K && J>=1+K && K+G>=2+L && M>=1+Q && 2*meter==-1+K-L+G && 1+2*meter+L>=K+G && H>=2*free_35 && 3*free_35>=1+H && free_35>=free_33 && H>=2*free_34 && 3*free_34>=1+H && free_33>=free_34 && free_33>=G && free_33>=J ], cost: 3+2*meter 75: f19 -> f19 : J'=free_33+J, K'=K+G, L'=2*meter+L, P'=free_33, [ H>=K && J>=1+K && K+G>=2+L && M>=1+Q && 2*meter==-1+K-L+G && 1+2*meter+L>=K+G && H>=2*free_35 && 3*free_35>=1+H && free_35>=free_33 && H>=2*free_34 && 3*free_34>=1+H && free_33>=free_34 && G>=1+free_33 ], cost: 3+2*meter 19: f19 -> f53 : Q_1'=G, [ K>=1+H ], cost: 1 14: f53 -> f10 : B'=-1+B, D'=E*D, [ Q_1>=H ], cost: 1 80: f53 -> [18] : K'=2*Q_1+K, L'=2+L, M'=M+G, O'=free_29, R'=2*Q_1, S'=free_25, T'=1, U'=free_27, V'=free_26, W'=1+free_27, X'=free_26, Y'=K, Z'=Q_1+K, A1'=free_31, [ H>=1+Q_1 && Q_1>=M && M+G>=2+L && Q>=K && 2*Q_1+K>=1+Q && 3+L>=M+G ], cost: 6 81: f53 -> [18] : L'=2*meter_1+L, M'=M+G, R'=2*Q_1, S'=free_25, T'=1, U'=free_27, V'=free_26, W'=1+free_27, X'=free_26, [ H>=1+Q_1 && Q_1>=M && M+G>=2+L && K>=1+Q && 2*meter_1==-1-L+M+G ], cost: 3+2*meter_1 82: f53 -> [18] : M'=M+G, R'=2*Q_1, S'=free_25, T'=1, U'=free_27, V'=free_26, W'=1+free_27, X'=free_26, [ H>=1+Q_1 && Q_1>=M && 1+L>=M+G ], cost: 3 83: f53 -> [18] : R'=2*Q_1, S'=free_25, T'=free_28, U'=free_27, V'=free_26, W'=1, X'=0, [ H>=1+Q_1 ], cost: 1 22: start -> f10 : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 13: [18] -> f53 : Q_1'=R, [ M>=1+Q_1 ], cost: 1 Eliminating 5 self-loops for location f19 Removing the self-loops: 71 72 73 74 75. Adding an epsilon transition (to model nonexecution of the loops): 89. Removed all Self-loops using metering functions (where possible): Start location: start 1: f10 -> f19 : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 ], cost: 1 84: f19 -> [19] : J'=free_33+J, K'=K+G, L'=2+L, M'=H+M, N'=-K+M+J, O'=free_18, P'=free_33, [ H>=K && J>=1+K && K+G>=2+L && Q>=M && H+M>=1+Q && 3+L>=K+G && H>=2*free_35 && 3*free_35>=1+H && free_35>=free_33 && H>=2*free_34 && 3*free_34>=1+H && free_33>=free_34 && G>=1+free_33 ], cost: 6 85: f19 -> [19] : J'=-free_33+J+free_22, K'=K+G, L'=2*meter+L, P'=free_22, [ H>=K && J>=1+K && K+G>=2+L && M>=1+Q && 2*meter==-1+K-L+G && H>=2*free_35 && 3*free_35>=1+H && free_35>=free_33 && H>=2*free_34 && 3*free_34>=1+H && free_33>=free_34 && J>=1+free_33 && free_33>=2*free_24 && 3*free_24>=1+free_33 && free_24>=free_22 && free_33>=2*free_23 && 3*free_23>=1+free_33 && free_22>=free_23 && free_33>=G && free_22>=G && free_22>=-free_33+J ], cost: 4+2*meter 86: f19 -> [19] : J'=-free_33+J+free_22, K'=K+G, L'=2*meter+L, P'=free_22, [ H>=K && J>=1+K && K+G>=2+L && M>=1+Q && 2*meter==-1+K-L+G && H>=2*free_35 && 3*free_35>=1+H && free_35>=free_33 && H>=2*free_34 && 3*free_34>=1+H && free_33>=free_34 && J>=1+free_33 && free_33>=2*free_24 && 3*free_24>=1+free_33 && free_24>=free_22 && free_33>=2*free_23 && 3*free_23>=1+free_33 && free_22>=free_23 && free_33>=G && G>=1+free_22 ], cost: 4+2*meter 87: f19 -> [19] : J'=free_33+J, K'=K+G, L'=2*meter+L, P'=free_33, [ H>=K && J>=1+K && K+G>=2+L && M>=1+Q && 2*meter==-1+K-L+G && H>=2*free_35 && 3*free_35>=1+H && free_35>=free_33 && H>=2*free_34 && 3*free_34>=1+H && free_33>=free_34 && free_33>=G && free_33>=J ], cost: 3+2*meter 88: f19 -> [19] : J'=free_33+J, K'=K+G, L'=2*meter+L, P'=free_33, [ H>=K && J>=1+K && K+G>=2+L && M>=1+Q && 2*meter==-1+K-L+G && H>=2*free_35 && 3*free_35>=1+H && free_35>=free_33 && H>=2*free_34 && 3*free_34>=1+H && free_33>=free_34 && G>=1+free_33 ], cost: 3+2*meter 89: f19 -> [19] : [], cost: 0 14: f53 -> f10 : B'=-1+B, D'=E*D, [ Q_1>=H ], cost: 1 80: f53 -> [18] : K'=2*Q_1+K, L'=2+L, M'=M+G, O'=free_29, R'=2*Q_1, S'=free_25, T'=1, U'=free_27, V'=free_26, W'=1+free_27, X'=free_26, Y'=K, Z'=Q_1+K, A1'=free_31, [ H>=1+Q_1 && Q_1>=M && M+G>=2+L && Q>=K && 2*Q_1+K>=1+Q && 3+L>=M+G ], cost: 6 81: f53 -> [18] : L'=2*meter_1+L, M'=M+G, R'=2*Q_1, S'=free_25, T'=1, U'=free_27, V'=free_26, W'=1+free_27, X'=free_26, [ H>=1+Q_1 && Q_1>=M && M+G>=2+L && K>=1+Q && 2*meter_1==-1-L+M+G ], cost: 3+2*meter_1 82: f53 -> [18] : M'=M+G, R'=2*Q_1, S'=free_25, T'=1, U'=free_27, V'=free_26, W'=1+free_27, X'=free_26, [ H>=1+Q_1 && Q_1>=M && 1+L>=M+G ], cost: 3 83: f53 -> [18] : R'=2*Q_1, S'=free_25, T'=free_28, U'=free_27, V'=free_26, W'=1, X'=0, [ H>=1+Q_1 ], cost: 1 22: start -> f10 : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 13: [18] -> f53 : Q_1'=R, [ M>=1+Q_1 ], cost: 1 19: [19] -> f53 : Q_1'=G, [ K>=1+H ], cost: 1 Applied chaining over branches and pruning: Start location: start 90: f10 -> [19] : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1+free_33, K'=K+free_4, L'=2+L, M'=free_3+M, N'=1-K+M, O'=free_18, P'=free_33, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && free_3>=K && 1>=1+K && K+free_4>=2+L && free_1>=M && free_3+M>=1+free_1 && 3+L>=K+free_4 && free_3>=2*free_35 && 3*free_35>=1+free_3 && free_35>=free_33 && free_3>=2*free_34 && 3*free_34>=1+free_3 && free_33>=free_34 && free_4>=1+free_33 ], cost: 7 91: f10 -> [19] : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1+free_33, K'=K+free_4, L'=2*meter+L, P'=free_33, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && free_3>=K && 1>=1+K && K+free_4>=2+L && M>=1+free_1 && 2*meter==-1+K-L+free_4 && free_3>=2*free_35 && 3*free_35>=1+free_3 && free_35>=free_33 && free_3>=2*free_34 && 3*free_34>=1+free_3 && free_33>=free_34 && free_33>=free_4 && free_33>=1 ], cost: 4+2*meter 92: f10 -> [19] : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1+free_33, K'=K+free_4, L'=2*meter+L, P'=free_33, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && free_3>=K && 1>=1+K && K+free_4>=2+L && M>=1+free_1 && 2*meter==-1+K-L+free_4 && free_3>=2*free_35 && 3*free_35>=1+free_3 && free_35>=free_33 && free_3>=2*free_34 && 3*free_34>=1+free_3 && free_33>=free_34 && free_4>=1+free_33 ], cost: 4+2*meter 93: f10 -> [19] : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 ], cost: 1 14: f53 -> f10 : B'=-1+B, D'=E*D, [ Q_1>=H ], cost: 1 94: f53 -> f53 : K'=2*Q_1+K, L'=2+L, M'=M+G, O'=free_29, Q_1'=2*Q_1, R'=2*Q_1, S'=free_25, T'=1, U'=free_27, V'=free_26, W'=1+free_27, X'=free_26, Y'=K, Z'=Q_1+K, A1'=free_31, [ H>=1+Q_1 && Q_1>=M && M+G>=2+L && Q>=K && 2*Q_1+K>=1+Q && 3+L>=M+G && M+G>=1+Q_1 ], cost: 7 95: f53 -> f53 : L'=2*meter_1+L, M'=M+G, Q_1'=2*Q_1, R'=2*Q_1, S'=free_25, T'=1, U'=free_27, V'=free_26, W'=1+free_27, X'=free_26, [ H>=1+Q_1 && Q_1>=M && M+G>=2+L && K>=1+Q && 2*meter_1==-1-L+M+G && M+G>=1+Q_1 ], cost: 4+2*meter_1 96: f53 -> f53 : M'=M+G, Q_1'=2*Q_1, R'=2*Q_1, S'=free_25, T'=1, U'=free_27, V'=free_26, W'=1+free_27, X'=free_26, [ H>=1+Q_1 && Q_1>=M && 1+L>=M+G && M+G>=1+Q_1 ], cost: 4 97: f53 -> f53 : Q_1'=2*Q_1, R'=2*Q_1, S'=free_25, T'=free_28, U'=free_27, V'=free_26, W'=1, X'=0, [ H>=1+Q_1 && M>=1+Q_1 ], cost: 2 22: start -> f10 : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 19: [19] -> f53 : Q_1'=G, [ K>=1+H ], cost: 1 Eliminating 4 self-loops for location f53 Removing the self-loops: 94 95 96 97 98 99. Adding an epsilon transition (to model nonexecution of the loops): 104. Removed all Self-loops using metering functions (where possible): Start location: start 90: f10 -> [19] : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1+free_33, K'=K+free_4, L'=2+L, M'=free_3+M, N'=1-K+M, O'=free_18, P'=free_33, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && free_3>=K && 1>=1+K && K+free_4>=2+L && free_1>=M && free_3+M>=1+free_1 && 3+L>=K+free_4 && free_3>=2*free_35 && 3*free_35>=1+free_3 && free_35>=free_33 && free_3>=2*free_34 && 3*free_34>=1+free_3 && free_33>=free_34 && free_4>=1+free_33 ], cost: 7 91: f10 -> [19] : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1+free_33, K'=K+free_4, L'=2*meter+L, P'=free_33, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && free_3>=K && 1>=1+K && K+free_4>=2+L && M>=1+free_1 && 2*meter==-1+K-L+free_4 && free_3>=2*free_35 && 3*free_35>=1+free_3 && free_35>=free_33 && free_3>=2*free_34 && 3*free_34>=1+free_3 && free_33>=free_34 && free_33>=free_4 && free_33>=1 ], cost: 4+2*meter 92: f10 -> [19] : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1+free_33, K'=K+free_4, L'=2*meter+L, P'=free_33, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && free_3>=K && 1>=1+K && K+free_4>=2+L && M>=1+free_1 && 2*meter==-1+K-L+free_4 && free_3>=2*free_35 && 3*free_35>=1+free_3 && free_35>=free_33 && free_3>=2*free_34 && 3*free_34>=1+free_3 && free_33>=free_34 && free_4>=1+free_33 ], cost: 4+2*meter 93: f10 -> [19] : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 ], cost: 1 100: f53 -> [20] : K'=2*Q_1+K, L'=2+L, M'=M+G, O'=free_29, Q_1'=2*Q_1, R'=2*Q_1, S'=free_25, T'=1, U'=free_27, V'=free_26, W'=1+free_27, X'=free_26, Y'=K, Z'=Q_1+K, A1'=free_31, [ H>=1+Q_1 && Q_1>=M && M+G>=2+L && Q>=K && 2*Q_1+K>=1+Q && 3+L>=M+G && M+G>=1+Q_1 ], cost: 7 101: f53 -> [20] : L'=2*meter_1+L, M'=M+G, Q_1'=2*Q_1, R'=2*Q_1, S'=free_25, T'=1, U'=free_27, V'=free_26, W'=1+free_27, X'=free_26, [ H>=1+Q_1 && Q_1>=M && M+G>=2+L && K>=1+Q && 2*meter_1==-1-L+M+G && M+G>=1+Q_1 ], cost: 4+2*meter_1 102: f53 -> [20] : M'=M+G, Q_1'=2*Q_1, R'=2*Q_1, S'=free_25, T'=1, U'=free_27, V'=free_26, W'=1+free_27, X'=free_26, [ H>=1+Q_1 && Q_1>=M && 1+L>=M+G && M+G>=1+Q_1 ], cost: 4 103: f53 -> [20] : Q_1'=2*Q_1, R'=2*Q_1, S'=free_25, T'=free_28, U'=free_27, V'=free_26, W'=1, X'=0, [ H>=1+Q_1 && M>=1+Q_1 ], cost: 2 104: f53 -> [20] : [], cost: 0 22: start -> f10 : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 19: [19] -> f53 : Q_1'=G, [ K>=1+H ], cost: 1 14: [20] -> f10 : B'=-1+B, D'=E*D, [ Q_1>=H ], cost: 1 Applied chaining over branches and pruning: Start location: start 105: f10 -> f53 : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1+free_33, K'=K+free_4, L'=2+L, M'=free_3+M, N'=1-K+M, O'=free_18, P'=free_33, Q_1'=free_4, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && free_3>=K && 1>=1+K && K+free_4>=2+L && free_1>=M && free_3+M>=1+free_1 && 3+L>=K+free_4 && free_3>=2*free_35 && 3*free_35>=1+free_3 && free_35>=free_33 && free_3>=2*free_34 && 3*free_34>=1+free_3 && free_33>=free_34 && free_4>=1+free_33 && K+free_4>=1+free_3 ], cost: 8 107: f10 -> f53 : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1+free_33, K'=K+free_4, L'=2*meter+L, P'=free_33, Q_1'=free_4, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && free_3>=K && 1>=1+K && K+free_4>=2+L && M>=1+free_1 && 2*meter==-1+K-L+free_4 && free_3>=2*free_35 && 3*free_35>=1+free_3 && free_35>=free_33 && free_3>=2*free_34 && 3*free_34>=1+free_3 && free_33>=free_34 && free_4>=1+free_33 && K+free_4>=1+free_3 ], cost: 5+2*meter 108: f10 -> f53 : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1, Q_1'=free_4, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && K>=1+free_3 ], cost: 2 106: f10 -> [21] : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1+free_33, K'=K+free_4, L'=2*meter+L, P'=free_33, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && free_3>=K && 1>=1+K && K+free_4>=2+L && M>=1+free_1 && 2*meter==-1+K-L+free_4 && free_3>=2*free_35 && 3*free_35>=1+free_3 && free_35>=free_33 && free_3>=2*free_34 && 3*free_34>=1+free_3 && free_33>=free_34 && free_33>=free_4 && free_33>=1 ], cost: 4+2*meter 109: f53 -> f10 : B'=-1+B, D'=E*D, K'=2*Q_1+K, L'=2+L, M'=M+G, O'=free_29, Q_1'=2*Q_1, R'=2*Q_1, S'=free_25, T'=1, U'=free_27, V'=free_26, W'=1+free_27, X'=free_26, Y'=K, Z'=Q_1+K, A1'=free_31, [ H>=1+Q_1 && Q_1>=M && M+G>=2+L && Q>=K && 2*Q_1+K>=1+Q && 3+L>=M+G && M+G>=1+Q_1 && 2*Q_1>=H ], cost: 8 110: f53 -> f10 : B'=-1+B, D'=E*D, L'=2*meter_1+L, M'=M+G, Q_1'=2*Q_1, R'=2*Q_1, S'=free_25, T'=1, U'=free_27, V'=free_26, W'=1+free_27, X'=free_26, [ H>=1+Q_1 && Q_1>=M && M+G>=2+L && K>=1+Q && 2*meter_1==-1-L+M+G && M+G>=1+Q_1 && 2*Q_1>=H ], cost: 5+2*meter_1 111: f53 -> f10 : B'=-1+B, D'=E*D, M'=M+G, Q_1'=2*Q_1, R'=2*Q_1, S'=free_25, T'=1, U'=free_27, V'=free_26, W'=1+free_27, X'=free_26, [ H>=1+Q_1 && Q_1>=M && 1+L>=M+G && M+G>=1+Q_1 && 2*Q_1>=H ], cost: 5 112: f53 -> f10 : B'=-1+B, D'=E*D, Q_1'=2*Q_1, R'=2*Q_1, S'=free_25, T'=free_28, U'=free_27, V'=free_26, W'=1, X'=0, [ H>=1+Q_1 && M>=1+Q_1 && 2*Q_1>=H ], cost: 3 113: f53 -> f10 : B'=-1+B, D'=E*D, [ Q_1>=H ], cost: 1 22: start -> f10 : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A Applied chaining over branches and pruning: Start location: start 114: f10 -> f10 : B'=-1+B, D'=free_2*D, E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1+free_33, K'=K+free_4, L'=2+L, M'=free_3+M, N'=1-K+M, O'=free_18, P'=free_33, Q_1'=free_4, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && free_3>=K && 1>=1+K && K+free_4>=2+L && free_1>=M && free_3+M>=1+free_1 && 3+L>=K+free_4 && free_3>=2*free_35 && 3*free_35>=1+free_3 && free_35>=free_33 && free_3>=2*free_34 && 3*free_34>=1+free_3 && free_33>=free_34 && free_4>=1+free_33 && K+free_4>=1+free_3 && free_4>=free_3 ], cost: 9 119: f10 -> f10 : B'=-1+B, D'=free_2*D, E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1+free_33, K'=K+free_4, L'=2*meter+L, P'=free_33, Q_1'=free_4, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && free_3>=K && 1>=1+K && K+free_4>=2+L && M>=1+free_1 && 2*meter==-1+K-L+free_4 && free_3>=2*free_35 && 3*free_35>=1+free_3 && free_35>=free_33 && free_3>=2*free_34 && 3*free_34>=1+free_3 && free_33>=free_34 && free_4>=1+free_33 && K+free_4>=1+free_3 && free_4>=free_3 ], cost: 6+2*meter 120: f10 -> f10 : B'=-1+B, D'=free_2*D, E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1, K'=K+2*free_4, L'=2+L, M'=M+free_4, O'=free_29, Q_1'=2*free_4, R'=2*free_4, S'=free_25, T'=1, U'=free_27, V'=free_26, W'=1+free_27, X'=free_26, Y'=K, Z'=K+free_4, A1'=free_31, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && K>=1+free_3 && free_3>=1+free_4 && free_4>=M && M+free_4>=2+L && free_1>=K && K+2*free_4>=1+free_1 && 3+L>=M+free_4 && M+free_4>=1+free_4 && 2*free_4>=free_3 ], cost: 10 121: f10 -> f10 : B'=-1+B, D'=free_2*D, E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1, L'=2*meter_1+L, M'=M+free_4, Q_1'=2*free_4, R'=2*free_4, S'=free_25, T'=1, U'=free_27, V'=free_26, W'=1+free_27, X'=free_26, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && K>=1+free_3 && free_3>=1+free_4 && free_4>=M && M+free_4>=2+L && K>=1+free_1 && 2*meter_1==-1-L+M+free_4 && M+free_4>=1+free_4 && 2*free_4>=free_3 ], cost: 7+2*meter_1 122: f10 -> f10 : B'=-1+B, D'=free_2*D, E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1, M'=M+free_4, Q_1'=2*free_4, R'=2*free_4, S'=free_25, T'=1, U'=free_27, V'=free_26, W'=1+free_27, X'=free_26, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && K>=1+free_3 && free_3>=1+free_4 && free_4>=M && 1+L>=M+free_4 && M+free_4>=1+free_4 && 2*free_4>=free_3 ], cost: 7 106: f10 -> [21] : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1+free_33, K'=K+free_4, L'=2*meter+L, P'=free_33, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && free_3>=K && 1>=1+K && K+free_4>=2+L && M>=1+free_1 && 2*meter==-1+K-L+free_4 && free_3>=2*free_35 && 3*free_35>=1+free_3 && free_35>=free_33 && free_3>=2*free_34 && 3*free_34>=1+free_3 && free_33>=free_34 && free_33>=free_4 && free_33>=1 ], cost: 4+2*meter 115: f10 -> [22] : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1+free_33, K'=K+free_4, L'=2*meter+L, P'=free_33, Q_1'=free_4, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && free_3>=K && 1>=1+K && K+free_4>=2+L && M>=1+free_1 && 2*meter==-1+K-L+free_4 && free_3>=2*free_35 && 3*free_35>=1+free_3 && free_35>=free_33 && free_3>=2*free_34 && 3*free_34>=1+free_3 && free_33>=free_34 && free_4>=1+free_33 && K+free_4>=1+free_3 ], cost: 5+2*meter 116: f10 -> [23] : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1+free_33, K'=K+free_4, L'=2*meter+L, P'=free_33, Q_1'=free_4, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && free_3>=K && 1>=1+K && K+free_4>=2+L && M>=1+free_1 && 2*meter==-1+K-L+free_4 && free_3>=2*free_35 && 3*free_35>=1+free_3 && free_35>=free_33 && free_3>=2*free_34 && 3*free_34>=1+free_3 && free_33>=free_34 && free_4>=1+free_33 && K+free_4>=1+free_3 ], cost: 5+2*meter 117: f10 -> [24] : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1+free_33, K'=K+free_4, L'=2*meter+L, P'=free_33, Q_1'=free_4, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && free_3>=K && 1>=1+K && K+free_4>=2+L && M>=1+free_1 && 2*meter==-1+K-L+free_4 && free_3>=2*free_35 && 3*free_35>=1+free_3 && free_35>=free_33 && free_3>=2*free_34 && 3*free_34>=1+free_3 && free_33>=free_34 && free_4>=1+free_33 && K+free_4>=1+free_3 ], cost: 5+2*meter 118: f10 -> [25] : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1+free_33, K'=K+free_4, L'=2*meter+L, P'=free_33, Q_1'=free_4, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && free_3>=K && 1>=1+K && K+free_4>=2+L && M>=1+free_1 && 2*meter==-1+K-L+free_4 && free_3>=2*free_35 && 3*free_35>=1+free_3 && free_35>=free_33 && free_3>=2*free_34 && 3*free_34>=1+free_3 && free_33>=free_34 && free_4>=1+free_33 && K+free_4>=1+free_3 ], cost: 5+2*meter 22: start -> f10 : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A Eliminating 5 self-loops for location f10 Removing the self-loops: 114 119 120 121 122. Adding an epsilon transition (to model nonexecution of the loops): 130. Removed all Self-loops using metering functions (where possible): Start location: start 125: f10 -> [26] : B'=-1+B, D'=free_2*D, E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1+free_33, K'=K+free_4, L'=2+L, M'=free_3+M, N'=1-K+M, O'=free_18, P'=free_33, Q_1'=free_4, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && free_3>=K && 1>=1+K && K+free_4>=2+L && free_1>=M && free_3+M>=1+free_1 && 3+L>=K+free_4 && free_3>=2*free_35 && 3*free_35>=1+free_3 && free_35>=free_33 && free_3>=2*free_34 && 3*free_34>=1+free_3 && free_33>=free_34 && free_4>=1+free_33 && K+free_4>=1+free_3 && free_4>=free_3 ], cost: 9 126: f10 -> [26] : B'=-1+B, D'=free_2*D, E'=free_2, F'=free_5, G'=1-K+2*meter+L, H'=free_3, Q'=free_1, J'=1+free_33, K'=1+2*meter+L, L'=2*meter+L, P'=free_33, Q_1'=1-K+2*meter+L, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=1-K+2*meter+L && D>=2*free_9 && 3*free_9>=1+D && 1-K+2*meter+L>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && free_3>=K && 1>=1+K && 1+2*meter+L>=2+L && M>=1+free_1 && free_3>=2*free_35 && 3*free_35>=1+free_3 && free_35>=free_33 && free_3>=2*free_34 && 3*free_34>=1+free_3 && free_33>=free_34 && 1-K+2*meter+L>=1+free_33 && 1+2*meter+L>=1+free_3 && 1-K+2*meter+L>=free_3 ], cost: 6+2*meter 127: f10 -> [26] : B'=-1+B, D'=free_2*D, E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1, K'=K+2*free_4, L'=2+L, M'=M+free_4, O'=free_29, Q_1'=2*free_4, R'=2*free_4, S'=free_25, T'=1, U'=free_27, V'=free_26, W'=1+free_27, X'=free_26, Y'=K, Z'=K+free_4, A1'=free_31, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && K>=1+free_3 && free_3>=1+free_4 && free_4>=M && M+free_4>=2+L && free_1>=K && K+2*free_4>=1+free_1 && 3+L>=M+free_4 && M+free_4>=1+free_4 && 2*free_4>=free_3 ], cost: 10 128: f10 -> [26] : B'=-1+B, D'=free_2*D, E'=free_2, F'=free_5, G'=1+2*meter_1+L-M, H'=free_3, Q'=free_1, J'=1, L'=2*meter_1+L, M'=1+2*meter_1+L, Q_1'=2+4*meter_1+2*L-2*M, R'=2+4*meter_1+2*L-2*M, S'=free_25, T'=1, U'=free_27, V'=free_26, W'=1+free_27, X'=free_26, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=1+2*meter_1+L-M && D>=2*free_9 && 3*free_9>=1+D && 1+2*meter_1+L-M>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && K>=1+free_3 && free_3>=2+2*meter_1+L-M && 1+2*meter_1+L-M>=M && 1+2*meter_1+L>=2+L && K>=1+free_1 && 1+2*meter_1+L>=2+2*meter_1+L-M && 2+4*meter_1+2*L-2*M>=free_3 ], cost: 7+2*meter_1 129: f10 -> [26] : B'=-1+B, D'=free_2*D, E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1, M'=M+free_4, Q_1'=2*free_4, R'=2*free_4, S'=free_25, T'=1, U'=free_27, V'=free_26, W'=1+free_27, X'=free_26, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && K>=1+free_3 && free_3>=1+free_4 && free_4>=M && 1+L>=M+free_4 && M+free_4>=1+free_4 && 2*free_4>=free_3 ], cost: 7 130: f10 -> [26] : [], cost: 0 22: start -> f10 : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 106: [26] -> [21] : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1+free_33, K'=K+free_4, L'=2*meter+L, P'=free_33, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && free_3>=K && 1>=1+K && K+free_4>=2+L && M>=1+free_1 && 2*meter==-1+K-L+free_4 && free_3>=2*free_35 && 3*free_35>=1+free_3 && free_35>=free_33 && free_3>=2*free_34 && 3*free_34>=1+free_3 && free_33>=free_34 && free_33>=free_4 && free_33>=1 ], cost: 4+2*meter 115: [26] -> [22] : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1+free_33, K'=K+free_4, L'=2*meter+L, P'=free_33, Q_1'=free_4, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && free_3>=K && 1>=1+K && K+free_4>=2+L && M>=1+free_1 && 2*meter==-1+K-L+free_4 && free_3>=2*free_35 && 3*free_35>=1+free_3 && free_35>=free_33 && free_3>=2*free_34 && 3*free_34>=1+free_3 && free_33>=free_34 && free_4>=1+free_33 && K+free_4>=1+free_3 ], cost: 5+2*meter 116: [26] -> [23] : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1+free_33, K'=K+free_4, L'=2*meter+L, P'=free_33, Q_1'=free_4, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && free_3>=K && 1>=1+K && K+free_4>=2+L && M>=1+free_1 && 2*meter==-1+K-L+free_4 && free_3>=2*free_35 && 3*free_35>=1+free_3 && free_35>=free_33 && free_3>=2*free_34 && 3*free_34>=1+free_3 && free_33>=free_34 && free_4>=1+free_33 && K+free_4>=1+free_3 ], cost: 5+2*meter 117: [26] -> [24] : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1+free_33, K'=K+free_4, L'=2*meter+L, P'=free_33, Q_1'=free_4, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && free_3>=K && 1>=1+K && K+free_4>=2+L && M>=1+free_1 && 2*meter==-1+K-L+free_4 && free_3>=2*free_35 && 3*free_35>=1+free_3 && free_35>=free_33 && free_3>=2*free_34 && 3*free_34>=1+free_3 && free_33>=free_34 && free_4>=1+free_33 && K+free_4>=1+free_3 ], cost: 5+2*meter 118: [26] -> [25] : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1+free_33, K'=K+free_4, L'=2*meter+L, P'=free_33, Q_1'=free_4, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && free_3>=K && 1>=1+K && K+free_4>=2+L && M>=1+free_1 && 2*meter==-1+K-L+free_4 && free_3>=2*free_35 && 3*free_35>=1+free_3 && free_35>=free_33 && free_3>=2*free_34 && 3*free_34>=1+free_3 && free_33>=free_34 && free_4>=1+free_33 && K+free_4>=1+free_3 ], cost: 5+2*meter Applied chaining over branches and pruning: Start location: start 136: start -> [26] : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 131: start -> [27] : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 132: start -> [28] : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 133: start -> [29] : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 134: start -> [30] : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 135: start -> [31] : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 106: [26] -> [21] : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1+free_33, K'=K+free_4, L'=2*meter+L, P'=free_33, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && free_3>=K && 1>=1+K && K+free_4>=2+L && M>=1+free_1 && 2*meter==-1+K-L+free_4 && free_3>=2*free_35 && 3*free_35>=1+free_3 && free_35>=free_33 && free_3>=2*free_34 && 3*free_34>=1+free_3 && free_33>=free_34 && free_33>=free_4 && free_33>=1 ], cost: 4+2*meter 115: [26] -> [22] : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1+free_33, K'=K+free_4, L'=2*meter+L, P'=free_33, Q_1'=free_4, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && free_3>=K && 1>=1+K && K+free_4>=2+L && M>=1+free_1 && 2*meter==-1+K-L+free_4 && free_3>=2*free_35 && 3*free_35>=1+free_3 && free_35>=free_33 && free_3>=2*free_34 && 3*free_34>=1+free_3 && free_33>=free_34 && free_4>=1+free_33 && K+free_4>=1+free_3 ], cost: 5+2*meter 116: [26] -> [23] : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1+free_33, K'=K+free_4, L'=2*meter+L, P'=free_33, Q_1'=free_4, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && free_3>=K && 1>=1+K && K+free_4>=2+L && M>=1+free_1 && 2*meter==-1+K-L+free_4 && free_3>=2*free_35 && 3*free_35>=1+free_3 && free_35>=free_33 && free_3>=2*free_34 && 3*free_34>=1+free_3 && free_33>=free_34 && free_4>=1+free_33 && K+free_4>=1+free_3 ], cost: 5+2*meter 117: [26] -> [24] : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1+free_33, K'=K+free_4, L'=2*meter+L, P'=free_33, Q_1'=free_4, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && free_3>=K && 1>=1+K && K+free_4>=2+L && M>=1+free_1 && 2*meter==-1+K-L+free_4 && free_3>=2*free_35 && 3*free_35>=1+free_3 && free_35>=free_33 && free_3>=2*free_34 && 3*free_34>=1+free_3 && free_33>=free_34 && free_4>=1+free_33 && K+free_4>=1+free_3 ], cost: 5+2*meter 118: [26] -> [25] : E'=free_2, F'=free_5, G'=free_4, H'=free_3, Q'=free_1, J'=1+free_33, K'=K+free_4, L'=2*meter+L, P'=free_33, Q_1'=free_4, [ D>=2*free_16 && 3*free_16>=1+D && free_16>=free_4 && D>=2*free_9 && 3*free_9>=1+D && free_4>=free_9 && free_2*D>=2*free_2*free_13 && 2*free_2*free_13+free_13>=1+free_2*D && free_13>=free_3 && free_2*D>=2*free_8*free_2 && free_8+2*free_8*free_2>=1+free_2*D && free_3>=free_8 && C>=free_2*free_12*D && free_2*free_12*D+free_12>=1+C && C>=free_17*free_2*D && free_17+free_17*free_2*D>=1+C && free_2*free_12*D>=2*free_17*free_2*free_7 && 2*free_17*free_2*free_7+free_7>=1+free_2*free_12*D && free_7>=free_1 && C>=free_2*free_15*D && free_2*free_15*D+free_15>=1+C && C>=free_2*free_6*D && free_2*free_6*D+free_6>=1+C && free_2*free_15*D>=2*free_11*free_2*free_6 && 2*free_11*free_2*free_6+free_11>=1+free_2*free_15*D && free_1>=free_11 && B>=1 && C>=free_2*D*free_14 && free_2*D*free_14+free_14>=1+C && free_14>=free_5 && C>=free_2*free_10*D && free_2*free_10*D+free_10>=1+C && free_5>=free_10 && free_3>=K && 1>=1+K && K+free_4>=2+L && M>=1+free_1 && 2*meter==-1+K-L+free_4 && free_3>=2*free_35 && 3*free_35>=1+free_3 && free_35>=free_33 && free_3>=2*free_34 && 3*free_34>=1+free_3 && free_33>=free_34 && free_4>=1+free_33 && K+free_4>=1+free_3 ], cost: 5+2*meter Applied chaining over branches and pruning: Start location: start 131: start -> [27] : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 132: start -> [28] : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 133: start -> [29] : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 134: start -> [30] : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 135: start -> [31] : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 137: start -> [32] : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 138: start -> [33] : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 139: start -> [34] : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 140: start -> [35] : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 141: start -> [36] : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A Final control flow graph problem, now checking costs for infinitely many models: Start location: start 131: start -> [27] : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 132: start -> [28] : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 133: start -> [29] : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 134: start -> [30] : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 135: start -> [31] : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 137: start -> [32] : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 138: start -> [33] : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 139: start -> [34] : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 140: start -> [35] : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A 141: start -> [36] : B'=1+A, C'=C*free^(1-B+A), D'=1, [ A>=B && 1+A>=1+A ], cost: 3-B+A Computing complexity for remaining 10 transitions. Found configuration with infinitely models for cost: 3-B+A and guard: A>=B && 1+A>=1+A: B: Pos, A: Pos, where: A > B 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 Final Cost: 3-B+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),?)